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.

**References**

Henkin, Leon. 1949. "The Completeness of the First-Order Functional Calculus", *Journal of Symbolic Logic*. 14: 159-166.

*This article is a stub. You can help Wikipedia by fixing it.*