pith. sign in

arxiv: 2604.19382 · v2 · submitted 2026-04-21 · 💻 cs.LO

A Sequent Calculus for General Inductive Definitions

Robbe Van den Eede , Marc Denecker This is my paper

Pith reviewed 2026-05-10 01:43 UTC · model grok-4.3

classification 💻 cs.LO
keywords sequent calculusinductive definitionsFO(ID)non-monotone definitionsstable semanticsproof theorylogic programmingwell-founded semantics
0
0 comments X

The pith

A sequent calculus SCFO(ID) extends LKID to prove theorems with general non-monotone inductive definitions.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper constructs SCFO(ID), a sequent calculus for first-order logic with inductive definitions (FO(ID)), by extending the existing LKID system. It overcomes the restriction to monotone definitions by incorporating elements of stable semantics from logic programming. This allows the calculus to handle a broader class of natural inductive definitions that arise in knowledge representation. A sympathetic reader would care because inductive definitions appear frequently in formal specifications and verification tasks, and a workable proof system makes rigorous reasoning about them possible. The authors support the system by proving several proof-theoretic properties and by working through concrete examples.

Core claim

We extend the sequent calculus LKID, which is based on the principle of mathematical induction, to SCFO(ID) for FO(ID). The central step is the accommodation of non-monotone inductive definitions by drawing on stable semantics. We then establish cut-elimination, soundness, and completeness results for the resulting calculus and illustrate its use on several examples.

What carries the argument

The rules obtained by adapting stable semantics into the sequent-calculus setting to manage non-monotone inductive definitions while preserving induction.

If this is right

  • Formal proofs become possible for theorems that involve general inductive definitions previously excluded by syntactic constraints.
  • The calculus retains cut-elimination and other standard proof-theoretic properties of LKID.
  • The system supports concrete examples drawn from knowledge representation and logic programming.
  • Proofs in SCFO(ID) correspond to reasoning that respects the stable-model treatment of non-monotone definitions.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The calculus may serve as a foundation for automated theorem-proving tools that accept FO(ID) inputs directly.
  • It offers a bridge between the proof-theoretic approach of sequent calculi and the model-theoretic semantics used in answer-set programming.
  • Similar adaptations could be attempted for other non-monotonic extensions of classical logic.
  • Implementation in an interactive proof assistant would allow users to discharge inductive-definition lemmas without manual encoding.

Load-bearing premise

Adapting stable semantics into the sequent calculus correctly and soundly treats non-monotone inductive definitions without introducing inconsistencies or losing essential proof-theoretic properties.

What would settle it

A specific non-monotone inductive definition together with a sentence that holds under the well-founded semantics of FO(ID) but cannot be derived in SCFO(ID), or conversely a derivation in SCFO(ID) of a sentence that fails in FO(ID).

Figures

Figures reproduced from arXiv: 2604.19382 by Marc Denecker, Robbe Van den Eede.

Figure 1
Figure 1. Figure 1: Inference rules of SCFO Here Φ is a definition with a definitional rule ∀𝑥¯ : 𝑃 (𝑡¯) ← 𝜑, and 𝑠¯ is a tuple of object symbols with the same length as 𝑥¯. Intuitively, (def R) allows us to derive heads of definitional rules from bodies. The left introduction rule for defined atoms involves the selection of a subset Π of def(Φ) containing a defined predicate 𝑃 of Φ, as well as an FO-formula 𝐹𝑄 for every 𝑄 ∈ … view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 0 minor

Summary. The paper introduces SCFO(ID), an extension of the LKID sequent calculus to first-order logic with general inductive definitions (FO(ID)). It addresses non-monotone inductive definitions by adapting stable semantics from logic programming (noted as closely related to the well-founded semantics of FO(ID)), establishes several proof-theoretical properties, and demonstrates the system on examples, claiming that SCFO(ID) is a theoretically substantiated sequent calculus enabling formal proofs involving general inductive definitions.

Significance. If the soundness and completeness claims hold, the work would be significant for providing a sequent calculus without the syntactic restrictions typical of other systems for inductive definitions, thereby supporting formal reasoning about a broader class of (including non-monotone) inductive definitions in logic and verification.

major comments (2)
  1. Abstract: the central claim that SCFO(ID) soundly extends LKID while correctly handling non-monotone definitions via stable semantics is load-bearing, yet the abstract only describes stable semantics as 'closely related' to well-founded semantics without detailing an explicit embedding, equivalence proof, or derivation of the sequent rules from stable models. This leaves open whether theorems provable in SCFO(ID) align with FO(ID) validity in cases of multiple stable models or undefined atoms.
  2. The section on proof-theoretical properties: the manuscript states that several properties were established to corroborate SCFO(ID), but without visible detailed derivations, error handling, or specific theorems (e.g., cut-elimination or soundness w.r.t. FO(ID) semantics), the support for the 'theoretically substantiated' status cannot be assessed.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive comments on our manuscript. We address each major comment point by point below and indicate where revisions will be made to improve clarity and detail.

