🚀 go-pugleaf

In article <CqMrr5.MKp@eskimo.com>, jimwa@eskimo.com (Jim Walters) wrote:

> miha0008@gold.tc.umn.edu (H. Reiju Mihara) writes:

> >Can somebody out there tell me as intuitively as possible how to prove that
> >a proof is free from Zorn's lemma?  Is it difficult to prove that?  Give
 
> Well, there is the somewhat yucky method of proving the relative consistency
> of Theorem+~AC given the consistency of Theorem. On the bright side, you would
> be free to use AC in that proof at the meta level.

I feel a little uneasy when I hear "consistency of Theorem."  To be a bit
precise, let me first fix a consistent axiom system and call it ZF
(whatever it is).  I suppose that axiom of choice (AC) is independent of
ZF.  I guess the {consistency} of Theorem t means that ZF+t is consistent. 
Assuming t is a theorem of ZF+AC, this implies that ~t is not a theorem of
(i.e., cannot be proved from) ZF.  
(Proof.  Since t is a theorem of the consistent system ZF+AC, it follows
that ~t is not a theorem of ZF+AC; hence, ~t is not a theorem of ZF
(because otherwise ~t becomes theorem of ZF+AC).)

So, satisfying the "consistency of Theorem" seems easy, as far as we are
interested in propositions provable from ZF+AC.  Suppose the "consitency of
Theorem t."  The above quotation says that there is a method to prove the
"relative consintency" of t+~AC.  I wonder whether under the assumption of
the consistency of t, the relative constency means the _consistency_ of
t+~AC.  Suppose so.  Then what can I get from the _consistency_ of t+~AC? 
I'm not sure what I can get.  All I can figure out (applying what is proved
in the previous paragraph) is that "t --> AC" is not a theorem of ZF, that
is, it cannot be proved that "t --> AC" from ZF.  This conclusion is not so
interesting for my purpose.  (In fact, let t= ~AC and see what happens.)

What I seem to need is a proof that ZF+~t is _inconsistent_.  If that is
the case, then t is provable from ZF by redutio ad absurdum.  
(Conversely, I propose that if t is provable from ZF, then ZF+~t is
inconsistent.  {Proof}. (?)  Suppose t is a theorem of ZF.  Then both t and
~t are theorems of ZF+~t.  Hence, ZF+~t is inconsistent.)  To show
inconsistency in a confident manner, maybe I have to work in a formal model
of set theory without AC, as Professor Rubin says.

Reiju
-- 
\\                                          //
  H. Reiju Mihara (miha0008@gold.tc.umn.edu) 
  is a name    of some sort 
                               of individual
//                                          \\