# Gödel's Completeness Theorem

A famous paper by Leon Henkin ("Completeness in the theory of types") begins as follows: "The first order functional calculus was proved complete by Gödel in 1930. Roughly speaking, this proof demonstrates that each formula of the calculus is a formal theorem which becomes a true sentence under every one of a certain intended class of interpretations of the formal system."

I do not understand the latter sentence. Indeed a non-provable formula has no reason to be a formal theorem and no reason to become true under every "sensible" interpretation. For me, it should be something like that: "this proof demonstrates that each formal theorem of the calculus becomes a true sentence under every one of a certain intended class of interpretations of the formal system." Since I trust Leon Henkin as a logician, I guess that I am missing something; maybe is my English the problem and do Henkin's sentence and my sentence have the same meaning?

• In ordinary English, it would be clearer to say that the completeness theorem shows that "each formula which is true in every intended interpretation, is, in fact, a formal theorem." The converse, which seems to be what you are suggesting, also holds but is known as "soundness" rather than "completeness" and is much simpler to prove, as it only requires that the inference rules and logical axioms preserve truth. The completeness proof requires that there are enough axioms and rules to formally prove every logical consequence of the axioms. – Ned Feb 3 '16 at 1:41
• @MauroALLEGRANZA and Rob Arthan: And, as said by Ned, it would be a statement of the trivial direction (the "soundness"), which does not reflect the deep content of Gödel's theorem (which is rather the converse). – user251130 Feb 3 '16 at 20:30
• @user251130: you are right. Mauro's suggestion does not fix the sentence. – Rob Arthan Feb 3 '16 at 23:06