On the No-Counterexample Interpretation

DOI10.2307/2586791MaRDI QIDQ4948521zbMATH OpenOpenAlexWikidataFDO

Authors Ulrich Kohlenbach

Publication date 10 May 2001

Published in Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2307/2586791

zbMATH Keywords

bar recursionfunctional interpretationGödel's \(T\)no-counterexample interpretation

Mathematics Subject Classification ID

Relative consistency and interpretations (03F25) First-order arithmetic and fragments (03F30) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50)

Recommendations

• scientific article; zbMATH DE number 1361536
• scientific article; zbMATH DE number 1302054
• Generalizing proofs in monadic languages (with a postscript by Georg Kreisel).

Cites work

• scientific article; zbMATH DE number 4033738 (Why is no real title available?)
• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• On n-quantifier induction
• On the Interpretation of Non-Finitist Proofs--Part I
• On the interpretation of non-finitist proofs–Part II
• Reflection Principles and their Use for Establishing the Complexity of Axiomatic Systems
• The syntax and semantics of infinitary languages
• Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES

Cited in

(20)

• On the arithmetical content of restricted forms of comprehension, choice and general uniform boundedness
• Dependent choice, `quote' and the clock
• Non-principal ultrafilters, program extraction and higher-order reverse mathematics
• On Spector's bar recursion
• Term extraction and Ramsey's theorem for pairs
• On the computational content of the Bolzano-Weierstraß Principle
• A uniform quantitative form of sequential weak compactness and Baillon's nonlinear ergodic theorem
• Computational interpretations of classical reasoning: from the epsilon calculus to stateful programs
• Gödel's Reformulation of Gentzen's First Consistency Proof For Arithmetic: The No-Counterexample Interpretation
• Measure theory and higher order arithmetic
• scientific article; zbMATH DE number 65749 (Why is no real title available?)
• scientific article; zbMATH DE number 1302054 (Why is no real title available?)
• scientific article; zbMATH DE number 1141703 (Why is no real title available?)
• Gödel functional interpretation and weak compactness
• A direct proof of Schwichtenberg's bar recursion closure theorem
• scientific article; zbMATH DE number 1361536 (Why is no real title available?)
• The true concurrency of Herbrand's theorem
• A complexity analysis of functional interpretations
• Herbrand analyses in geometry: a case study
• Non-elementary compression of first-order proofs in deep inference using epsilon-terms

This page was built for publication: On the No-Counterexample Interpretation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4948521)