On some non-classical extensions of second-order intuitionistic propositional calculus
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.
- A secondary semantics for Second Order Intuitionistic Propositional Logic
- Non-axiomatizable second order intuitionistic propositional logic
- On second order intuitionistic propositional logic without a universal quantifier
- On an interpretation of second order quantification in first order intuitionistic propositional logic
- On some extensions of intuitionistic logic
- scientific article; zbMATH DE number 3976993
- Extensionalizing intensional second-order logic
- Some conservative extension results on classical and intuitionistic sequent calculi
- Proof-search of propositional intuitionistic logic sequents by means of classical logic calculus
- Mereotopology in 2nd-order and modal extensions of intuitionistic propositional logic
- A Topological Model for Intuitionistic Analysis with Kripke's Scheme
- An interpretation of intuitionistic analysis
- Automorphisms of \(\Omega\)
- Constructive set theory
- scientific article; zbMATH DE number 3645093 (Why is no real title available?)
- scientific article; zbMATH DE number 3724439 (Why is no real title available?)
- scientific article; zbMATH DE number 3557754 (Why is no real title available?)
- scientific article; zbMATH DE number 3438823 (Why is no real title available?)
- scientific article; zbMATH DE number 3216177 (Why is no real title available?)
- Second order propositional operators over Cantor space
- Non-axiomatizable second order intuitionistic propositional logic
- Propositional quantification in the topological semantics for S4
- Continuous truth. II: Reflections
- scientific article; zbMATH DE number 7229466 (Why is no real title available?)
- On second order intuitionistic propositional logic without a universal quantifier
- On an interpretation of second order quantification in first order intuitionistic propositional logic
- Pitts' quantifiers are not topological quantification
This page was built for publication: On some non-classical extensions of second-order intuitionistic propositional calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1061123)
