zbMATH — the first resource for mathematics

Second order propositional operators over Cantor space. (English) Zbl 0790.03005
Summary: We consider propositional operators defined by propositional quantification in intuitionistic logic. More specifically, we investigate the propositional operators of the form \(A^*: p\mapsto\exists q\) \((p\equiv A(q))\), where \(A(q)\) is one of the following formulae: \((\neg\neg q\to q)\lor\neg\neg q\), \((\neg\neg q\to q)\to (\neg\neg q\lor\neg q)\), \(((\neg\neg q\to q)\to (\neg\neg q\lor\neg q))\to((\neg\neg q\to q)\lor\neg\neg q)\). The equivalence of \(A^*(p)\) to \(\neg\neg p\) is proved over the standard topological interpretation of intuitionistic second order propositional logic over Cantor space.
We relate topological interpretations of second order intuitionistic propositional logic over Cantor space with the interpretation of propositional quantifiers (as the strongest and weakest interpolant in Heyting calculus) suggested by A. Pitts. One of the merits of Pitts’ interpretation is shown to be valid for the interpretation over Cantor space.

03B15 Higher-order logic; type theory (MSC2010)
03B20 Subsystems of classical logic (including intuitionistic logic)
Full Text: DOI
[1] G. Kreisel,Monadic operators defined by means of propositional quantification in intuitionistic logic,Reports on Mathematical Logic 12 (1981), pp. 9–15. · Zbl 0464.03051
[2] A. Pitts,On an interpretation of second order quantification in the first order intuitionistic propositional logic,Journal of Symbolic Logic 57 (1992), pp. 33–52. · Zbl 0763.03009
[3] A. S. Troelstra,On a second order propositional operator in intuitionistic logic,Studia Logica 40 (1981), pp. 113–139. · Zbl 0473.03022
[4] P. Wojtylak,Collapse of a class of infinite disjunctions in intuitionistic propositional logic,Reports on Mathematical Logic 16 (1983), pp. 37–49. · Zbl 0599.03024
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.