[FOM] Compactness and (weak) completeness

[G. Aldo Antonelli]

On 12/29/10 9:00 AM, Stephen Simpson wrote:

> It is provable in RCA_0 that the following are pairwise equivalent.
> 1. The completeness theorem for countable languages.
> 2. The compactness theorem for countable languages.
> 3. WKL_0, i.e., RCA_0 + Weak K"onig's Lemma.
> However, full K"onig's Lemma is equivalent over RCA_0 to the much stronger
> system ACA_0.
> A reference is Section IV.3 of my book Subystems of Second Order
> Arithmetic.

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.

The reason this seems to require a combinatorial principle such as 
(weak) KL is that a non-terminating truth tree (for instance) is such 
that, for every n, it contains an open branch of length n. KL then 
delivers an infinite open branch, from which a counter-model can be 
extracted in standard ways.

Thomas Forster put forward that such use of KL for weak completeness can 
be dispensed with in the case of countable languages. Is this true or 
(which comes to same thing) mentioned in SSOA?

-- Aldo


*****************************************
G. Aldo Antonelli
Professor of Philosophy
University of California, Davis
http://philosophy.ucdavis.edu/antonelli
antonelli at ucdavis.edu +1 530 554 1368