Zero–one law (logic)

In mathematical logic, zero-one law is a property of a logic saying that any property is either almost surely true or almost surely false. Zero-one law holds for first-order logic (without function symbols), first-order logic extended with fixed point operators and first-order with infinite disjunctions and conjunctions. It does not hold for monadic second order logic.

As pointed out by Yuri Gurevich, zero-one law was proven for first-order logic by Yu. V. Glebskii, D. I. Kogan, M. I. Liogon'kii & V. A. Talanov and independently by Ronald Fagin.

Principle

In this article, to keep it simple, we talk about graphs instead of considering arbitrary structures. Given a sentence $\varphi$ in some logic, we define $\mu _{n}(\varphi )$ to be the proportion of graphs that satisfy $\varphi$ among the graphs with exactly $n$ vertices. We say that a logic has the zero-one law if $\mu _{n}(\varphi )$ converges to 1 or 0, for any sentence $\varphi$ of that logic. We set $\mu (\varphi )$ to be that limit to which $\mu _{n}(\varphi )$ converges when $n$ grows to infinity.

Examples

We give the examples given in p. 236.

Even

Any logic in which "being of size even" is expressible by a formula $\varphi$ does not have the zero-one law. Indeed, $\mu _{n}(\varphi )=1$ if $n$ is even and $\mu _{n}(\varphi )=0$ if $n$ is odd. And the sequence $(1,0,1,0,1,0,...)$ does not converge.

Isolated vertex

Consider the first-order formula $\varphi$ that says that there is an isolated vertex: $\exists x\forall y\lnot E(x,y)$. We have $\mu _{n}(\varphi )\leq {\frac {n\cdot 2^{\binom {n-1}{2}}}{2^{\binom {n}{2}}}}={\frac {n}{2^{n-1}}}$

Indeed, first $2^{\binom {n}{2}}$is the total number of graphs with exactly $n$ vertices. Second, there are $n$ choices for the isolated vertex, and $2^{\binom {n-1}{2}}$ways to put edges on the remaining vertices. Thus, $n\cdot 2^{\binom {n-1}{2}}$is an upper bound on the number of graphs with $n$ vertices having an isolated vertex. Thus, $\mu (\varphi )=0$.

First-order logic

In this section, we consider first-order logic without function symbols. Note that with function symbols, zero-one law may fail. For instance, the formula $p(c)$where $c$ is a constant symbol (i.e. a function symbol of arity 0) would be true half of the times.

Statement

Theorem—First-order logic has the zero-one law: for all first-order formulas $\phi$, either $\mu (\varphi )=0$ or $\mu (\varphi )=1$.

First-order logic has the zero-one law. The main ingredients of the proof presented in (their proof is about first-order logic with infinite conjunctions and disjunctions but the idea is similar) are the following.

First we introduce so-called extension axioms. The extension axiom $EA_{n,m}$ says that for any two disjoint subsets $X$ and $Y$ of respective cardinality $n$ and $m$, there is a point $z$ connected to any points in $X$, but no points in $Y$. We show that $\mu (EA_{n,m})=1$.

Second, via pebble games, they prove that if two finite graphs satisfy all the extension axioms $EA_{n,m}$ with $n,m\leq k$, then they satisfy the same first-order formulas with at most $k$ variables.

Decidability

The Rado graph which is the model in which true formulas are exactly the formulas $\varphi$ such that $\mu (\varphi )=1$

Theorem—It is decidable to know whether $\mu (\varphi )=0$ or $\mu (\varphi )=1$ for a given first-order formula $\phi$.

We can define the theory ${\textbf {EA}}$ of all extension axioms. This theory is $\omega$-categorial, meaning that it has only one countable model up to isomorphism. It turns out that model is the Rado graph. Thus, by Lowenheim-Skolem theorem, we can prove that ${\textbf {EA}}$ is complete, meaning that for any sentence $\varphi$, either $\varphi$ or $\lnot \varphi$ is entailed by ${\textbf {EA}}$. As ${\textbf {EA}}$ is recursive (we have an algorithm that tells whether a formula is an extension axiom or not), we can decide whether $\varphi$ or $\lnot \varphi$ is entailed by ${\textbf {EA}}$, which is equivalent to deciding whether $\mu (\varphi )=1$ or $\mu (\varphi )=0$. Moreover this problem has been shown to be PSPACE-complete.

Other logics

The following logics have the zero-one law:

• First-order logic (as seen above)
• First-order logic $L_{\infty \omega }^{\omega }$ with infinite conjunctions and disjunctions (see Theorem 12.2 in )
• First-order logic with least fixed-point operators, first-order logic with inflationary fixed-point operators, with partial fixed-point operators (see Corollary 12.3 in )
• $\exists SO(\exists ^{*}\forall ^{*})$ (see Theorem 12.12 in )
• $\exists SO(\exists ^{*}\forall \exists ^{*})$ (see Theorem 12.15 in )
• First-order logic on grids

The following logics do not have the zero-one law:

• First-order logic with least fixed-point operators with a predicate < interpreted as a total order on the domain (see second paragraph after Corollary 12.3 in )
• $\exists SO(\forall \forall \exists )$ even if the FO part does not use equality (see Theorem 12.16 in )
• MSO (see Exercice 12.6 in )
• First-order logic with unary function symbols does not have the zero-one law, but has the convergence law, meaning that for all formulas $\varphi$, the quantity $\mu _{n}(\varphi )$ converges.