Second order intuitionistic propositional logic of the real line is decidable

TL;DR

This paper proves that the set of formulas in second order intuitionistic propositional logic that are true in the algebra of open subsets of reals or rationals is decidable, contrasting with the undecidability of the general case.

Contribution

It demonstrates the decidability of truth in specific algebraic structures for second order intuitionistic propositional logic, which was previously known to be undecidable.

Findings

Truth in the algebra of open subsets of reals is decidable.

Truth in the algebra of open subsets of rationals is decidable.

Contrasts with the undecidability of the general second order intuitionistic propositional logic.

Abstract

It is known that the set of tautologies of second order intuitionistic propositional logic, $\mathrm{IPC} 2$, is undecidable. Here, we prove that the sets of formulas of $\mathrm{IPC} 2$ which are true in the algebra of open subsets of reals or rationals are decidable.