[FOM] Induction, cut, and normalization
williamtait at mac.com
Sat Feb 19 13:45:20 EST 2011
On Feb 19, 2011, at 12:12 AM, Panu Raatikainen wrote:
> Apparently the presence of the (unrestricted) induction schema blocks
> the cut-elimination. What, exactly, happens, if we rather have a
> system of natural deduction ? Normalization fails somehow?
No, strong normalization holds for arithmetic in ND---any sequence of eliminations of introductions followed by eliminations of the same constant will terminate in a deduction in which no introduction is followed by an elimination of the same constant. (Its a special case of strong normalization for the Curry-Howard theory of types.) But there will be cases of, say, forall x phi(x) followed by phi(t), where the first of these is the conclusion of an instance of mathematical induction (an elimination rule).
More information about the FOM