[FOM] Induction, cut, and normalization

[Sara Negri]

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

Academy Research Fellow,
Ph.D., Docent of Logic,
Department of Philosophy,
University of Helsinki,
http://www.helsinki.fi/~negri/