Computing with Gödel's Completeness Theorem

Explore the computational aspects of Gödel's completeness theorem in this 46-minute lecture from the Hausdorff Trimester Program on Types, Sets and Constructions. Delve into various approaches to computing with Gödel's completeness, including the work of Krivine, Berardi, and Valentini using "exploding models" and A-translation. Examine a direct computational formulation of Henkin's proof and investigate a novel approach that utilizes Kripke forcing translation. Discover how this method transforms the completeness statement into one concerning Kripke semantics. Learn about the concept of direct-style provability for Kripke forcing translation and its parallels with classical logic. Uncover the computational content of this approach, which "reifies" a proof of validity into a proof of derivability, offering new insights into the relationship between logic and computation.

Hugo Herbelin: Computing with Gödel's Completeness Theorem