Abstract
We consider propositional operators defined by propositional quantification in intuitionistic logic. More specifically, we investigate the propositional operators of the formA* :p ↦ ∃q(p ≡A(q)) whereA(q) is one of the following formulae: (¬¬q →q) V ¬¬q, (¬¬q →q) → (¬¬q V ¬q), ((¬¬q →q) → (¬¬q V ¬q)) → ((¬¬q →q) V ¬¬q). The equivalence ofA*(p) to ¬¬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.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
G. Kreisel,Monadic operators defined by means of propositional quantification in intuitionistic logic,Reports on Mathematical Logic 12 (1981), pp. 9–15.
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.
A. S. Troelstra,On a second order propositional operator in intuitionistic logic,Studia Logica 40 (1981), pp. 113–139.
P. Wojtylak,Collapse of a class of infinite disjunctions in intuitionistic propositional logic,Reports on Mathematical Logic 16 (1983), pp. 37–49.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Połacik, T. Second order propositional operators over cantor space. Stud Logica 53, 93–105 (1994). https://doi.org/10.1007/BF01053024
Received:
Revised:
Issue Date:
DOI: https://doi.org/10.1007/BF01053024