{"id":"arxiv/2609.26337","url":"https://arxiv.org/abs/2609.26337","tags":["cs.LO","math.LO"],"score":0,"title":"An Infinitary and a Cyclic Sequent Calculus for Non-Monotone Inductive Definitions","domain":"cs.LO","source":"arxiv","authors":["Robbe Van den Eede"],"reviews":0,"subject":"cs.LO","summary":"Inductive definitions are an important form of knowledge in mathematics and computer science. Two common techniques to prove theorems about inductive definitions are the principle of mathematical induction and the principle of infinite descent. To formalize these principles, Brotherston and Simpson introduced the sequent calculus proof systems LKID, for mathematical induction, and LKIDω and CLKIDω , for infinite descent. LKIDω is an infinitary system, in which proofs are infinite trees, and CLKIDω a cyclic system, in which proofs are finite graphs. However, these calculi restrict to monotone…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-09-22","reactions":{}}