Personal tools
You are here: Home Events Abstract Archives 2006-2007 Sequent Calculus Proof Systems for Inductive Definitions (Ph.D. completion seminar)

Sequent Calculus Proof Systems for Inductive Definitions (Ph.D. completion seminar)

James Brotherston University of Edinburgh 4pm Tuesday 17th October 2006 Room 2511, JCMB, King's Buildings

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.
Document Actions