Almost sure theory

We all know that the Hilbert's Enstceidungsproblem, i.e. deciding whether a first-order sentence is true, is undecidable. Church, Turing, and others proved it. Recall that first-order logic admits the 0-1 law, i.e., every FO sentence is almost surely true (AST) or almost surely false (ASF). So, what about the problem of deciding whether an FO sentence be AST? It turns out that this is decidable. I shall outline some important ideas for proving this statement.

Let us restrict ourselves to graphs as before. In proving that FO admits the 0-1 law, we mentioned the extension axioms EA = {P_k}_{k ∈ N}, where N is the set of all natural numbers. Extension axioms are nothing more than graph properties. In our case, P_ks are FO-expressible. Although for the purpose of this post we need not understand what our extension axioms are, I will just define it for future reference:

∀x₁, ..., x_2k( ∧_{i ≠ j} x_i &ne x_j ->

∃z( ∧_{1 ≤ i ≤ 2k} z ≠ x_i

∧_{i ≤ k} E(z,x_i)

∧_{i > k} ¬E(z,x_i)))

Recall that a theory T is a set of sentences. A model of T is a structure that satisfies all sentences of T. The theory T is consistent if it has a model, and it is complete iff for each sentence f (of the same vocabulary), we have either T |= f, i.e. every model of T is a model of f, or T |= ¬ f. A consistent and complete theory T is decidable if it is possible to decide whether T |= f, for any given sentence f.

Theorem: EA is consistent (and has a unique countable model), complete, and decidable

We will not prove the first two statements, as we will need more model theory (see Libkin's "Elements of Finite Model Theory" for more details). To prove that EA is decidable, we need only invoke an old result from recursive theory that every recursively axiomatizable theory is decidable. The above definition of P_k gives us a recursive enumeration of the axioms.

The unique countable model for EA, denoted RG, is called the random graph, as its probabilistic construction is often emphasized in the literature. Using the above theorem, we derive an easy corollary:

Corollary: For any FO sentence f, RG |= f iff μ(f) = 1.

With these results, it is a breeze to conclude that deciding whether an FO sentence be AST is computable. To determine the exact complexity of the problem, one needs a more hairy analysis, which we will not do here. It turns out that the problem is PSPACE-complete, the proof of which can be found in

E. Granjean. Complexity of the first-order theory of almost all finite structures, Information and Control, Volume 57, 1983.

Recent work in this area mostly deals with determining fragments of second-order logic that admits the 0-1 law, and whether the almost sure theory with respect to the fragment be decidable. [It is easy to see that SO in its full power does not admit the 0-1 law.] This, however, lies outside the scope of our current discussion.