[FOM] infinite logical derivations

[Noam Zeilberger]

On Mon, Aug 20, 2007 at 07:02:23PM +0300, praatika at mappi.helsinki.fi wrote:
> 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. 
> 
> I am not sure how much sense the idea of a genuinely infinitely long proof 
> makes... What would count as the conclusion (the theorem) of such a proof, 
> given it would never terminate ?

Girard's ludics[1] explicitly allows infinitely-deep sequent
calculus-style derivations.  The ideas behind this are not that
strange, although ludics is kind of a quirky setting.  One thing you
can do with infinitely-deep proofs is define derivations
co-inductively.  Girard uses this to define the "fax", a sort of
untyped eta-expansion for arbitrary proofs, but more concretely you
can think of eta-expansion at recursive types[2].  In this case,
there's no real problem in defining the conclusion of the proof, since
we read the derivation bottom-up, and the "last step" (the root of the
tree) is a proper inference rule.

On the other hand, Girard even allows derivations that are "badly
infinite", not necessarily defined by co-induction, and which thus may
not have a well-defined last step.  Such proofs can be used to prove
an *arbitrary* conclusion: really they are only pseudo-proofs, since
they must be accepted on "faith".  Girard defines another sort of
improper inference rule called the "daimon", which can conclude
anything *immediately*, i.e. from no premises.  The point behind all
this unusual liberality is that by starting with a sufficiently large
space of "bogus" proofs, one can define a very natural topology on
(non-bogus) proofs using cut-elimination.

Noam                                                                              
[1]Girard, J.-Y.  Locus Solum, Mathematical Structures in Computer
Science 11, pp. 301-506, 2001.  Available at
http://iml.univ-mrs.fr/~girard/0.ps
[2]Brandt, M. and Henglein, F. 1998. Coinductive axiomatization of
recursive type equality and subtyping. Fundam. Informaticae 33:4,
pp. 309-338, 1998.