Formalization of arithmetic: Reviewer needed!

Stream: mathlib4

[Paweł Balawender]

Hey!

For the past couple of months I have been exploring ways to formalize results from the field of arithmetic (in particular, bounded arithmetic). I am basing my work on the book Logical Foundations of Proof Complexity (full text available on anna's) The results are beautiful and are of the form "if you can prove theorem defining function f(x) in this logic, then the algorithm you implicitly used to prove this theorem is in PTIME (or LOGSPACE, or AC^0 ...)". There's a bunch of ways to formalize such theorems, most of which not really feasible; but I found a satisfactory approach, which enables us to transfer proofs from paper to computer, for (I think?) most of the field of arithmetic. An example of this is as follows (Draft: Exercise 3.8, page 36 = page 47 of the main.dvi PDF file; in official print, Exercise III.1.8, page 42 = 60 of pdf): these are theorems provable in the theories we study (with proof sketches on the screenshot):
image.png
and this if my formalization of commutativity of multiplication:
image.png

what my approach does not enable is reasoning about the deduction system itself (because the deduction system is the implementation of Lean). But it does enable us to digitalize most of interesting theorems in this field.

The weakest theory studied (V^0) does not allow us to define a sorting function, nor prove the Pigeonhole principle. But we can add an axiom (taking us from AC^0 to TC^0 complexity class) which allows us to do that (and I have a sketch of formalization of Pigeonhole in theory for TC^0). This is quite nice, because we realistically can extract programs from these proofs - which gives us a program with a "certified" complexity class (conditions: we believe proofs of Cook and Nguyen; we believe our custom code extraction procedure).

I am still working on the code and results are slightly scattered around, but I want to start looking for someone willing to review my code when it's ready, as I haven't meet too many people knowing both Lean and something about arithmetic :) Please check out my repo, especially the proofs conducted inside of the weak logic IDelta0 here: add_cancel_right. I will be very grateful for every piece of early feedback and will be happy to include it now, before the code grows and it becomes more difficult to change design :)

Perhaps it's worth noting that I have already presented this work at aitp 2025! You can check out the slides here: link, and in the repo there is also the abstract I submitted and the reviews it received ;) When I was submitting the abstract, I wasn't sure how to design this formalization, so it was completely speculative if it'd work. But it: a) was interesting enough anyway b) turned out that the formalization is completely doable and very convenient to work with

[Dexin Zhang]

This sounds really interesting! I read a bit about the extraction algorithm, and if I understand correctly, the extraction algorithm takes the witness term out from ⟨term, proof⟩ : ∃ x, proposition. What would happen if the proposition is proved via contradiction?

[Paweł Balawender]

Dexin Zhang said:

This sounds really interesting! I read a bit about the extraction algorithm, and if I understand correctly, the extraction algorithm takes the witness term out from ⟨term, proof⟩ : ∃ x, proposition. What would happen if the proposition is proved via contradiction?

Thanks for the interest @Dexin Zhang ! There are two things here.

First is that the way of doing extraction I have in this file is not general. My code here only handles the special case of this particular binary addition theorem. More generally, this approach will surely not support functions that rely on classical logic to prove that the result exists. However, it shouldn't be a problem to extract code from a function which constructively builds the result, but then proves its correctness classically. E.g. in my extraction example, when I find the (term, proof) : \exists x, proposition, i ignore the proof anyway - no problem if it uses contradiction. The thing is that the function we create and ultimately run is not guaranteed to be correct (i.e. that the result satisfies some formula) anyway.

Second thing is much deeper. In this area, "witnessing theorems" are considered, which say that if you can prove the existence of the result of a function in one of these theories, then you can actually compute the result in the corresponding complexity class. The proof of such a theorem should ideally correspond to a general code extraction procedure. For example, in the screenshot, $V^1$ is the theory for polytime, so if you can prove existence there, you can compute the result in polytime.

image.png
This is a relatively active area of research. The problem is that the proofs they traditionally do are uncomputable; I looked at the two proofs in Logical Foundations for the theory $V^0$, and they don't lead to any practical code extraction mechanism. I also asked a question on mathoverflow some time ago, but didn't get anything useful. And at STOC this year there was even a talk titled "Witnessing Theorems — Converting Proofs into Algorithms" by Sam Buss, but I haven't been able to find any intel on what was in it :< Cook and Nguyen state, while talking about witnessing for $V^0$ that the proofs are "not difficult to find" (screenshot) - perhaps they are right? I haven't tried to do it on my own as I don't have the best intuition on the complexity of these logical algorithms such as cut elimination.
image.png

[Dexin Zhang]

@Paweł Balawender Thanks for the explanation. If I understand correctly, witness theorems you mentioned are telling us "if proofs exist, then algorithms in certain complexities exist", but that does not give us a translation procedure from proofs to algorithms, right? Would the case be easier when the proofs are intuitionistic (not using excluded middle)?

