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.

Resulting Publications

Main References