:: Basic facts about inaccessible and measurable cardinals
:: by Josef Urban
::
:: Received April 14, 2000
:: Copyright (c) 2000-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FINSET_1, CARD_1, XBOOLE_0, SUBSET_1, CARD_5, SETFAM_1, TARSKI,
ZFMISC_1, ORDINAL1, CARD_2, FUNCT_1, RELAT_1, ORDINAL2, FUNCT_2, CARD_3,
FUNCOP_1, FUNCT_5, CARD_FIL;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCOP_1,
BINOP_1, FUNCT_5, SETFAM_1, FINSET_1, ORDINAL1, CARD_1, RELSET_1,
FUNCT_2, ORDINAL2, CARD_2, CARD_3, CARD_5;
constructors SETFAM_1, WELLORD2, BINOP_1, FUNCOP_1, ORDINAL2, FUNCT_5, CARD_2,
CARD_5, NUMBERS, RELSET_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1,
FINSET_1, CARD_1, CARD_5, CARD_2;
requirements NUMERALS, SUBSET, BOOLE;
begin
theorem :: CARD_FIL:1
for x being set for X being infinite set holds card {x} in card X;
scheme :: CARD_FIL:sch 1
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-Family of 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);
notation
let X,S;
synonym dual S for COMPLEMENT S;
end;
reserve S for non empty Subset-Family of X;
registration
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 in N holds meet S1 in S;
end;
definition
let X,N,S;
pred S is_additive_with N means
:: CARD_FIL:def 4
for S1 being non empty set st S1 c= S & card S1 in N holds union S1 in S;
end;
notation
let X,N,F;
synonym F is_complete_with N for F is_multiplicative_with N;
end;
notation
let X,N,I;
synonym I is_complete_with N for I is_additive_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-Family of X;
definition
let X;
func Filters(X) -> non empty Subset-Family of bool X equals
:: CARD_FIL:def 9
{S where S is
Subset-Family of 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) in 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) in card X;
theorem :: CARD_FIL:19
Y in Frechet_Ideal(X) iff card Y in 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;
registration
let X;
cluster non principal being_ultrafilter for Filter of X;
end;
registration
let X;
cluster uniform being_ultrafilter -> non principal for 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 c= 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_cardinal;
end;
registration
cluster inaccessible -> regular limit_cardinal for Aleph;
end;
theorem :: CARD_FIL:25
omega is inaccessible;
definition
let IT be Aleph;
attr IT is strong_limit means
:: CARD_FIL:def 14
for N st N in IT holds exp(2,N) in IT;
end;
theorem :: CARD_FIL:26
omega is strong_limit;
theorem :: CARD_FIL:27
M is strong_limit implies M is limit_cardinal;
registration
cluster strong_limit -> limit_cardinal for Aleph;
end;
theorem :: CARD_FIL:28
GCH implies (M is limit_cardinal 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;
end;
registration
cluster strongly_inaccessible -> regular strong_limit for Aleph;
end;
theorem :: CARD_FIL:29
omega is strongly_inaccessible;
theorem :: CARD_FIL:30
M is strongly_inaccessible implies M is inaccessible;
registration
cluster strongly_inaccessible -> inaccessible for 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;
end;
theorem :: CARD_FIL:32
for A 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;
registration
let M;
cluster nextcard M -> non limit_cardinal;
end;
registration
cluster non limit_cardinal infinite for Cardinal;
end;
registration
cluster non limit_cardinal -> regular for Aleph;
end;
definition
let M be non limit_cardinal Cardinal;
func predecessor M -> Cardinal means
:: CARD_FIL:def 17
M = nextcard it;
end;
registration
let M be non limit_cardinal 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_cardinal 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})
c= predecessor M ) & for K1 holds card (M \ union {T.(N1,K1): N1 in predecessor
M}) c= predecessor M;
end;
:: this is pretty long
theorem :: CARD_FIL:34
ex T st T is_Ulam_Matrix_of M;
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 c= 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_cardinal;
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;