[FOM] A proof that cannot be formalized in ZFC

[Kenny Easwaran]

I think the step that causes problems is the following:

> By translating this proof
> from the formal language of ZFC into English (that is, by applying
> the standard interpretation), we get a proof -- a mathematical proof
> in the everyday sense -- that ZFC has no model, contrary to the
> assumption that ZFC is consistent.

This step assumes that a formal proof in ZFC can be translated into "a
mathematical proof in the everyday sense" - but this is only correct
if ZFC is in fact true.

A related sort of reasoning is to argue that if a theory is true, then
it is consistent.  This is clearly correct (assuming that
paraconsistent logicians are wrong), but (by Godel's 2nd
incompleteness theorem) it is definitely not entailed by ZFC, or any
extension of it.

Best,
Kenny Easwaran

On 10/5/07, Finnur Larusson <finnur.larusson at adelaide.edu.au> wrote:
>
> Dear FOM members,
>
> I am a mathematician with a layman's interest in logic and
> foundations.  I would be grateful if someone who knows more than I do
> would tell me whether the following remarks make sense -- or have I
> perhaps rediscovered a well-known fallacy?
>
> Let con(ZFC) be a sentence in ZFC asserting that ZFC has a model.
> Let S be the theory ZFC+con(ZFC).  Let con(S) be a sentence in S (or
> ZFC) asserting that S has a model.  We assume throughout that ZFC is
> consistent.
>
> Claim 1.  S is consistent.
>
> Proof.  Assume S is inconsistent, that is, has no model.  This means
> that there is no model of ZFC in which con(ZFC) is true, so the
> negation of con(ZFC) has a proof in ZFC.  By translating this proof
> from the formal language of ZFC into English (that is, by applying
> the standard interpretation), we get a proof -- a mathematical proof
> in the everyday sense -- that ZFC has no model, contrary to the
> assumption that ZFC is consistent.
>
> Claim 2.  There is no proof in ZFC that con(ZFC) implies con(S).
>
> Proof.  By Claim 1 and Godel's Second Incompleteness Theorem applied
> to S, con(S) is unprovable in S.
>
> Thus we seem to have a down-to-earth mathematical statement ("If ZFC
> is consistent, so is S") with a proof that, provably, cannot be
> formalized in ZFC.  This appears to contradict the common belief that
> all mathematics can be formalized in ZFC.  Is my argument correct?
> If so, it must be well known -- are there other such examples?  If
> not, where is the mistake?
>
> Thanks and best regards,
> Finnur Larusson
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>