License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2021.23
URN: urn:nbn:de:0030-drops-139188
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/13918/
Go to the corresponding LIPIcs Volume Portal

Kirst, Dominik ; Hermes, Marc

Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq

pdf-format:
LIPIcs-ITP-2021-23.pdf (0.8 MB)

Abstract

We mechanise the undecidability of various first-order axiom systems in Coq, employing the synthetic approach to computability underlying the growing Coq Library of Undecidability Proofs. Concretely, we cover both semantic and deductive entailment in fragments of Peano arithmetic (PA) and Zermelo-Fraenkel set theory (ZF), with their undecidability established by many-one reductions from solvability of Diophantine equations, i.e. Hilbert’s tenth problem (H10), and the Post correspondence problem (PCP), respectively. In the synthetic setting based on the computability of all functions definable in a constructive foundation, such as Coq’s type theory, it suffices to define these reductions as meta-level functions with no need for further encoding in a formalised model of computation.
The concrete cases of PA and ZF are prepared by a general synthetic theory of undecidable axiomatisations, focusing on well-known connections to consistency and incompleteness. Specifically, our reductions rely on the existence of standard models, necessitating additional assumptions in the case of full ZF, and all axiomatic extensions still justified by such standard models are shown incomplete. As a by-product of the undecidability of ZF formulated using only membership and no equality symbol, we obtain the undecidability of first-order logic with a single binary relation.

BibTeX - Entry

@InProceedings{kirst_et_al:LIPIcs.ITP.2021.23,
  author =	{Kirst, Dominik and Hermes, Marc},
  title =	{{Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{23:1--23:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/13918},
  URN =		{urn:nbn:de:0030-drops-139188},
  doi =		{10.4230/LIPIcs.ITP.2021.23},
  annote =	{Keywords: undecidability, synthetic computability, first-order logic, incompleteness, Peano arithmetic, ZF set theory, constructive type theory, Coq}
}

Keywords: undecidability, synthetic computability, first-order logic, incompleteness, Peano arithmetic, ZF set theory, constructive type theory, Coq
Collection: 12th International Conference on Interactive Theorem Proving (ITP 2021)
Issue Date: 2021
Date of publication: 21.06.2021
Supplementary Material: Software: https://www.ps.uni-saarland.de/extras/axiomatisations/

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI