#### Abstract

I will summarise the main ideas and results appearing in my PhD thesis,
recently completed under the supervision of Alex Simpson.

We give 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.

Our first system LKID adopts a direct approach to inductive proof, with
induction rules formulated as rules for introducing
inductively defined predicates on the left of sequents. We show this
system to be cut-free complete with respect to a natural
class of Henkin models. As a corollary, we obtain cut-eliminability
for LKID.

Our second proof system LKIDw formalises a version of the well-known method
of *infinite descent* `a la Fermat. In this system, the
left-introduction rules for inductively defined
predicates are simple case distinction rules, but proofs are allowed to be infinite trees,
so an infinitary, global condition on proof trees
is required to ensure soundness of such proofs. This system is cut-free
complete with respect to standard models, from which one can 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 practical finite representations and the
soundness condition on proofs is thus decidable.

In fact, any LKID proof can be transformed into a CLKIDw proof.
We conjecture that the two systems
are actually equivalent, i.e., that proof by induction is equivalent
to regular proof by infinite descent for inductively defined relations.

We will assume a basic familiarity with the fundamentals of first-order
logic and sequent calculus.

[Hide Abstract]