An Epsilon Substitution Method for a Theory of Non-iterated Inductive Definitions
by
Grigori Mints
Stanford University

The scheme of Hilbert's \epsilon substitution method for the theory ID₁ of one inductive definition introduced in [1] left open details of the definition of a ``collapsing'' step when the fixpoint I ^{< \Omega} of the inductive definition is replaced by I ^{< \xi} for some countable ordinal \xi. Now this transformation is defined as follows.

The n-th step of the \epsilon substitution process for ID₁ generates in addition to an \epsilon-substitution S_n also a finite derivation d_n (encoding in fact certain infinite derivation). An ordinal o(d) < \psi(\epsilon_\Omega+1) (Howard ordinal) is effectively assigned to every finite derivation [2]. The collapsing step applied to an \epsilon substitution S_i uses \xi = D(o(d')), where D is a standard collapsing function [3] and d' is a certain subderivation of d_i. The ordinal o(S_n) is defined in terms of o(d_n).

Theorem. If S_n is not a solving substitution, then o(S_n) > o(S_n+1). Hence every \epsilon substitution process for ID₁ terminates in a solving substitution.

References

[1] An approach to an epsilon-substitution method for ID1. Preprint, Institute Mittag-Leffler, no 45, MLI, Stockholm 2001.
[2] A Termination Proof for Epsilon Substitutions Using Partial Derivations, to appear in Theoretical Computer Science
[3] Proof Theory, Lecture Notes in Mathematics, v. 1407, 1989, Springer Verlag

Date received: March 17, 2003

Copyright © 2003 by the author(s). The author(s) of this document and the organizers of the conference have granted their consent to include this abstract in Atlas Mathematical Conference Abstracts. Document # cajy-20.