Abstract
I will summarise the main ideas and results appearing in my PhD thesis,
recently completed at LFCS 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. The main developments are:
- a finitary proof system with induction rules that is
cut-free complete with respect to a natural class of Henkin models, with
semantic cut-elimination arising as a corollary;
- an infinitary proof system formalising a version of Fermat's method
of *infinite descent*, in which proofs are allowed to be infinite trees,
and an infinitary, global condition on proof trees is required to ensure
soundness.
This system is cut-free complete with respect to standard models, with
semantic
cut-elimination again arising as a corollary;
- a cyclic proof system arising as the natural restriction of the infinitary
system
to proofs representable by finite graphs. This system, in contrast to the
full
infinitary system, is suitable for practical formal reasoning. Furthermore,
it subsumes proof
by induction in the finitary system above. We conjecture that the two
systems are
actually equivalent, i.e. that proof by induction is equivalent to regular
proof by
infinite descent.
We will assume a basic familiarity with the fundamentals of first-order
logic and sequent calculus.