Class Description

SO: Second-Order logic

We define second-order variable has got an arity ${\displaystyle k}$ and represent any proposition of arity ${\displaystyle k}$. 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 ${\displaystyle k}$ times are the ${\displaystyle k}$th level of the polynomial hierarchy.

This means that SO with only existential second-order quantification is equal to ${\displaystyle \Sigma ^{1}}$ which is NP, and with only universal quantification is equal to ${\displaystyle \Pi ^{1}}$ which is Co-NP.

Linked From

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.

More about...

SO(Horn): Second-order in Horn form

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.

More about...

SO(Krom): Second-order in Krom form

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.

More about...

SO[LFP]: Second-Order logic with least fixed point

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.

More about...

SO[TC]: Second-Order logic with transitive closure

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.

More about...

SO[${\displaystyle t(n)}$]: Iterated Second-Order logic

SO[${\displaystyle t(n)}$] is to SO as FO[${\displaystyle t(n)}$] is to FO. But we now also have second-order quantifier in the quantifier block.

In Descriptive complexity we can see that :

• SO[${\displaystyle n^{O(1)}}$] is equal to PSPACE it is also another way to write SO(TC)
• SO[${\displaystyle 2^{n^{O(1)}}}$] is equal to EXPTIME it is also another way to write SO(LFP)

More about...