:: Veblen Hierarchy
:: by Grzegorz Bancerek
::
:: Received October 18, 2010
:: Copyright (c) 2010-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 ORDINAL6, CARD_1, RELAT_1, FUNCT_1, CLASSES2, NUMBERS, TARSKI,
XBOOLE_0, SUBSET_1, ORDINAL1, ORDINAL2, WELLORD1, WELLORD2, ABIAN,
CARD_3, MATROID0, ORDINAL4, NAT_1, ARYTM_3, CLASSES1, VALUED_0, AFINSQ_1,
ORDINAL5, ZFMISC_1, FINSET_1, MESFUNC8, NAGATA_1, ORDINAL3, PRE_TOPC,
AOFA_000;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1,
FUNCT_2, FINSET_1, ORDINAL1, ORDINAL2, XCMPLX_0, NAT_1, ORDINAL3, ABIAN,
WELLORD1, WELLORD2, CARD_1, ORDINAL4, CARD_3, AFINSQ_1, CLASSES1,
CLASSES2, NUMBERS, ORDINAL5;
constructors WELLORD1, WELLORD2, CLASSES1, ABIAN, CARD_3, AFINSQ_1, ORDINAL3,
ORDINAL5, NAT_1, RELSET_1, NUMBERS;
registrations XBOOLE_0, RELAT_1, RELSET_1, FUNCT_1, FINSET_1, FUNCT_2,
ORDINAL1, ORDINAL2, CARD_1, WELLORD2, ORDINAL3, CLASSES2, CARD_5,
ORDINAL4, CARD_LAR, ORDINAL5, CLASSES1, AFINSQ_1, SUBSET_1;
requirements SUBSET, BOOLE, NUMERALS;
begin :: Preliminaries
reserve a,b,c,d for Ordinal;
reserve l for non empty limit_ordinal Ordinal;
reserve u for Element of l;
reserve A for non empty Ordinal;
reserve e for Element of A;
reserve X,Y,x,y,z for set;
reserve n,m for Nat;
definition
let X be set;
attr X is ordinal-membered means
:: ORDINAL6:def 1
ex a st X c= a;
end;
registration
cluster ordinal -> ordinal-membered for set;
let X;
cluster On X -> ordinal-membered;
end;
theorem :: ORDINAL6:1
X is ordinal-membered iff for x st x in X holds x is ordinal;
registration
cluster ordinal-membered for set;
end;
registration
let X be ordinal-membered set;
cluster -> ordinal for Element of X;
end;
theorem :: ORDINAL6:2
X is ordinal-membered iff On X = X;
theorem :: ORDINAL6:3
for X being ordinal-membered set holds X c= sup X;
theorem :: ORDINAL6:4
a c= b iff b nin a;
theorem :: ORDINAL6:5
x in a\b iff b c= x & x in a;
registration let a,b;
cluster a\b -> ordinal-membered;
end;
theorem :: ORDINAL6:6
for f being Function st f is_isomorphism_of RelIncl X, RelIncl Y
for x,y st x in X & y in X holds x c= y iff f.x c= f.y;
theorem :: ORDINAL6:7
for X,Y being ordinal-membered set
for f being Function st f is_isomorphism_of RelIncl X, RelIncl Y
for x,y st x in X & y in X holds x in y iff f.x in f.y;
theorem :: ORDINAL6:8
[x,y] in RelIncl X implies x c= y;
theorem :: ORDINAL6:9
for f1,f2 being Sequence holds f1 c= f1^f2;
::$CT
theorem :: ORDINAL6:11
a c= b iff epsilon_a c= epsilon_b;
theorem :: ORDINAL6:12
a in b iff epsilon_a in epsilon_b;
registration
let X be ordinal-membered set;
cluster union X -> ordinal;
end;
registration
let f be Ordinal-yielding Function;
cluster rng f -> ordinal-membered;
end;
registration
let a;
cluster id a -> Sequence-like Ordinal-yielding;
end;
registration
let a;
cluster id a -> increasing for Ordinal-Sequence;
end;
registration
let a;
cluster id a -> continuous for Ordinal-Sequence;
end;
registration
cluster non empty increasing continuous for Ordinal-Sequence;
end;
definition
let f be Sequence;
attr f is normal means
:: ORDINAL6:def 2
f is increasing continuous Ordinal-Sequence;
end;
definition
let f be Ordinal-Sequence;
redefine attr f is normal means
:: ORDINAL6:def 3
f is increasing continuous;
end;
registration
cluster normal -> Ordinal-yielding for Sequence;
cluster normal -> increasing continuous for Ordinal-Sequence;
cluster increasing continuous -> normal for Ordinal-Sequence;
end;
registration
cluster non empty normal for Sequence;
end;
theorem :: ORDINAL6:13
for f being Ordinal-Sequence holds
f is non-decreasing implies f|a is non-decreasing;
definition
let X;
func ord-type X -> Ordinal equals
:: ORDINAL6:def 4
order_type_of RelIncl On X;
end;
definition
let X be ordinal-membered set;
redefine func ord-type X equals
:: ORDINAL6:def 5
order_type_of RelIncl X;
end;
registration
let X be ordinal-membered set;
cluster RelIncl X -> well-ordering;
end;
registration
let E be empty set;
cluster On E -> empty;
end;
registration
let E be empty set;
cluster order_type_of E -> empty;
end;
theorem :: ORDINAL6:14
ord-type {} = 0;
theorem :: ORDINAL6:15
ord-type {a} = 1;
theorem :: ORDINAL6:16
a <> b implies ord-type {a,b} = 2;
theorem :: ORDINAL6:17
ord-type a = a;
definition
let X;
func numbering X -> Ordinal-Sequence equals
:: ORDINAL6:def 6
canonical_isomorphism_of(RelIncl ord-type X, RelIncl On X);
end;
theorem :: ORDINAL6:18
dom numbering X = ord-type X & rng numbering X = On X;
theorem :: ORDINAL6:19
for X being ordinal-membered set holds rng numbering X = X;
theorem :: ORDINAL6:20
card dom numbering X = card On X;
theorem :: ORDINAL6:21
numbering X is_isomorphism_of RelIncl ord-type X, RelIncl On X;
reserve f for Ordinal-Sequence;
theorem :: ORDINAL6:22
f = numbering X & x in dom f & y in dom f implies (x c= y iff f.x c= f.y);
theorem :: ORDINAL6:23
f = numbering X & x in dom f & y in dom f implies (x in y iff f.x in f.y);
registration
let X;
cluster numbering X -> increasing;
end;
registration
let X,Y be ordinal-membered set;
cluster X \/ Y -> ordinal-membered;
end;
registration
let X be ordinal-membered set, Y be set;
cluster X \ Y -> ordinal-membered;
end;
theorem :: ORDINAL6:24
for X,Y being ordinal-membered set
st for x,y st x in X & y in Y holds x in y
holds (numbering X)^(numbering Y) is_isomorphism_of
RelIncl ((ord-type X)+^(ord-type Y)), RelIncl (X \/ Y);
theorem :: ORDINAL6:25
for X,Y being ordinal-membered set
st for x,y st x in X & y in Y holds x in y
holds numbering(X \/ Y) = (numbering X)^(numbering Y);
theorem :: ORDINAL6:26
for X,Y being ordinal-membered set
st for x,y st x in X & y in Y holds x in y
holds ord-type(X \/ Y) = (ord-type X)+^(ord-type Y);
begin :: Fixpoints of a Normal Function
theorem :: ORDINAL6:27
for f being Function st x is_a_fixpoint_of f holds x in rng f;
definition
let f be Ordinal-Sequence;
func criticals f -> Ordinal-Sequence equals
:: ORDINAL6:def 7
numbering {a where a is Element of dom f: a is_a_fixpoint_of f};
end;
theorem :: ORDINAL6:28
On {a where a is Element of dom f: a is_a_fixpoint_of f}
= {a where a is Element of dom f: a is_a_fixpoint_of f};
theorem :: ORDINAL6:29
x in dom criticals f implies (criticals f).x is_a_fixpoint_of f;
theorem :: ORDINAL6:30
rng criticals f = {a where a is Element of dom f: a is_a_fixpoint_of f} &
rng criticals f c= rng f;
registration let f;
cluster criticals f -> increasing;
end;
theorem :: ORDINAL6:31
x in dom criticals f implies x c= (criticals f).x;
theorem :: ORDINAL6:32
dom criticals f c= dom f;
theorem :: ORDINAL6:33
b is_a_fixpoint_of f implies
ex a st a in dom criticals f & b = (criticals f).a;
theorem :: ORDINAL6:34
a in dom criticals f & b is_a_fixpoint_of f & (criticals f).a in b
implies succ a in dom criticals f;
theorem :: ORDINAL6:35
succ a in dom criticals f & b is_a_fixpoint_of f & (criticals f).a in b
implies (criticals f).succ a c= b;
theorem :: ORDINAL6:36
f is normal & union X in dom f & X is non empty &
(for x st x in X ex y st x c= y & y in X & y is_a_fixpoint_of f)
implies union X = f.union X;
theorem :: ORDINAL6:37
f is normal & union X in dom f & X is non empty &
(for x st x in X holds x is_a_fixpoint_of f)
implies union X = f.union X;
theorem :: ORDINAL6:38
l c= dom criticals f & a is_a_fixpoint_of f &
(for x st x in l holds (criticals f).x in a)
implies l in dom criticals f;
theorem :: ORDINAL6:39
f is normal & l in dom criticals f implies
(criticals f).l = Union ((criticals f)|l);
registration
let f be normal Ordinal-Sequence;
cluster criticals f -> continuous;
end;
theorem :: ORDINAL6:40
for f1,f2 being Ordinal-Sequence st f1 c= f2
holds criticals f1 c= criticals f2;
begin :: Fixpoints in a Universal Set
reserve U,W for Universe;
registration
let U;
cluster normal for Ordinal-Sequence of U;
end;
definition
let U,a;
mode Ordinal-Sequence of a,U is Function of a, On U;
end;
registration
let U,a;
cluster -> Sequence-like Ordinal-yielding for Ordinal-Sequence of a,U;
end;
definition
let U,a;
let f be Ordinal-Sequence of a,U;
let x;
redefine func f.x -> Ordinal of U;
end;
theorem :: ORDINAL6:41
a in U implies for f being Ordinal-Sequence of a,U holds Union f in U;
theorem :: ORDINAL6:42
a in U implies for f being Ordinal-Sequence of a,U holds sup f in U;
scheme :: ORDINAL6:sch 1
CriticalNumber2
{U() -> Universe, a() -> Ordinal of U(),
f() -> Ordinal-Sequence of omega, U(),
phi(Ordinal) -> Ordinal}:
a() c= Union f() & phi(Union f()) = Union f() &
for b st a() c= b & b in U() & phi(b) = b holds Union f() c= b
provided
omega in U()
and
for a st a in U() holds phi(a) in U()
and
for a,b st a in b & b in U() holds phi(a) in phi(b)
and
for a being Ordinal of U() st a is non empty limit_ordinal
for phi being Ordinal-Sequence
st dom phi = a & for b st b in a holds phi.b = phi(b)
holds phi(a) is_limes_of phi
and
f().0 = a()
and
for a st a in omega holds f().(succ a) = phi(f().a);
scheme :: ORDINAL6:sch 2
CriticalNumber3
{U() -> Universe, a() -> Ordinal of U(), phi(Ordinal) -> Ordinal}:
ex a being Ordinal of U() st a() in a & phi(a) = a
provided
omega in U()
and
for a st a in U() holds phi(a) in U()
and
for a,b st a in b & b in U() holds phi(a) in phi(b)
and
for a being Ordinal of U() st a is non empty limit_ordinal
for phi being Ordinal-Sequence
st dom phi = a & for b st b in a holds phi.b = phi(b)
holds phi(a) is_limes_of phi;
reserve F,phi for normal Ordinal-Sequence of W;
theorem :: ORDINAL6:43
omega in W & b in W implies ex a st b in a & a is_a_fixpoint_of phi;
theorem :: ORDINAL6:44
omega in W implies criticals F is Ordinal-Sequence of W;
theorem :: ORDINAL6:45
f is normal implies
for a st a in dom criticals f holds f.a c= (criticals f).a;
begin :: Sequences of Sequences of Ordinals
definition
let U;
let a,b be Ordinal of U;
redefine func exp(a,b) -> Ordinal of U;
end;
definition
let U,a such that
a in U;
func U exp a -> Ordinal-Sequence of U means
:: ORDINAL6:def 8
for b being Ordinal of U holds it.b = exp(a,b);
end;
registration
cluster omega -> non trivial;
end;
registration
let U;
cluster non trivial finite for Ordinal of U;
end;
registration
cluster non trivial finite for Ordinal;
end;
registration
let U;
let a be non trivial Ordinal of U;
cluster U exp a -> normal;
end;
definition
let g be Function;
attr g is Ordinal-Sequence-valued means
:: ORDINAL6:def 9
x in rng g implies x is Ordinal-Sequence;
end;
registration
let f be Ordinal-Sequence;
cluster <%f%> -> Ordinal-Sequence-valued;
end;
definition ::: MESFUNC8:def 1 generalized
let f be Function;
attr f is with_the_same_dom means
:: ORDINAL6:def 10
rng f is with_common_domain;
end;
registration
let f be Function;
cluster {f} -> with_common_domain;
end;
registration
let f be Function;
cluster <%f%> -> with_the_same_dom;
end;
registration
cluster non empty Ordinal-Sequence-valued with_the_same_dom for Sequence;
end;
registration
let g be Ordinal-Sequence-valued Function;
let x be object;
cluster g.x -> Relation-like Function-like;
end;
registration
let g be Ordinal-Sequence-valued Function;
let x;
cluster g.x -> Sequence-like Ordinal-yielding;
end;
registration
let g be Sequence;
let a;
cluster g|a -> Sequence-like;
end;
registration
let g be Ordinal-Sequence-valued Function;
let X;
cluster g|X -> Ordinal-Sequence-valued;
end;
registration
let a,b;
cluster -> Ordinal-yielding Sequence-like for Function of a,b;
end;
definition
let g be Ordinal-Sequence-valued Sequence;
func criticals g -> Ordinal-Sequence equals
:: ORDINAL6:def 11
numbering {a where a is Element of dom(g.0): a in dom(g.0) &
for f st f in rng g holds a is_a_fixpoint_of f};
end;
reserve g for Ordinal-Sequence-valued Sequence;
theorem :: ORDINAL6:46
for g holds
{a where a is Element of dom(g.0): a in dom(g.0) &
for f st f in rng g holds a is_a_fixpoint_of f} is ordinal-membered;
theorem :: ORDINAL6:47
a in dom g & b in dom criticals g
implies (criticals g).b is_a_fixpoint_of g.a;
theorem :: ORDINAL6:48
x in dom criticals g implies x c= (criticals g).x;
theorem :: ORDINAL6:49
f in rng g implies dom criticals g c= dom f;
theorem :: ORDINAL6:50
dom g <> {} & (for c st c in dom g holds b is_a_fixpoint_of g.c) implies
ex a st a in dom criticals g & b = (criticals g).a;
theorem :: ORDINAL6:51
dom g <> {} & l c= dom criticals g &
(for f st f in rng g holds a is_a_fixpoint_of f) &
(for x st x in l holds (criticals g).x in a)
implies l in dom criticals g;
theorem :: ORDINAL6:52
for g st dom g <> {} & for a st a in dom g holds g.a is normal
holds l in dom criticals g implies
(criticals g).l = Union ((criticals g)|l);
theorem :: ORDINAL6:53
for g st dom g <> {} & for a st a in dom g holds g.a is normal
holds criticals g is continuous;
theorem :: ORDINAL6:54
for g st dom g <> {} & for a st a in dom g holds g.a is normal
for a,f st a in dom criticals g & f in rng g holds f.a c= (criticals g).a;
theorem :: ORDINAL6:55
for g1,g2 being Ordinal-Sequence-valued Sequence
st dom g1 = dom g2 & dom g1 <> {} & for a st a in dom g1 holds g1.a c= g2.a
holds criticals g1 c= criticals g2;
definition
let g be Ordinal-Sequence-valued Sequence;
func lims g -> Ordinal-Sequence means
:: ORDINAL6:def 12
dom it = dom (g.0) & for a st a in dom it holds
it.a = union {g.b.a where b is Element of dom g: b in dom g};
end;
theorem :: ORDINAL6:56
for g being Ordinal-Sequence-valued Sequence
st dom g <> {} & dom g in U &
for a st a in dom g holds g.a is Ordinal-Sequence of U
holds lims g is Ordinal-Sequence of U;
begin :: Veblen Hierarchy
definition
let x;
func OS@ x -> Ordinal-Sequence equals
:: ORDINAL6:def 13
x if x is Ordinal-Sequence otherwise the Ordinal-Sequence;
func OSV@ x -> Ordinal-Sequence-valued Sequence equals
:: ORDINAL6:def 14
x if x is Ordinal-Sequence-valued Sequence
otherwise the Ordinal-Sequence-valued Sequence;
end;
definition
let U;
func U-Veblen -> Ordinal-Sequence-valued Sequence means
:: ORDINAL6:def 15
dom it = On U & it.0 = U exp omega &
(for b st succ b in On U holds it.succ b = criticals (it.b)) &
(for l st l in On U holds it.l = criticals (it|l));
end;
registration
cluster uncountable for Universe;
end;
theorem :: ORDINAL6:57
for U being Universe holds U is uncountable iff omega in U;
theorem :: ORDINAL6:58
a in b & b in U & omega in U & c in dom(U-Veblen.b)
implies U-Veblen.b.c is_a_fixpoint_of U-Veblen.a;
theorem :: ORDINAL6:59
l in U & (for c st c in l holds a is_a_fixpoint_of U-Veblen.c)
implies a is_a_fixpoint_of lims(U-Veblen|l);
theorem :: ORDINAL6:60
a c= b & b in U & omega in U & c in dom(U-Veblen.b) &
(for c st c in b holds U-Veblen.c is normal)
implies U-Veblen.a.c c= U-Veblen.b.c;
theorem :: ORDINAL6:61
l in U & a in U & b in l &
(for c st c in l holds U-Veblen.c is normal Ordinal-Sequence of U)
implies (lims(U-Veblen|l)).a is_a_fixpoint_of U-Veblen.b;
theorem :: ORDINAL6:62
omega in U & a in U implies U-Veblen.a is normal Ordinal-Sequence of U;
theorem :: ORDINAL6:63
omega in U & U c= W & a in U implies U-Veblen.a c= W-Veblen.a;
theorem :: ORDINAL6:64
omega in U & a in U & b in U & omega in W & a in W & b in W implies
U-Veblen.b.a = W-Veblen.b.a;
theorem :: ORDINAL6:65
l in U & (for a st a in l holds
U-Veblen.a is normal Ordinal-Sequence of U)
implies lims(U-Veblen|l) is non-decreasing continuous Ordinal-Sequence of U;
registration
let a;
cluster Tarski-Class(a \/ omega) -> uncountable;
end;
definition
let a,b;
func a-Veblen(b) -> Ordinal equals
:: ORDINAL6:def 16
(Tarski-Class(a \/ b \/ omega))-Veblen.a.b;
end;
definition
let n,b;
redefine func n-Veblen(b) -> Ordinal equals
:: ORDINAL6:def 17
(Tarski-Class(b \/ omega))-Veblen.n.b;
end;
theorem :: ORDINAL6:66
a in Tarski-Class(a\/b\/c);
theorem :: ORDINAL6:67
omega in U & a in U & b in U implies b-Veblen a = U-Veblen.b.a;
theorem :: ORDINAL6:68
0-Veblen(a) = exp(omega,a);
theorem :: ORDINAL6:69
b-Veblen((succ b)-Veblen a) = (succ b)-Veblen a;
theorem :: ORDINAL6:70
b in c implies b-Veblen(c-Veblen a) = c-Veblen a;
theorem :: ORDINAL6:71
a c= b iff c-Veblen a c= c-Veblen b;
theorem :: ORDINAL6:72
a in b iff c-Veblen a in c-Veblen b;
theorem :: ORDINAL6:73
a-Veblen b in c-Veblen d iff
a = c & b in d or
a in c & b in c-Veblen d or
c in a & a-Veblen b in d;
begin :: Epsilon Numbers
reserve U for uncountable Universe;
theorem :: ORDINAL6:74
U-Veblen.1 = criticals(U exp omega);
theorem :: ORDINAL6:75
1-Veblen(a) is epsilon;
theorem :: ORDINAL6:76
for e being epsilon Ordinal ex a st e = 1-Veblen a;
theorem :: ORDINAL6:77
1-Veblen(a) = epsilon_a;