Extensional Gödel functional interpretation. A consistency proof of classical analysis
From MaRDI portal
Cited in
(29)- Equivalence of bar recursors in the theory of functionals of finite type
- A very strong intuitionistic theory
- Theory of proofs (arithmetic and analysis)
- On the arithmetical content of restricted forms of comprehension, choice and general uniform boundedness
- Remarks on Herbrand normal forms and Herbrand realizations
- Bounded functional interpretation
- Strongly uniform bounds from semi-constructive proofs
- On Spector's bar recursion
- Term extraction and Ramsey's theorem for pairs
- Light monotone Dialectica methods for proof mining
- Spielquantorinterpretation unstetiger Funktionale der höheren Analysis
- Measure theory and higher order arithmetic
- Strong normalization of barrecursive terms without using infinite terms
- Ein starker Normalisationssatz für die bar-rekursiven Funktionale
- Über das Markov-Prinzip
- Über das Markov-Prinzip II
- Primitive recursion and the chain antichain principle
- Delimited control operators prove double-negation shift
- Some logical metatheorems with applications in functional analysis
- A logical uniform boundedness principle for abstract metric and hyperbolic spaces
- Modal functional (``Dialectica) interpretation
- Classical provability of uniform versions and intuitionistic provability
- General logical metatheorems for functional analysis
- A complexity analysis of functional interpretations
- On uniform weak König's lemma
- Elimination of extensionality in Martin-Löf type theory
- Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation
- Pointwise hereditary majorization and some applications
- Bounded functional interpretation and feasible analysis
This page was built for publication: Extensional Gödel functional interpretation. A consistency proof of classical analysis
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2560813)
