2026-08-06T08:11:19Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:11406 2024-03-06T10:46:04Z ddc:004 open_access

A Simpler Undecidability Proof for System F Inhabitation Dudenhefner, Andrej Rehof, Jakob System F Lambda Calculus Inhabitation Propositional Logic Provability Undecidability Coq Formalization 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". Schloss Dagstuhl – Leibniz-Zentrum für Informatik Andrej Dudenhefner and Jakob Rehof 2019 Is Part Of LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2018.2 urn:nbn:de:0030-drops-114061 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.2 eng https://creativecommons.org/licenses/by/3.0/legalcode