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 and arity to be a subset of -tuple of relation of order and arity . When 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 and arity to relations of order and arity and test of equality between two relations of the same order and arity.

is the set of formulae with quantification up to order O. (resp. ) is defined as the set of formula in beginning by an existential (resp universal) quantifier followed by at most alternation of quantifiers.

This class was defined in [HT06], and it was proved that where is the th level of the polynomial hierarchy.

Linked From

No class.