Is the Green-Tao primes theorem true or pseudo-true? [closed]

Question

The Green-Tao primes theorem "The primes contain arbitrarily long arithmetic progressions" Ann Math 2008, is certainly a tour de force and extremely technical.

The authors point out that they have taken precautions to not use Axiom of Choice. Choice is mentioned several times in the paper, eg p.485:

In particular we shall always remain in the finitary setting of ZN , in contrast to the standard ergodic theory framework in which one takes weak limits (invoking the axiom of choice) to pass to an infinite measure-preserving system.

p.516:

In the original ergodic theory arguments of Furstenberg this algorithm was not guaranteed to terminate, and indeed one required the axiom of choice (in the guise of Zorn’s lemma) in order to conclude the structure theorem. However, in our setting we can terminate in a bounded number of steps...

In terms of constructive vs classical mathematics however AC is only one of the forbidden axioms. Another is excluded middle. But I can't follow the paper to understand whether results that invoke excluded middle are used.

Kolmogorov, in "On the tertium non datur principle" writes "a proposition is pseudo-true if its double negation is true".

Is the Green-Tao theorem true or pseudo-true?

Answer 1

Concerning just classical logic and the use of AC, I am surprised to hear that precautions were taken to avoid AC, since the theorem is expressible in first-order number theory, and such statements are absolute from the set-theoretic universe $V$ to the constructible universe $L$, where the axiom of choice holds. It follows from this that the axiom of choice has no bearing on the argument, and any use of the axiom of choice could be omitted simply by pointing out this absoluteness. So actually, no precautions were necessary.

The basic situation is that the arithmetic consequences of ZFC are precisely the same as the arithmetic consequences of ZF, and so one may assume AC for such purposes without loss of generality.

A similar situation arises for example with Fermat's last theorem, meaning that it wouldn't have mattered whether or not Wiles had used AC in his proof. Even if he had, we could have constructed a new proof that does not use AC by arguing that we may first assume V=L and hence AC without loss of generality, since the truth of FLT is not affected by moving to L, and then carrying out the previous proof.