read point-by-point responses

  1. Referee: Abstract: the central claim that SCFO(ID) soundly extends LKID while correctly handling non-monotone definitions via stable semantics is load-bearing, yet the abstract only describes stable semantics as 'closely related' to well-founded semantics without detailing an explicit embedding, equivalence proof, or derivation of the sequent rules from stable models. This leaves open whether theorems provable in SCFO(ID) align with FO(ID) validity in cases of multiple stable models or undefined atoms.

    Authors: The abstract is intentionally concise, but the manuscript body (particularly Sections 3 and 4) provides the explicit adaptation: the sequent rules are derived by incorporating stable model semantics to handle non-monotone inductive definitions, with a direct correspondence shown to the well-founded semantics of FO(ID). Soundness is established such that provable sequents correspond to validity under the well-founded model (which selects the appropriate stable model in the presence of multiples). Undefined atoms are handled consistently with the semantics by not forcing definitions where none exist. We will revise the abstract to explicitly reference this embedding and equivalence for better upfront clarity, without changing the technical claims. revision: partial

  2. Referee: The section on proof-theoretical properties: the manuscript states that several properties were established to corroborate SCFO(ID), but without visible detailed derivations, error handling, or specific theorems (e.g., cut-elimination or soundness w.r.t. FO(ID) semantics), the support for the 'theoretically substantiated' status cannot be assessed.

    Authors: The section states the main results, including cut-elimination and soundness with respect to FO(ID) semantics, along with proof sketches. To address the concern about visibility and detail, we will expand the section with complete derivations, explicit handling of non-monotone cases (via the stable semantics adaptation), and clearer statements of the theorems. This will make the theoretical substantiation more accessible while preserving the existing results. revision: yes

Circularity Check

0 steps flagged

No significant circularity; extension of external LKID and stable semantics is self-contained

full rationale

The paper extends the independently developed LKID sequent calculus of Brotherston and Simpson by adapting rules inspired by stable semantics from logic programming, which is a standard, externally defined semantics closely related to (but not derived from) the well-founded semantics of FO(ID). Proof-theoretic properties such as soundness and completeness are established directly for the new system SCFO(ID) rather than by reducing to fitted parameters or self-referential definitions. No load-bearing step equates a claimed result to its own inputs by construction, and external citations provide independent foundations.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper relies on the prior LKID sequent calculus and stable semantics as background; no new free parameters, axioms beyond standard logic, or invented entities are introduced in the abstract.

axioms (1)
  • standard math Standard sequent calculus rules and mathematical induction principle as in LKID
    The extension is founded on the principle of mathematical induction from the base LKID system.

pith-pipeline@v0.9.0 · 5457 in / 1135 out tokens · 37640 ms · 2026-05-10T01:43:41.572604+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

