Henkin on Completeness

Abstract

The Completeness of Formal Systems is the title of the thesis that Henkin presented at Princeton in 1947 under the supervision of Alonzo Church. A few years after the defense of his thesis, Henkin published two papers in the Journal of Symbolic Logic: the first, on completeness for first-order logic (Henkin in J. Symb. Log. 14(3):159–166, 1949), and the second one, devoted to completeness in type theory (Henkin in J. Symb. Log. 15(2):81–91, 1950). In 1963, Henkin published a completeness proof for propositional type theory (Henkin in J. Symb. Log. 28(3):201–216, 1963), where he devised yet another method not directly based on his completeness proof for the whole theory of types. In this paper, these tree proofs are analyzed, trying to understand not just the result itself but also the process of discovery, using the information provided by Henkin in Bull. Symb. Log. 2(2):127–158, 1996. In the third section, we present two completeness proofs that Henkin used to teach us in class. It is surprising that the first-order proof of completeness that Henkin explained in class was not his own but was developed by using Herbrand’s theorem and the completeness of propositional logic. In 1963, Henkin published An extension of the Craig–Lyndon interpolation theorem, where one can find a different completeness proof for first-order logic; this is the other completeness proof Henkin told us about. We conclude this paper, by introducing two expository papers on this subject. Henkin was an extraordinary insightful professor, and in 1967, he published two works that are very relevant for the subject addressed here: Truth and provability (Henkin in Philosophy of Science Today, pp. 14–22, 1967) and Completeness (Henkin in Philosophy of Science Today, pp. 23–35, 1967).