Document Open Access Logo

Undecidability of Dyadic First-Order Logic in Coq

Authors Johannes Hostert , Andrej Dudenhefner , Dominik Kirst

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2022.19.pdf
  • Filesize: 0.79 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
  • Theory of computation → Type theory
  • Theory of computation → Logic and verification
Keywords
  • undecidability
  • synthetic computability
  • first-order logic
  • Coq

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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 Get BibTex

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) https://doi.org/10.4230/LIPIcs.ITP.2022.19

Author Details

Johannes Hostert
  • Universität des Saarlandes, Saarland Informatics Campus, Saarbrücken, Germany
Andrej Dudenhefner
  • Universität des Saarlandes, Saarland Informatics Campus, Saarbrücken, Germany
Dominik Kirst
  • Universität des Saarlandes, Saarland Informatics Campus, Saarbrücken, Germany

Acknowledgements

We thank Yannick Forster for valuable feedback on drafts of this paper.

Supplementary Materials

References

  1. Wilhelm Ackermann. Beiträge zum Entscheidungsproblem der Mathematischen Logik. Mathematische Annalen, 112:419-432, 1936. URL: https://doi.org/10.1007/BF01565424.
  2. Andrej Bauer. First Steps in Synthetic Computability Theory. Electronic Notes in Theoretical Computer Science, 155:5-31, 2006. Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI). URL: https://doi.org/10.1016/j.entcs.2005.11.049.
  3. Paul Bernays. Beiträge Zur Reduktionstheorie des Logischen Entscheidungsproblems. Journal of Symbolic Logic, 2(2):84-85, 1937. URL: https://doi.org/10.2307/2267374.
  4. Alonzo Church. A note on the Entscheidungsproblem. Journal of Symbolic Logic, 1(1):40-41, 1936. URL: https://doi.org/10.2307/2269326.
  5. Thierry Coquand and Gérard Huet. The calculus of constructions. Information and Computation, 76(2):95-120, 1988. URL: https://doi.org/10.1016/0890-5401(88)90005-3.
  6. Martin Davis, Hilary Putnam, and Julia Robinson. The Decision Problem for Exponential Diophantine Equations. Annals of Mathematics, 74(3):425-436, 1961. URL: https://doi.org/10.2307/1970289.
  7. Nicolaas Govert De Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. In Indagationes Mathematicae (Proceedings), volume 75, pages 381-392. Elsevier, 1972. Google Scholar
  8. Yannick Forster. Computability in Constructive Type Theory. PhD thesis, Saarland University, 2021. URL: https://ps.uni-saarland.de/~forster/thesis.php.
  9. Yannick Forster, Dominik Kirst, and Gert Smolka. On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, pages 38-51, New York, NY, USA, 2019. Association for Computing Machinery. URL: https://doi.org/10.1145/3293880.3294091.
  10. Yannick Forster, Dominik Kirst, and Dominik Wehr. Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory: Extended Version. Journal of Logic and Computation, 31(1):112-151, January 2021. URL: https://doi.org/10.1093/logcom/exaa073.
  11. Yannick Forster, Dominique Larchey-Wendling, Andrej Dudenhefner, Edith Heiter, Dominik Kirst, Fabian Kunze, Gert Smolka, Simon Spies, Dominik Wehr, and Maximilian Wuttke. A Coq library of undecidable problems. In CoqPL 2020 The Sixth International Workshop on Coq for Programming Languages, 2020. Google Scholar
  12. Harvey Friedman. Classically and intuitionistically provably recursive functions. In Gert H. Müller and Dana S. Scott, editors, Higher Set Theory, pages 21-27, Berlin, Heidelberg, 1978. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/BFb0103100.
  13. Gerhard Gentzen. Die Widerspruchsfreiheit der reinen Zahlentheorie. Mathematische Annalen, 112:493-565, 1936. URL: https://doi.org/10.1007/BF01565428.
  14. Kurt Gödel. Zur intuitionistischen Arithmetik und Zahlentheorie - Ergebnisse eines Mathematischen Kolloquiums, 1928-1933. Google Scholar
  15. Kurt Gödel. Die Vollständigkeit der Axiome des logischen Funktionenkalküls. Monatshefte für Mathematik und Physik, 37(1):349-360, December 1930. URL: https://doi.org/10.1007/BF01696781.
  16. Yuri Gurevich. The decision problem for the logic of predicates and of operations. Algebra and Logic, 8:160-174, May 1969. URL: https://doi.org/10.1007/BF02306690.
  17. Hugo Herbelin and Gyesik Lee. Formalizing Logical Metatheory - Semantical Cut-Elimination using Kripke Models for first-order Predicate Logic, 2014. URL: https://formal.hknu.ac.kr/Kripke/.
  18. David Hilbert and Wilhelm Ackermann. Grundzüge der Theoretischen Logik. Springer Verlag, 1928. URL: https://doi.org/10.1007/978-3-662-00049-6.
  19. Johannes Hostert, Mark Koch, and Dominik Kirst. A Toolbox for Mechanised First-Order Logic. In The Coq Workshop 2021, 2021. Google Scholar
  20. László Kalmár. Zurückführung des Entscheidungsproblems auf den Fall von Formeln mit einer einzigen, binären, Funktionsvariablen. Compositio Mathematica, 4:137-144, 1937. URL: http://www.numdam.org/item/CM_1937__4__137_0/.
  21. László Kalmár. On the reduction of the decision problem. First paper. Ackermann prefix, a single binary predicate. Journal of Symbolic Logic, 4(1):1-9, 1939. URL: https://doi.org/10.2307/2266211.
  22. Dominik Kirst and Marc Hermes. Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq. In Interactive Theorem Proving - 12th International Conference, ITP 2021, Rome, Italy. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.23.
  23. Dominik Kirst and Dominique Larchey-Wendling. Trakhtenbrot’s Theorem in Coq. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning, pages 79-96, Cham, 2020. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-51054-1_5.
  24. Georg Kreisel. On weak completeness of intuitionistic predicate logic. Journal of Symbolic Logic, 27(2):139-158, 1962. URL: https://doi.org/10.2307/2964110.
  25. Dominique Larchey-Wendling and Yannick Forster. Hilbert’s Tenth Problem in Coq. In 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany. 4th International Conference on Formal Structures for Computation and Deduction, 2019. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.27.
  26. Leopold Löwenheim. Über Möglichkeiten im Relativkalkül. Mathematische Annalen, 76:447-470, 1915. URL: https://doi.org/10.1007/BF01458217.
  27. Yuri V. Matiyasevich. Enumerable sets are Diophantine. Doklady Akademii Nauk SSSR, 191:279-282, 1970. URL: https://doi.org/10.1142/9789812564894_0013.
  28. Frank Pfenning and Christine Paulin-Mohring. Inductively defined types in the calculus of constructions. In International Conference on Mathematical Foundations of Programming Semantics, pages 209-228. Springer, 1989. Google Scholar
  29. Emil L. Post. A variant of a recursively unsolvable problem. Bulletin of the American Mathematical Society, 52(4):264-268, 1946. Google Scholar
  30. Fred Richman. Church’s thesis without tears. Journal of Symbolic Logic, 48(3):797-803, 1983. URL: https://doi.org/10.2307/2273473.
  31. Alfred Tarski. I: A General Method in Proofs of Undecidability. In Alfred Tarski, editor, Undecidable Theories, volume 13 of Studies in Logic and the Foundations of Mathematics, pages 1-34. Elsevier, 1953. URL: https://doi.org/10.1016/S0049-237X(09)70292-7.
  32. The Coq Development Team. The Coq Proof Assistant, January 2021. URL: https://doi.org/10.5281/zenodo.4501022.
  33. Boris Trakhtenbrot. The Impossibility of an Algorithm for the Decidability Problem on Finite Classes. In Proceedings of the USSR Academy of Sciences, 1950. Google Scholar
  34. Alan M. Turing. On Computable Numbers, with an Application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, 2(42):230-265, 1936. URL: https://doi.org/10.1112/plms/s2-42.1.230.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact