A MARRIAGE OF BROUWER’S INTUITIONISM AND HILBERT’S FINITISM I: ARITHMETIC
DOI10.1017/jsl.2018.6OpenAlexW3120965290MaRDI QIDQ5082051
Publication date: 15 June 2022
Published in: The Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/jsl.2018.6
consistency strengthinterpretabilityintuitionistic mathematicsHilbert's programmeKleene's second modelGodel's incompleteness theoremsCoquand-Hofmann forcingfunction-based second order arithmeticLifschitz's realizabilityRussian recursive mathematicssemi-classical principle
Constructive and recursive analysis (03F60) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Intuitionistic mathematics (03F55) Relative consistency and interpretations (03F25)
Related Items (6)
Cites Work
- Constructive Zermelo-Fraenkel set theory and the limited principle of omniscience
- Brouwer's fan theorem as an axiom and as a contrast to Kleene's alternative
- A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP
- Finite sets and infinite sets in weak intuitionistic arithmetic
- Weak König's lemma implies Brouwer's fan theorem: a direct proof
- Sequences of real functions on [0,1 in constructive reverse mathematics]
- The strength of extensionality. I: Weak weak set theories with infinity
- Factorization of polynomials and \(\Sigma ^ 0_ 1\) induction
- Constructivism in mathematics. An introduction. Volume II
- The proof-theoretic analysis of \(\Sigma_{1}^{1}\) transfinite dependent choice
- Fragments of HA based on \(\Sigma_ 1\)-induction
- Bounded inductive dichotomy: separation of open and clopen determinacies with finite alternatives in constructive contexts
- A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\)
- Classical consequences of continuous choice principles from intuitionistic analysis
- A fan-theoretic equivalent of the antithesis of Specker's theorem
- Two simple sets that are not positively Borel
- Formalizing forcing arguments in subsystems of second-order arithmetic
- Interpreting classical theories in constructive ones
- A note on the independence of premiss rule
- Ramsey's Theorem and the Pigeonhole Principle in Intuitionistic Mathematics
- Lifschitz' realizability
- Determinacy of Wadge classes and subsystems of second order arithmetic
- Partial realizations of Hilbert's program
- Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
- Fragments of Heyting arithmetic
- A NOTE ON PREDICATIVE ORDINAL ANALYSIS I: ITERATED COMPREHENSION AND TRANSFINITE INDUCTION
- TRUTHS, INDUCTIVE DEFINITIONS, AND KRIPKE-PLATEK SYSTEMS OVER SET THEORY
- TRUNCATION AND SEMI-DECIDABILITY NOTIONS IN APPLICATIVE THEORIES
- A new method for establishing conservativity of classical systems over their intuitionistic version
- Transfinite dependent choice and ω-model reflection
- A constructive proof of the dense existence of nowhere-differentiable functions in C [ 0 , 1 ]
- Systems of predicative analysis
- Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
- Logical Approaches to Computational Barriers
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: A MARRIAGE OF BROUWER’S INTUITIONISM AND HILBERT’S FINITISM I: ARITHMETIC
