English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We study various formulations of the completeness of first-order logicphrased in constructive type theory and mechanised in the Coq proof assistant.Specifically, we examine the completeness of variants of classical andintuitionistic natural deduction and sequent calculi with respect tomodel-theoretic, algebraic, and game-theoretic semantics. As completeness withrespect to the standard model-theoretic semantics \`a la Tarski and Kripke isnot readily constructive, we analyse connections of completeness theorems toMarkov's Principle and Weak K\"onig's Lemma and discuss non-standard semanticsadmitting assumption-free completeness. We contribute a reusable Coq libraryfor first-order logic containing all results covered in this paper.

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