On some non-classical extensions of second-order intuitionistic propositional calculus
type: Item
instance of: scholarly article
title: On some non-classical extensions of second-order intuitionistic propositional calculus
zbMATH Open document ID: 0569.03026
DOI: 10.1016/0168-0072(84)90010-1
published in: Annals of Pure and Applied Logic
publication date: 1984-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03F55
Mathematics Subject Classification ID: 03G30
zbMATH DE Number: 3908429
zbMATH Keywords: continuity principles
zbMATH Keywords: truth value object
zbMATH Keywords: topos
author: Andre Scedrov
MaRDI profile type: Publication
full work available at URL: 0168-0072(84)90010-1
OpenAlex ID: W1995421582
cites work: An interpretation of intuitionistic analysis
cites work: Q4133603
cites work: Q3050433
cites work: Automorphisms of \(\Omega\)
cites work: Q5343325
cites work: A Topological Model for Intuitionistic Analysis with Kripke's Scheme
cites work: Q4404863
cites work: Constructive set theory
cites work: Q3912576
Recommended article: A secondary semantics for Second Order Intuitionistic Propositional Logic
Recommended article: Non-axiomatizable second order intuitionistic propositional logic
Recommended article: On second order intuitionistic propositional logic without a universal quantifier
Recommended article: On an interpretation of second order quantification in first order intuitionistic propositional logic
Recommended article: Q5413327
Recommended article: Q3743301
Recommended article: Extensionalizing intensional second-order logic
Recommended article: Q4981450
Recommended article: Proof-search of propositional intuitionistic logic sequents by means of classical logic calculus
Recommended article: Mereotopology in 2nd-Order and Modal Extensions of Intuitionistic Propositional Logic
description: scientific article; zbMATH DE number 3908429