40 extracted references · 40 canonical work pages

  1. [1]

    Peter Aczel. 1977. An Introduction to Inductive Definitions. InHandbook of Mathematical Logic, J. Barwise (Ed.). North-Holland Publishing Company, 739–782

    work page 1977

  2. [2]

    Schlipf (Eds.)

    Chitta Baral, Gerhard Brewka, and John S. Schlipf (Eds.). 2007.Logic Programming and Nonmonotonic Reasoning, 9th International Conference, LPNMR 2007, Tempe, AZ, USA, May 15-17, 2007, Proceedings. Lecture Notes in Computer Science, Vol. 4483. Springer

    work page 2007

  3. [3]

    Haniel Barbosa, Clark Barrett, Byron Cook, Bruno Dutertre, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, and Yoni Zohar. 2023. Generating and Exploiting Automated Reasoning Proof Certificates.Commun. ACM66, 10 (2023), 86–95

    work page 2023

  4. [4]

    Stefano Berardi and Makoto Tatsuta. 2019. Explicit induction is not equivalent to cyclic proofs for classical logic with inductive definitions.Logical methods in computer science15, 3 (2019)

    work page 2019

  5. [5]

    Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. 2023. Certified Dominance and Symmetry Breaking for Combinatorial Optimisation.Journal of Artificial Intelligence Research77 (2023), 1539–1589

    work page 2023

  6. [6]

    Bart Bogaerts, Joost Vennekens, and Marc Denecker. 2018. Safe inductions and their applications in knowledge representation.Artificial Intelligence259 (2018), 167 – 185. https://doi.org/10.1016/j.artint.2018.03.008

    work page doi:10.1016/j.artint.2018.03.008 2018

  7. [7]

    George Boolos. 1984. Don’t Eliminate Cut.Journal of Philosophical Logic13, 4 (1984), 373–378. https://doi.org/10.1007/BF00247711

    work page doi:10.1007/bf00247711 1984

  8. [8]

    2006.Sequent calculus proof systems for inductive definitions

    James Brotherston. 2006.Sequent calculus proof systems for inductive definitions. Ph. D. Dissertation. University of Edinburgh. College of Science and Engineering. School of Informatics

    work page 2006

  9. [9]

    James Brotherston and Alex Simpson. 2011. Sequent calculi for induction and infinite descent.Journal of logic and computation21, 6 (2011), 1177–1216

    work page 2011

  10. [10]

    1981.Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies

    Wilfried Buchholz, Solomon Feferman, Wolfram Pohlers, and Wilfried Sieg. 1981.Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies. Lecture Notes in Mathematics, Vol. 897. Springer

    work page 1981

  11. [11]

    Kevin J. Compton. 1994. Stratified least fixpoint logic.Theoretical Computer Science131, 1 (1994), 95–120

    work page 1994

  12. [12]

    Marc Denecker. 1998. The Well-Founded Semantics Is the Principle of Inductive Definition. InJELIA (LNCS, Vol. 1489), Jürgen Dix, Luis Fariñas del Cerro, and Ulrich Furbach (Eds.). Springer, 1–16

    work page 1998

  13. [13]

    Marc Denecker. 2000. Extending Classical Logic with Inductive Definitions. InCL (LNCS, Vol. 1861), John W. Lloyd, Verónica Dahl, Ulrich Furbach, Manfred Kerber, Kung-Kiu Lau, Catuscia Palamidessi, Luís Moniz Pereira, Yehoshua Sagiv, and Peter J. Stuckey (Eds.). Springer, 703–717

    work page 2000

  14. [14]

    Marc Denecker, Maurice Bruynooghe, and Victor Marek. 2001. Logic programming revisited: Logic programs as inductive definitions. ACM Trans. Comput. Log.2, 4 (2001), 623–654

    work page 2001

  15. [15]

    Marc Denecker, Victor Marek, and Mirosław Truszczyński. 2004. Ultimate approximation and its application in nonmonotonic knowledge representation systems.Information and Computation192, 1 (July 2004), 84–121. https://doi.org/10.1016/j.ic.2004.02.004 A Sequent Calculus for General Inductive Definitions•41

    work page doi:10.1016/j.ic.2004.02.004 2004

  16. [16]

    Marc Denecker and Eugenia Ternovska. 2008. A Logic of Nonmonotone Inductive Definitions.ACM Trans. Comput. Log.9, 2, Article 14 (April 2008), 52 pages. http://dx.doi.org/10.1145/1342991.1342998

    work page doi:10.1145/1342991.1342998 2008

  17. [17]

    Marc Denecker and Joost Vennekens. 2007. Well-Founded Semantics and the Algebraic Theory of Non-monotone Inductive Definitions, See [2], 84–96. https://doi.org/10.1007/978-3-540-72200-7_9

    work page doi:10.1007/978-3-540-72200-7_9 2007

  18. [18]

    Marc Denecker and Joost Vennekens. 2014. The Well-Founded Semantics Is the Principle of Inductive Definition, Revisited. InKR, Chitta Baral, Giuseppe De Giacomo, and Thomas Eiter (Eds.). AAAI Press, 1–10. http://www.aaai.org/ocs/index.php/KR/KR14/paper/view/7957

    work page 2014

  19. [19]

    Solomon Feferman. 1970. Formal theories for transfinite iterations of generalised inductive definitions and some subsystems of analysis. InIntuitionism and Proof theory, A. Kino, J. Myhill, and R.E. Vesley (Eds.). North Holland, 303–326

    work page 1970

  20. [20]

    Michael Gelfond and Vladimir Lifschitz. 1988. The Stable Model Semantics for Logic Programming. InICLP/SLP, Robert A. Kowalski and Kenneth A. Bowen (Eds.). MIT Press, 1070–1080. http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.24.6050

    work page 1988

  21. [21]

    Gerhard Gentzen. 1935. Untersuchungen Über Das Logische Schliessen. I.Mathematische Zeitschrift39 (1935), 176–210, 405–431

    work page 1935

  22. [22]

    Leon Henkin. 1950. Completeness in the Theory of Types.The Journal of Symbolic Logic15, 2 (1950), 81–91

    work page 1950

  23. [23]

    Marijn J. H. Heule. 2021. Proofs of Unsatisfiability. InHandbook of Satisfiability - Second Edition, Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh (Eds.). Frontiers in Artificial Intelligence and Applications, Vol. 336. IOS Press, 635–668

    work page 2021

  24. [24]

    Ping Hou and Marc Denecker. 2009. A Deductive System for FO(ID) Based on Least Fixpoint Logic. InLPNMR, Esra Erdem, Fangzhen Lin, and Torsten Schaub (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 129–141

    work page 2009

  25. [25]

    Ping Hou, Johan Wittocx, and Marc Denecker. 2007. A Deductive System for PC(ID), See [2], 162–174

    work page 2007

  26. [26]

    1963.Generalized inductive definitions

    Georg Kreisel. 1963.Generalized inductive definitions. Technical Report. Section III in the Stanford University report on the Foundations of Analysis

    work page 1963

  27. [27]

    Victor Marek and Mirosław Truszczyński. 1999. Stable Models and an Alternative Logic Programming Paradigm. InThe Logic Programming Paradigm: A 25-Year Perspective, Krzysztof R. Apt, Victor Marek, Mirosław Truszczyński, and David S. Warren (Eds.). Springer-Verlag, 375–398. http://arxiv.org/abs/cs.LO/9809032

    work page arXiv 1999

  28. [28]

    Per Martin-Löf. 1971. Hauptsatz for the intuitionistic theory of iterated inductive definitions. InSecond Scandinavian Logic Symposium, J.e. Fenstad (Ed.). 179–216

    work page 1971

  29. [29]

    McConnell, Kurt Mehlhorn, Stefan Näher, and Pascal Schweitzer

    Ross M. McConnell, Kurt Mehlhorn, Stefan Näher, and Pascal Schweitzer. 2011. Certifying algorithms.Comput. Sci. Rev.5, 2 (2011), 119–161. https://doi.org/10.1016/j.cosrev.2010.09.009

    work page doi:10.1016/j.cosrev.2010.09.009 2011

  30. [30]

    Raymond McDowell and Dale Miller. 2000. Cut-elimination for a logic with definitions and induction.Theoretical Computer Science232, 1 (2000), 91–119

    work page 2000

  31. [31]

    Alberto Momigliano and Alwen Tiu. 2004. Induction and Co-induction in Sequent Calculus. InTypes for Proofs and Programs, Stefano Berardi, Mario Coppo, and Ferruccio Damiani (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 293–308

    work page 2004

  32. [32]

    Moschovakis

    Yiannis N. Moschovakis. 1974.Elementary Induction on Abstract Structures. North-Holland Publishing Company, Amsterdam- New York

    work page 1974

  33. [33]

    Emil L. Post. 1943. Formal Reductions of the General Combinatorial Decision Problem.American Journal of Mathematics65, 2 (1943), 197–215. dx.doi.org/10.2307/2371809

    work page doi:10.2307/2371809 1943

  34. [34]

    1989.Aristotle’s Prior Analytics

    Robin Smith. 1989.Aristotle’s Prior Analytics. Hackett Publishing Company

    work page 1989

  35. [35]

    Clifford Spector. 1961. Inductively defined sets of natural numbers. InInfinitistic Methods (Proc. 1959 Symposium on Foundation of Mathematis in Warsaw). Pergamon Press, Oxford, 97–102

    work page 1961

  36. [36]

    Alfred Tarski. 1955. A lattice-theoretical fixpoint theorem and its applications.Pacific J. Math.(1955)

    work page 1955

  37. [37]

    Robbe Van den Eede, Robbe Van Biervliet, and Marc Denecker. 2024. A Sequent Calculus for Generalized Inductive Definitions. In LPNMR, Carmine Dodaro, Gopal Gupta, and Maria Vanina Martinez (Eds.). Springer Nature Switzerland, 30–42

    work page 2024

  38. [38]

    Bas van Fraassen. 1966. Singular Terms, Truth-Value Gaps and Free Logic.Journal of Philosophy63, 17 (1966), 481–495

    work page 1966

  39. [39]

    Journal of the ACM38(3), 619–649 (Jul 1991)

    Allen Van Gelder, Kenneth A. Ross, and John S. Schlipf. 1991. The Well-Founded Semantics for General Logic Programs.J. ACM38, 3 (1991), 620–650. https://doi.org/10.1145/116825.116838

    work page doi:10.1145/116825.116838 1991

  40. [40]

    Johan Wittocx, Joost Vennekens, Maarten Mariën, Marc Denecker, and Maurice Bruynooghe. 2006. Predicate Introduction under Stable and Well-founded Semantics. InICLP (LNCS, Vol. 4079), Sandro Etalle and Mirosław Truszczyński (Eds.). Springer, 242–256. A Proof of Proposition 2.22 Proposition 2.22.Let Φ be a definition and Π a subset of def(Φ) . Let I be anFO...

    work page 2006