It is known that the algebra of open subsets of the real line constitutes a sound and complete semantics for intuitionistic propositional logic, IPC. IPC has PSPACE complete set of tautologies. However, if we add quantification over propositions then the resulting logic, second order intuitionistic propositional logic, IPC2, has undecidable set of theorems. Moreover, the open subsets of the real line are still sound but no longer complete semantics for IPC2. I will state some properties of IPC2 with respect to the real line semantics and sketch the proof of decidability of sentences of IPC2 true in this model.