The existential fragment of second-order propositional intuitionistic logic is undecidable

References

• Appel, A. W. (1991). Compiling with continuations. Cambridge University Press.
   Google Scholar
• Arts, T., & Dekkers, W. (1993). Embedding first order predicate logic in second order propositional logic [Technical Report 93-02]. Katholieke Universiteit Nijmegen.
   Google Scholar
• Börger, E., Grädel, E., & Gurevich, Y. (1997). The classical decision problem, Perspectives in Mathematical Logic. Springer.
   Google Scholar
• Clarence Protin, M. (2021). Type inhabitation of atomic polymorphism is undecidable. Journal of Logic and Computation, 31(2), 416–425. https://doi.org/10.1093/logcom/exaa090
   Web of Science ®Google Scholar
• de Barros Santos, J., Vieira, B. L., & Haeusler, E. H. (2016). A unified procedure for provability and counter-model generation in minimal implicational logic. Electronic Notes in Theoretical Computer Science, 324, 165–179. WEIT 2015, the Third Workshop-School on Theoretical Computer Science.https://doi.org/10.1016/j.entcs.2016.09.014.
   Google Scholar
• Dowek, G., & Jiang, Y. (2006). Eigenvariables, bracketing and the decidability of positive minimal predicate logic. Theoretical Computer Science, 360(1–3), 193–208. https://doi.org/10.1016/j.tcs.2006.01.053.
   Web of Science ®Google Scholar
• Dudenhefner, A., & Rehof, J.. (2018). A simpler undecidability proof for system F inhabitation. In P. Dybjer, J. E. Santo, & L. Pinto (Eds.), 24th International Conference on Types for Proofs and Programs, TYPES 2018, June 18–21, 2018, Braga, Portugal, Volume 130 of LIPIcs (pp. 2:1–2:11). Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.TYPES.2018.2.
   Google Scholar
• Ferreira, F. (2006). Comments on predicative logic. Journal of Philosophical Logic, 35(1), 1–8. https://doi.org/10.1007/s10992-005-9001-z http://www.jstor.org/stable/30226856.
   Web of Science ®Google Scholar
• Fujita, K.-E.. (2005). Galois embedding from polymorphic types into existential types. In P. Urzyczyn (Ed.), Typed Lambda Calculi and Applications, 7th International Conference, TLCA 2005, Nara, Japan, April 21–23, 2005, Proceedings, Number 3461 in Lecture Notes in Computer Science (pp. 194–208). https://doi.org/10.1007/11417170_15.
   Google Scholar
• Fujita, K.-E., & Schubert, A.. (2009). Existential type systems with no types in terms. In P.-L. Curien (Ed.), Typed Lambda Calculi and Applications 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1–3, 2009. Proceedings, Volume 5608 of Lecture Notes in Computer Science (pp. 112–126). Springer-Verlag.
   Google Scholar
• Gabbay, D. M. (1974). On 2nd order intuitionistic propositional calculus with full comprehension. Archive for Mathematical Logic, 16(3–4), 177–186. https://doi.org/10.1007/BF02015377
   Google Scholar
• Girard, J.-Y. (1971). Une extension de l'interpretation de Gödel a l'analyse, et son application a l'elimination des coupures dans l'analyse et la theorie des types. In J. E. Fenstad (Ed.), Proceedings of the Second Scandinavian Logic Symposium, Volume 63 of Studies in Logic and the Foundations of Mathematics (pp. 63–92). Elsevier. https://doi.org/10.1016/S0049-237X(08)70843-7.
   Google Scholar
• Kato, Y., & Nakazawa, K. (2009). Type checking and inference are equivalent in lambda calculi with existential types. In WFLP '09: 18th International Workshop on Functional and (Constraint) Logic Programming (pp. 31–44).
   Google Scholar
• Kozen, D. C. (1997). Automata and computability. New York, NY, Springer.
   Google Scholar
• Läufer, K., & Odersky, M. (1994). Polymorphic type inference and abstract data types. ACM Transactions on Programming Languages and Systems, 16(5), 1411–1430. https://doi.org/10.1145/186025.186031.
   Web of Science ®Google Scholar
• Löb, M. H. (1976). Embedding first order predicate logic in fragments of intuitionistic logic. The Journal of Symbolic Logic, 41(4), 705–718. https://doi.org/10.2307/2272390
   Web of Science ®Google Scholar
