:: Mahlo and inaccessible cardinals
:: by Josef Urban
::
:: Received August 28, 2000
:: Copyright (c) 2000-2021 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 CARD_1, FINSET_1, ORDINAL1, XBOOLE_0, TARSKI, CARD_3, CARD_5,
ORDINAL2, SUBSET_1, RCOMP_1, XXREAL_2, SETFAM_1, FUNCT_1, NUMBERS,
RELAT_1, ARYTM_3, CARD_FIL, CARD_2, CLASSES1, ZFMISC_1, CLASSES2,
CARD_LAR, NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, RELAT_1,
CLASSES1, FUNCT_1, XCMPLX_0, NAT_1, SETFAM_1, FINSET_1, FUNCT_2,
ORDINAL2, NUMBERS, CARD_2, CARD_3, CARD_5, CARD_FIL, CLASSES2;
constructors WELLORD2, ORDINAL2, NAT_1, CARD_2, CLASSES1, CLASSES2, CARD_5,
CARD_FIL, RELSET_1, NUMBERS;
registrations XBOOLE_0, ORDINAL1, RELSET_1, ORDINAL3, CARD_1, CLASSES2,
CARD_5, CARD_FIL, CARD_3, CLASSES1, CARD_2, NAT_1;
requirements NUMERALS, SUBSET, BOOLE;
begin
:: ::
:: Some initial settings ::
:: ::
registration
cluster cardinal infinite -> limit_ordinal for Ordinal;
end;
registration
cluster non empty limit_ordinal -> infinite for Ordinal;
end;
registration
cluster non limit_cardinal -> non countable for Aleph;
end;
registration
cluster regular non countable for Aleph;
end;
:: Closed, unbounded and stationary sets
reserve A,B for limit_ordinal infinite Ordinal;
reserve B1,B2,B3,B5,B6,D, C for Ordinal;
reserve X for set;
definition
let A,X;
pred X is_unbounded_in A means
:: CARD_LAR:def 1
X c= A & sup X = A;
pred X is_closed_in A means
:: CARD_LAR:def 2
X c= A & for B st B in A holds sup (X /\ B)=B implies B in X;
end;
definition
let A,X;
pred X is_club_in A means
:: CARD_LAR:def 3
X is_closed_in A & X is_unbounded_in A;
end;
reserve X for Subset of A;
definition
let A,X;
attr X is unbounded means
:: CARD_LAR:def 4
sup X = A;
attr X is closed means
:: CARD_LAR:def 5
for B st B in A holds sup (X /\ B)=B implies B in X;
end;
notation
let A,X;
antonym X is bounded for X is unbounded;
end;
theorem :: CARD_LAR:1
X is_club_in A iff X is closed unbounded;
:: should be probably in ordinal2
theorem :: CARD_LAR:2
X c= sup X;
theorem :: CARD_LAR:3
(X is non empty & for B1 st B1 in X ex B2 st B2 in X & B1 in B2 )
implies sup X is limit_ordinal infinite Ordinal;
theorem :: CARD_LAR:4
X is bounded iff ex B1 st B1 in A & X c= B1;
theorem :: CARD_LAR:5
not sup (X /\ B) = B implies ex B1 st B1 in B & (X /\ B) c= B1;
theorem :: CARD_LAR:6
X is unbounded iff for B1 st B1 in A ex C st C in X & B1 c= C;
theorem :: CARD_LAR:7
X is unbounded implies X is non empty;
theorem :: CARD_LAR:8
X is unbounded & B1 in A implies ex B3 being Element of A st B3
in { B2 where B2 is Element of A: B2 in X & B1 in B2};
definition
let A,X,B1;
assume
X is unbounded;
assume
B1 in A;
func LBound(B1,X) -> Element of X equals
:: CARD_LAR:def 6
inf { B2 where B2 is Element
of A: B2 in X & B1 in B2};
end;
theorem :: CARD_LAR:9
X is unbounded & B1 in A implies LBound(B1,X) in X & B1 in LBound(B1,X);
theorem :: CARD_LAR:10
[#] A is closed unbounded;
theorem :: CARD_LAR:11
B1 in A & X is closed unbounded implies X \ B1 is closed unbounded;
theorem :: CARD_LAR:12
B1 in A implies A \ B1 is closed unbounded;
definition
let A,X;
attr X is stationary means
:: CARD_LAR:def 7
for Y being Subset of A holds Y is closed
unbounded implies X /\ Y is non empty;
end;
theorem :: CARD_LAR:13
for X,Y being Subset of A holds (X is stationary & X c= Y
implies Y is stationary);
definition
let A;
let X be set;
pred X is_stationary_in A means
:: CARD_LAR:def 8
X c= A & for Y being Subset of A
holds Y is closed unbounded implies X /\ Y is non empty;
end;
theorem :: CARD_LAR:14
for X,Y being set holds (X is_stationary_in A & X c= Y & Y c= A
implies Y is_stationary_in A);
:: belongs e.g. to setfam?
definition
let X be set;
let S be Subset-Family of X;
redefine mode Element of S -> Subset of X;
end;
theorem :: CARD_LAR:15
X is stationary implies X is unbounded;
definition
let A,X;
func limpoints X -> Subset of A equals
:: CARD_LAR:def 9
{B1 where B1 is Element of A: B1 is
infinite limit_ordinal & sup (X /\ B1) = B1};
end;
theorem :: CARD_LAR:16
X /\ B3 c= B1 implies B3 /\ limpoints X c= succ B1;
theorem :: CARD_LAR:17
X c= B1 implies limpoints X c= succ B1;
theorem :: CARD_LAR:18
limpoints X is closed;
:: mainly used for MahloReg, LimUnb says this usually doesnot happen
theorem :: CARD_LAR:19
X is unbounded & limpoints X is bounded implies ex B1 st B1 in A
& {succ B2 where B2 is Element of A : B2 in X & B1 in succ B2} is_club_in A;
reserve M for non countable Aleph;
reserve X for Subset of M;
registration
let M;
cluster cardinal infinite for Element of M;
end;
reserve N,N1 for cardinal infinite Element of M;
theorem :: CARD_LAR:20
for M being Aleph for X being Subset of M holds X is unbounded
implies cf M c= card X;
theorem :: CARD_LAR:21
for S being Subset-Family of M st for X being Element of S holds
X is closed holds meet S is closed;
theorem :: CARD_LAR:22
omega in cf M implies for f being sequence of X holds sup rng f in M;
theorem :: CARD_LAR:23
omega in cf M implies for S being non empty Subset-Family of M st (
card S in cf M & for X being Element of S holds X is closed unbounded ) holds
meet S is closed unbounded;
theorem :: CARD_LAR:24
omega in cf M & X is unbounded implies for B1 st B1 in M ex B st
B in M & B1 in B & B in limpoints X;
theorem :: CARD_LAR:25
omega in cf M & X is unbounded implies limpoints X is unbounded;
definition
let M;
attr M is Mahlo means
:: CARD_LAR:def 10
{ N : N is regular } is_stationary_in M;
attr M is strongly_Mahlo means
:: CARD_LAR:def 11
{ N : N is strongly_inaccessible} is_stationary_in M;
end;
theorem :: CARD_LAR:26
M is strongly_Mahlo implies M is Mahlo;
theorem :: CARD_LAR:27
M is Mahlo implies M is regular;
theorem :: CARD_LAR:28
M is Mahlo implies M is limit_cardinal;
theorem :: CARD_LAR:29
M is Mahlo implies M is inaccessible;
theorem :: CARD_LAR:30
M is strongly_Mahlo implies M is strong_limit;
theorem :: CARD_LAR:31
M is strongly_Mahlo implies M is strongly_inaccessible;
:: ::
:: Proof that strongly inaccessible is model of ZF ::
:: ::
begin
reserve A for Ordinal;
reserve x,y,X,Y for set;
:: shouldnot be e.g. in CARD_1? or is there st. more general?
theorem :: CARD_LAR:32
(for x st x in X ex y st y in X & x c= y & y is Cardinal)
implies union X is Cardinal;
theorem :: CARD_LAR:33
for M being Aleph holds (card X in cf M & for Y st Y in X holds
card Y in M) implies card union X in M;
theorem :: CARD_LAR:34
M is strongly_inaccessible & A in M implies card Rank A in M;
theorem :: CARD_LAR:35
M is strongly_inaccessible implies card Rank M = M;
theorem :: CARD_LAR:36
M is strongly_inaccessible implies Rank M is Tarski;
theorem :: CARD_LAR:37
for A being non empty Ordinal holds Rank A is non empty;
registration
let A be non empty Ordinal;
cluster Rank A -> non empty;
end;
theorem :: CARD_LAR:38
M is strongly_inaccessible implies Rank M is Universe;