AN ANALYSIS OF THE CONSTRUCTIVE CONTENT OF HENKIN’S PROOF OF GÖDEL’S COMPLETENESS THEOREM

Abstract Gödel’s completeness theorem for classical first-order logic is one of the most basic theorems of logic. Central to any foundational course in logic, it connects the notion of valid formula, i.e., a formula satisfied in all models, to the notion of provable formula. We survey a few standard formulations and proofs of the completeness theorem before focusing on the formal description of a slight modification of Henkin’s proof within intuitionistic second-order arithmetic. It is usual, in the context of the completeness of intuitionistic logic with respect to various semantics, such as Kripke or Beth semantics, to follow the Curry–Howard correspondence and to interpret the proofs of completeness as programs which turn proofs of validity for these semantics into proofs of derivability. We apply this approach to Henkin’s proof to phrase it as a program which transforms any proof of validity with respect to Tarski semantics into a proof of derivability. By doing so, we hope to shed some “effective” light on the relation between Tarski semantics and syntax: proofs of validity are syntactic objects with which we can compute.