• Mints, G. E. (1968). Solvability of the problem of deducibility in LJ for a class of formulas not containing negative occurrences of quantifiers. Steklov Inst., 98, 135–145.
   Google Scholar
• Mitchell, J. C., & Plotkin, G. D. (1988). Abstract types have existential type. ACM Transactions on Programming Languages and Systems, 10(3), 470–502. https://doi.org/10.1145/44501.45065.
   Web of Science ®Google Scholar
• Montagu, B., & Rémy, D.. (2009). Modeling abstract types in modules with open existential types. In Z. Shao & B. C. Pierce (Eds.), Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21–23, 2009 (pp. 354–365). ACM. https://doi.org/10.1145/1480881.1480926.
   Google Scholar
• Reynolds, J. C. (1974). Towards a theory of type structure. In B. J. Robinet (Ed.), Programming Symposium, Proceedings Colloque sur la Programmation, Paris, France, April 9–11, 1974, Volume 19 of Lecture Notes in Computer Science, (pp. 408–423). Springer. https://doi.org/10.1007/3-540-06859-7_148.
   Google Scholar
• Reynolds, J. C. (1998). Theories of programming languages. Cambridge University Press.
   Google Scholar
• Rummelhoff, I. (2007). Polymorphic Π1 types and a simple approach to propositions, types and sets [PhD thesis]. University of Oslo.
   Google Scholar
• Russo, C. V. (2004). Types for modules. Electronic Notes in Theoretical Computer Science, 60, 3–421. https://doi.org/10.1016/S1571-0661(05)82621-0. https://www.sciencedirect.com/science/article/pii/S1571066105826210.
   Google Scholar
• Schubert, A., Urzyczyn, P., & Zdanowski, K. (2017). On the Mints hierarchy in first-order intuitionistic logic. Logical Methods in Computer Science, 12(4), 1–25. https://doi.org/10.2168/LMCS-12(4:11)2016.
   Web of Science ®Google Scholar
• Sørensen, M. H., & Urzyczyn, P. (2006). Lectures on the Curry–Howard isomorphism, Studies in Logic and the Foundations of Mathematics; Vol. 149. Elsevier Science Inc.
   Google Scholar
• Sørensen, M. H., & Urzyczyn, P. (2010). A syntactic embedding of predicate logic into second-order propositional logic. Notre Dame J. Formal Log., 51(4), 457–473. https://doi.org/10.1215/00294527-2010-029.
   Web of Science ®Google Scholar
• Tatsuta, M.. (2007). Simple saturated sets for disjunction and second-order existential quantification. In S. R. Della Rocca (Ed.), Typed lambda calculi and applications (pp. 366–380). Springer.
   Google Scholar
• Tatsuta, M., Fujita, K.-E., Hasegawa, R., & Nakano, H. (2010). Inhabitation of polymorphic and existential types. Annals of Pure and Applied Logic, 161(11), 1390–1399. https://doi.org/10.1016/j.apal.2010.04.009.
   Web of Science ®Google Scholar
• Tatsuta, M., & Mints, G. (2005). A simple proof of second-order strong normalization with permutative conversions. Annals of Pure and Applied Logic, 136(1–2), 134–155. Festschrift on the occasion of Wolfram Pohlers' 60th birthday. https://doi.org/10.1016/j.apal.2005.05.009.
   Web of Science ®Google Scholar
• Urzyczyn, P. (1997). Inhabitation in typed lambda-calculi (a syntactic approach). In P. de Groote (Ed.), Typed Lambda Calculi and Applications, Third International Conference on Typed Lambda Calculi and Applications, TLCA '97, Nancy, France, April 2–4, 1997, Proceedings, Volume 1210 of Lecture Notes in Computer Science (pp. 373–389). Springer.
   Google Scholar
• Xue, T., & Xuan, Q. (2008). Proof search and counter model of positive minimal predicate logic. Electronic Notes in Theoretical Computer Science, 212, 87–102. Proceedings of the First International Conference on Foundations of Informatics, Computing and Software (FICS 2008). https://doi.org/10.1016/j.entcs.2008.04.055.
   Google Scholar
• Zdanowski, K. (2009). On second order intuitionistic propositional logic without a universal quantifier. The Journal of Symbolic Logic, 74(1), 157–167. https://doi.org/10.2178/jsl/1231082306.
   Web of Science ®Google Scholar