Completeness theorems for first-order logic analysed in constructive type theory

DOI10.1007/978-3-030-36755-8_4MaRDI QIDQ2177578zbMATH OpenOpenAlexFDO

Authors Yannick Forster, Dominik Kirst, Dominik Wehr

Publication date 6 May 2020

Full work available at URL https://arxiv.org/abs/2006.04399

Mathematics Subject Classification ID

Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35) Type theory (03B38) Metamathematics of constructive systems (03F50)

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 `a la Tarski and Kripke is not readily constructive, we analyse connections of completeness theorems to Markov's Principle and Weak K"onig'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.

Recommendations

• Intuitionistic completeness of first-order logic
• Unified Classical Logic Completeness
• Theorem Proving in Higher Order Logics
• Semantic completeness of first-order theories in constructive reverse mathematics
• The completeness of Heyting first-order logic

Cited in

(26)

• Constructive and mechanised meta-theory of intuitionistic epistemic logic
• Soundness and completeness proofs by coinductive methods
• Semantic completeness of first-order theories in constructive reverse mathematics
• Krull dimension of types in a class of first-order theories
• On the meaning of logical completeness
• scientific article; zbMATH DE number 5872251 (Why is no real title available?)
• The completeness of Heyting first-order logic
• scientific article; zbMATH DE number 3853065 (Why is no real title available?)
• Analytic Tableaux for Simple Type Theory and its First-Order Fragment
• (In)consistency of Extensions of Higher Order Logic and Type Theory
• scientific article; zbMATH DE number 1341477 (Why is no real title available?)
• scientific article; zbMATH DE number 1507179 (Why is no real title available?)
• Formalizing the meta-theory of first-order predicate logic
• Optimized encodings of fragments of type theory in first order logic
• Constructive completeness for modal logic with transitive closure
• Completeness theorems for first-order logic analysed in constructive type theory
• Trakhtenbrot’s Theorem in Coq
• scientific article; zbMATH DE number 7566073 (Why is no real title available?)
• scientific article; zbMATH DE number 226803 (Why is no real title available?)
• Completeness in Proof-Theoretic Semantics
• Material dialogues for first-order logic in constructive type theory
• \textsf{LOGIC}: a Coq library for logics
• Logical consequence and first-order soundness and completeness: a bottom up approach
• Material dialogues for first-order logic in constructive type theory: extended version
• Countability of inductive types formalized in the object-logic level
• Separating Markov's principles

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Completeness theorems for first-order logic analysed in constructive type theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2177578)