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

The provability problem in intuitionistic propositional second-order logic with existential quantifier and implication $ (\exists,\to) $ (∃ , →) 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. [ABSTRACT FROM AUTHOR]