Reverse mathematics and Dirichlet's theorem(Arithmetic prog)

Stream: maths

[Juho Pitkänen]

Does anyone know how strong axioms are required to prove it? Could it be provable in PA? Has it been proven in Lean yet?

[Violeta Hernández]

Lean's theory is actually slightly stronger than ZFC, so that probably doesn't give you a good answer.

[Kevin Buzzard]

Lean is not a good tool to answer these questions. The Lean proof of Dirichlet's theorem tells you that Dirichlet's theorem is provable in Lean's type theory. It would be nice to imagine that we could now set some kind of program loose on the proof and this program would come back reporting that the proof actually works in some fragment of PA or whatever, but unfortunately this seems to be far from reality. Yes I am pretty sure that you can prove primes in AP in PA, it wouldn't be much fun, you could just mimic Dirichlet's original proof (which makes extensive use of the real numbers) but then just rewrite everything in terms of sequences of rationals.

[Juho Pitkänen]

I see, thanks

[James E Hanson]

I agree with Kevin's assessment that there would be no fundamental subtlety with formalizing Dirirchlet's original proof in Peano arithmetic. With the right layer of definitions, it wouldn't even look that different (i.e., you can talk about $\Delta_n$-definable real numbers and derivatives and integrals of $\Delta_n$-definable functions for a fixed $n$ internally in PA.

For results in number theory, it's really only in proofs that involve large-scale categorical machinery (like certain notions of cohomology) where it becomes unclear how to proceed.

[Paweł Balawender]

I am currently working on formalizing reverse maths in Lean. We can write robust formalizations of proofs in weaker logics. The theories I am interested in are Cook and Nguyen's logics characterizing complexity classes.

The approach is:

1. bundle the single axioms you need in a structure or a class:
   image.png

   

2. to add axiom schema of induction, you need a deep embedding of logical formulas to determine that a formula is $\Delta_0$, $\Sigma_1$ etc. For that you need to use Mathlib.ModelTheory.Syntax

3. you don't deep-embed the deduction system; Lean is your deduction system, and you quantify over every model to prove a theorem. Lean logic leaks into the system; I don't know how to forbid users from using exfalso, but such leakage should be detectable afterwards. What would be bad is weird aspects of Lean type theory allowing you to cheat, but it's not obvious they can when you quantify over every model of just your basic axioms

Check out my proof of 'addition is associative'. It's done in $I\Delta_0$, Peano axioms with induction restricted to formulas with bounded quantifiers only. In more interesting theories, e.g. $V^0$, pigeonhole is not provable; but it suffices to add an axiom (leading us to a higher complexity class) to make it provable; here's my sketch of 'Pigeonhole Principle is provable in logic corresponding to binary circuit reductions with a $\text{TC}^0$-complete problem added'. The sketch has sorries, but it's not bad; they faithfully transfer lemmas from the original proof in the book: page 292 of draft (310 of the main.dvi pdf file linked above)
image.png

[Paweł Balawender]

Important: you might be interested in second-order arithmetic. I have only considered first-order theories, although my intuition is that the framework should be very similar. Encoding second-order logic into first-order logic should work for the purpose of proving anything inside of the theory. I might be wrong thought, I haven't tried doing that (but would love to see RCA0 being formalized the same way as my theories) :)

Btw, check out the recent thread about logical works in Lean: my thread about need for future reviewer of my code :) link and the more general thread created afterwards: formalizing logic in lean

[Juho Pitkänen]

Pawel, I’ll check your work out. I’m mainly interested in first order stuff, so I don’t mind the focus on those

[James E Hanson]

I found out more this morning. Jeremy Avigad's paper Number theory and elementary arithmetic (which can be found here) discusses some of the history of formalizations of Dirichlet's theorem on arithmetic progressions in weak fragments of arithmetic. It seems that Takeuti (in 1978) developed enough complex analysis in Peano arithmetic to make the ordinary proof go through directly. Then Sudac showed in 2001 that Dirichlet's theorem is provable in $I\Sigma_1$ (a relatively weak fragment of Peano arithmetic) and then Cornaros and Dimitracopoulos showed that the proof goes through in $I\Delta_0 +$"$2^x$ is a total function", which is an even weaker fragment.

[James E Hanson]

Paweł Balawender said:

Important: you might be interested in second-order arithmetic. I have only considered first-order theories, although my intuition is that the framework should be very similar. Encoding second-order logic into first-order logic should work for the purpose of proving anything inside of the theory. I might be wrong thought, I haven't tried doing that (but would love to see RCA0 being formalized the same way as my theories) :)

This is maybe an unfortunate aspect of the terminology, but technically second-order arithmetic (and fragments thereof) are treated as two-sorted first-order theories in reverse math, so other than the issue of dealing with many-sorted first-order logic (which I believe has not been done in Lean yet?), it should be possible to approach fragments of second-order arithmetic the same way.

[Paweł Balawender]

James E Hanson said:

Paweł Balawender said:

Important: you might be interested in second-order arithmetic. I have only considered first-order theories, although my intuition is that the framework should be very similar. Encoding second-order logic into first-order logic should work for the purpose of proving anything inside of the theory. I might be wrong thought, I haven't tried doing that (but would love to see RCA0 being formalized the same way as my theories) :)

This is maybe an unfortunate aspect of the terminology, but technically second-order arithmetic (and fragments thereof) are treated as two-sorted first-order theories in reverse math, so other than the issue of dealing with many-sorted first-order logic (which I believe has not been done in Lean yet?), it should be possible to approach fragments of second-order arithmetic the same way.

Wow nice, I didn't know that they treat it as two-sorted first-order. This can be worked with!

For the details of encoding: section 4.5 https://www.karlin.mff.cuni.cz/~krajicek/cook-nguyen.pdf
I used this concept to define the 2-sorted, first-order theory $V^0$ of Cook and Nguyen, having num (representing unary numbers) and str (representing binary numbers / finite sets of integers): https://github.com/ruplet/formalization-of-bounded-arithmetic/blob/79cfe660f91da0133bc9bee5b8e7f528de1f685c/BoundedArithmetic/V0.lean#L121

i am working hard to make the code nice (and it will be nice), but it's a lot of content and takes me days to clean up :) sorry for sending you work in progress