🚀 go-pugleaf

In article <miha0008-010694062507@dialup-3-144.gw.umn.edu> miha0008@gold.tc.umn.edu (H. Reiju Mihara) writes:

   >What I seem to need is a proof that ZF+~t is _inconsistent_.

  This means showing that t is a theorem of ZF. Of course if your
concern is with establishing that a proof of yours does not rely on
(any equivalent of) AC, you could in theory aim at formalizing the
proof to the point where you know that the formalization uses
predicate logic and some axioms of ZF. In practice this is hardly a
useful approach, since you will quickly grow tired of the lengthy and
error-prone business of formalization. The standard method is simply
to inspect the proof as it stands and note that there is no use of AC.
Of course, for this inspection to be reliable you must have given the
proof in sufficient detail, you must be aware of potentially
problematic areas of the proof, and you must know what is required to
prove any theorems that you invoke without proof. But the same is true if
you want to check a proof for validity. If your proof does contain
some implicit invocation of AC that you have overlooked, it will be
pointed out to you soon enough.