That actually brings up a question: given a proof S in ZFC of an arithmetic statement T, how tightly can we bound the size of the proof of the smallest proof in ZF of T in terms of the length of S? It isn’t immediately obvious to me even that there’s any such bound that is a computable function. So it may be that although the proof of FLT doesn’t require choice, the length of any such proof will be much too long for a human to ever work out. (This issue obviously goes away if there’s a way to make absoluteness constructive. I don’t know of any but I’m not a model theory person.)

]]>Also, Douglas was referring to Schoenfeld’s absoluteness theorem, which tells us that all the *purely arithmetical* consequences of ZFC can be proved in ZF alone. That implies that the proof of FLT can’t possibly need the axiom of choice.

Ok, it seems tricky point, in fact Wiles’ proof may involve even worse stuff like Grothendieck Universes

If “Shoenfield” has a paper can you link ?

]]>Good point, in fact it’s not clear (afaik) whether Mochizuki’s recent claimed proof of the abc conjecture satisfies ZFC – but suppose his argument turns out to be quite persuasive, but requiring an addition axiom(s) – how would the mathematics community respond?

I was fascinated by the Goodstein Theorem as a student, since it was a very concrete example of a sequence of numbers which converge to zero (incredibly after massive explosive growth) – but the convergence can not be proved in Peano arithmetic. There are no infinities involved, the sequence just grows very large but finite and always descends back to zero. However, you just need to add an axiom to allow transfinite ordinals, then the proof is simple!

So I lost my fascination, as it seemed just a clever game where you can find “mysteries” but you solve them by additional rules to cover the “mystery”

side note: I attended a public lecture at the Cambridge Newton Institute shortly after Andrew WIles had claimed a proof of FLT, the proof was still not verified. John Coates gave the lecture and at the end Stephen Hawking asked a question – “Does the proof use the axiom of choice?” – Poor John Coates was very uncomfortable giving an answer, he said no, it was all very straightforward constructions that didn’t employ AC. To be fair to professor Coates, the proof was not fully understood at the time, and Wiles had yet to provide the crucial Euler system to fix a big error. As it turns out, it is now accepted that the axiom of choice IS required in Wiles’ proof.

So how do people feel about a proof of FLT requiring a slightly “dodgy” (“unnatural”?) axiom – is that satisfactory? Should we require a proof in ZF alone (not ZFC)?

]]>In particular, it is natural to sharpen the question to

Which of the Millennium Prize problems can be stated as a postulate that can be falsified by a $\Pi^0_1$ counterexample?

There are two classes of answers.

The first class of answers accepts the problem statements in their present form: then if we further assume P≠NP, then the Riemann Hypothesis is the sole Millennium Prize problem that can be falsified by an $\Pi^0_1$ counterexample whose form can presently be envisioned.

The second class notes that Millennium Prize problem statements *can* be amended (at the discretion of the Scientific Advisory Board (SAB) of the Clay Mathematics Institute (CMI)).

Then the following question is (seemingly) entirely open

Can any of the Millennium Prize problem statements be reasonably amended — PvsNP in particular— so as to be stated as a postulate that can be falsified by a $\Pi^0_1$ counterexample?

Opinions vary widely in regard to the second question … this variation signifies a healthy and vigorous mathematical community (needless to say).

**Conclusion** It is reasonable to consider whether amended postulates associated to the Millennium Prize statement of the PvsNP problem might simultaneously evade proof obstructions *and* still address practical questions like “do there exist dynamical systems — including both physical systems and ciphers — that provably *cannot* be simulated/solved in with resources in P?”