I'm currently in a theory of computing class and as such I have been looking up information about P vs NP and other complexity classes out of curiosity. In the process I cam across a blog post discussing a recent "proof" (it turned out to be wrong of course) of P not equal NP and in it they discussed the FO(LFP) complexity class.


Now I've understood all complexity classes so far, but even after reading to Wikipedia, and complexity zoo entries on FO and first order logic I still don't understand this complexity class at all. I have come to the understanding that FO is the set of all algorithms or problems (correct me if I'm wrong) that can be solved using first order logic which somehow avoids entering the realm of algorithmics. The problem is I don't understand what the first order part of first order logic means or how algorithms are represented as such.


Now Wikipedia simply defined it as being not higher order logic which was pretty vegue. I have a good understanding of boolean logic and some understanding of logic in general, but I have the feeling that due to all the special notation that is used in the explanations I read I am not seeing the forest for the trees. Can someone explain to me what property of first order logic makes it different from other kinds of logic and give an example of how this can represent an algorithm?



FO complexity class
In complexity theory, it is customary to talk about the complexity of languages, i.e., of sets of finite strings of symbols from some alphabet. When one regards FO as a complexity class, the context is broader; one talks about the complexity of sets of finite structures. By a (finite) structure is meant a (finite) set with some specified functions and relations on it (and distinguished elements too, but I prefer to think of those as 0-ary functions). Some of these classes of structures admit descriptions of the form "all the finite structures in which $S$ is true" where $S$ is a statement built up from 


* symbols for relations and functions (and distinguished elements),
* equality,
* variables that range over elements of the structure,
* Boolean connectives (and, or, not), and
* quantifiers (for all, for some).


A class with such a description is said to be a FO class, or an FO-definable class of structures (the statement $S$ being its FO-definition). The phrase "first-order" that "FO" abbreviates refers to the fact that the variables in $S$ range only over elements of the structure; second-order statements could have variables ranging over subsets of the structure or relations or functions on the structure; third-order would allow variables ranging over things like sets of relations, etc.


The context here, dealing with finite structures, subsumes the traditional context that deals with finite strings over an alphabet $A$. A string of length $n$ can be regarded as a structure with $n$ elements (representing the $n$ positions in the string), the left-to-right ordering relation $\lt$ on these positions, and, for each $a\in A$, a unary predicate $C\_a$ which is true of an element (i.e., of a position) iff the string has symbol $a$ in that position. In this way, the general definition of "FO class" can be applied to classes of strings. Much of the complexity-theoretic interest in FO definability, however, comes from the fact that structures are more general than strings. A structure with a linear ordering of its elements can be coded as a string, but there are interesting issues about complexity of classes of unordered finite structures.


