Completeness theorems for first-order logic analysed in constructive type theory: Extended version. (21st January 2021)

• Record Type: Journal Article
• Authors: Forster, Yannick; Kirst, Dominik; Wehr, Dominik
• Is Part Of: Journal of logic and computation. Volume 31:Number 1(2021)
• Page Start: 112
• Page End: 151
• Publication Date: 2021-01-21
• Subjects: First-order logic -- completeness -- type theory -- Tarksi semantics -- Kripke semantics -- algebraic semantics -- dialogue semantics -- constructive logic -- constructive reverse mathematics -- Coq; Logic programming -- Periodicals; Logic, Symbolic and mathematical -- Periodicals; Computational complexity -- Periodicals; 005.115
• DOI: 10.1093/logcom/exaa073
• Languages: English
• ISSNs: 0955-792X

Abstract

Abstract: We study various formulations of the completeness of first-order logic phrased in constructive type theory and mechanised in the Coq proof assistant. Specifically, we examine the completeness of variants of classical and intuitionistic natural deduction and sequent calculi with respect to model-theoretic, algebraic, and game-theoretic semantics. As completeness with respect to the standard model-theoretic semantics à la Tarski and Kripke is not readily constructive, we analyse connections of completeness theorems to Markov's Principle and Weak Kőnig's Lemma and discuss non-standard semantics admitting assumption-free completeness. We contribute a reusable Coq library for first-order logic containing all results covered in this paper.