🚀 go-pugleaf

The following is a compilation of two messages (with minor edition) I got
from A.C. Expert (not a real name) or, Professor Rubin (supposedly a real
name).  

-------forwarded message---------------------------------------
[1]
Date: Mon, 30 May 1994 09:14:28 -0500
From: hrubin@stat.purdue.edu (Herman Rubin)
Organization: Purdue University Statistics Department

In article <miha0008-290594232646@dialup-1-74.gw.umn.edu> you write:
>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?  

The "usual" method of proving that methods not assuming some form of
the Axiom of Choice are used is to do things in a formal model of set
theory without it.  The customary accepted models are Zermelo-Fraenkel
or von Neumann-Bernays-Godel, which are equivalent for set forms.

A detailed discussion of this can be found in our book, "Equivalents
of the Axiom of Choice" (or "Equivalents of the Axiom of Choice" II;
this is not an addendum but a revision).

If a function can be explicitly constructed, it does not require any
form of the Axiom of Choice.  But beware; most books "prove" that the
countable union of countable sets is countable; this proof uses a weak
form of the Axiom of Choice, and is not true without something non-
constructive.  But that the rational numbers, or the algebraic numbers,
or the set of well-formed formulas, is countable requires no such 
nasty process.

[2]
Date: Tue, 31 May 1994 07:55:51 -0500
From: hrubin@stat.purdue.edu (Herman Rubin)

The notion of constructive here is not that of the intuitionists; a 
finite number of choices can be made, and proofs by contradiction are
allowed.  And there are Cohen models in which the reals are a countable
union of countable sets.  There are other non-constructive forms weaker
than the axiom of choice; work is still being done on this.

-- 
Herman Rubin, Dept. of Statistics, Purdue Univ., West Lafayette
IN47907-1399
Phone: (317)494-6054
hrubin@stat.purdue.edu (Internet, bitnet)  
{purdue,pur-ee}!snap.stat!hrubin(UUCP)