Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis
From MaRDI portal
Publication:5537358
DOI10.2307/2270450zbMath0156.00804OpenAlexW1966245774MaRDI QIDQ5537358
William Alvin Howard, Georg Kreisel
Publication date: 1966
Published in: Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2307/2270450
Related Items
A NOTE ON FRAGMENTS OF UNIFORM REFLECTION IN SECOND ORDER ARITHMETIC, Principles of bar induction and continuity on Baire space, Some logical metatheorems with applications in functional analysis, Equivalence of bar induction and bar recursion for continuous functions with continuous moduli, Brouwer's fan theorem as an axiom and as a contrast to Kleene's alternative, Projective sets, intuitionistically, Unnamed Item, The Borel Hierarchy Theorem from Brouwer's intuitionistic perspective, Validating Brouwer's continuity principle for numbers using named exceptions, Unnamed Item, Spielquantorinterpretation unstetiger Funktionale der höheren Analysis, Two simple sets that are not positively Borel, Some derived rules of intuitionistic second order arithmetic, Über das Markov-Prinzip II, On the No-Counterexample Interpretation, Theory of proofs (arithmetic and analysis), An extension of Schütte's Klammersymbole, A new model for intuitionistic analysis, Exercising Nuprl’s Open-Endedness, Extended bar induction in applicative theories, Ordinal analysis of simple cases of bar recursion, Informal theory of choice sequences, On the computational content of the axiom of choice, Some results on cut-elimination, provable well-orderings, induction and reflection, Constructive Recursive Functions, Church’s Thesis, and Brouwer’s Theory of the Creating Subject: Afterthoughts on a Parisian Joint Session, Everywhere-defined continuous functionals, Extracting Lisp programs from constructive proofs: A formal theory of constructive mathematics based on Lisp, Some purely topological models for intuitionistic analysis, Classical provability of uniform versions and intuitionistic provability
Cites Work
