文章基本信息

标题：A Simpler Undecidability Proof for System F Inhabitation
本地全文：下载
作者：Andrej Dudenhefner ; Jakob Rehof
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2019
卷号：130
页码：1-11
DOI：10.4230/LIPIcs.TYPES.2018.2
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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".
关键词：System F; Lambda Calculus; Inhabitation; Propositional Logic; Provability; Undecidability; Coq; Formalization