Van der Waerden's theorem implies the infinitude of the primes

(Sam Buss and Denis Hirschfeld helped me on this post.)

I was reading the table of contents of the American Math Monthly and saw an article by Levent Alpoge entitled

Van der Waerden and the primes

in which he showed from VDW's theorem that the set of primes is infinite. The article is  here and here. My writeup of it is here.  Prof K saw me reading the paper.

 K: I see you are interested in proving the set of primes is infinite from VDW's theorem.

BILL: Yes, who wouldn't be!!!!

 K: Well, lots of people. Including me. Can't you just state VDW's theorem and then give the normal proof? Would that count? Besides, we already have an easy proof that the set of primes is  infinite without using VDW's theorem.

I turn K's comments  into a valid question:  What does it mean to prove A from B if A is already known?

 There are two issues here, informal and formal.

Informally:  If you look at the proof of VDW-->primes infinite the steps in that proof look easier than than the usual proof that the set of primes is infinite. And the proof is certainly different. If you read the paper you will see that I am certainly not smuggling in the usual proof. Also, the proof truly does use VDW's theorem.

Formally one could (and people working in Reverse Mathematics do similar things- see the books Subsystems of Second order Arithmetic by Simpson,, and  Slicing the Truth, reviewed here) devise a weak axiom system that itself cannot prove the set of Primes is Infinite, but can prove the implication VDW-->Primes infinite.  Note that Reverse Mathematics does this sort of thing, but for proofs involving infinite objects, nothing like what I am proposing here.

Open Problem 1: Find a proof system where the implication VDW-->Primes infinte can be proven, but primes infinite cannot. Sam Buss pointed out to me that for the weak system IΔ₀ it is not known if it can prove the primes are infinite.

Open Problem 2: Find a proof system where you can do both proofs, but the prove of the implication is much shorter. Perhaps look at (VDW--> there are at least n primes) and (there are at least n primes)
and look at the length of proof as a function of n.

Open Problem 3: The statement there are no primes with  n bits, the with leading bit 1 can be expressed as a propositional statement. Get lower bounds on its refuation in (say) resolution. (A commenter pointed out an error in a prior version of this one so be wary- there may be an error here as well.)

I am suggesting work on the reverse mathematics of systems much weaker than RCA₀. I do not know if this is a paper, a PhD thesis, a career, a dead end, or already pretty much done but I am not aware of it.