2026-07-23T19:12:36Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16728 2024-03-06T10:58:09Z ddc:004 open_access

Undecidability of Dyadic First-Order Logic in Coq Hostert, Johannes Dudenhefner, Andrej Kirst, Dominik undecidability synthetic computability first-order logic Coq 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Johannes Hostert and Andrej Dudenhefner and Dominik Kirst 2022 Is Part Of LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2022.19 urn:nbn:de:0030-drops-167280 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.19 eng https://creativecommons.org/licenses/by/4.0/legalcode