Coinduction in Grounded Arithmetic
Bryan Ford
arXiv preprint 2611.00176
October 30, 2026
Abstract:
A grounded arithmetic counts a sentence as 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 wherever it has a value and prove sentences it leaves without
one. The dichotomy replaces the underivable hypothesis that an order
is well-founded by the derivable one that its steps are decided; the
change of model pays for the move. With ground induction the
dichotomy derives the omniscience rule of the sibling arithmetic
\oga, so the system has no semantics whose certificates for universals
are its own proofs. 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.
See also: