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

Abstract

The provability problem in intuitionistic propositional second-order logic with existential quantifier and implication $(\mathrm{\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.

Keywords:

• Second-order logic
• propositional logic
• second-order type system
• lambda calculus
• existential quantification

Acknowledgements

We thank the anonymous referees for comments that helped to improve the paper.

Disclosure statement

No potential conflict of interest was reported by the author(s).

Notes

1 A position in a formula is negative when it occurs in the assumption part of an odd number of implications; otherwise it is positive.

2 The depth of root is zero.

3 For the cautious reader: $P(x,y)\mathit{\epsilon }\mathrm{\Gamma }$ means $P(\phi ,\psi )\in \mathrm{\Gamma }$, where $\mathrm{tg}(\phi )=x,\mathrm{tg}(\psi )=y$. In addition $\mathrm{\Gamma }⊢\mathit{Var}(\phi )$ and $\mathrm{\Gamma }⊢\mathit{Var}(\psi )$, because Γ is legal. Hence x, y are individual variables (Lemma 4.2), so $|x|,|y|$ are well defined.

Additional information

Funding

The work of Aleksy Schubert and Paweł Urzyczyn was partly supported by Ministerstwo Edukacji i Nauki IDUB POB 3 programme at the University of Warsaw. The work of Ken-etsu Fujita was partly supported by Japan Society for the Promotion of Science Grants-in-Aid for Scientific Research KAKENHI [grant numbers 17K05343 and 20K03711].