8
$\begingroup$

Godel's Completeness Theorem is a straightforward consequence of Skolem 1922 and yet this conclusion was not drawn by Skolem himself. In a letter to Wang (Dec. 7, 1967 in Godel 2003) Godel gives an explanation for this oversight:

At that time, nobody (including Skolem himself) drew this conclusion ... I think the explanation is not hard to find. It lies in a widespread lack, at that time, of the required epistemological attitude toward metamathematics and toward nonfinitary reasoning.

I know some form of Konig's Infinity Lemma or the "law of infinite conjunction" (Quine) is necessary to prove semantic completeness, but (a) is this what Godel must be referring to as "nonfinitary reasoning", and (b) where/how does this law figure in Godel's original proof?

Improve this question
$\endgroup$
2
  • 3
    $\begingroup$ Can you give a more precise reference for "Skolem 1922" and for the claim that the completeness theorem is a straightforward consequence? $\endgroup$
    – Alex Kruckman
    Commented Jul 17, 2019 at 23:53
  • $\begingroup$ @AlexKruckman Godel says before the quote above: "The completeness theorem, mathematically, is indeed an almost trivial consequence of Skolem 1922." Goldfarb and Wang corroborate this. Skolem 1922 is "Some Remarks on Axiomatized Set Theory" in From Frege to Godel. $\endgroup$
    – Mallik
    Commented Jul 18, 2019 at 3:04

1 Answer 1

Reset to default
9
$\begingroup$

The best write-up I know of Godel's proof of the completeness theorem is by Avigad, in his paper Godel and the metamathematical tradition (section $4$). Avigad divides the proof into $5$(ish) steps, and step $2$ crucially uses Konig's lemma:

Step $2$: If a set $\Gamma$ of propositional formulas is not refutable, it has a satisfying truth assignment. Write $\Gamma=\{\varphi_0,\varphi_1,\varphi_2,...\}$. Build a finitely branching tree where the nodes at level one are all the truth assignments to variables of $\varphi_0$ that make $\varphi_0$ true; the nodes at level two are all the truth assignments to variables of $\varphi_0\wedge\varphi_1$ that make that formula true; and so on. (The descendants of a node are all the truth assignments that extend it.) If, at some level $k$, there is no satisfying assignment to $\varphi_0\wedge\varphi_1\wedge ...\wedge\varphi_{k-1}$, then, by step $1$, $\Gamma$ is refutable. Otherwise, by Konig’s lemma, there is a path through the tree, which corresponds to a satisfying truth assignment for $\Gamma$.

(Emphasis mine.) This is the only way Konig gets used here.

Specifically, here's what's going on in the rest of the proof:

  • Step $1$ is just the completeness theorem for propositional logic for individual sentences (which Step $2$ lifts to sets of sentences via Konig).

  • Step $3$ shows completeness for individual $\forall^*\exists^*$-sentences without function symbols or equality, and is entirely straightforward.

  • Step $4$ extends Step $3$ to individual sentences without function symbols or equality to arbitrary-complexity sentences, a la Skolem.

  • Step $???$ extends the result of Steps $3$ and $4$ to arbitrary sets of such sentences. Avigad doesn't mention this step by name, instead relegating it to the end of Steps $3$ and $4$, but I think it's worth stating separately. However, this extension doesn't involve an application of Konig's lemma, just annoying bookkeeping.

  • Step $5$ wraps everything up by observing that function symbols can be replaced by relation symbols and additional axioms saying they behave as graphs of functions, and that equality can be replaced with a binary relation together with new axioms for its handling (we just take an appropriate quotient structure at the end of the day). This is again entirely straightforward.

As to whether that's what Godel meant by "nonfinitary reasoning," I'm not sure. Personally Skolem 1922 already feels pretty nonfinitary (in a good way) to me. My personal guess is that it's a bit more subtle than that: the missing philosophical ingredient was perhaps the realization that nonfinitary methods are relevant to finitary conclusions, even in foundational topics. As opposed to an elementary submodel, a proof is a fully finite object, and it was definitely surprising to me at least that infinitary reasoning could be used to demonstrate the existence of a proof (in fact, the completeness theorem itself deeply shocked me when I first learned it).

Improve this answer
$\endgroup$
7
  • $\begingroup$ The existence of a proof is a nonconstructive result though, right, just by contraposition of the model existence formulation. Can you say a bit more about why that result was surprising to you? (That answer was very relevant to my purposes). $\endgroup$
    – Mallik
    Commented Jul 18, 2019 at 3:56
  • 2
    $\begingroup$ @Mallik "The existence of a proof is a nonconstructive result though, right, just by contraposition of the model existence formulation." No, you need the completeness theorem to say that - and that's what we're talking about proving in the first place! Pre-completeness theorem, and using anachronistic notation, the set of valid sentences is a priori $\Pi^1_1$ - to check whether a sentence is valid you would need to check every possible (countable) model. Why should there be a "combinatorial" description of validity? The compactness theorem is already incredibly surprising here. (continued) $\endgroup$
    – Noah Schweber
    Commented Jul 18, 2019 at 5:59
  • 3
    $\begingroup$ But completeness goes further. A priori the compactness theorem only says that there is some "finitely-based" proof system characterizing validity, but $(i)$ it doesn't say that there needs to be a computable such system and $(ii)$ it certainly doesn't suggest that such a system could be simply describable - and indeed already discovered! Think of it this way: why, barring the completeness theorem itself, would you expect some particular list of sequent rules to be complete? Completeness is something that is often taken for granted, but it's quite surprising. $\endgroup$
    – Noah Schweber
    Commented Jul 18, 2019 at 6:03
  • 1
    $\begingroup$ More specifically, I would say it's not "there is a completeness result" that is surprising, it's "this tiny easy list of axioms that we know and understand gives a complete system" that is surprising. $\endgroup$
    – Maxime Ramzi
    Commented Jul 18, 2019 at 9:03
  • 1
    $\begingroup$ @Max Oh I see, my bad - I fully agree with you. I interpreted "completeness result" much more narrowly. $\endgroup$
    – Noah Schweber
    Commented Jul 18, 2019 at 22:45

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .