The existential fragment of second-order propositional intuitionistic logic is undecidable
Ken-etsu Fujita, Aleksy Schubert, Paweł Urzyczyn, Konrad Zdanowski · Journal of Applied Non-Classical Logics · 2024
The provability problem in intuitionistic propositional second-order logic with existential quantifier and implication (∃,→) is proved to be undecidable in presence of free type variables (constants). This contrasts with the result that inutitionistic propositional second-order logic with existential quantifier, conjunction and negation is decidable.