# Bachelor’s Thesis

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.

### Links

### Resulting Publications

- Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory [Preprint]

Yannick Forster, Dominik Kirst, Dominik Wehr

LFCS 2020, Deerfield Beach, Florida, USA, 2020. - Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory: Extended Version [Preprint]

Yannick Forster, Dominik Kirst, Dominik Wehr

Journal of Logic and Computation, Volume 31, Issue 1, January 2021

#### Main References

- An analysis of the constructive content of Henkin’s proof of Gödel’s completeness theorem

Hugo Herbelin, Danko Ilik. Draft, 2016 - A Henkin-style completeness proof for the pure implica-tional calculus

George Schumm. Notre Dame J. Formal Logic, 16(3):402–404, 1975. - Forcing-based cut-elimination for Gentzen-style intuitionistic sequent calculus

Hugo Herbelin, Gyesik Lee. Workshop on Logic, Language, Information and Computation, 2009 - Sequent calculus, dialogues, and cut elimination

Morten Sørensen, Pawel Urzyczyn. Reflections on Type Theory, λ-Calculus, and the Mind, p. 253-261, 2007