Coinduction in Grounded Arithmetic

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.