Dominik Wehr: Bachelor's Thesis

Saarland University Computer Science

Constructive analysis of first-order completeness proofs in Coq

Advisors: Dominik Kirst, Yannick Forster


Completeness and soundness are important properties of many deduction systems. A deduction system is complete if every semantically valid formula can be derived in that system. As first-order logic is widely used, a proof of its completeness, first given by Gödel in 1929 and later simplified by Henkin in 1947, is of great interest. The proof of first-order completeness has traditionally been presented using classical assumptions.

In my Bachelor's thesis, I will analyze various completeness proofs for first-order logic on their constructiveness by formalizing them in the interactive proof assistant Coq. Among them, a constructive proof of Henkin's model existence theorem for classical first-order logic, mainly due to a proof by Herbelin and Ilik, a proof of completeness of Kripke semantics with exploding models for an intuitionistic first-order Gentzen system, due to Herbelin and Lee, and a proof of completeness of generalized intuitionistic dialogues based on the approach of Sørensen and Urzyczyn.



Legal notice, Privacy policy