[FOM] Induction, cut, and normalization

[William Tait]

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). 

Bill Tait