[FOM] Induction, cut, and normalization

[Jeffrey Sarnat]

This is a common misconception. Really it depends 
entirely on how you formulate induction.

For example, Martin-Löf proved normalization for 
an intuitionistic, natural-deduction formulation 
of arithmetic based on iterated inductive 
definitions in "Hauptsatz for the intuitionistic 
theory of of iterated inductive definitions." 
Moreover, James Brotherston proved 
cut-elimination for a classical, sequent-calculus 
formulation of this system in his thesis.

Problems tend to arise when induction is 
formulated axiomatically, but, in my opinion, 
this fundamentally has more to do with the 
proof-theoretic ill-behavedness of axioms than 
with the nature of induction itself.

It's also worth mentioning that, if one is 
satisfied with proving cut elimination on a 
restricted class of formulae/sequents (e.g. 
atomic formulae, the empty sequent) then the 
induction axiom (and axioms in general) can usually be eliminated.

       Jeff



On Sat, 19 Feb 2011, 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?

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: <mailto:panu.raatikainen at helsinki.fi>panu.raatikainen at helsinki.fi

http://www.mv.helsinki.fi/home/praatika/

_______________________________________________
FOM mailing list
<mailto:FOM at cs.nyu.edu>FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom