Priority Arguments and Epsilon Substitutions

2008/12/18 by Henry Towsner, Towsner, Henry
Computer Science · Mathematics · #03D25 #03F05 #03F30 #Computability, Logic, AI Algorithms #FOS: Mathematics #Logic (math.LO) #Logic, programming, and type systems #math.LO #msc:03D25 #msc:03F05 #msc:03F30 #semigroups and automata theory

paper · pdf · doi:10.48550/arxiv.0812.3434

arxiv created 2008/12/18 · openalex publication_date 2008/12/18 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

Kreisel has observed that the termination proof for Hilbert's epsilon-substitution method bears a resemblance to the priority arguments used in recursion theory. We make this precise by proving the termination using a framework for priority arguments due to Lerman and Lempp.

Related

• The Practice of Finitism: Epsilon Calculus and Consistency Proofs in Hilbert's Program
• Le problème intensionnel de la quantification chez Hilbert (The intensional problem of quantification in Hilbert)
• A positive solution to Hilbert's 10th problem
• Epsilon Substitution for ID₁ via Cut-Elimination
• A Majorization Order on Monomials and Termination of a Successive Difference Substitution Algorithm