Publication details

Saarland University Computer Science

Undecidability of Dyadic First-Order Logic in Coq

Johannes Hostert, Andrej Dudenhefner, Dominik Kirst

13th International Conference on Interactive Theorem Proving (ITP 2022), Haifa, Israel, 2022

We develop and mechanize compact proofs of the undecidability of various problems for dyadic first-order logic over a small logical fragment. In this fragment, formulas are restricted to only a single binary relation, and a minimal set of logical connectives. We show that validity, satisfiability, and provability, along with finite satisfiability and finite validity are undecidable, by directly reducing from a suitable binary variant of Diophantine constraints satisfiability. Our results improve upon existing work in two ways: First, the reductions are direct and significantly more compact than existing ones. Secondly, the undecidability of the small logic fragment of dyadic first-order logic was not mechanized before. We contribute our mechanization to the Coq Library of Undecidability Proofs, utilizing its synthetic approach to computability theory.

Project page

Download PDF        Show BibTeX               

Login to edit

Legal notice, Privacy policy