[FOM] The gold standard and FLT

[Arnon Avron]

Tim,
 
> When I publish a proof in algebraic combinatorics, am I supposed to
> make it clear whether I've used Replacement?  Weak Koenig's Lemma?
> Powerset?  Am I supposed to figure out whether my argument can be
> formalized in bounded arithmetic?

My answer here have two parts.

1) The question we were dealing with here was not what strength of induction
   (say) is used in the proof, but whether something stronger than
   ZFC is used here. For me personally, 
   ZFC itself, and even finite-order PA (in contrast
   to first-order PA) are also  too strong for accepting a full
   proof of something like FLT in them as  establishing the truth
   of the theorem in 100% certainty. However, I am in a minority here.  
   In contrast, I am pretty sure that  concerning going beyond ZFC 
   most of the mathematicians in the world feel like me.
   (They just usually do not know that the published alleged proof, 
   as is, at least  officially rely on assumptions that go beyond ZFC.)
   Your own story about the expert who sweared to you that
   that proof does not really go beyond ZFC is a good  demonstration
   of my point. Why did he feel the need to swear, and
   why did you ask him about it at the first place, if
   neither of you think that this point is important?

2) If you prove famous a open problem, of general interest
   to all mathematicians (and not only for them), like Goldbach
   conjecture, Riemann Hypothesis, or P not equal NP, then yes,
   you will have to find out and make it clear what
   are the assumptions that you rely on. It would be
   important to know whether the proof uses replacement,
   or powerset, or (to a lesser degree) the strength of
   the induction principles used in your proof. 

> You're conflating whether an argument is *rigorous* with whether an
> argument can be rewritten to use *weaker axioms than officially
> permitted*.  There are no "standard, eternal criteria" for which
> axioms can be used over the counter and which ones require a
> doctor's prescription.

It is you who is conflating arguments here. I did not say in my
previous messages anything about what are the permitted axioms.
My "standard, eternal criteria" was only the need to be clear about
what are the assumptions used in the proof. Once this is
clear, every mathematician can decide for herself/himself
to what extent s/he thinks the truth of the claim has
been established. I believe that  there are degrees of certainty here.
A valid proof in first-order PA provides 100% certainty
(for me, at least). A valid proof in MK (say) - much, much less.

Arnon