I wrote my Bachelor’s thesis at the Programming Systems Lab at Saarland university, advised by Dominik Kirst, and Yannick Forster and supervised by Gert Smolka. Broadly, the thesis dealt with completeness proofs of first-order logic in a constructive setting, more specifically the type theory of Coq which was used to mechanize all of thesis' results.
The thesis can be roughly split into two halves. The first half is concerned with the ∀,→,⊥-fragment of first-order logic, both over Tarski and Kripke models. We unify different known results into a coherent construction: For both kinds of models, the fragment is constructively complete for minimal models (which treat ⊥ as an arbitrary logical constant) and exploding models (which treat ⊥ positively). Completeness for standard models (which interpret ⊥ as an absurdity) is equivalent to Markov’s principle and thus not provable in the pure type theory of Coq.
The second half is concerned with Lorenzen’s formal dialogues for intuitionistic first-order logic. For this, we first adapt Sørensen’s and Urzyczyn’s generic completeness proof for finitely branching, classical dialogues to infinitely branching, intuitionistic dialogues. We then specialize it to obtain a completeness proof for full intuitionistic first-order logic.
- Forster, Kirst, Wehr. Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory [View preprint]
LFCS 2020, Deerfield Beach, Florida, USA, 2020.
- Forster, Kirst, Wehr. Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory: Extended Version [View preprint]
Journal of Logic and Computation, Volume 31, Issue 1, January 2021
- Herbelin, Ilik. An analysis of the constructive content of Henkin’s proof of Gödel’s completeness theorem. Draft, 2016
- Schumm. A Henkin-style completeness proof for the pure implica-tional calculus. Notre Dame J. Formal Logic, 16(3):402–404, 1975.
- Herbelin, Lee. Forcing-based cut-elimination for Gentzen-style intuitionistic sequent calculus. Workshop on Logic, Language, Information and Computation, 2009
- Sørensen, Urzyczyn. Sequent calculus, dialogues, and cut elimination. Reflections on Type Theory, λ-Calculus, and the Mind, p. 253-261, 2007