[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
[mizar] Re: AC and strongly inaccessible cardinals
This letter is in response to two letters ([Trybulec1] and
[Trybulec2]) of Professor Trybulec to the Mizar mailing list. These
letters discuss two papers ([Tarski1] and [Tarski2]) of Alfred
Tarski. (Precise cites to the two Trybulec letters and to the papers
of Tarski appear in the references at the end of this letter.) Since
the discussion of the points raised in these letters originated on the
FOM mailing list, and the topics seem of interest to that list, I am
also ccing my letter to the FOM mailing list.
Let me begin by summarizing the points of Professor Trybulec's letter
with which I disagree:
1) ZF + "there are arbitrarily large universes" implies the Axiom of
Choice.
2) ZF + "there are arbitrarily large inaccessible cardinals" implies
the axiom of choice.
Actually the situation with 2) is somewhat delicate. With the
"correct" definition of "strongly inaccessible cardinal" this claim
is definitely wrong. However, with the definition of strongly
inaccessible cardinal" used in Mizar, it is true that the existence
of a proper class of strongly inaccessible casrdinals entails the
axiom of choice. The proof, however, does not go via Tarski's
work. It makes essential use of the Axiom of Foundation which plays
no essential role in Tarski's work.
3) The proofs of Urban (in the Mizar article CARD_LAR (cf. THEOREM
37) are relevant to this topic.
Unfortunately for the topic under discussion, the whole treatment
of cardinals in Mizar relies on the axiom of choice. In particular,
the proof of the cited theorem makes essential use of the axiom of
choice.
(Professor Trybulec's suggestion that this theorem might be
relevant was put forth tentatively. I just want to record that it
is definitely *not* relevant.)
DEFINITIONS
First, work in ZFC, Then we can identify cardinals with initial
ordinals. (An initial ordinal is an ordinal which is not equipotent
with any smaller ordinal.)
A cardinal kappa is **strongly inaccessible** if:
1) It is uncountable;
2) It is regular;
3) For every cardinal lambda < kappa, the power set of lambda has
cardinal less than kappa.
I remark that this definittion (which is standard) is not the one
used in the Mizar Mathematical Library (MML). They replace 1) by
1') It is infinite.
Now two definitions which are provably equivalent in ZFC might not
be provably equivalent in the weaker theory ZF. The paper [Blass]
shows that this indeed happens with the notion of "inaccessible
cardinal". The paper [Blass] considers four different variants of
the notion (and proves by constructing suitable models that they
all difer. Two of them are relevant for our present purposes.
Work in ZF:
A cardinal (initial ordinal) kappa is **i-inaccessible** if:
1) It is uncountable;
2) It is regular;
3) If lambda is an initial ordinal less than kappa, then the power
set of lambda is well-orderable, and equipotent with some ordinal
less than kappa.
Notice that clause 3) of this definition has a lot of choice
smuggled in. For example, it is immediately clear (in ZF) that if
there is an i-strongly inaccessible cardinal, then the reals are
well-ordered. (Take lambda = aleph_0.)
The second notion is that of **v-inaccessible cardinal**. Following
[Blass] we give two variantions of the definition. (We refer to
[Blass] for the proof that they are equivalent.)
The two variations start the same way. To be v-inaccessible, kappa
must be an initial ordinal.
In the first variation of the definition, kappa is v-strongly
inaccessible iff V_kappa (the collection of sets of rank less than
kappa) is a model of "second-order ZF). (Basically, in the two
schemes of ZF ("replacement" and "selection") there is one instance
of the scheme for every subset of V_kappa.)
Here is the second definition of v-inaccessible:
An initial ordinal, kappa, is v-inaccessible if it is:
1) Uncountable;
2) Regular;
3) Whenever alpha is less than kappa, there is no function which
maps V_alpha (the set of sets of rank less than alpha) onto kappa.
Next we recall the definition of a Grothendieck universe. Good
references for this concept are [G1] and [G2].
A Grothendieck universe is a set U such that:
1) U is transitive;
2) If x, y are in U, so is {x,y};
3) If x is in U, the power set of x, P(x), is in U;
4) If x is in U, union(x) is in U;
5) If A is a subset of U, I is a member of U, and there is a
surjective map of I onto A, then A is in U.
The terminology of a "Tarski class" comes from Mizar (Cf. CLASSES1:
def 2). The concept is implicit in Tarski's Axiom A which we will
discuss in a moment.
U is a Tarski class iff:
1) If A is in U and B is a subset of A, then B is in U;
2) If A is in U, then P(A) is in U;
3) If A is a subset of U, and A is not equipotent with U, then A
is in U.
Tarsi proves in [Tarski2] that every Tarski class is
well-orderable. The proof can be carried out in Zermelo set theory
without use of the axioms of foundation or choice.
There are trivial examples of the notion of "Grothendieck universe"
and "Tarski class". For example, the empty set is an example of
both of these concepts. So is the collection V_omega of all
hereditarily finite sets. We say that a Grothendieck universe or
Tarski class is non-trivial if it has an infinite member.
There are close connections between the various concepts we have
introduced. (The following assertions are all provable in ZF.) If
kappa is a v-inaccessible cardinal, then V_kappa is a non-trivial
Grothendieck universe. Conversely, if U is a non-trivial
Grothendieck universe, then the set of ordinals in U is a
v-inaccessible cardinal. Every i-inaccesible cardinal is
v-inaccessible. But the converse does not hold (as is shown in
[Blass] Theorem 17.) If U is a non-trivial Tarski class, then the
set of ordinals in U is i-inaccessible. Let I be the proposition
that there is a strongly inaccessible cardinal. We will sketch
presently the proof that if ZFC + I is consistent, then there is a
model of ZF in which there is an i-inaccessible, kappa, such that
V_kappa is not a Tarski class.
Neither of the notions of non-trivial Grothendieck universe or
non-trivial Tarski class implies the other. It is easy to construct
examples of Tarski classes (whose set of ordinals is strongly
inaccessible) that are not transitive. (The construction needs a
strongly inaccessible cardinal as input, of course.) And our
Example I (below) will give a non-trivial Grothendieck universe
which is not well-orderable and hence not a Tarski class.
TARSKI-GROTHENDIECK SET THEORY
Here are three axiomitizations of the same theory (= set of
theorems):
1) ZFC + "For every ordinal lambda, there is a strongly inaccessible
cardinal kappa with kappa > lambda."
2) ZFC + "Every set x is a member of a Grothendieck universe U".
3) ZFC + "Every set xis a member of some Tarski class".
Tarski's axiom A is the assertion that every set x is a member os
some Tarski class. (The term "Tarski class" is not used by Tarski.)
Tarski remarks that in the presence of axiom A many of the axioms
of ZFC become redundent. Indeed, we can get the same theory with
the following axioms:
Extensionality, Foundation, Null Set, Pair Set, Replacement, Union,
and Axiom A.
AXIOM A AND THE AXIOM of CHOICE
What Tarski proves (cf. Corollary 7 of [Tarski2]) is the
following. (The proof can easily be formalized in Zermelo set
theory without use of the axioms of choice or foundation.)
Let X be a set. Let S be { Y | Y is a subset of X of cardinality
less than X}, Then if S is equipotent with X, then X is
well-orderable.
For the application to Axiom A, we can get by with the following
weaker result:
Let X be a set. Suppose that every subset Y of X is either a member
of X or equipotent with X. Then X is well-orderable.
As Trybulec remarks, this weaker result has a somewhat easier
proof. I first sketch the proof in ZF and then remark how the proof
can be compressed into Zermelo set theory without the axiom of
Foundation.
Let X be as above. Let W be the set of all z such that:
1) z is an ordinal;
2) z is a subset of X;
3) z is not equipotent with X.
Clearly, W is an initial segment of the ordinals and hence an
ordinal. By our hypothesis on X, W is a subset of X. If W is not
equipotent with X, then W is a member of W (which contradicts
Foundation).
So W *is* equipotent with X and hence X is well-orderable.
To carry out this proof without the use of the axioms of
Replacement and Foundation (though with the axiom of Separation) we
proceed as follows. We define an ordinal as a transitive set which
is well-ordered by epsilon. Since we don't have the axiom of
replacement, we can't prove that every well-ordered set is
isomorphic to an ordinal. But our argument never used that. To
deduce a contradiction from "W is a member of W" we proceed as
follows: Since epsilon well-orders W, for every member x of W we
have not (x epsilon x). So if W in W, this remark applies to W and
W is not a member of W. Contradiction!
FIRST EXAMPLE:
We give a model of ZF + "Every set is a member of Grothendieck
universe" + "The reals are not well-orderable". Our example is a
slight variant of the model used in [Blass] to prove their Theorem
17.
Start with a transitive countable model M of ZFC + V = L + "There
are arbitrarily large inaccessible cardinals". Force to adjoin a
single generic subset of omega , x, to M, getting M[x].
It is well-known that we can find a model N such that M \subset N
\subset M[x] and the reals of N are not well-orderd. (One way to do
this is as follows. For i in omega, let x_i be the set of j such
that 2^i3^j is in x. Let b = {x_i: i in omega}. Then take N to be
the smallest transitive model of ZF which contains b and all the
ordinals of M.
It is easy to verify that if kappa is inaccessible in M, then
V_kappa (as computed in N) is a Grothendieck universe. The details
can be found in [Blass] in the proof of their Theorem 17.
Note that in this model, if kappa is v-inaccessible in M, then it is
so in M[x] as well and hence also in N.
ARBITRAILY LARGE i-INACCESSIBLES
We next wish to explain why ZF + "There are arbitraily large
i-inaccessibles" proves the axiom of choice.
The key result is the following which is established during the
proof of Theorem 11 of [Blass]:
Let kappa be i-inaccessible. Let alpha be an ordinal less than
kappa. Then V_alpha is well-orderable.
From this it follows immediately that if there are arbitraily large
i-inaccessibles then every V_alpha is well-orderable. Hence (using
the Axiom of Foundation) every set is well-orderable and AC
follows.
WHY v-INACCESSIBLE IS THE RIGHT FORMULATION OF "STRONGLY
INACCESSIBLE" IN tHE ABSENCE OF ChOICE
1) The concept of i-inaccessilbe has a lot of choice built
in. Cf. That if kappa is i-inaccessible, then for every alpha
less than kappa, V_alpha is well-orderable.
2) In the absence of choice, the connection between universes and
inaccessibles is preserved if we use v-inaccessibles but not if
we use i-inaccessibles.
3) If M is a transitive class model of ZFC and N is a transitive
inner model of ZF with N \subset M, then if kappa is
inaccessible in M, kappa is v-inaccessilbe in N (but as Example
1 shows) need not be i-inaccessible.
EXAMPLE 2
This is a model of all the axioms of ZF (except the axiom of
Foundation) in which the axiom of choice fails but there are
arbitraily large i-inaccessilbe cardinals.
Basically the model is a variant of the simplest Fraenkel-Mostowski
model where one adjoins a set of individials which is an amorphous
set without a well-ordering. In order to have extensionality our
individuals will be sets x such that x = {x}. (Of course,
foundation must fail.)
The starting model M from which we do this variant of the FM
construction will be a model of ZFC + V = L + "There are arbitraily
large inaccessible cardinals". The well-founded sets of the resulting
FM model are just our starting model M. In particular, the
inaccessible cardinals in our original model remain i-inaccessible in
our final model.
This example is important since it shows that the reason that a proper
class of i-inaccessibles yields choice has nothing to do with Tarski's
results. For, as noted previously, Tarski's proofs make no essential
use of the Axiom of Foundation.
EXAMPLE 3
The following theorem is proved in the Mizar Mathematical Library.
theorem :: CARD_LAR:37
M is strongly_inaccessible implies Rank M is being_Tarski-Class;
The question is raised whether this proof needs the axiom of
choice. We shall sketch an example which shows that it must.
Later, we shall point out the precise place in the Mizar proof where
the axiom of choice is used.
We start with a model M of ZFC + V = L + "There is precisely one
inaccessible cardinal, kappa."
We do an Easton style forcing adjoining for each infinite regular
cardinal lambda < kappa lambda^+ generic subsets of lambda. (Here
lambda^+ is the least cardinal greater than lambda.) Call the
resulting model M_1. M_1 is a model of ZFC + GCH and kappa remains
inaccessible in M_1.
Our desired model, N will be an inner model of M_1. Before
describing it we need to establish some notation. Let A(lamda, eta)
be the eta^th generic subset of lambda adjoined in our forcing
extension. (So A(lambda,eta) is defined for lambda an infinite
regular cardinal less than kappa and eta < lambda^+.)
Let X be the set of infinite regular cardinals less than kappa.
For lambda in X, let B(lambda) = {A(lambda, eta) | eta < lambda^+}.
So B is a function with domain X.
Let W be the set V_kappa, as computed in M_1.
We can now describe the model N. It is the smallest inner model (of
ZF) of M_1 containing all the ordinals of M_1, as well as the sets W
and B.
Here are some properties of N:
1) In N, kappa is i-inaccessible.
(This follows easily from the facts that kappa is inaccessible
in M_1 and that W is an element of N.)
2) In N, there is no choice function h with domain X such that
h(lambda) is a member of B(lambda) for all lambda in X.
This is proved by a standard symmetry argument using the
group of automorphisms of the forcing conditions used to
obtain M_1 from M.
3) In N, V_kappa = W.
(This is clear.)
4) In N, V_kappa is not well-orderable
This follows immediately from 2).
5) In N, V_kappa is not a Tarski class.
This is immediate from 4) since every Tarski class is
well-orderable.
DELVING INTO THE MIZAR MML
In this last section I want to nail down two points. Example 3
shows that the proof of Theorem 37 of CARD_LAR must make
essential use of the axiom of choice. I want to track down
where this usage occurs.
Second, I want to unpack the definition of strongly
inaccessible in Mizar and show it amounts to "i-inaccessible or
equal to aleph_0".
Let's turn to the first task. The proof of CARD_LAR:37 appeals
to CARD_LAR:36 in the justification of the proof of claim A4.
In the proof of CARD_LAR:36 appeal is made to CARD_3:62 in the
proof of claim A9.
In the proof of CARD_3:62 appeal is made to WELLORD2:26 in the
proof of claim A6.
But WELLORD2:26 simply asserts that every set can be
well-ordered which is well known to be an equivalent of the
axiom of choice.
Finally, here are the cites for the Mizar definition of
"strongly inaccessible cardinal".
The definition of "cardinal" and of "the cardinal of a set X"
are give in the article CARD_1 and are thoroughly based on the
axiom of choice. A cardinal is defined as an ordinal which is
not equipotent with any smaller ordinal. The cardinal of a set
X is defined as the least ordinal equipotent with X. (That
there is an ordinal equipotent with any set X, requires the
well-ordering theorem or euivalently, the axiom of choice.)
Cardinal exponetiation (the notation is exp(M,N)) is defined in
the familiar way in CARD_2 as the cardinal number of the set
of functions which map N to M.
The definition of "strongly inaccessible cardinal" is given in
the article CARD_FIL. First an inaccessible cardinal is
defined as an infinite cardinal which is regular and a limit
cardinal. (The definition of "limit cardinal" is tweaked so
that aleph_0 is a limit cardinal.
The definition of strongly inaccessible cardinal kappa is an
inaccessible cardinal such that for any cardinal N < kappa, we
have exp(2, N) < kappa. As I said, this is almost the
defintion of an i-inaccessible cardinal. However, the
definitions are tweaked so that a strongly inaccessible
cardinal (in the sense of Mizar) is either aleph_0 or an
i-inaccessible cardinal.
REFERENCES
Before giving the list of references, I need to explain how I will
indicate abbreviated URLs. The problem I am trying to get around is
that some web addresses (notably aol.com) reject any letters that
contain urls from shurl.net.
I use the notation [7Su] to denote the URL obtained from the following
string:
#http#:#//#shurl#.#net#/#7Su#
by deleting every occurrence of the hash character (#).
Of course, similar unpacking will get the url associated to
e. g. [7Sv].
[Blass]
Andreas Blass, Ioanna M. Dimitriou, Benedikt L\"{o}we
Inaccessible Cardinals without the Axiom of Choice
Fundamenta Mathematicae, vol. 194(2007), pp. 179-189.
This paper appears on the web at the URL
http://dare.uva.nl/document/25381
OR
[6QG]
[G1]
This is the Wikipedia article on Grothendieck universes:
http://en.wikipedia.org/wiki/Grothendieck_universe
OR
[6QF]
[G2]
This is some notes of N. Bourbaki on Grothendieck universes in an
appendix (Appendix II) to SGA 4 Expose I.
http://modular.fas.harvard.edu/sga/sga/4-1/4-1t_185.html
OR
[8w8]
[Tarski1]
Alfred Tarski
Ueber unerreichbare Kardinalzahlen,
Fundamenta Mathematicae, vol.30 (1938), pp.68-89.
This paper appears on the web at the URL
http://matwbn.icm.edu.pl/ksiazki/fm/fm30/fm30113.pdf
OR
[7Wd]
[Tarski2]
Alfred Tarski
On Well-ordered Subsets of any Set,
Fundamenta Mathematicae, vol.32 (1939), pp.176-183
http://matwbn.icm.edu.pl/ksiazki/fm/fm32/fm32115.pdf
OR
[7We]
[Trybulec1]
Posting January 12, 2008 04:35 of Andrzej Trybulec to Mizar-Forum
http://permalink.gmane.org/gmane.comp.mathematics.mizar/825
OR
[7Wm]
[Trybulec2]
Posting January 12, 2008 05:00 of Andrzej Trybulec to Mizar-Forum
http://permalink.gmane.org/gmane.comp.mathematics.mizar/826
OR
[7Wo]
[Urban]
Posting January 12, 2008 09:17 of Josef Urban to Mizar-Forum
http://permalink.gmane.org/gmane.comp.mathematics.mizar/827
OR
[7Wq]