A Constructive Analysis of First-Order Completeness Theorems in Coq

Type: Bachelor’s thesis
Advisors: Dominik Kirst and Yannick Forster
Supervisor: Gert Smolka
Institution: Saarland University, Programming Systems Lab

Digital copy: Available here
Coq mechanization: CoqDoc and github

Resulting Publications

Abstract

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 ⊥ pos- itively, 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 require- ments for multiple variants of standard completeness by identifying the principle of double-negation elimination and two different formulations of Markov’s princi- ple 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 complete- ness 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.