**Advisors:** Andrej Dudenhefner and Dominik Kirst

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.

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

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

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.

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

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