# [FOM] Induction, cut, and normalization

Sara Negri sara.negri at helsinki.fi
Sat Feb 19 14:40:48 EST 2011

```Dear FOM and Panu:

It is customary to say that normalization fails for natural deduction
for Heyting arithmetic, or that cut elimination fails for a
corresponding sequent system. This is partly a terminological matter.
There is no subformula property for derivations, even if a suitable
definition of normality applies. Say, one can have what I have called
general elimination rules and normality defined by: All major
premisses of elimination rules are assumptions. This is a weak notion
for Heyting arithmetic, but not empty. For example, one can prove the
existence property in this way by simple proof transformations (as in
my paper "Normal form and existence property for derivations in
Heyting arithmetic").

Looking at a sequent formulation, cuts can be eliminated, but the
subformula property fails. In fact, a suitable formulation of the rule
of induction has cut as a special case, so nothing that useful is
gained. I leave out the contexts:

-> A(0)   A(x) -> A(x')  A(t)->C
-------------------------------Ind
->C

t is any term. The standard induction rule comes out when A(t)=C. If A
does not depend on x, and you leave out the second premiss because it
is just A -> A, then that instance of Ind is just cut. Trace of A is
lost.

regards, Jan von Plato

(visiting Sara Negri's FOM-mail)

Quoting "Panu Raatikainen" <panu.raatikainen at helsinki.fi>:

> 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?
>
> Best,
>
> Panu
>
>
>
> --
> Panu Raatikainen
>
> Ph.D., University Lecturer
> Docent in Theoretical Philosophy
>
> Theoretical Philosophy
> Department of Philosophy, History, Culture and Art Studies
> P.O. Box 24  (Unioninkatu 38 A)
> FIN-00014 University of Helsinki
> Finland
>
> E-mail: panu.raatikainen at helsinki.fi
>
> http://www.mv.helsinki.fi/home/praatika/
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
>

Sara Negri