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

MaRDI QIDQ2560813zbMATH OpenFDO

Authors Horst Luckhardt

Publication date 1973

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

Mathematics Subject Classification ID

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

Cited in

(29)

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

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)