Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000 Association of Mizar Users

### Basic Facts about Inaccessible and Measurable Cardinals

by
Josef Urban

MML identifier: CARD_FIL
[ Mizar article, MML identifier index ]

```environ

vocabulary ORDINAL1, ORDINAL2, BOOLE, FINSET_1, CARD_1, CARD_5, SETFAM_1,
FILTER_0, SUBSET_1, FILTER_2, TARSKI, WAYBEL_0, ZFMISC_1, CARD_2,
FUNCT_1, RELAT_1, WAYBEL11, FUNCT_2, CARD_3, PRALG_1, FUNCT_5, CARD_FIL,
HAHNBAN;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PRALG_1,
BINOP_1, FUNCT_5, SETFAM_1, FINSET_1, ORDINAL1, FUNCT_2, ORDINAL2,
CARD_1, CARD_2, CARD_3, CARD_5;
constructors XREAL_0, WELLORD2, BINOP_1, PRALG_1, CARD_2, CARD_5, ZFREFLE1,
XCMPLX_0, MEMBERED;
clusters FUNCT_1, ORDINAL1, CARD_1, CARD_5, RELSET_1, FINSET_1, SUBSET_1,
PRALG_1, SETFAM_1, MEMBERED, NUMBERS, ORDINAL2;
requirements NUMERALS, SUBSET, BOOLE;

begin

:: this should be in ordinal2
definition
cluster being_limit_ordinal Ordinal;
end;

definition let X,Y be set;
redefine func X \ Y -> Subset of X;
end;

theorem :: CARD_FIL:1
for x being set for X being infinite set holds Card {x} <` Card X;

definition let X be infinite set;
cluster Card X -> infinite;
end;

scheme ElemProp{D()-> non empty set,x()->set,P[set]}:
P[x()]
provided  x() in {y where y is Element of D(): P[y]};

::::::::::::::::::::::   Initial reservations   :::::::::::::::::::::

reserve N for Cardinal;
reserve M for Aleph;
reserve X for non empty set;
reserve Y,Z,Z1,Z2,Y1,Y2,Y3,Y4 for Subset of X;
reserve S for Subset-Family of X;
reserve x for set;

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::                                                                 ::
::         Necessary facts about filters and ideals on sets        ::
::                                                                 ::
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

theorem :: CARD_FIL:2
{ X } is non empty Subset-Family of X & not {} in { X } &
for Y1,Y2 holds (Y1 in { X } & Y2 in { X } implies Y1 /\ Y2 in { X }) &
((Y1 in { X } & Y1 c= Y2) implies Y2 in { X });

definition let X;
mode Filter of X -> non empty Subset-Family of X means
:: CARD_FIL:def 1
(not {} in it) &
for Y1,Y2 holds (Y1 in it & Y2 in it implies Y1 /\ Y2 in it) &
((Y1 in it & Y1 c= Y2) implies Y2 in it);
end;

theorem :: CARD_FIL:3
for F being set holds F is Filter of X iff
(F is non empty Subset-Family of X &
not {} in F &
for Y1,Y2 holds (Y1 in F & Y2 in F implies Y1 /\ Y2 in F) &
((Y1 in F & Y1 c= Y2) implies Y2 in F));

theorem :: CARD_FIL:4
{ X } is Filter of X;

reserve F,Uf for Filter of X;

theorem :: CARD_FIL:5
X in F;

theorem :: CARD_FIL:6
Y in F implies not (X \ Y) in F;

theorem :: CARD_FIL:7
for I being non empty Subset of bool X st (for Y holds Y in I iff Y` in F)
holds (not X in I) &
for Y1,Y2 holds (Y1 in I & Y2 in I implies Y1 \/ Y2 in I) &
((Y1 in I & Y2 c= Y1) implies Y2 in I);

definition
let X,S;
redefine func COMPLEMENT S;
synonym dual S;
end;

reserve S for non empty Subset-Family of X;

definition let X,S;
cluster COMPLEMENT S -> non empty;
end;

theorem :: CARD_FIL:8
dual S = {Y:Y` in S};

