Sequent calculi for induction and infinite descent.
Journal of Logic and Computation
This article formalizes and compares two different styles of reasoning with inductively defined predicates, each style being encapsulated by a corresponding sequent calculus proof system.The first system, LKID, supports traditional proof by induction, with induction rules formulated as rules for introducing inductively defined predicates on the left of sequents.We show LKID to be cut-free complete with respect to a natural class of Henkin models; the eliminability of cut follows as a corollary. The second system, LKID ω, uses infinite (non-well-founded) proofs to represent arguments by infinite descent. In this system, the left-introduction rules for inductively defined predicates are simple case-split rules, and an infinitary, global condition on proof trees is required in order to ensure soundness.We show LKIDω to be cut-free complete with respect to standard models, and again infer the eliminability of cut. The infinitary system LKID ω is unsuitable for formal reasoning. However, it has a natural restriction to proofs given by regular trees, i.e. to those proofs representable by finite graphs, which is so suited. We demonstrate that this restricted 'cyclic' proof system, CLKIDω, subsumes LKID, and conjecture that CLKIDω and LKID are in fact equivalent, i.e. that proof by induction is equivalent to regular proof by infinite descent. © 2010 The Author.
|Title:||Sequent calculi for induction and infinite descent|
|Keywords:||cut-elimination, cyclic proof, inductive definitions, infinite descent, Sequent calculus|
|UCL classification:||UCL > School of BEAMS > Faculty of Engineering Science
UCL > School of BEAMS > Faculty of Engineering Science > Computer Science
Archive Staff Only