Realizing Brouwer's sequences
type: Item
instance of: scholarly article
title: Realizing Brouwer's sequences
zbMATH Open document ID: 0863.03031
DOI: 10.1016/0168-0072(94)00047-6
author: Richard E. Vesley
published in: Annals of Pure and Applied Logic
publication date: 1996-11-25T00:00:00Z
review text: In this paper, the author, who assumes familiarity with FIM [\textit{S. C. Kleene} and the author, The foundations of intuitionistic mathematics (1965; Zbl 0133.24601)], puts forward a new interpretation, that generalizes to higher-type Kleene's functional realizability (FIM). Three formal systems, \(S_1\), \(S_2\), and \(S^*\), each extending the previous one, are introduced, all expressed in an extension \(L^*\) of the language \(L\) of FIM, that contains a constant functor (function of one variable) primitive the name for a particular ``lawless'' sequence \(\omega\). This novelty allows the expression in \(L^*\) of the property of a choice sequence to be lawless by means of the formula \[ LS(\alpha): \exists z \biggl(\text{Seq} (z) \wedge \alpha \in z \wedge \forall i \bigl(i \geq lh(z) \to \alpha (i) = \omega (i) \bigr) \biggr) . \] \((U,R)\)-realizability, with \(U\) standing for Kleene's ``universal spread'' of FIM, and with \(R\) standing for the set of total recursive functions, is introduced to code continuous functions, and it is shown that all theorems in \(S^*\) (whence all in \(S_2\) and \(S_1)\) are \((U,R)\)-realizable. The only nonconstructive argument is used in the proof that the only axiom scheme that was added to \(S_2\) to get \(S^*\), namely CONT!, is \((U,R)\)-realizable. \(S_2\) (in fact, already \(S_1\) together with one of the principles for lawless sequences LS4) is an exclusively intuitionistic formal system, for it becomes inconsistent once \(\neg \neg A\to A\) is added to it. The lawless axioms for \(S_2\) are sufficiently strong to reject even the Ščedrov-Vesley [\textit{A. Ščedrov} and the author, Arch. Math. Logik Grundlagenforsch. 23, 153-160 (1983; Zbl 0533.03033)] weak version of Markov's principle.
reviewed by: Victor V. Pambuccian
Mathematics Subject Classification ID: 03F55
Mathematics Subject Classification ID: 03F50
zbMATH DE Number: 933090
zbMATH Keywords: FIM
zbMATH Keywords: foundations of intuitionistic mathematics
zbMATH Keywords: choice sequence
zbMATH Keywords: continuous functions
zbMATH Keywords: lawless sequences
zbMATH Keywords: intuitionistic formal system
MaRDI profile type: Publication
full work available at URL: 0168-0072(94)00047-6
OpenAlex ID: W2074208814
cites work: Points and Spaces
cites work: The completeness of intuitionistic propositional calculus for its intended interpretation
cites work: An interpretation of intuitionistic analysis
cites work: Q5604441
cites work: Q3958458
cites work: Q3671978
cites work: On the interpretation of intuitionistic number theory
cites work: Q5812175
cites work: Q3281965
cites work: Formalized recursive functionals and formalized realizability
cites work: Q5343325
cites work: A remark on free choice sequences and the topological completeness proofs
cites work: Q5539743
cites work: On the idea(l) of logical closure
cites work: Formal systems for some branches of intuitionistic analysis
cites work: Q4281259
cites work: Q5579001
cites work: On a weakening of Markov's Principle
cites work: Q5593817
cites work: Spreads or choice sequences?
cites work: Q4126323
cites work: Constructivism in mathematics. An introduction. Volume II
Recommended article: A classical view of the intuitionistic continuum
Recommended article: Church's thesis, continuity, and set theory
Recommended article: General recursive realizability and intuitionistic logic
Recommended article: Q4215635
Recommended article: Q5436705
Recommended article: Recursion over realizability structures
Recommended article: General recursive realizability and basic logic
Recommended article: Analyzing realizability by Troelstra's methods
Recommended article: Unavoidable sequences in constructive analysis
Recommended article: On the ubiquity of certain total type structures (extended abstract)
description: scientific article; zbMATH DE number 933090