Publication details
Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory
Yannick Forster, Dominik Kirst, Dominik Wehr
Symposium on Logical Foundations Of Computer Science (LFCS 2020), January 4-7, 2020, Deerfield Beach, Florida, U.S.A., January 2020
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 semantics. As completeness with respect to standard model-theoretic semantics is not readily constructive, we analyse the assumptions necessary for particular syntax fragments 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.
Link to Coq formalisation
Download PDF
Show BibTeX
@CONFERENCE{ForsterEtAl:2019:Completeness,
title = {Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory},
author = {Yannick Forster and Dominik Kirst and Dominik Wehr},
year = {2020},
month = {Jan},
booktitle = {Symposium on Logical Foundations Of Computer Science (LFCS 2020), January 4-7, 2020, Deerfield Beach, Florida, U.S.A.},
}
Login to edit
Legal notice, Privacy policy
