Formalization of bounded arithmetic

In this project, I explore a way to formalize the results from the field of bounded arithmetic, most notably from the book Logical Foundations of Proof Complexity from 2010 by Stephen Cook and Phuong Nguyen.

The design and motivation behind this project was presented at AITP 2025 in Aussois, France.

If successful, it could contribute towards:

• providing a sensible way to certify computational complexity bounds of computer programs
• providing a new way of extracting computer programs from mathematical theorems
• perhaps getting a few logicians interested in formal verification

Please see the file for a demonstration.

Current todo list

• we could probably do without modifying the mathlib.ModelTheory library (which now, modified, is in BoundedArithmetic/BoundedModelTheory)
• it seems in reach to formalize that -defines the relation.
• the design has to be slightly altered, as now when proving theorems in , we can't use already proved lemmas for . Typeclasses should be utilized to enable this behaviour
• a huge milestone for this project is to formalize that defines sorting
• demonstrate how code can be extracted from constructive proofs of definability of functions
• explore potential for proof automatization coming from finite axiomatizability of

Problems in this project

Single-sorted logic only

The design of mathlib.ModelTheory is fundamentally single-sorted. When I started working on , I re-wrote parts of the library to supports two sorts. It is feasible, but it is much easier to use explicit typing rules to encode two-sorted theory as a single-sorted one. This is demonstrated in file V0.lean

Too classical

ModelTheory sets internally. This is not ideal, as in our setting we need to check if a formula is , , etc. and defining the existential quantifier like this completely breaks this. It also breaks the computational content of the proofs. For these reasons, I rewrote parts of ModelTheory to not do this substitution. I applied sorry where it was necessary for the library to work; these should be very safe, as the change is not important for the semantics.

Now it seems likely that we could do without modifying ModelTheory by just not caring about it. It is a task of a lower priority so I have left dealing with that for now.

Many lemmas missing

Working on this project at this stage requires proving many lemmas about ModelTheory.BoundedFormula definitions for our types. This is good and perhaps will contribute to making this library even better.

Very slow simp

This is something I have not dealt with yet, and it is a problem - simplifying the formulas resulting from creating the induction axioms is very slow. It makes my VSCode laggy, my computer heat and, most annoyingly, the apply? and rw? tactics timeout. This definitely has to be addressed so that the simplifications are fast and simple.

Existing works

Foundation project

Most notably, there is an active project on formalizing logic in Lean 4, Foundations. Their design, however, doesn't enable to solve the crux problem I want to solve - to extract useful computation from the proofs. They focus on mathematical theories, whereas my desired focus are two-sorted theories capturing complexity classes. Foundations' design doesn't align well with Mathlib.ModelTheory`, and also doesn't foster convenient extraction of code from proofs. Initially I thought that some of their proofs are conducted in the Lean model only (due to using lemmas from Mathlib inside of the object-theory proofs), this is not the case however. That was addressed in my discussion with the developers.

Flypitch project

In a brekathrough effort, contributors of the Flypitch project managed to formalize the proof of independence of continuum hypothesis from ZFC. They obviously considered the notion of provability.

Developments in Rocq

The environment of Rocq seemed to better foster this project, as the community of Lean is entirely nonconstructive and is less likely to be interested in results about reverse mathematics. Importantly, these projects exist:

• Rocq library to work with FOL
• Notable work on FOL in Rocq

Just a shallow embedding

The obvious approach for this project is to embed our weak logic shallowly inside of Rocq / Lean / Isabelle. It works well for the single axioms. There is a catch though - all these systems have a single Prop type (or equivalent) and have completely no way of expressing $\Delta_0-Prop$ or $\Sigma_1-Prop$. Without a deep embedding of at least the syntax of logic, it doesn't seem possible to proceed in any of the existing systems. And a deep embedding of the logic obviously doesn't foster any way of proving these deeply embedded formulas without implementing the whole model theory and proving in generalized model.

Shallow embedding + nice syntactical macros to ease proving in object theory

Initially I had thought that the only feasible (i.e. not taking years of work) way to approach this is to do everything in Lean, as a shallow embedding, but using syntactical macros provide frontend enabling proving in the object theory and making cheating harder / easily visible to the reader.

I found some pointers on how could it looks like:

• Presentation by Simon Hudon
• Iris Proof mode for Lean

Obviously, our current approach is good enough and doesn't need improving the frontend for now.

Contact

Please contact me at ruplet+bounded at ruplet dot com.

History of the project

This project is a part of my Master's thesis at the University of Warsaw. My Master's project was to answer how to design programming languages to capture precisely a particular complexity class. The works are in a separate repository.

This project, as my whole Master's program, has been supported by the ZSM IDUB program.