\input zb-basic
\input zb-ioport
\iteman{io-port 05901629}
\itemau{Towsner, Henry}
\itemti{Priority arguments and epsilon substitution.}
\itemso{Feferman, Solomon (ed.) et al., Proofs, categories and computations. Essays in honor of Grigori Mints. With the collaboration of Vladik Kreinovich, Vladimir Lifschitz, and Ruy de Queiroz. London: College Publications (ISBN 978-1-84890-012-7/pbk). Tributes 13, 251-266 (2010).}
\itemab
The starting point of this paper is Kreisel's remark that Hilbert's epsilon substitution method -- a classical technique developed first by Ackermann for proving the 1-consistency of arithmetic -- bears resemblance to finite injury priority arguments. On the one hand, {\it Y. Yang} [Arch. Math. Logic 34, No. 2, 97--112 (1995; Zbl 0826.03028)] showed that $n$th-level arguments in the Lerman-Lempp hierarchy of priority arguments succeed iff the fragment of Peano Arithmetic PA based on $\mathrm{I}\Sigma_n$, the induction schema restricted to $\Sigma_n$-formulas, is 1-consistent. So an iterated-trees-style $O^{(n)}$-priority proof of a theorem can be formalized in the fragment of PA based on $\mathrm{I} \Sigma_n$. On the other hand, the Lermann-Lempp framework has been extended to transfinite levels of the hyperarithmetical hierarchy; this suggests a connection with the 1-consistency of PA extended to transfinite induction up to particular ordinals. The present author shows that the $\varepsilon$-substitution method works by means of a priority argument. The crucial idea is that of finite injury relationship between two trees (see Sections 3--4). The main construction takes place by building trees which are then used for defining solving substitutions (see 5.1--5.2 and Theorem 35; a substitution roughly being a partial function possibly assigning numerical values to $\varepsilon$-terms). The link with ordinal analysis is made clear by the conclusive lemma, which states that, once we have a finite injury relation between two trees $T_1$ and $T_2$ and $T_2$ has ordinal height $\alpha$, then there exists a height function for the tree $T_1$ into $\omega^\alpha$.
\itemrv{Andrea Cantini (Firenze)}
\itemcc{}
\itemut{finite injury method; epsilon substitution method; ordinal analysis}
\itemli{}
\end