[FOM] Formalization Thesis: A second attempt

[Timothy Y. Chow]

Daniel Mehkeri wrote:
> I agree with the thesis, but what about its converse?
> 
>   ... any formal proof of S from the axioms of ZFC(+/-) corresponds 
>   to a mathematically acceptable proof of the original statement.
> 
> The thesis and its converse are separately plausible. But a single 
> system that comprises EXACTLY the acceptable proofs is much less 
> plausible. Your argument about the success of formalisation only
> applies to the forward direction. In fact by allowing a +/- on ZFC 
> you basically admit that there is no such system, which should be
> unique up to proof-theoretic reduction. The converse is false.
> 
> The thesis plus the negation of its converse means that ZFC(+/-) 
> produces proofs that aren't always acceptable. That's fine by me, but 
> probably not what you meant to imply. Among other things it doesn't 
> suit your purposes: Con(ZFC(+/-)) is then the wrong proposition.

I don't think these observations cause any real problems.  My goal is to 
explain why Goedel's 2nd theorem is relevant to Hilbert's program.  [Note 
to Sazonov: Of course, all this was figured out long ago and I am not 
offering anything "new" in the sense of original philosophical or 
mathematical research; what is perhaps "new" is the particular 
*pedagogical* idea of giving the Formalization Thesis a name.  If you 
think there is no need to come up with a better way to explain these 
concepts to the non-specialist then I suspect you have not spent much time 
lately trying to do so.]  So it's not a problem, from my perspective, to 
grant tentatively the possibility that ZFC (say) comprises EXACTLY the 
acceptable proofs.  In fact, I daresay that a sizable fraction of my 
intended audience DOES think something like that, although they may not 
have articulated it explicitly.  If the conversation ever gets to the 
point where my audience understands the points you're making here then the 
battle is already won and the war has moved on to a different arena.

Tim