On some non-classical extensions of second-order intuitionistic propositional calculus (Q1061123)

Hyland gave general sufficient conditions on a topological space X under which continuity principles hold in the internal logic of sheaves on X. Because truth values are the open subsets of X, one hopes that such conditions might be more directly expressed in terms of underlying second order propositional calculus, rather than via a detour through a sheaf interpretation. Another motivation for the author's approach is a result of Higgs that every monic automorphism on the truth value object \(\Omega\) of a topos is an involution. The stronger requirement \(\forall p,q((fp\leftrightarrow fq)\leftrightarrow (p\leftrightarrow q))\to \forall p(fp\leftrightarrow p)\) is shown to be equivalent to a purely propositional formula \(\forall p[((p\leftrightarrow q)\leftrightarrow q)\to p]\to q\), and to be consistent with \(\forall \alpha \exists n\) continuity with parameters, bar induction, and Kripke's schema. Letting \(q=\perp\) yields a proper weakening, with \(\forall p[p\vee (p\to q)]\to q\) being properly intermediate. This last formula follows from the full \(\forall \alpha \exists n\) continuity, but it is independent from the parameterless version. It is also shown that the parameterless \(\forall \alpha \exists n\) continuity implies that no function from a set of the Baire space to the power set of a singleton \((=\Omega)\) can have a section.