Sascha Kehrli
B.Sc. thesis advised by Bryan Ford and Roger Wattenhofer
September 30, 2025
Abstract:
This thesis presents a foundational formalization of Grounded Arithmetic (GA),
a first-order arithmetic based on the principles of Grounded Deduction (GD),
directly within the Isabelle/Pure framework. Unlike classical and constructive
logics, which impose strict termination requirements on definitions to preserve
consistency, GD admits arbitrary recursion at the definitional level. To remain
consistent, GA weakens other inference rules, many of which demand explicit
habeas quid termination proofs of subexpressions as premises. The goal of this
thesis is to investigate the feasibility of GA as a practical basis for
mathematical and computational reasoning by fully axiomatizing it in Pure.
The formalization, Isabelle/GA, achieves three main contributions. It provides
a complete axiomatization of GA in Pure, together with definitions of core
arithmetic functions using the native recursive definitional mechanism of GA,
and proofs of their fundamental properties. It develops a suite of reasoning
tools, such as subgoal solvers, syntactic extensions, and methods for case
analysis and induction, automating many of GA’s habeas quid proof obligations
and moving away from axiom-level proofs. Finally, it shows GA’s expressive
power by encoding inductive datatypes via Cantor tuples and proving their
essential properties, demonstrated by a fully verified List datatype.
The resulting system demonstrates that GA “works”, despite many weakened
inference rules: one can reason productively in it, prove termination of
functions beyond primitive recursion such as Ackermann’s function, and encode
arbitrary inductive datatypes. While the implementation of a fully general
definitional mechanism for inductive datatypes remains future work, the
foundations developed here provide the necessary basis. Altogether, this thesis
shows that grounded reasoning is practical and that GA has the potential to
mature into a serious alternative foundation for reasoning about computation.