[FOM] Induction, cut, and normalization
jeffrey.sarnat at gmail.com
Sun Feb 20 18:47:54 EST 2011
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.
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?
Ph.D., University Lecturer
Docent in Theoretical Philosophy
Department of Philosophy, History, Culture and Art Studies
P.O. Box 24 (Unioninkatu 38 A)
FIN-00014 University of Helsinki
E-mail: <mailto:panu.raatikainen at helsinki.fi>panu.raatikainen at helsinki.fi
FOM mailing list
<mailto:FOM at cs.nyu.edu>FOM at cs.nyu.edu
More information about the FOM