# Cut-elimination (transfinite induction base step)

I am having problems with the base step in a proof by transfinite induction. Consider a certain language $Z_{\infty}$, a language similar to PA but with an $\omega$-rule and a cut rule among its inference rules . I suppose the reader knows what a deduction system is, what a derivation/proof is, what an ordinal assignment to the formulas in a derivation is and what a degree (or cut-rank) is. If a formula $A$ is an axiom of $Z_{\infty}$, we agree that its ordinal (i.e. the ordinal assigned to its derivation) is $0$. Now consider the following theorem (cut-elimination).

Theorem. Given a proof for a formula $A$ in $Z_{\infty}$ of positive degree $m$ and ordinal $\alpha$, there exists a proof of $A$ whose degree is $< m$, with $2^\alpha$ as ordinal.

Proof. By transfinite induction on $\alpha$. Let $\alpha = 0$; then the proof of $A$ cannot contain cuts and so its degree is $0$. Suppose the theorem proven for all ordinals $<\alpha$... [CUT]

Now, let's state the theorem for $\alpha = 0$. I am stuck on the following points:

1) the theorem requires something like an ordinal of a proof that have positive degree. But in the case $\alpha=0$ (there are no cuts, so the degree is $0$) how can it be positive? Is this correct? Is it a vacuously true argument?

2) The theorem states that the 'new' proof obtained has $2^\alpha$ as ordinal... but when $\alpha=0$ (so $A$ is an axiom of $Z_{\infty}$), how can we find a proof with ordinal $2^0 = 1$ ??? (Remember that if $A$ is an axiom then its ordinal is - by definition - $0$.)

Thanks.

-
Adding a reference would help. For the first one, I am guessing that changing positive to non-negative should fix it. About the second question, you can modify it to say it is a proof with ordinal at most ... – Kaveh Jul 12 '11 at 1:00
For the first question, recall that a statement of the form "Given a [blah-blah-blah], something happens" is vacuously true if there is no [blah-blah-blah]. In the case at hand, when $\alpha=0$, there is no "proof $\dots$ of positive degree $m$ and ordinal $\alpha$", so the theorem is vacuously true in this case. – Andreas Blass Nov 10 '12 at 17:10