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 φ {\displaystyle \varphi } in some logic, we define μ n ( φ ) {\displaystyle \mu _{n}(\varphi )} to be the proportion of graphs that satisfy φ {\displaystyle \varphi } among the graphs with exactly n {\displaystyle n} vertices. We say that a logic has the zero-one law if μ n ( φ ) {\displaystyle \mu _{n}(\varphi )} converges to 1 or 0, for any sentence φ {\displaystyle \varphi } of that logic. We set μ ( φ ) {\displaystyle \mu (\varphi )} to be that limit to which μ n ( φ ) {\displaystyle \mu _{n}(\varphi )} converges when n {\displaystyle 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 φ {\displaystyle \varphi } does not have the zero-one law. Indeed, μ n ( φ ) = 1 {\displaystyle \mu _{n}(\varphi )=1} if n {\displaystyle n} is even and μ n ( φ ) = 0 {\displaystyle \mu _{n}(\varphi )=0} if n {\displaystyle n} is odd. And the sequence ( 1 , 0 , 1 , 0 , 1 , 0 , . . . ) {\displaystyle (1,0,1,0,1,0,...)} does not converge.
Isolated vertex Consider the first-order formula φ {\displaystyle \varphi } that says that there is an isolated vertex: ∃ x ∀ y ¬ E ( x , y ) {\displaystyle \exists x\forall y\lnot E(x,y)} . We have μ n ( φ ) ≤ n ⋅ 2 ( n − 1 2 ) 2 ( n 2 ) = n 2 n − 1 {\displaystyle \mu _{n}(\varphi )\leq {\frac {n\cdot 2^{\binom {n-1}{2}}}{2^{\binom {n}{2}}}}={\frac {n}{2^{n-1}}}}
Indeed, first 2 ( n 2 ) {\displaystyle 2^{\binom {n}{2}}} is the total number of graphs with exactly n {\displaystyle n} vertices. Second, there are n {\displaystyle n} choices for the isolated vertex, and 2 ( n − 1 2 ) {\displaystyle 2^{\binom {n-1}{2}}} ways to put edges on the remaining vertices. Thus, n ⋅ 2 ( n − 1 2 ) {\displaystyle n\cdot 2^{\binom {n-1}{2}}} is an upper bound on the number of graphs with n {\displaystyle n} vertices having an isolated vertex. Thus, μ ( φ ) = 0 {\displaystyle \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 ) {\displaystyle p(c)} where c {\displaystyle c} is a constant symbol (i.e. a function symbol of arity 0) would be true half of the times.
Statement
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 E A n , m {\displaystyle EA_{n,m}} says that for any two disjoint subsets X {\displaystyle X} and Y {\displaystyle Y} of respective cardinality n {\displaystyle n} and m {\displaystyle m} , there is a point z {\displaystyle z} connected to any points in X {\displaystyle X} , but no points in Y {\displaystyle Y} . We show that μ ( E A n , m ) = 1 {\displaystyle \mu (EA_{n,m})=1} . Second, via pebble games, they prove that if two finite graphs satisfy all the extension axioms E A n , m {\displaystyle EA_{n,m}} with n , m ≤ k {\displaystyle n,m\leq k} , then they satisfy the same first-order formulas with at most k {\displaystyle k} variables.
Decidability
We can define the theory EA {\displaystyle {\textbf {EA}}} of all extension axioms. This theory is ω {\displaystyle \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 EA {\displaystyle {\textbf {EA}}} is complete, meaning that for any sentence φ {\displaystyle \varphi } , either φ {\displaystyle \varphi } or ¬ φ {\displaystyle \lnot \varphi } is entailed by EA {\displaystyle {\textbf {EA}}} . As EA {\displaystyle {\textbf {EA}}} is recursive (we have an algorithm that tells whether a formula is an extension axiom or not), we can decide whether φ {\displaystyle \varphi } or ¬ φ {\displaystyle \lnot \varphi } is entailed by EA {\displaystyle {\textbf {EA}}} , which is equivalent to deciding whether μ ( φ ) = 1 {\displaystyle \mu (\varphi )=1} or μ ( φ ) = 0 {\displaystyle \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 ∞ ω ω {\displaystyle 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 )
∃ S O ( ∃ ∗ ∀ ∗ ) {\displaystyle \exists SO(\exists ^{*}\forall ^{*})} (see Theorem 12.12 in )
∃ S O ( ∃ ∗ ∀ ∃ ∗ ) {\displaystyle \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 )
∃ S O ( ∀ ∀ ∃ ) {\displaystyle \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 φ {\displaystyle \varphi } , the quantity μ n ( φ ) {\displaystyle \mu _{n}(\varphi )} converges.
References