theorem :: CARD_FIL:9
dual S = {Y`:Y in S};

definition let X;
mode Ideal of X -> non empty Subset-Family of X means
:: CARD_FIL:def 2
(not X in it) &
for Y1,Y2 holds (Y1 in it & Y2 in it implies Y1 \/ Y2 in it) &
((Y1 in it & Y2 c= Y1) implies Y2 in it);
end;

definition let X,F;
redefine func dual F -> Ideal of X;
end;

reserve I for Ideal of X;

theorem :: CARD_FIL:10
(for Y holds not (Y in F & Y in dual F)) &
(for Y holds not (Y in I & Y in dual I));

theorem :: CARD_FIL:11
{} in I;

definition let X,N,S;
pred S is_multiplicative_with N means
:: CARD_FIL:def 3
for S1 being non empty set st
(S1 c= S & Card S1 <` N) holds meet S1 in S;
end;

definition let X,N,S;
:: CARD_FIL:def 4
for S1 being non empty set st
(S1 c= S & Card S1 <` N) holds union S1 in S;
end;

definition let X,N,F;
redefine pred F is_multiplicative_with N;
synonym F is_complete_with N;
end;

definition let X,N,I;
synonym I is_complete_with N;
end;

theorem :: CARD_FIL:12
S is_multiplicative_with N implies dual S is_additive_with N;

definition let X,F;
attr F is uniform means
:: CARD_FIL:def 5
for Y holds Y in F implies Card Y = Card X;
attr F is principal means
:: CARD_FIL:def 6
ex Y st Y in F & ( for Z holds Z in F implies Y c= Z);
attr F is being_ultrafilter means
:: CARD_FIL:def 7
for Y holds Y in F or (X \ Y) in F;
end;

definition let X,F,Z;
func Extend_Filter(F,Z) -> non empty Subset-Family of X equals
:: CARD_FIL:def 8
{Y: ex Y2 st (Y2 in {Y1 /\ Z : Y1 in F} & Y2 c= Y)};
end;

theorem :: CARD_FIL:13
for Z1 holds ( Z1 in Extend_Filter(F,Z) iff ex Z2 st Z2 in F & Z2 /\ Z c= Z1)
;

theorem :: CARD_FIL:14
(for Y1 st Y1 in F holds Y1 meets Z) implies ( Z in Extend_Filter(F,Z) &
Extend_Filter(F,Z) is Filter of X & F c= Extend_Filter(F,Z) );

reserve S,S1 for Subset of bool X;

definition let X;
func Filters(X) -> non empty Subset-Family of bool X equals
:: CARD_FIL:def 9
{S where S is Subset of bool X : S is Filter of X};
end;

theorem :: CARD_FIL:15
for S being set holds S in Filters(X) iff S is Filter of X;

reserve FS for non empty Subset of Filters(X);

theorem :: CARD_FIL:16
FS is c=-linear implies union FS is Filter of X;

theorem :: CARD_FIL:17
for F ex Uf st F c= Uf & Uf is being_ultrafilter;

reserve X for infinite set;
reserve Y,Y1,Y2,Z for Subset of X;
reserve F,Uf for Filter of X;

definition let X;
func Frechet_Filter(X) -> Filter of X equals
:: CARD_FIL:def 10
{ Y :  Card (X \ Y) <` Card X};
end;

definition let X;
func Frechet_Ideal(X) -> Ideal of X equals
:: CARD_FIL:def 11
dual Frechet_Filter(X);
end;

theorem :: CARD_FIL:18
Y in Frechet_Filter(X) iff Card (X \ Y) <` Card X;

theorem :: CARD_FIL:19
Y in Frechet_Ideal(X) iff Card Y <` Card X;

theorem :: CARD_FIL:20
Frechet_Filter(X) c= F implies F is uniform;

theorem :: CARD_FIL:21
Uf is uniform being_ultrafilter implies Frechet_Filter(X) c= Uf;

definition let X;
cluster non principal being_ultrafilter Filter of X;
end;

definition let X;
cluster uniform being_ultrafilter -> non principal Filter of X;
end;

theorem :: CARD_FIL:22
for F being being_ultrafilter Filter of X for Y holds
Y in F iff not Y in dual F;

reserve x for Element of X;

theorem :: CARD_FIL:23
F is non principal being_ultrafilter & F is_complete_with Card X
implies F is uniform;

begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::                                                                       ::
::            Inaccessible and measurable cardinals, Ulam matrix         ::
::                                                                       ::
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

