Priority Arguments and Epsilon Substitutions

TL;DR

This paper formalizes the connection between the termination proof of Hilbert's epsilon-substitution method and priority arguments in recursion theory, using a framework by Lerman and Lempp.

Contribution

It provides a precise proof of termination for epsilon-substitution using priority argument techniques, bridging two areas of mathematical logic.

Findings

Termination of epsilon-substitution proven via priority arguments

Framework by Lerman and Lempp applied to epsilon-substitution

Clarifies the relationship between Hilbert's method and recursion theory

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.