eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-11-18
2:1
2:11
10.4230/LIPIcs.TYPES.2018.2
article
A Simpler Undecidability Proof for System F Inhabitation
Dudenhefner, Andrej
1
Rehof, Jakob
1
Technical University of Dortmund, Dortmund, Germany
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".
https://drops.dagstuhl.de/storage/00lipics/lipics-vol130-types2018/LIPIcs.TYPES.2018.2/LIPIcs.TYPES.2018.2.pdf
System F
Lambda Calculus
Inhabitation
Propositional Logic
Provability
Undecidability
Coq
Formalization