Document Open Access Logo

A Simpler Undecidability Proof for System F Inhabitation

Authors Andrej Dudenhefner, Jakob Rehof



PDF
Thumbnail PDF

File

LIPIcs.TYPES.2018.2.pdf
  • Filesize: 0.53 MB
  • 11 pages

Document Identifiers

Author Details

Andrej Dudenhefner
  • Technical University of Dortmund, Dortmund, Germany
Jakob Rehof
  • Technical University of Dortmund, Dortmund, Germany

Acknowledgements

We would like to thank Paweł Urzyczyn for sharing his insights on second order propositional logic provability, which helped to develop the presented results.

Cite AsGet BibTex

Andrej Dudenhefner and Jakob Rehof. A Simpler Undecidability Proof for System F Inhabitation. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 2:1-2:11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.TYPES.2018.2

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".

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • System F
  • Lambda Calculus
  • Inhabitation
  • Propositional Logic
  • Provability
  • Undecidability
  • Coq
  • Formalization

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. T. Arts and W. Dekkers. Embedding first order predicate logic in second order propositional logic. Technical report 93-02, Katholieke Universiteit Nijmegen, 1993. Google Scholar
  2. H. Barendregt. Introduction to Generalized Type Systems. J. Funct. Program., 1(2):125-154, 1991. Google Scholar
  3. A. Dudenhefner. Reduction from Diophantine equations to provability in IPC2 / System F. https://github.com/mrhaandi/ipc2. Accessed: 2018-09-18.
  4. Y. Forster, E. Heiter, and G. Smolka. Verification of PCP-Related Computational Reductions in Coq. In Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, pages 253-269, 2018. URL: https://doi.org/10.1007/978-3-319-94821-8_15.
  5. D. M. Gabbay. On 2nd order intuitionistic propositional calculus with full comprehension. Archive for Mathematical Logic, 16(3):177-186, 1974. Google Scholar
  6. P. Giannini and S. Ronchi Della Rocca. Characterization of typings in polymorphic type discipline. In Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS '88), Edinburgh, Scotland, UK, July 5-8, 1988, pages 61-70, 1988. URL: https://doi.org/10.1109/LICS.1988.5101.
  7. J. Girard. Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur. PhD thesis, Université Paris VII, 1972. Google Scholar
  8. M. H. Löb. Embedding First Order Predicate Logic in Fragments of Intuitionistic Logic. J. Symb. Log., 41(4):705-718, 1976. URL: https://doi.org/10.2307/2272390.
  9. D. Martin. Hilbert’s tenth problem is unsolvable. The American Mathematical Monthly, 80(3):233-269, 1973. Google Scholar
  10. K. Sakaguchi. A Formalization of Typed and Untyped lambda-Calculi in SSReflect-Coq and Agda2. https://github.com/pi8027/lambda-calculus. Accessed: 2019-04-02.
  11. M. H. Sørensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2006. Google Scholar
  12. M. H. Sørensen and P. Urzyczyn. A Syntactic Embedding of Predicate Logic into Second-Order Propositional Logic. Notre Dame Journal of Formal Logic, 51(4):457-473, 2010. URL: https://doi.org/10.1215/00294527-2010-029.
  13. P. Urzyczyn. Inhabitation in Typed Lambda-Calculi (A Syntactic Approach). In Typed Lambda Calculi and Applications, Third International Conference on Typed Lambda Calculi and Applications, TLCA '97, Nancy, France, April 2-4, 1997, Proceedings, pages 373-389, 1997. URL: https://doi.org/10.1007/3-540-62688-3_47.
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