[FOM] infinite logical derivations
Alex Simpson
Alex.Simpson at ed.ac.uk
Thu Aug 23 10:33:49 EDT 2007
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
More information about the FOM
mailing list