[FOM] Formalization Thesis: A second attempt

[Daniel Méhkeri]

>  Given any precise mathematical statement, one can exhibit a formal 
>  sentence S in the first-order language of set theory with the 
>  property that any mathematically acceptable proof of the original 
>  mathematical statement can be mimicked to produce a formal proof of
>  S from the axioms of ZFC.
>
> As I said in my original FOM post, my focus is not so much on ZFC 
> particularly; that is, I will not quibble with someone who wishes to 
> replace "ZFC" with another system that is somewhat weaker or stronger.
>
> As you can see, I have avoided the problematic term "faithfully 
> expressed" that generated so many objections previously.  My question 
> now is, does anybody here disagree with the Formalization Thesis as 
> stated above?  

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.

Regards,
Daniel