[FOM] Formalization Thesis: A second attempt

Timothy Y. Chow tchow at alum.mit.edu
Tue May 25 14:16:58 EDT 2010

```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
> 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
```