theorem :: CARD_FIL:24
nextcard N <=` exp(2,N);

definition
pred GCH means
:: CARD_FIL:def 12
for N being Aleph holds nextcard N = exp(2,N);
end;

definition let IT be Aleph;
attr IT is inaccessible means
:: CARD_FIL:def 13
IT is regular limit;
synonym IT is_inaccessible_cardinal;
end;

definition
cluster inaccessible -> regular limit Aleph;
end;

theorem :: CARD_FIL:25
alef 0 is inaccessible;

definition let IT be Aleph;
attr IT is strong_limit means
:: CARD_FIL:def 14
for N st N <` IT holds exp(2,N) <` IT;
synonym IT is_strong_limit_cardinal;
end;

theorem :: CARD_FIL:26
alef 0 is strong_limit;

theorem :: CARD_FIL:27
M is strong_limit implies M is limit;

definition
cluster strong_limit -> limit Aleph;
end;

theorem :: CARD_FIL:28
GCH implies (M is limit implies M is strong_limit);

definition let IT be Aleph;
attr IT is strongly_inaccessible means
:: CARD_FIL:def 15
IT is regular strong_limit;
synonym IT is_strongly_inaccessible_cardinal;
end;

definition
cluster strongly_inaccessible -> regular strong_limit Aleph;
end;

theorem :: CARD_FIL:29
alef 0 is strongly_inaccessible;

theorem :: CARD_FIL:30
M is strongly_inaccessible implies M is inaccessible;

definition
cluster strongly_inaccessible -> inaccessible Aleph;
end;

theorem :: CARD_FIL:31
GCH implies ( M is inaccessible implies M is strongly_inaccessible);

definition let M;
attr M is measurable means
:: CARD_FIL:def 16
ex Uf being Filter of M st Uf is_complete_with M
& Uf is non principal being_ultrafilter;
synonym M is_measurable_cardinal;
end;

theorem :: CARD_FIL:32
for A being being_limit_ordinal Ordinal for X being set st
X c= A holds sup X = A implies union X = A;

theorem :: CARD_FIL:33
M is measurable implies M is regular;

definition let M;
cluster nextcard M -> non limit;
end;

definition
cluster non limit infinite Cardinal;
end;

definition
cluster non limit -> regular Aleph;
end;

definition
let M be non limit Cardinal;
func predecessor M -> Cardinal means
:: CARD_FIL:def 17
M = nextcard it;
end;

definition
let M be non limit Aleph;
cluster predecessor M -> infinite;
end;

definition  :: infinite matrix
let X be set;
let N,N1 be Cardinal;
mode Inf_Matrix of N,N1,X is Function of [:N,N1:],X;
end;

reserve X for set;
reserve M for non limit Aleph;
reserve F for Filter of M;
reserve N1,N2,N3 for Element of predecessor M;
reserve K1,K2 for Element of M;
reserve T for Inf_Matrix of predecessor M , M, bool M;

definition   :: Ulam matrix on nextcard N;
let M,T;
pred T is_Ulam_Matrix_of M means
:: CARD_FIL:def 18

(for N1,K1,K2 holds K1<>K2 implies T.(N1,K1) /\ T.(N1,K2) is empty ) &
(for K1,N1,N2 holds N1<>N2 implies T.(N1,K1) /\ T.(N2,K1) is empty ) &
(for N1 holds Card (M \ union {T.(N1,K1): K1 in M}) <=` predecessor M ) &
(for K1 holds Card (M \ union {T.(N1,K1): N1 in predecessor M}) <=`
predecessor M );
end;

:: this is pretty long
theorem :: CARD_FIL:34
ex T st T is_Ulam_Matrix_of M;

:: also a little longer
theorem :: CARD_FIL:35
for M for I being Ideal of M st
(I is_complete_with M & Frechet_Ideal(M) c= I)
ex S being Subset-Family of M st
Card S = M &
( for X1 being set st X1 in S holds not X1 in I ) &
for X1,X2 being set st (X1 in S & X2 in S & X1 <> X2) holds X1 misses X2;

theorem :: CARD_FIL:36
for X for N being Cardinal st N <=` Card X
ex Y being set st Y c= X & Card Y = N;

theorem :: CARD_FIL:37
for M holds not ex F st
( F is uniform being_ultrafilter & F is_complete_with M );

reserve M for Aleph;

theorem :: CARD_FIL:38
M is measurable implies M is limit;

theorem :: CARD_FIL:39
M is measurable implies M is inaccessible;

theorem :: CARD_FIL:40
M is measurable implies M is strong_limit;

theorem :: CARD_FIL:41
M is measurable implies M is strongly_inaccessible;

```