> Just to remind collegues that the "proof that if ZF is consistent then ZFC
> is consistent" is carried out in ZF, by the method of inner models (Godel,
> 1939).
> AJ Franco Oliveira
In fact the proof can be carried out in much weaker systems than ZF, in
particular in PA (Peano Arithmetic).
Martin Davis