The existential fragment of second-order propositional intuitionistic logic is undecidable
From MaRDI portal
Publication:6117326
DOI10.1080/11663081.2024.2312774OpenAlexW4392518522MaRDI QIDQ6117326
Konrad Zdanowski, Paweł Urzyczyn, Aleksy Schubert, Ken-etsu Fujita
Publication date: 20 March 2024
Published in: Journal of Applied Non-Classical Logics (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1080/11663081.2024.2312774
propositional logicsecond-order logiclambda calculusexistential quantificationsecond-order type system
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A syntactic embedding of predicate logic into second-order propositional logic
- Inhabitation of polymorphic and existential types
- Lectures on the Curry-Howard isomorphism
- Types for modules
- A unified procedure for provability and counter-model generation in minimal implicational logic
- Comments on predicative logic
- Eigenvariables, bracketing and the decidability of positive minimal predicate logic
- Sovability of the problem of deducibility in LJ for a class of formulas not containing negative occurrences of quantifiers
- A simple proof of second-order strong normalization with permutative conversions
- Simple Saturated Sets for Disjunction and Second-Order Existential Quantification
- On second order intuitionistic propositional logic without a universal quantifier
- Existential Type Systems with No Types in Terms
- Embedding first order predicate logic in fragments of intuitionistic logic
- Theories of Programming Languages
- On 2nd order intuitionistic propositional calculus with full comprehension
- Modeling abstract types in modules with open existential types
- Proof Search and Counter Model of Positive Minimal Predicate Logic
- Typed Lambda Calculi and Applications
- Type inhabitation of atomic polymorphism is undecidable
- On the Mints Hierarchy in First-Order Intuitionistic Logic
This page was built for publication: The existential fragment of second-order propositional intuitionistic logic is undecidable
