[FOM] From Compactness to Completeness (corrected and expanded)

[Stephen G Simpson]

G. Aldo Antonelli writes:
 > The question (which at least I took myself to be presenting to the
 > list) is whether the *weaker* form of completeness also requires
 > K"onig's lemma.
 > 
 > By the weaker version of completeness I meant the claim that every
 > valid first-order formula is provable, the proof of which usually
 > proceeds by extracting a counter-model from a non-terminating proof
 > search.

This weak version of completeness "requires" a weak version of
K"onig's Lemma, provided we interpret "requires" as it is usually
interpreted in reverse mathematics.  Namely, the weak version of
completeness is equivalent over RCA_0 to a statement which we might
call

   Lightface Weak K"onig's Lemma:

   Every infinite computable subtree of the full binary tree has an
   infinite path.

Of course Lightface Weak K"onig's Lemma is not provable in RCA_0,
because not every infinite computable subtree of the full binary tree
has a computable infinite path.

On the other hand, the weak version of completeness does not "require"
the full K"onig's Lemma.  The distinction is somewhat subtle.  Weak
K"onig's Lemma says: every infinite subtree of the full binary tree
has an infinite path.  K"onig's Lemma says: every infinite, finitely
branching tree has an infinite path.  See also Sections IV.3 and III.7
of my book, Subsystems of Second Order Arithmetic.

Let me use this opportunity to make a general comment on reverse
mathematics which perhaps has not been sufficiently emphasized.

The explicit purpose of reverse mathematics is to discover which set
existence axioms are needed in order to prove core mathematical
theorems.  However, most mathematicians (including me) do not view the
Completeness Theorem and other theorems of mathematical logic as
"core" mathematics.  In this sense, Section III.7 of my book does not
by itself establish Weak K"onig's Lemma as a standard axiom for
reverse mathematics.  Similarly, my remark above does not by itself
establish Lightface Weak K"onig's Lemma as a standard axiom for
reverse mathematics.

In case somebody would like to see a more "core-like" mathematical
statement which is equivalent to Lightface Weak K"onig's Lemma, I
offer the following.

  Define a Wang tile to be a unit square with colored edges.  Let F be
  a finite set of Wang tiles.  Consider the problem of tiling the
  plane with copies of tiles from F in such a way that adjacent tiles
  have matching colors on the common edge.  Assume that for each n it
  is possible to tile an n by n square.  Then, it is possible to tile
  the entire plane.

The fact that Lightface Weak K"onig's Lemma is equivalent over RCA_0
to this statement about tiling problems can be proved using the
somewhat difficult techniques of Berger, Robinson, and Myers.

 @Book{berger,
   author          {Robert Berger},
   title           {The {U}ndecidability of the {D}omino {P}roblem},
   publisher       {American Mathematical Society},
   year            1966,
   number          66,
   series          {Memoirs of the American Mathematical Society},
   note            {72 pages}}

 @Article{rr-tilings,
   author          {Raphael M. Robinson},
   title           {Undecidability and nonperiodicity of tilings
            of the plane},
   journal         {Inventiones Mathematicae},
   year            1971,
   volume          12,
   pages           {177--209}
 }

 @Article{myers-tilings,
   author          {Dale Myers},
   title           {Nonrecursive tilings of the plane, {II}},
   journal         {Journal of Symbolic Logic},
   year            1974,
   volume          39,
   pages           {286--294}
 }

Stephen G. Simpson
Professor of Mathematics
Pennsylvania State University
http://www.math.psu.edu/simpson/
foundations of mathematics, recursion theory, mathematical logic