## Sequent calculus proof systems for inductive definitions

##### View/Open

##### Date

11/2006##### Author

Brotherston, James

##### Metadata

##### Abstract

Inductive definitions are the most natural means by which to represent many families of structures
occurring in mathematics and computer science, and their corresponding induction / recursion
principles provide the fundamental proof techniques by which to reason about such
families. This thesis studies formal proof systems for inductive definitions, as needed, e.g., for
inductive proof support in automated theorem proving tools. The systems are formulated as
sequent calculi for classical first-order logic extended with a framework for (mutual) inductive
definitions.
The default approach to reasoning with inductive definitions is to formulate the induction
principles of the inductively defined relations as suitable inference rules or axioms, which are
incorporated into the reasoning framework of choice. Our first system LKID adopts this direct
approach to inductive proof, with the induction rules formulated as rules for introducing atomic
formulas involving inductively defined predicates on the left of sequents. We show this system
to be sound and cut-free complete with respect to a natural class of Henkin models. As a
corollary, we obtain cut-admissibility for LKID.
The well-known method of infinite descent `a la Fermat, which exploits the fact that there are
no infinite descending chains of elements of well-ordered sets, provides an alternative approach
to reasoning with inductively defined relations. Our second proof system LKIDw formalises
this approach. In this system, the left-introduction rules for formulas involving inductively
defined predicates are not induction rules but simple case distinction rules, and an infinitary,
global soundness condition on proof trees — formulated in terms of “traces” on infinite paths
in the tree — is required to ensure soundness. This condition essentially ensures that, for
every infinite branch in the proof, there is an inductive definition that is unfolded infinitely
often along the branch. By an infinite descent argument based upon the well-foundedness of
inductive definitions, the infinite branches of the proof can thus be disregarded, whence the
remaining portion of proof is well-founded and hence sound. We show this system to be cutfree
complete with respect to standard models, and again infer the admissibility of cut.
The infinitary system LKIDw 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.
This restricted “cyclic” proof system, CLKIDw, is suitable for formal reasoning since proofs
have finite representations and the soundness condition on proofs is thus decidable.
We show how the formulation of our systems LKIDw and CLKIDw can be generalised to
obtain soundness conditions for a general class of infinite proof systems and their corresponding
cyclic restrictions. We provide machinery for manipulating and analysing the structure of
proofs in these essentially arbitrary cyclic systems, based primarily on viewing them as generating
regular infinite trees, and we show that any proof can be converted into an equivalent
proof with a restricted cycle structure. For proofs in this “cycle normal form”, a finitary, localised soundness condition exists that is strictly stronger than the general, infinitary soundness
condition, but provides more explicit information about the proof.
Finally, returning to the specific setting of our systems for inductive definitions, we show
that any LKID proof can be transformed into a CLKIDw proof (that, in fact, satisfies the finitary
soundness condition). We conjecture that the two systems are in fact equivalent, i.e. that proof
by induction is equivalent to regular proof by infinite descent.