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

zbMath0262.02031MaRDI QIDQ2560813

Horst Luckhardt

Publication date: 1973

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

Mathematics Subject Classification ID

03-02: Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations

03F99: Proof theory and constructive mathematics

Related Items

Some logical metatheorems with applications in functional analysis, A Logical Uniform Boundedness Principle for Abstract Metric and Hyperbolic Spaces, Classical provability of uniform versions and intuitionistic provability, General logical metatheorems for functional analysis, On uniform weak König's lemma, Primitive recursion and the chain antichain principle, Delimited control operators prove double-negation shift, A complexity analysis of functional interpretations, 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, 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, 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