Blog
About

1
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory (Extended Version)

      Preprint

      , ,

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          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.

          Related collections

          Author and article information

          Journal
          08 June 2020
          Article
          2006.04399

          http://arxiv.org/licenses/nonexclusive-distrib/1.0/

          Custom metadata
          extended version of https://link.springer.com/chapter/10.1007/978-3-030-36755-8_4
          cs.LO math.LO

          Theoretical computer science, Logic & Foundation

          Comments

          Comment on this article