Extensional Gödel functional interpretation. A consistency proof of classical analysis

zbMath0262.02031MaRDI QIDQ2560813

Publication date: 1973

Published in: Lecture Notes in Mathematics (Search for Journal in Brave)

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Proof theory and constructive mathematics (03F99)

Related Items (29)

Measure theory and higher order arithmetic ⋮ On Spector's bar recursion ⋮ Light monotone Dialectica methods for proof mining ⋮ Term extraction and Ramsey's theorem for pairs ⋮ Some logical metatheorems with applications in functional analysis ⋮ Strong normalization of barrecursive terms without using infinite terms ⋮ Bounded functional interpretation and feasible analysis ⋮ Equivalence of bar recursors in the theory of functionals of finite type ⋮ Elimination of extensionality in Martin-Löf type theory ⋮ Primitive recursion and the chain antichain principle ⋮ Delimited control operators prove double-negation shift ⋮ Unnamed Item ⋮ Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation ⋮ A Logical Uniform Boundedness Principle for Abstract Metric and Hyperbolic Spaces ⋮ Ein starker Normalisationssatz für die bar-rekursiven Funktionale ⋮ Spielquantorinterpretation unstetiger Funktionale der höheren Analysis ⋮ Über das Markov-Prinzip ⋮ Bounded functional interpretation ⋮ A complexity analysis of functional interpretations ⋮ Strongly uniform bounds from semi-constructive proofs ⋮ A very strong intuitionistic theory ⋮ General logical metatheorems for functional analysis ⋮ Über das Markov-Prinzip II ⋮ On uniform weak König's lemma ⋮ Theory of proofs (arithmetic and analysis) ⋮ Remarks on Herbrand normal forms and Herbrand realizations ⋮ On the arithmetical content of restricted forms of comprehension, choice and general uniform boundedness ⋮ Classical provability of uniform versions and intuitionistic provability ⋮ Pointwise hereditary majorization and some applications

This page was built for publication: Extensional Gödel functional interpretation. A consistency proof of classical analysis