Johannes Hostert: Bachelor's Thesis

The Undecidability of First-order Logic over Small Signatures

Advisors: Andrej Dudenhefner and Dominik Kirst

Summary

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.

Goals

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

Validity for Tarski models
Provability in an abstract deduction system
Validity for Kripke models
Satisfiablity for Tarski/Kripke models
Finite satisfiability

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:

Validity for Tarski models
Provability in an abstract deduction system
Validity for Kripke models
Satisfiablity for Tarski/Kripke models

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.

References

Über Möglichkeiten im Relativkalkül. Löwenheim 1915
On Computable Numbers, with an Application to the Entscheidungsproblem. Turing 1936
A note on the Entscheidungsproblem. Church 1936
Zurückführung des Entscheidungsproblems auf den Fall von Formeln mit einer einzigen, binären, Funktionsvariablen. Kalmár 1937
Enumerable Sets are Diophantine. Matiyasevich 1970
Hilbert's Tenth Problem in Coq. Larchey-Wendling et al 2019
On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem. Forster et al 2019
The Coq library of undecidability proofs
Trakhtenbrot’s Theorem in Coq - A Constructive Approach to Finite Model Theory. Kirst and Larchey-Wendling 2020
Elements of Finite Model Theory. Libkin 2012 (textbook)
The Impossibility of an Algorithm for the Decidability Problem on Finite Classes. Trakhtenbrot 1950

Resources

In-development source code: (Github)
A memo on the validity/provability/staisfiability reductions can be found here.
Slides for my first Bachelor Seminar Talk can be found here.
Slides for my second Bachelor Seminar Talk can be found here.
Slides for my final Bachelor Seminar Talk can be found here.
My final thesis can be found here. Note that this version contains some fixes, the original version as submitted to the examination office can be found here.

Legal notice, Privacy policy