First-Order Logic in Coq

The Coq Library of Undecidability Proofs is library of formalized proofs of the undecidability of various problems, originally developed at Saarland University, but nowadays it’s a collaborative effort by people from multiple universites. Note that I was not involved in the creation of that library, but I have contributed to it. One of the main contributors was Yannick Forster, and much of the work is further described in his Ph.D. thesis (Forster, 2021).

First-order logic (FOL) is logic that can be used as a foundation of mathematics. For example, classical ZF set theory is commonly defined as a theory of first-order logic. It occupies a sweat spot as being strong enough to define interesting theory, while still validating important meta-mathematical and model-theoretical lemmas like Completeness or Löwenheim-Skolem. As a logic, it is concerned with answering question like “what is a formula” and “when is a formula true?” One way of defining truth is with a first-order proof system that describes what proofs in FOL look like. While there are several different (and usually equivalent) ways of defining when a formula is true, it turns out that all of these are undecidable(Turing, 1936).

From 2020 to 2022, I was involved in several projects involving this library, and the emerging Coq Library for First-Order Logic.

My Bachelor’s Thesis

As part of my Bachelor’s thesis, we (Dominik Kirst, Andrej Dudenhefner, and me) formalized the undecidability of several such problems in the Library of Undecidability Proofs. Concretely, we proved that e.g. provability is already undecidable when one considers a quite restricted variant of first-order logic, namely first-order logic with a single binary relation. This is by no means a novel result: There is a rich theory on how one can turn more complicated first-order formulas (with perhaps several binary relations, or even ternary relations, …) into simpler ones. It is well-known that a single binary relation symbol is enough to encode any FOL formula, thereby being undecidable, while FOL with only unary symbols is fully decidable (Börger et al., 2001).

But what is meant by these symbols? Consider, for example, the first-order theory of natural numbers, which allows you to express formulas such as \(\forall n : (n+1) * (n+1) = n*n + (1+1)*n + 1\). We can see that this uses the function symbols \(+\) and \(*\), the constant \(1\) as well as the relation symbol \(=\). Such formulas are not allowed in the restricted subset, since they feature function and constant symbols. Instead, only formulas involving logical connectives, quantifiers, variables and \(=\) (the one binary relation symbol) would be allowed in that restricted subset of FOL. Note that the binary relation \(=\) does not need to be equality, in general, it can be an arbitrary relation (if it was always equality, things would be decidable).

To show that this is undecidable, we used a very fancy numerical relation discovered by Andrej, which is easy to axiomatize while also being strong enough to encode arbitrary computations in the natural numbers. We call that relation \(\style{display: inline-block; transform: rotate(270deg) scale(1.5) translate(1pt,0pt)}{\textasciitilde}\) and it is defined on pairs of natural numers:

This relation is very easy to characterize inductively, since the \(c\) and \(d\) components form a Gaussian sum. In fact, it is fully characterized by the following inference rules:

By choosing this relation as the one binary relation we are allowed to have in our restricted version of first-order logic, and by doing many more technical encoding tricks, we can create a FOL formula that is only provable if a certain Turing Machine halts / if a certain Diophantine equation system has a solution. It then follows that provability is undecidable.

In my Bachelor Thesis (Hostert, 2021), we did this, while also handling several other undecidable problems in FOL, not just provability. Based on the thesis, we also wrote a paper (Hostert et al., 2022), which was presented at the ITP conference. More information can be found here.

Coq Tooling for FOL

I was not the only one who formalized aspects of FOL meta-theory. In fact this was only a Bachelor’s Thesis, so the idea of formalizing FOL meta-theory was not mine to start with. My thesis was part of a larger program led by Dominik, who was also working on Completeness, the Church-Rosser theorems, and other important theorems of FOL meta-theory. Since meta-theory was a significant focus of the work, meta-theoretic concerns came first when formalizing the core definitions of first-order logic itself. This lead to a problem: It was often quite tedious to use the library for doing actual proofs using e.g. the first-order proof system. In other words, it was easier to talk about FOL than to work inside the logic. Unfortunately, a lot of meta-theoretic arguments still require a significant amount of proofs inside the logic, and this was therefore painful. To solve this, Mark Koch, Dominik, and I developed several tools (Hostert et al., 2021) which together made it much more pleasant to actually work within FOL, while still keeping the formalization well-suited for doing metatheory. We created two main utilities: A proof mode for first-order proofs, and a reification tactic to make using axiom schemes nicer.

I mostly worked on the latter, the reification tactic. Axiom schemes are a common concept in FOL, since the first in first-order means that one can not quantify over propositions. So, when formalizing the natural numbers in FOL, one can not simply formulate an induction axiom, since induction uses second-order quantification, as it is a general method for proving any property on natural numbers. Instead, one creates an infinite number of axioms, all following the same scheme, but so that there is an induction axiom for every first-order statement one would want to prove by induction. But then, using the scheme requires showing that a property is representable as a first-order formula. This is usually straightforward, but can be rather tedious. The tooling we developed here automates this problem.

The implementation idea is rather simple: It takes a Coq term, and tries to recast it’s syntax as a first-order formula. Doing this requires MetaCoq, since one has to inspect Coq’s syntax, in Coq. Part of this project was also exploring how well-suited MetaCoq is for these kinds of projects, and figuring how to improve it.

Further Consolidation, creating the Coq Library for FOL

Dominik’s line of research on formalizing various aspects of FOL turned out to be quite productive. After some years, there was a significant collection of formalized proofs, many of which are further described in Dominik’s thesis (Kirst, 2022). Unfortunately, these proofs were not really organized, instead lying around in different repositories, and often using slightly different definitions of what first-order logic even is. Dominik and I spend a lot of time cleaning this all up and organizing it into a nice library, the Coq Library for First-Order Logic. This consolidated library (Kirst et al., 2022) was presented at the 2022 Coq Workshop, and can also be found on GitHub. It shares some code with the Coq Library of Undecidability, but most of the proofs developed in it are not about undecidability.

Dominik and I continue to maintain that library. While Dominik continues do to research formalizing FOL, I don’t contribute to it anymore.