FOM: reply to McLarty

[Harvey Friedman]

Reply to McLarty 5:16PM 3/3/99:

>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)"

Yes. More specifically, EFA proves:

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

>But if EFA proves both those inset quoted
>statements, then it seems that EFA proves
>
>         "ZFC proves Consis(ZFC)"

No.
>
>Do you mean to say that EFA does prove:
>
>        "ZFC proves Consis(ZFC)"?

No.