Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory

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 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.

Appendices

A Overview of Deduction Systems

Definition 55

Intuitionistic natural deduction is defined as follows:

We write $\vdash \varphi$ whenever $\varphi$ is intuitionistically provable from the empty context.

Definition 56

Classical natural deduction is defined as follows:

We write $\vdash _c\varphi$ whenever $\varphi$ is classically provable from the empty context.

Definition 57

The intuitionistic sequent calculus LJT is defined as follows:

Definition 58

The intuitionistic sequent calculus LJ is defined as follows:

B Notes on the Coq Formalisation

Our formalisation consists of about 7500 lines of code, with an even split between specification and proofs. The code is structured as follows.

Section	Specification	Proofs
Preliminaries Autosubst	169	53
Preliminaries for	680	599
Tarski Semantics	655	682
Kripke Semantics	342	255
On Markov’s Principle	593	978
Preliminaries for	523	430
Heyting Semantics	297	456
Dialogue Semantics	312	488
Total	3571	3941

In general, we find that Coq provides the ideal grounds for formalising projects like ours. It has external libraries supporting the formalisation of syntax, enough automation to support the limited amounts we need and allows constructive reverse mathematics due to its axiomatic minimality.

In the remainder of the section, we elaborate on noteworthy design choices of the formalisation.

Formalisation of Binders. There are various competing techniques to formalise binders in proof assistants. In first-order logic, binders occur in quantification. The chosen technique especially affects the definition of deduction systems and can considerably ease or impede proofs of standard properties like weakening.

We opted for a de Bruijn representation of variables and binders with parallel substitutions. The Autosubst 2 tool [49] provides convenient automation for the definition of and proofs about this representation of syntax.

Notably, our representation then results in very straightforward proofs for weakening with only 5 lines. In contrast, using other representations for binders results in considerably more complicated weakening proofs, e.g. 150 lines in an approach using names [14] and 95 lines in an approach using traced syntax [23].

Also note that first-order logic has the simplest structure of binders possible: Since quantifiers range over terms, but terms do not contain binders, we do not need a prior notion of renaming, as usually standard in de Bruijn presentations of syntax. This observation results in more compact code (because usually, every statement on substitutions has to be proved for renamings first, with oftentimes the same proof) and was incorporated into Autosubst 2, which now does not generate renamings if they are not needed. Furthermore, we remark that the HOAS encoding of such simple binding structures results in a strictly positive inductive type and would thus be in principle definable in Coq.

Formalisation of Signatures. Our whole development is parametrised against a signature, defined as a typeclass in Coq:

We implement term and predicate application using the dependent vector type. While the vector type is known to cause issues in dependent programming, in this instance it was the best choice. Recursion on terms is accepted by Coq’s guardness checker, and while the generated induction principle (as is always the case for nested inductives) is too weak, a sufficient version can easily be implemented by hand:

Syntactic Fragments. There are essentially four ways to formalise the syntactic fragment . First, we could parametrise the type of formulas with tags, as done in [14] and second, we could use well-explored techniques for modular syntax [26, 9]. However, both of these approaches would not be compatible with the Autosubst tool. Additionally, modular syntax would force users of our developed library for first-order logic to work on the peculiar representation of syntax using containers or functors instead of regular inductive types.

The third option is to only define the type , and then define a predicate on this formulas characterising the fragment . This approach introduces many additional assumptions in almost all statements, decreasing their readability and yielding many simple but repetitive proof obligations. Furthermore, we would have to parameterise natural deduction over predicates as well, in order for the (IE) rule to not introduce terms e.g. containing $\dot{\exists }$ when only deductions over should be considered.

To make the formalisation as clear and reusable as possible, we chose the fourth and most simple possible approach: We essentially duplicate the contents of Sect. 2 for both and , resulting in two independent developments on top of the two preliminary parts.

Parametrised Deduction Systems. When defining the minimal, intuitionistic, and classical versions of natural deduction, a similar issue arises. Here, we chose to use one single predicate definition, where the rules for explosion and Peirce can be enabled or disabled using tags, which are parameters of the predicate.

We can then define all considered variants of ND by fixing those parameters:

This definition allows us to give for instance a general weakening proof, which can then be instantiated to the different versions. Similarly, we can give a parametrised soundness proof, and depending on the parameters fix required properties on the models used in the definition of validity.

Object Tactics. At several parts of our developments we have to build concrete ND derivations. This can always be done by explicitly applying the constructors of the ND predicate, which however becomes tedious quickly. We thus developed object tactics reminiscent of the tactics available in Coq. The tactic ointros for instance applies the (II) rule, whereas the tactic oapply can apply hypotheses, i.e. combine the rules (IE) and (C). All object tactics are in the file FullND.v.

Extraction to $\lambda$-Calculus. The proof that completeness of provability w.r.t. standard Tarski and Kripke semantics is equivalent to $\mathsf {MP}_\mathsf {L}$ crucially relies on an $\mathsf {L}$-enumeration of provable formulas. While giving a Coq enumeration is easy using techniques described in [14], the translation of any function to a model of computation is considered notoriously hard. We use the framework by Forster and Kunze [16] which allows the automated translation of Coq functions to $\mathsf {L}$.

Using the framework was mostly easy and spared us considerable formalisation effort. However, the framework covers only simple types, whereas our representation of both terms and formulas contains the dependent vector type. We circumvent this problem by defining a non-dependent term type term’ and a predicate wf characterising exactly the terms in correspondence with our original type of terms.

We then define a formula type form’ based on term’ and a suitable deduction system. One can give a bijection between well-formed non-dependent terms term’ and dependent terms term and prove the equivalence of the corresponding deduction systems under this bijection.

Functions working on term’ and form’ were easily extracted to $\mathsf {L}$ using the framework, yielding an $\mathsf {L}$-enumerability proof for ND essentially with no manual formalisation effort.

Library of Formalised Undecidable Problems in Coq. We take the formalisation of synthetic undecidability from [14], which is part of the Coq library of formalised undecidable problems [12]. The reduction from $\mathsf {L}$-halting to provability is factored via Turing machines, Minsky machines, binary stack machines and the Post correspondence problem (PCP), all part of the library as well.

Equations Package. Defining non-structurally recursive functions is sometimes considered hard in Coq and other proof assistants based on dependent type theory. One such example is the function $[\![ \_ ]\!]$ used to embed formulas into Heyting algebras (Definition 45). We use the Equations package [48] to define this function by recursion on the size of the formula, ignoring terms. The definition then becomes entirely straightforward and the provided simp tactic, while sometimes a bit premature, enables compact proofs.