论文标题
在建设性类型理论（扩展版本）中分析的一阶逻辑的完整定理（扩展版）
Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory (Extended Version)
论文作者
论文摘要
我们研究了在建设性类型理论中的一阶逻辑词的完整性，并在COQ证明助手中机械化的各种公式。具体而言，我们研究了相对于模型理论，代数和游戏理论语义的古典和直觉自然推论和序列骨的变体的完整性。关于标准模型理论语义的完整性 - tarski和Kripke并不容易建设性，我们分析了完整性定理与马尔可夫原理的联系，并弱König的引理，并讨论非标准的语义，以承认无假设的完整性。我们为一阶逻辑提供了可重复使用的COQ库，其中包含本文中涵盖的所有结果。
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.
