scientific article

DOI<3::AID-MALQ3>3.0.CO;2-6 10.1002/1521-3870(200201)48:1<3::AID-MALQ3>3.0.CO;2-6zbMath0988.03087MaRDI QIDQ2776806

Jeremy Avigad

Publication date: 22 July 2002

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

fixed pointsPeano arithmeticfunctionals1-consistency of arithmeticcombinatorial independenceepsilon-substitution

Mathematics Subject Classification ID

First-order arithmetic and fragments (03F30) Functionals in proof theory (03F10) Recursive ordinals and ordinal notations (03F15) Relative consistency and interpretations (03F25)

Related Items

Constructive forcing, CPS translations and witness extraction in Interactive realizability, Herbrand complexity and the epsilon calculus with equality, A constructive analysis of learning in Peano arithmetic, Computational Interpretations of Classical Reasoning: From the Epsilon Calculus to Stateful Programs, Bar recursion over finite partial functions, Interactive Realizability for second-order Heyting arithmetic with EM1 and SK1, Ackermann's substitution method (remixed), Gödel's Reformulation of Gentzen's First Consistency Proof For Arithmetic: The No-Counterexample Interpretation, Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM 1, The epsilon calculus and Herbrand complexity

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Finite functions and the necessary use of large cardinals
• Elementary descent recursion and proof theory
• Epsilon substitution method for theories of jump hierarchies
• Strong termination for the epsilon substitution method
• AN ORDINAL ANALYSIS OF ADMISSIBLE SET THEORY USING RECURSION ON ORDINAL NOTATIONS
• Functionals defined by transfinite recursion
• The substitution method