Home - Topics - Papers - Talks - Theses - Blog - CV - Photos - Funny

Formalizing Grounded Arithmetic atop Isabelle/Pure

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.

B.Sc. Thesis: PDF

Implementation: GitHub

See also:



Topics: Logic Programming Languages Formal Verification Grounded Deduction Bryan Ford