[FOM] Infinite proofs

[Alex Simpson]

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 
Verlag, 1975.

  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

-- 
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