[FOM] Infinite proofs
Alex.Simpson at ed.ac.uk
Tue Aug 21 12:22:10 EDT 2007
Panu Raatikainen writes:
> Infinitary proofs such as those using the omega-rule and discussed e.g. in
> the entry by Hazen I mentioned, are not, literally, infinitely long.
> Rather, they allow steps with infinitely many premises, but a "proof" is
> still finitely long in the sense that it has only finitely many steps.
Presumably what you mean is that proofs are well-founded
trees, so every branch is finite. Nonetheless, such proofs still
have, in general, an infinite "height" given by a countable ordinal
defined in the natural way by (transfinite) induction on the
proof structure. Such ordinal heights are the basis for many
modern presentations of Gentzen's consistency proof for arithmetic
(see, for example, Schwichtenberg's expository article in the
Handbook of Mathematical Logic).
Since you do not seem happy with well-founded proofs, perhaps
you are looking for systems involving non-well-founded proofs.
Here are two references that consider non-well-founded sequent-calculus
proofs, one old one new:
G. Kreisel, G. E. Mints, and S. G. Simpson. "The use of abstract
language in elementary metamathematics: Some pedagogic examples."
In R. Parikh, editor, Logic Colloquium
Vol. 453 of Lecture Notes in Mathematics, pages 38-131. Springer
J. Brotherston and A. Simpson
Complete Sequent Calculi for Induction and Infinite Descent
Proceedings LICS 2007 (Available from our webpages.)
Also, Mints (and others subsequently) have considered "continuous
cut-elimination" which performs cut-elimination on arbitrary
non-well-founded rule trees (avoiding any induction on the
height of proofs).
Alex Simpson, LFCS, School of Informatics, Univ. of Edinburgh, UK
Email: Alex.Simpson at ed.ac.uk Tel: +44 (0)131 650 5113
Web: http://homepages.inf.ed.ac.uk/als Fax: +44 (0)131 667 7209
More information about the FOM