[FOM] From Compactness to Completeness

[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önig'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 weaker version of completeness "requires" Weak K"onig's Lemma, in
the sense that it implies it over RCA_0.  (In fact, the two statements
are equivalent over RCA_0.)  However, it does not "require" the full
K"onig's Lemma.  See Sections IV.3 and III.7 of my book, Subsystems of
Second Order Arithmetic.

Note: 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.

 > Is this true or (which comes to same thing) mentioned in SSOA?

I strove to make SOSOA as comprehensive as possible, but ultimately I
ran up against G"odel's Incompleteness Theorem.

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