zbMATH — the first resource for mathematics

On some non-classical extensions of second-order intuitionistic propositional calculus. (English) Zbl 0569.03026
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.

03F55 Intuitionistic mathematics
03G30 Categorical logic, topoi
Full Text: DOI
[1] Dalen, D.van, An interpretation of intuitionistic analysis, Annals math. logic, 13, 1-43, (1978) · Zbl 0399.03049
[2] Dummett, M., Elements of intuitionism, (1977), Clarendon Press Oxford · Zbl 0358.02032
[3] Fourman, M.P.; Scott, D.S., Sheaves and logic, (), 302-401, Lecture Notes in Math. · Zbl 0415.03053
[4] Johnstone, P.T., Automorphisms of ω, Algebra universalis, 9, 1-7, (1979) · Zbl 0392.18005
[5] Kleene, S.C.; Vesley, R.E., Foundations of intuitionistic mathematics, (1965), North-Holland, Amsterdam · Zbl 0133.24601
[6] Krol, M.D., A topological model for intuitionistic analysis with Kripke’s schema, Z. math. logik grundlagen math., 24, 427-436, (1978) · Zbl 0418.03039
[7] Moschovakis, J.R., A topological interpretation of second-order intuitionistic arithmetic, Compositio math., 26, 261-276, (1973) · Zbl 0279.02018
[8] Myhill, J., Constructive set theory, J. symbolic logic, 40, 347-382, (1975) · Zbl 0314.02045
[9] Myhill, J.; Ščedrov, A., On an extension of the intuitionistic propositional calculus, Notices AMS, A-21, (Jan. 1979), (Preliminary Report)
[10] Ščedrov, A., Consistency and independence results in intuitionistic set theory, (), 54-86, Lecture Notes in Math
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.