2 Search Results for "Hermes, Marc"

Document
DOI: 10.4230/LIPIcs.FSCD.2022.9
An Analysis of Tennenbaum’s Theorem in Constructive Type Theory

Authors: Marc Hermes and Dominik Kirst

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
Tennenbaum’s theorem states that the only countable model of Peano arithmetic (PA) with computable arithmetical operations is the standard model of natural numbers. In this paper, we use constructive type theory as a framework to revisit and generalize this result. The chosen framework allows for a synthetic approach to computability theory, by exploiting the fact that, externally, all functions definable in constructive type theory can be shown computable. We internalize this fact by assuming a version of Church’s thesis expressing that any function on natural numbers is representable by a formula in PA. This assumption allows for a conveniently abstract setup to carry out rigorous computability arguments and feasible mechanization. Concretely, we constructivize several classical proofs and present one inherently constructive rendering of Tennenbaum’s theorem, all following arguments from the literature. Concerning the classical proofs in particular, the constructive setting allows us to highlight differences in their assumptions and conclusions which are not visible classically. All versions are accompanied by a unified mechanization in the Coq proof assistant.
Cite as

Marc Hermes and Dominik Kirst. An Analysis of Tennenbaum’s Theorem in Constructive Type Theory. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{hermes_et_al:LIPIcs.FSCD.2022.9,
  author =	{Hermes, Marc and Kirst, Dominik},
  title =	{{An Analysis of Tennenbaum’s Theorem in Constructive Type Theory}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{9:1--9:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.9},
  URN =		{urn:nbn:de:0030-drops-162909},
  doi =		{10.4230/LIPIcs.FSCD.2022.9},
  annote =	{Keywords: first-order logic, Peano arithmetic, Tennenbaum’s theorem, constructive type theory, Church’s thesis, synthetic computability, Coq}
}
Document
DOI: 10.4230/LIPIcs.ITP.2021.23
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq

Authors: Dominik Kirst and Marc Hermes

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

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.
Cite as

Dominik Kirst and Marc Hermes. Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 23:1-23:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.23},
  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}
}
  • Refine by Author
  • 2 Hermes, Marc
  • 2 Kirst, Dominik

  • Refine by Classification
  • 2 Theory of computation → Constructive mathematics
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 2 Coq
  • 2 Peano arithmetic
  • 2 constructive type theory
  • 2 first-order logic
  • 2 synthetic computability
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2021
  • 1 2022

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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact