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