May I have some clarification about original proof of Gödel's Completeness Theorem compared to "standard" Henkin's proof based on Model Existence Lemma ?

My understanding of Gödel's original proof is this :

1) Perform some syntactical transformation, in order to reduce the general problem to a particular class of wffs

2) Build an assignment of object to te free vars of the "reduced" formula in order to satisfy it. The assignment is built up using n-uples of natural number corresponding to index of the free vars.

3) The last step is made using some sort of König's Lemma.

From a "philosophical" perspective, Gödel made two assumptions (in line with his "platonism") : the existence of natural number and some properties of infinite sets (König's Lemma).

The Henkin proof needs (if I remember well) Zorn's Lemma and build up the model using only "syntactical objects" : the constants of the language as witnesses.

There are also other proofs (based on Ultrafilters) but they are (for me) less transparent then Henkin's one.

So it seems to me that the theorem needs a "big amount" of set theory. Is it true ? If so, this fact gives us some information about the foundational issue regarding first-order logic and higher-order logic (according to Quine : not "real" logic at all, but set theory in disguise) ?


  • 4
    $\begingroup$ This is not a forum, it is a question and answer site. So please ask clear questions on mathematics. $\endgroup$ – Michael Greinecker Nov 12 '13 at 10:09
  • $\begingroup$ You can try to re-ask the question by pinpointing the exact spot where you need clarification. (It would be better to ask a new question.) Please read very carefully the advice given in the help center mathoverflow.net/help It might also help to look at how other questions are asked at this site, with attention to precision and specificity. $\endgroup$ – Todd Trimble Nov 12 '13 at 12:16
  • 4
    $\begingroup$ Henkin's proof was a genuine simplification. Goedel's original proof used a lot of Skolem-function type ideas to construct the model. Henkin realized---he has said that the proof came to him in a dream---that it suffices merely that the witness be provided by a constant, and the witness need not be so closely tied to the objects for which it is the witness. $\endgroup$ – Joel David Hamkins Nov 12 '13 at 12:32
  • 5
    $\begingroup$ I would encourage you to edit your question to make it more plain that you are familiar with Goedel's original proof of the completeness theorem (since logicians these days are not usually familiar with the original argument), and you want to know whether Henkin's proof is merely a technical simplification, or does it provide greater insight. I think that would be a great question and it should be re-opened. (I've already voted to re-open, since I would be interested to see such answers from those more knowledgeable than I am with Godel's historical argument.) $\endgroup$ – Joel David Hamkins Nov 12 '13 at 15:01
  • 1
    $\begingroup$ I have also voted to reopen, but/and I second Joel's comment re: editing. $\endgroup$ – Noah Schweber Nov 12 '13 at 19:10

With regard to the amount of set theory required to prove the completeness theorem, the wikipedia page on The completeness theorem asserts:

When considered over a countable language, the completeness and compactness theorems are equivalent to each other and equivalent to a weak form of choice known as weak König's lemma, with the equivalence provable in RCA0 (a second-order variant of Peano arithmetic restricted to induction over Σ01 formulas). Weak König's lemma is provable in ZF, the system of Zermelo–Fraenkel set theory without axiom of choice, and thus the completeness and compactness theorems for countable languages are provable in ZF. However the situation is different when the language is of arbitrary large cardinality since then, though the completeness and compactness theorems remain provably equivalent to each other in ZF, they are also provably equivalent to a weak form of the axiom of choice known as the ultrafilter lemma. In particular, no theory extending ZF can prove either the completeness or compactness theorems over arbitrary (possibly uncountable) languages without also proving the ultrafilter lemma on a set of same cardinality, knowing that on countable sets, the ultrafilter lemma becomes equivalent to weak König's lemma.

| cite | improve this answer | |
  • $\begingroup$ I deleted an answer I had given because I had not read Joel's answer sufficiently well. The only new bit of information that it had was that it was Henkin himself who showed the equivalence of the compactness theorem and the completeness theorem with the ultrafilter lemma. The reference being: Metamathematical theorems equivalent to the prime ideal theorems for Boolean algebras, Bull. Amer. Math. Soc, 60, pages 387--388, 1954. $\endgroup$ – tci Nov 13 '13 at 19:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.