[FOM] infinite logical derivations

[Alex Simpson]

Replying to my earlier posting, Panu Raatikainen writes:

> It should be only remembered that all such infinitary "proofs", 
> whether well-founded or not, are EXTREMELY different from what is 
> usually meant by a "proof", i.e., where one can always effectively 
> check whether an alleged proof really counts as a proof or not.

In my LICS 2007 paper with Brotherston ("Complete sequent calculi for 
induction and infinite descent") we consider a
system in which rules are finitary, but in which proofs are
infinite non-well-founded trees of rule applications (subject to a 
combinatorial constraint that ensures soundness). Our proof system is 
intended to provide a formalization of (one possible notion of) proof 
by infinite descent.

While it is true that such infinite proofs cannot be effectively 
checked in general, there is a natural subclass of infinite
proofs that can: the class of *regular proofs* - i.e., those infinite 
proof trees that have only finitely many distinct subtrees. Such proof 
trees can be presented
as finite graphs, and the combinatorial soundness constraint over such 
graphs can be decided by a B\"uchi automaton.

Our paper contains an unsolved question, which may be of interest
to some readers of this list. Our "cyclic proofs" (as informally 
described above) are easily shown to subsume ordinary proof by 
induction. We conjecture that, conversely, any statement provable
by a cyclic proof is also provable by induction. Informally, this 
conjecture says that proof by induction is equivalent to regular proof 
by infinite descent.

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