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?