zbMATH — the first resource for mathematics

Operators defined by propositional quantification and their interpretation over Cantor space. (English) Zbl 0806.03008
Summary: Second-order intuitionistic propositional logic and its interpretation over Cantor space are considered. We focus on the propositional operators of the form \(A^*(p)= \exists q(p\equiv A(q))\), where \(A(q)\) is a monadic propositional formula in the standard language \(\{\neg, \vee,\wedge, \to\}\). It is shown that, over Cantor space, all operators \(A^*(p)\) are equivalent to appropriate formulae in \(\{\neg, \vee,\wedge, \to\}\) with the only variable \(p\). The coincidence, while restricting to the operators \(A^*\), of topological interpretation over Cantor space and Pitts’ interpretation of propositional quantifiers (as interpolants) is obtained as a corollary.

03B15 Higher-order logic; type theory (MSC2010)
03B20 Subsystems of classical logic (including intuitionistic logic)