This paper studies, by way of an example, the intuitionistic propositional connective * defined in the language of second order propositional logic by * ≡ ∃Q. In full topological models * is not generally definable but over Cantor-space and the reals it can be classically shown that *↔ ⅂⅂P; on the other hand, this is false constructively, i.e. a contradiction with Church's thesis is obtained. This is comparable with some well-known results on the completeness of intuitionistic first-order predicate logic. Over (...) [0, 1], the operator * is undefinable. We show how to recast this argument in terms of intuitive intuitionistic validity in some parameter. The undefinability argument essentially uses the connectedness of [0, 1]; most of the work of recasting consists in the choice of a suitable intuitionistically meaningful parameter, so as to imitate the effect of connectedness. Parameters of the required kind can be obtained as so-called projections of lawless sequences. (shrink)

In this paper second order intuitionistic propositional logic and its interpretation over Cantor space are considered. We focus on the propositional operators of the form $A^{*}=\exists q )$ where $A$ is a monadic propositional formula in the standard language $\{\neg, \vee, \wedge, \rightarrow \}$. It is shown that, over Cantor space, all operators $A^{*}$ are equivalent to appropriate formulae in $\{\neg, \vee, \wedge, \rightarrow \}$ 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 is obtained as a corollary. (shrink)