[FOM] Formalization Thesis: A second attempt

[Gyorgy Sereny]

On Sun, 23 May 2010, Daniel Mehkeri wrote:

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

The converse seems to be false. The simple reason is that even
the simplest and shortest potential candidate for being a 
`mathematically acceptable proof' of the original statement
corresponding to a formal proof of S might be completely
incomprehensible for a human being (e.g., it is too long or too
complex for us to grasp its meaning). In this case, the notion
of a `mathematically acceptable proof' cannot meaningfully
be applied to it.


Gyorgy Sereny