[Paweł Balawender]

Dexin Zhang said:

Paweł Balawender Thanks for the explanation. If I understand correctly, witness theorems you mentioned are telling us "if proofs exist, then algorithms in certain complexities exist", but that does not give us a translation procedure from proofs to algorithms, right? Would the case be easier when the proofs are intuitionistic (not using excluded middle)?

I suspect it should be the case! I think you can go one step further and use classical logic to prove properties about the witness (for x, y, prove that phi(x, y)), but only use constructive reasoning to show the witness (forall x, exists y)

[Paweł Balawender]

Btw, @Dexin Zhang I like your recent commits in ModelTheory.Arithmetic.Presburger! I think that we can resolve your TODO in Presburger.Basic Define the theory of Presburger arithmetic and prove its properties (quantifier elimination, completeness, etc). with the approach I used to define IDelta0. In particular, we would just have to remove the 'Delta0' restriction from induction and remove multiplication from IDelta0 to get Presburger?

[Dexin Zhang]

Paweł Balawender said:

I suspect it should be the case! I think you can go one step further and use classical logic to prove properties about the witness (for x, y, prove that phi(x, y)), but only use constructive reasoning to show the witness (forall x, exists y)

Got it. I definitely agree with you, and I'd like to see how far this approach can go :slight_smile:

[Dexin Zhang]

Paweł Balawender said:

Btw, Dexin Zhang I like your recent commits in ModelTheory.Arithmetic.Presburger! I think that we can resolve your TODO in Presburger.Basic Define the theory of Presburger arithmetic and prove its properties (quantifier elimination, completeness, etc). with the approach I used to define IDelta0. In particular, we would just have to remove the 'Delta0' restriction from induction and remove multiplication from IDelta0 to get Presburger?

Thanks for your interest! Yes, it's pretty similar, though I plan to define the theory of Presburger arithmetic syntactically (e.g. you can see the existing docs#FirstOrder.Language.Theory.field). The reasoning will be on the models (since Mathlib does not contain any proof system), just like what you did in your repo. Honestly speaking I haven't make too much progress on that :innocent:

[Paweł Balawender]

Dexin Zhang said:

Paweł Balawender said:

Btw, Dexin Zhang I like your recent commits in ModelTheory.Arithmetic.Presburger! I think that we can resolve your TODO in Presburger.Basic Define the theory of Presburger arithmetic and prove its properties (quantifier elimination, completeness, etc). with the approach I used to define IDelta0. In particular, we would just have to remove the 'Delta0' restriction from induction and remove multiplication from IDelta0 to get Presburger?

Thanks for your interest! Yes, it's pretty similar, though I plan to define the theory of Presburger arithmetic syntactically (e.g. you can see the existing docs#FirstOrder.Language.Theory.field). The reasoning will be on the models (since Mathlib does not contain any proof system), just like what you did in your repo. Honestly speaking I haven't make too much progress on that :innocent:

Cool! It will be nice when we have a proof system in mathlib indeed, though it's probably still a long way ahead. If you plan to go back to reasoning on models, I'll be glad to help

[James E Hanson]

Dexin Zhang said:

Paweł Balawender Thanks for the explanation. If I understand correctly, witness theorems you mentioned are telling us "if proofs exist, then algorithms in certain complexities exist", but that does not give us a translation procedure from proofs to algorithms, right? Would the case be easier when the proofs are intuitionistic (not using excluded middle)?

These results don't really work the same way as constructive algorithm extraction (although they are related). What these theorems say is really "If theory $T$ proves that algorithm $A$ computes a total function, then $A$ has time complexity $X$."

The subtlety is going to be in terms of extracting a more specific bound (like a polynomial for polytime) from a given proof. That requires analysis of the totality proof.

[Paweł Balawender]

James E Hanson said:

Dexin Zhang said:

Paweł Balawender Thanks for the explanation. If I understand correctly, witness theorems you mentioned are telling us "if proofs exist, then algorithms in certain complexities exist", but that does not give us a translation procedure from proofs to algorithms, right? Would the case be easier when the proofs are intuitionistic (not using excluded middle)?

These results don't really work the same way as constructive algorithm extraction (although they are related). What these theorems say is really "If theory $T$ proves that algorithm $A$ computes a total function, then $A$ has time complexity $X$."

The subtlety is going to be in terms of extracting a more specific bound (like a polynomial for polytime) from a given proof. That requires analysis of the totality proof.

Yes, if you want to obtain a bound like $n^2$ time, this approach will not provide it yet.

I would like to learn more about the complexity of finding a witness, given a (nonconstructive) proof as input. I saw some results about it being $NC^1$-complete for some proof system, and since this is lower than LOGSPACE, it’s quite feasible