A Sequent Calculus for General Inductive Definitions

TL;DR

This paper introduces a new sequent calculus, SCFO(ID), for FO(ID) logic that supports general non-monotone inductive definitions, extending previous systems and enabling formal proofs involving complex inductive constructs.

Contribution

It extends the LKID calculus to handle non-monotone inductive definitions inspired by stable semantics, broadening proof capabilities for FO(ID).

Findings

Established proof-theoretical properties of SCFO(ID)

Demonstrated the calculus on various examples

Supports formal proofs of theorems with general inductive definitions

Abstract

Inductive definitions are an important form of knowledge. The logic FO(ID) is an extension of classical first-order logic FO with general non-monotone inductive definitions. Most existing proof systems for inductive definitions impose syntactic constraints on their definitions, thereby excluding many useful and natural definitions. We extend an existing sequent calculus LKID by Brotherston and Simpson, founded on the principle of mathematical induction, to a sequent calculus SCFO(ID) for FO(ID). The main challenge in this extension is the accommodation of non-monotone inductive definitions. To overcome this challenge, we draw inspiration from the stable semantics, which is a commonly used semantics in logic programming that is closely related to the well-founded semantics behind FO(ID). We corroborate SCFO(ID) by establishing several proof-theoretical properties and through demonstration on various examples. In conclusion, SCFO(ID) is a theoretically substantiated sequent calculus for FO(ID), enabling formal proofs of theorems involving general inductive definitions.