Class Description

HO: High-Order logic

High order logic is an extension of Second order, First order where we add quantification over higher order variables.

We define a relation of order ${\displaystyle o}$ and arity ${\displaystyle k}$ to be a subset of ${\displaystyle k}$-tuple of relation of order ${\displaystyle o-1}$ and arity ${\displaystyle k}$. When ${\displaystyle o=1}$ it is by extension a first order variable. "The quantification of formula in HO is over a given order (which is a straightforward extension of SO where we add quantification over constants (first-order variables) and relations (second-order variables)). The atomic predicates now can be general application of relations of order ${\displaystyle o}$ and arity ${\displaystyle k}$ to ${\displaystyle k}$ relations of order ${\displaystyle o-1}$ and arity ${\displaystyle a}$ and test of equality between two relations of the same order and arity.

${\displaystyle HO^{o}}$ is the set of formulae with quantification up to order O. ${\displaystyle \Sigma _{j}^{i}}$(resp. ${\displaystyle \Pi _{j}^{i}}$) is defined as the set of formula in ${\displaystyle HO^{i+1}}$ beginning by an existential (resp universal) quantifier followed by at most ${\displaystyle j-1}$ alternation of quantifiers.

This class was defined in [HT06], and it was proved that ${\displaystyle \Sigma _{j}^{i}=\exp _{2}^{i-1}(n^{O}(1))^{\Sigma _{j-1}^{P}}}$ where ${\displaystyle \Sigma _{j-1}^{P}}$ is the ${\displaystyle j}$th level of the polynomial hierarchy.

Linked From

No class.