Update procedures and the 1-consistency of arithmetic

DOI10.1002/1521-3870(200201)48:1%3C3::AID-MALQ3%3E3.0.CO;2-6MaRDI QIDQ2776806zbMATH OpenFDO

Authors Jeremy Avigad

Publication date 22 July 2002

Published in Mathematical Logic Quarterly (MLQ) (Search for Journal in Brave)

Full work available at URL https://figshare.com/articles/journal_contribution/Update_Procedures_and_the_1-Consistency_of_Arithmetic/6493070

zbMATH Keywords

1-consistency of arithmeticcombinatorial independenceepsilon-substitutionfixed pointsfunctionalsPeano arithmetic

Mathematics Subject Classification ID

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

Cites work

• AN ORDINAL ANALYSIS OF ADMISSIBLE SET THEORY USING RECURSION ON ORDINAL NOTATIONS
• Elementary descent recursion and proof theory
• Epsilon substitution method for theories of jump hierarchies
• Finite functions and the necessary use of large cardinals
• Functionals defined by transfinite recursion
• scientific article; zbMATH DE number 3857078 (Why is no real title available?)
• scientific article; zbMATH DE number 1215495 (Why is no real title available?)
• scientific article; zbMATH DE number 733384 (Why is no real title available?)
• scientific article; zbMATH DE number 227056 (Why is no real title available?)
• Strong termination for the epsilon substitution method
• The substitution method

Cited in

(11)

• Ackermann's substitution method (remixed)
• 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
• Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM 1
• A constructive analysis of learning in Peano arithmetic
• Updateable Inner Product Argument with Logarithmic Verifier and Applications
• Bar recursion over finite partial functions
• Constructive forcing, CPS translations and witness extraction in interactive realizability
• Interactive realizability for second-order Heyting arithmetic with EM1 and SK1
• Herbrand complexity and the epsilon calculus with equality
• The epsilon calculus and Herbrand complexity

This page was built for publication: Update procedures and the 1-consistency of arithmetic

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