[FOM] Formalization Thesis: A second attempt
Daniel Méhkeri
dmehkeri at yahoo.ca
Sun May 23 13:03:24 EDT 2010
> 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
More information about the FOM
mailing list