Johannes Hostert: Bachelor's Thesis

Saarland University Computer Science

The Undecidability of First-order Logic over Small Signatures

Advisors: Andrej Dudenhefner and Dominik Kirst


The decidability of first order logic was an open question until 1938, when Church and Turing showed that many interesting properties of FOL are not decidable. Importantly, it is undecidable whether a statement is valid in all models, satisfied by a specific model or provable in an abstract deduction system.
Attention then shifted towards finding a better characterisation of what properties FOL must have to be undecidable. Notably, FOL with only unary predicate and function symbols is decidable, while FOL with a binary predicate is not.
All of these results have been formalised in this chair's library of undecidable problems. However, these proofs often employ a series of syntax compression steps which culminate in a single binary relation. We however propose a single reduction from a variant of Diophantine constraints, which aims to show a minimal logic undecidable without any signature compression steps. To our understanding, this has not been done previously. The scope of this bachelor thesis is to develop the required reductions and to formalize them in Coq, as part of the aforementioned library.


We aim to show that the following problems are undecidable for FOL with a minimal signature:

Current state

A memo outlining the current state can be found below. To summarize, we have mechanized a reduction from a variant of Diophantine constraints satisfiability to the following FOL problems: The reduction uses a single binary relation and is within the forall-implicative fragment, thus having a minimal signature. We have not yet used the mentioned proof mode, as it does not support having a dependant list of hypotheses.

Furthermore, we have now formalized a reduction from finite satisfiability. To be precise, we have mechanized the result that it is undecidable in general whether a certain FOL formula is satisfied by a finite model, if that formula has a single binary relation. Since finite satisfiability assumes that models behave classically, i.e. they are listable and all atomic predicates are decidable, this result still holds for formulas residing in the forall-implicative fragment with negation. Negation is necessary for satisfiability.



Legal notice, Privacy policy