← 研踪 PaperTrailarXiv:2611.00176 · v2
Coinduction in Grounded Arithmetic
首次提交 2026-10-30 22:42
版本更新 2026-11-11 16:36
雷达观测 2026-11-13 11:11
摘要
A grounded arithmetic counts a sentence true only when a terminating process establishes it; a sentence no such process settles has no value. Such a logic can state that an event happens, but not that it never happens under unbounded choice. This paper extends such a logic so that it can. The base is Reflective Grounded Arithmetic (RGA) with Inductive Grounded Arithmetic (IGA)'s least-fixed-point reading and ground induction. It adds a separate greatest-fixed-point former $ν$ with Park's coinduction rule, proves that one former cannot carry both ground induction and coinduction, and adds a dichotomy rule: the classical disjunction between a least-fixed-point atom and the greatest-fixed-point atom of its dual, under a derivable premise that the body's leaves are decided. The systems are sound for an explicit model reading every $ν$-body at its greatest fixed point, hence consistent; they agree with the least model where it has a value and prove sentences it leaves without one. The dichotomy trades the underivable hypothesis that an order is well-founded for the derivable one that its steps are decided, at the price of a change of model. With ground induction the dichotomy derives the omniscience rule of the sibling system OGA, so the system has no semantics whose certificates for universals are its own proofs; without the dichotomy it has one, though unsound for the least model. The systems prove, as single sentences, that every decided tree is well-founded or has an infinite branch given by a term, total in the new model; that random assignment terminates while its divergent twin runs forever; that a fair loop terminates and the alternating-bit protocol delivers every message; that open games are determined; that the termination gap in Nakata and Uustalu's trace semantics closes; and that Cinderella wins the bucket game at capacity three. Isabelle/HOL checks every result.
作者备注：major revision; now 89 pages
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v2 · 2026-11-11 16:36 · 最新观测版本
Coinduction in Grounded Arithmetic
A grounded arithmetic counts a sentence true only when a terminating process establishes it; a sentence no such process settles has no value. Such a logic can state that an event happens, but not that it never happens under unbounded choice. This paper extends such a logic so that it can. The base is Reflective Grounded Arithmetic (RGA) with Inductive Grounded Arithmetic (IGA)'s least-fixed-point reading and ground induction. It adds a separate greatest-fixed-point former $ν$ with Park's coinduction rule, proves that one former cannot carry both ground induction and coinduction, and adds a dichotomy rule: the classical disjunction between a least-fixed-point atom and the greatest-fixed-point atom of its dual, under a derivable premise that the body's leaves are decided. The systems are sound for an explicit model reading every $ν$-body at its greatest fixed point, hence consistent; they agree with the least model where it has a value and prove sentences it leaves without one. The dichotomy trades the underivable hypothesis that an order is well-founded for the derivable one that its steps are decided, at the price of a change of model. With ground induction the dichotomy derives the omniscience rule of the sibling system OGA, so the system has no semantics whose certificates for universals are its own proofs; without the dichotomy it has one, though unsound for the least model. The systems prove, as single sentences, that every decided tree is well-founded or has an infinite branch given by a term, total in the new model; that random assignment terminates while its divergent twin runs forever; that a fair loop terminates and the alternating-bit protocol delivers every message; that open games are determined; that the termination gap in Nakata and Uustalu's trace semantics closes; and that Cinderella wins the bucket game at capacity three. Isabelle/HOL checks every result.
查看此版本解读 →查看此版本原文 ↗