We define second-order variable has got an arity and represent any proposition of arity . They are usually written in upper-case.
Second order logic is the set of FO formulae where we add quantification over second-order variables.
Every formuale is equivalent to a formulae in prenex normal form, where we first write quantification on variable on second order and then a FO-formulae in prenex normal form.
In Descriptive complexity we can see that SO is equal to PH, more precisely we have that formulae in prenex normal form where existential and universal of second order alternate times are the th level of the polynomial hierarchy.
This means that SO with only existential second-order quantification is equal to which is NP, and with only universal quantification is equal to which is Co-NP.
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.
SO(horn) is the set of boolean queries definable with second-order formulae in normal form such that the quantifier-free part of the formula is in conjunctive normal form with at most one positive instance of a quantified relation per clause. (Atomic queries to the database don't count.)
It was shown in [Grä92] that this class is equal to P.
Those formulae can be made in prenex form where the second order is existential and the first order universal without loss of generality.
SO(krom) is the set of boolean queries definable with second-order formulae in normal form such that the quantifier-free part of the formula is in Krom form, which means that in every clause there is at most two literals and the first-order portion contains no existential quantifiers.
It was shown in [Grä92] that this class is equal to NL.
Those formulaes can be made in prenex form where the second order is existential and the first order universal without loss of generalities.
SO[LFP] is to SO what FO[LFP] is to FO. The LFP operator can now also take second-order variable as argument.
In Descriptive complexity we can see that SO[LFP] is equal to EXPTIME.
SO[TC] is to SO as FO[TC] is to FO. The TC operator can now also take second-order variable as argument.
In Descriptive complexity we can see thatSO[TC] is equal to PSPACE.
SO[] is to SO as FO[] is to FO. But we now also have second-order quantifier in the quantifier block.
In Descriptive complexity we can see that :