License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2018.2
URN: urn:nbn:de:0030-drops-114061
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11406/
Go to the corresponding LIPIcs Volume Portal

Dudenhefner, Andrej ; Rehof, Jakob

A Simpler Undecidability Proof for System F Inhabitation

pdf-format:
LIPIcs-TYPES-2018-2.pdf (0.5 MB)

Abstract

Provability in the intuitionistic second-order propositional logic (resp. inhabitation in the polymorphic lambda-calculus) was shown by Löb to be undecidable in 1976. Since the original proof is heavily condensed, Arts in collaboration with Dekkers provided a fully unfolded argument in 1992 spanning approximately fifty pages. Later in 1997, Urzyczyn developed a different, syntax oriented proof. Each of the above approaches embeds (an undecidable fragment of) first-order predicate logic into second-order propositional logic.
In this work, we develop a simpler undecidability proof by reduction from solvability of Diophantine equations (is there an integer solution to P(x_1, ..., x_n) = 0 where P is a polynomial with integer coefficients?). Compared to the previous approaches, the given reduction is more accessible for formalization and more comprehensible for didactic purposes. Additionally, we formalize soundness and completeness of the reduction in the Coq proof assistant under the banner of "type theory inside type theory".

BibTeX - Entry

@InProceedings{dudenhefner_et_al:LIPIcs:2019:11406,
  author =	{Andrej Dudenhefner and Jakob Rehof},
  title =	{{A Simpler Undecidability Proof for System F Inhabitation}},
  booktitle =	{24th International Conference on Types for Proofs and Programs (TYPES 2018)},
  pages =	{2:1--2:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-106-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{130},
  editor =	{Peter Dybjer and Jos{\'e} Esp{\'\i}rito Santo and Lu{\'\i}s Pinto},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/11406},
  URN =		{urn:nbn:de:0030-drops-114061},
  doi =		{10.4230/LIPIcs.TYPES.2018.2},
  annote =	{Keywords: System F, Lambda Calculus, Inhabitation, Propositional Logic, Provability, Undecidability, Coq, Formalization}
}

Keywords: System F, Lambda Calculus, Inhabitation, Propositional Logic, Provability, Undecidability, Coq, Formalization
Collection: 24th International Conference on Types for Proofs and Programs (TYPES 2018)
Issue Date: 2019
Date of publication: 18.11.2019
Supplementary Material: https://github.com/mrhaandi/ipc2

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