FOM: questions to Friedman

[Colin McLarty]

Harvey Friedman 3 Mar 1999 15:20:21 answered my question
>
>>        "For every T, if T is a finitely axiomatized fragment of ZFC,
>>        then ZFC proves Consis(T)"
>>
>>Do you claim this statement is provable in EFA?

by saying

>Yes.

I may well misunderstand something. It has happened. But if you could answer
some questions for me it will help me see where I am wrong, if indeed I am.
Does EFA also prove the following?

        "If ZFC proves [Consis(T) for every finitely axiomatized 
        fragment of ZFC], then ZFC proves Consis(ZFC)"

I believe it does, since EFA proves: "Each proof in ZFC is a proof in some
finitely axiomatized fragment". But if EFA proves both those inset quoted
statements, then it seems that EFA proves

         "ZFC proves Consis(ZFC)"

Is this last step of mine wrong? I would be surprized since modus ponens
adds no real complexity.

Do you mean to say that EFA does prove:

        "ZFC proves Consis(ZFC)"?