Leon Henkin is a logician, currently Emeritus Professor at the University of California at Berkeley. He is principally known for the "Henkin Completeness Proof": his version of the proof of the semantic completeness of standard systems of first-order logic.

Henkin's result was not novel — it had first been proved by Kurt Gödel in his doctoral dissertation which was completed in 1929. (See Gödel's completeness theorem. Gödel published a version of the proof in 1930.) Henkin's proof is much easier to survey than Gödel's and has thus become the standard choice of completeness proof for presentation in introductory classes and texts.

It is non-constructive (a pure existence proof): while it assures you that if a sentence α follows (semantically) from a set of sentences Σ, then there is a proof of α from Σ, it gives no indication of the nature of that proof.

Later, Henkin generalized this result to a variant of Church's higher-order logic. This variant uses general models (also called Henkin models): the higher types need not be interpreted by the full space of functions - a subset of the function space may be used instead.

References

• Henkin, Leon. 1949. The Completeness of the First-Order Functional Calculus, Journal of Symbolic Logic. 14: 159-166.
• Henkin, Leon. 1950. Completeness in the theory of types, Journal of Symbolic Logic 15: 81-91.

External links

• An interview with Henkin and others about their experiences at Princeton
• An interview with Henkin about his experience at Princeton

Year of birth missing | 20th century mathematicians | Logicians | American mathematicians

Leon Henkin | Leon Henkin