DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2022.19

Undecidability of Dyadic First-Order Logic in Coq

Authors: Johannes Hostert, Andrej Dudenhefner, and Dominik Kirst

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract

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.

Cite as

Johannes Hostert, Andrej Dudenhefner, and Dominik Kirst. Undecidability of Dyadic First-Order Logic in Coq. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{hostert_et_al:LIPIcs.ITP.2022.19,
  author =	{Hostert, Johannes and Dudenhefner, Andrej and Kirst, Dominik},
  title =	{{Undecidability of Dyadic First-Order Logic in Coq}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{19:1--19:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.19},
  URN =		{urn:nbn:de:0030-drops-167280},
  doi =		{10.4230/LIPIcs.ITP.2022.19},
  annote =	{Keywords: undecidability, synthetic computability, first-order logic, Coq}
}

Search Results

Documents authored by Hostert, Johannes

Undecidability of Dyadic First-Order Logic in Coq

Abstract

Cite as

Thanks for your feedback!

Could not send message