First order logic is the smallest logical class of logic language. It is the base of Descriptive complexity and equal to the class AC0.
When we use logic formalism, the input is a structure, usually it is either strings (of bits or over an alphabet) whose elements are position of the strings, or graphs whose elements are vertices. The measure of the input will there be the size of the structure.Whatever the structure is, we can suppose that there are relation that you can test, by example is true iff there is an edge from to if the structure is a graph, and is true iff the nth letter of the string is 1. We also have constant, who are special elements of the structure, by example if we want to check reachability in a graph, we will have to choose two constant s and t.
In descriptive complexity we almost always suppose that there is a total order over the elements and that we can check equality between elements. This let us consider elements as number, is the number iff there is elements such that . Thanks to this we also want the primitive "bit", where is true if only the th bit of is 1. (We can replace by plus and time, ternary relation such that is true iff and is true iff ).
Since in a computer elements are only pointers or string of bits, those assumptions make sense, and those primitive functions can be calculated in most of the small complexity classes. We can also imagine FO without those primitives, which gives us smaller complexity classes.
The language FO is then defined as the closure by conjunction ( ), negation () and universal quantification () over element of the structures. We also often use existential quantification () and disjunction () but those can be defined thanks to the 3 first symbols.
The semantics of the formulae in FO is straightforward, is true iff is false, is true iff is true and is true, and () is true iff whatever element we decide that is we can choose, is true.
A query in FO will then be to check if a FO formulae is true over a given structure, this structure is the input of the problem. One should not confuse this kind of problem with checking if a quantified boolean formula is true, which is the definition of QBF, which is PSPACE-complete. The difference between those two problem is that in QBF the size of the problem is the size of the formula and elements are just boolean value, whereas in FO the size of the problem is the size of the structure and the formula is fixed.
Every formulae is equivalent to a formulae in prenex normal form where we put recursively every quantifier and then a quantifier-free formulae.
An especially important subclass of AC, corresponding to constant-depth, unbounded-fanin, polynomial-size circuits with AND, OR, and NOT gates.
Computing the Parity or Majority of n bits is not in AC0 [FSS84].
There are functions in AC0 that are pseudorandom for all statistical tests in AC0 [NW94]. But there are no functions in AC0 that are pseudorandom for all statistical tests in QP (quasipolynomial time) [LMN93].
[LMN93] showed furthermore that functions with AC0 circuits of depth d are learnable in QP, given their outputs on O(2log(n)^O(d)) randomly chosen inputs. On the other hand, this learning algorithm is essentially optimal, unless there is a 2n^o(1) algorithm for factoring [Kha93].
Although there are no good pseudorandom functions in AC0, [IN96] showed that there are pseudorandom generators that stretch n bits to n+Θ(log n), assuming the hardness of a problem based on subset sum.
AC0 contains NC0, and is contained in QACf0 and MAC0.
In descriptive complexity, uniform AC0 can be characterized as the class of problems expressible by first-order predicates with addition and multiplication operators - or indeed, with ordering and multiplication, or ordering and division (see [Lee02]). So it's equivalent to the class FO, and to the alternating logtime hierarchy.
[BLM+98] showed the following problem is complete for depth-k AC0 circuits (with a uniformity condition):
The class of dynamic problems solvable using first-order predicates.
Basically what this means is that an algorithm maintains some polynomial-size data structure (say a graph), and receives a sequence of updates (add this edge, delete that one, etc.). For each update, it computes a new value for the data structure in FO -- that is, for each bit of the data structure, there is an FO function representing the new value of that bit, which takes as input both the update and the previous value of the data structure. At the end the algorithm needs to answer some question (i.e. is the graph connected?).
See [HI02] for more information, and a complete problem for Dyn-FO.
See also Dyn-ThC0.
FO(pfp) is the set of boolean queries definable with first-order formulae with a partial fixed point operator.
Let be an integer, vectors of variables, a second-order variable of arity , and a FO(PFP) function using and as variables, then we can define iteratively such that and which means that the property is true on the input if is true on input , and when the variable is replaced by . Then, either there is a fixed point, or the list of is looping.
PFP( is defined as the value of the fixed point of on y if there is a fixed point, else as false.
Since s are property of arity , there is at most values for the s, so with a poly-space counter we can check if there is a loop or not.
It was proved in [Imm98] that FO(pfp) is equal to PSPACE.
FO(TC) is the set of boolean queries definable with first-order formulae with a transitive closure (TC) operator.
TC is defined this way: let be a positive integer and be vectors of variables, then TC( is true if there exist variables such that and for all . Here, is a formula over written in FO(TC) and means that the variables and are replaced by and .
Every formula of TC can be written in a normal form FO( where is a FO formula and we suppose that there is an order on the model where variables are quantified, so we can choose the minimum and maximum element.
It was shown in [Imm98] page 150 that this class is equal to NL.
Let be a function from integers to integers. abbreviates and abbreviates .
A quantifier block is a list where the s are quantifier free FO-formulae and each s is either or .If is a quantifier block then is the block consisting of iterated copies of . Note that there are quantifiers in the list, but only k variables; each variable is used times.
FO[] consists of the FO-formulae with quantifier blocks that are iterated times.
In Descriptive complexity we can see that :
The class of decision problems solvable by a uniform family of polynomial-size, unbounded-fanin, depth O(log log n) circuits with AND, OR, and NOT gates. Equals FO(log log n).
Defined in [BKL+00], where it was also shown that many problems on finite groups are in FOLL.
Contains uniform AC0, and is contained in uniform AC1.
Is not known to be comparable to L or NL.
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.
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.
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 :