Henkin's completeness proof: forty years later.
Hugues Leblanc, Peter J. Roeper, Michael Thau, George E. Weaver · Notre Dame Journal of Formal Logic · 1991
1 In his 1949 paper, completeness of the first-order calculus, Henkin developed what is now called the method of (individual) terms to establish that every consistent set of statements of a first-order language L a model of cardinality α, a the number of statements of L. The idea is to start with such a set S, construct a so-called term-extension L of L by adding a new terms to the vocabulary of L, extend 5 to a maximally consistent and term-complete set Soo of statements of L, and construct a model of S& whose domain consists of the terms of L. When restricted to L, the model in question automatically constitutes one of S. Henkin's result come to be known as the Strong Completeness Theorem for First-Order L. Another, and more familiar, version of the theorem it that if a statement A ofL is true in every model of a set S of statements ofL, then A is provable from S. Henkin himself did not bother to prove this. He merely proved the special case of it, known as the Weak Completeness Theorem for First-Order L9 where S is 0 . A model like the one Henkin constructed for his set Ŝ , is commonly known as a Henkin model. It is the kind of model in which each member of the domain has a name. Henkin accomplished this by making each member of his domain a name of itself, a radical move at the time. In consequence, though, the restriction of his model to L does not constitute a Henkin model of S, a pity in the event that S does have such a model. To commemorate the publication of Henkin's paper, we offer here two new completeness proofs for first-order Z,. The language considered by Henkin had an unspecified number of terms to start with, but those played no special role in his proof. The one we construct in Section 2 denumerably many, and these will play a crucial role in our proofs. In the first of them, begun in Section 3 and concluded in Section 5, no new terms will be added; in the second, presented in Section 5 and relating to truth-value semantics, denumerably many will be. The proofs are sharpenings of proofs of Leblanc's in [10]. They have two cases each, Case One minding the consistent sets of statements of L that extend without the