Advisors: Dominik Kirst, Yannick Forster
First-order logic stands out among systems of similar expressivity as its deduction systems can be shown to be complete with regards to naive semantic accounts of validity. A deduction system is complete if it can prove every semantically valid formula. Historically, many proofs of first-order completeness have relied on non-constructive reasoning principles. In this thesis, we analyze multiple completeness theorems for variants of Gentzen's natural deduction and sequent calculus with regards to model and game semantics for first-order logic to determine which non-constructive principles are required to prove them.
In the first half of this thesis, we constructively analyze completeness theorems for the ∀,→,⊥-fragment of first-order logic with regards to different notions of Tarski and Kripke models. We show that Veldman exploding models, which treat ⊥ positively, and minimal models, which treat ⊥ as an arbitrary logical constant, admit fully constructive completeness proofs. We also demonstrate the non-constructivity of completeness with regards to standard Tarski and Kripke models by relating them to the stability of provability. We derive tight characterizations of the requirements for multiple variants of standard completeness by identifying the principle of double-negation elimination and two different formulations of Markov's principle with the stability of provability restricted to different classes of theories.
The second half of the thesis is concerned with dialogue game semantics for full intutionistic first-order logic. We first give generic and fully constructive completeness proofs with regards to formal intuitionistic E- and D-dialogues. We then derive the completeness of the full intuitionistic sequent calculus with regards to formal first-order dialogues from this general result.
The analyses of this thesis are carried out in the calculus of inductive constructions and have been formalized in the interactive proof assistant Coq.