:: On same equivalents of well-foundedness
:: by Piotr Rudnicki and Andrzej Trybulec
::
:: Received February 25, 1997
:: Copyright (c) 1997-2021 Association of Mizar Users

:: General preliminaries

theorem Th1: :: WELLFND1:1

for X being functional set st ( for f, g being Function st f in X & g in X holds
f tolerates g ) holds
union X is Function

proof end;

scheme :: WELLFND1:sch 1
PFSeparation{ F₁() -> set , F₂() -> set , P₁[ set ] } :

ex PFS being Subset of (PFuncs (F₁(),F₂())) st
for pfs being PartFunc of F₁(),F₂() holds
( pfs in PFS iff P₁[pfs] )

proof end;

:: Cardinals

registration

let X be set ;

cluster nextcard X -> non empty ;

coherence
not nextcard X is empty by CARD_1:def 3;

end;

registration

cluster non empty epsilon-transitive epsilon-connected ordinal non finite cardinal regular for set ;

existence
ex b₁ being Aleph st b₁ is regular by CARD_5:30;

end;

theorem Th2: :: WELLFND1:2

for M being regular Aleph
for X being set st X c= M & card X in M holds
sup X in M

proof end;

:: Relational structures

theorem Th3: :: WELLFND1:3

for R being RelStr
for x being set holds the InternalRel of R -Seg x c= the carrier of R

proof end;

definition

let R be RelStr ;
let X be Subset of R;

redefine attr X is lower means :Def1: :: WELLFND1:def 1
for x, y being object st x in X & [y,x] in the InternalRel of R holds
y in X;

compatibility
( X is lower iff for x, y being object st x in X & [y,x] in the InternalRel of R holds
y in X )

proof end;

end;

:: deftheorem Def1 defines lower WELLFND1:def 1 :
for R being RelStr
for X being Subset of R holds
( X is lower iff for x, y being object st x in X & [y,x] in the InternalRel of R holds
y in X );

theorem Th4: :: WELLFND1:4

for R being RelStr
for X being Subset of R
for x being set st X is lower & x in X holds
the InternalRel of R -Seg x c= X

proof end;

theorem Th5: :: WELLFND1:5

for R being RelStr
for X being lower Subset of R
for Y being Subset of R
for x being set st Y = X \/ {x} & the InternalRel of R -Seg x c= X holds
Y is lower

proof end;

definition

let R be RelStr ;

attr R is well_founded means :: WELLFND1:def 2
the InternalRel of R is_well_founded_in the carrier of R;

end;

:: deftheorem defines well_founded WELLFND1:def 2 :
for R being RelStr holds
( R is well_founded iff the InternalRel of R is_well_founded_in the carrier of R );

registration

cluster non empty well_founded for RelStr ;

existence
ex b₁ being RelStr st
( not b₁ is empty & b₁ is well_founded )

proof end;

end;

definition

let R be RelStr ;
let X be Subset of R;

attr X is well_founded means :Def3: :: WELLFND1:def 3
the InternalRel of R is_well_founded_in X;

end;

:: deftheorem Def3 defines well_founded WELLFND1:def 3 :
for R being RelStr
for X being Subset of R holds
( X is well_founded iff the InternalRel of R is_well_founded_in X );

registration

let R be RelStr ;

cluster well_founded for Element of bool the carrier of R;

existence
ex b₁ being Subset of R st b₁ is well_founded

proof end;

end;

definition

let R be RelStr ;

func well_founded-Part R -> Subset of R means :Def4: :: WELLFND1:def 4
it = union { S where S is Subset of R : ( S is well_founded & S is lower ) } ;

existence
ex b₁ being Subset of R st b₁ = union { S where S is Subset of R : ( S is well_founded & S is lower ) }

proof end;

uniqueness
for b₁, b₂ being Subset of R st b₁ = union { S where S is Subset of R : ( S is well_founded & S is lower ) } & b₂ = union { S where S is Subset of R : ( S is well_founded & S is lower ) } holds
b₁ = b₂ ;

end;

:: deftheorem Def4 defines well_founded-Part WELLFND1:def 4 :
for R being RelStr
for b₂ being Subset of R holds
( b₂ = well_founded-Part R iff b₂ = union { S where S is Subset of R : ( S is well_founded & S is lower ) } );

registration

let R be RelStr ;

cluster well_founded-Part R -> lower well_founded ;

coherence
( well_founded-Part R is lower & well_founded-Part R is well_founded )

proof end;

end;

theorem Th6: :: WELLFND1:6

for R being non empty RelStr
for x being Element of R holds {x} is well_founded Subset of R

proof end;

theorem Th7: :: WELLFND1:7

for R being RelStr
for X, Y being well_founded Subset of R st X is lower holds
X \/ Y is well_founded Subset of R

proof end;

theorem Th8: :: WELLFND1:8

for R being RelStr holds
( R is well_founded iff well_founded-Part R = the carrier of R )

proof end;

theorem Th9: :: WELLFND1:9

for R being non empty RelStr
for x being Element of R st the InternalRel of R -Seg x c= well_founded-Part R holds
x in well_founded-Part R

proof end;

:: Well-founded induction

scheme :: WELLFND1:sch 2
WFMin{ F₁() -> non empty RelStr , F₂() -> Element of F₁(), P₁[ set ] } :

ex x being Element of F₁() st
( P₁[x] & ( for y being Element of F₁() holds
( not x <> y or not P₁[y] or not [y,x] in the InternalRel of F₁() ) ) )

provided

A1: P₁[F₂()] and
A2: F₁() is well_founded

proof end;

:: WF iff WFInduction

theorem Th10: :: WELLFND1:10

for R being non empty RelStr holds
( R is well_founded iff for S being set st ( for x being Element of R st the InternalRel of R -Seg x c= S holds
x in S ) holds
the carrier of R c= S )

proof end;

scheme :: WELLFND1:sch 3
WFInduction{ F₁() -> non empty RelStr , P₁[ set ] } :

for x being Element of F₁() holds P₁[x]

provided

A1: for x being Element of F₁() st ( for y being Element of F₁() st y <> x & [y,x] in the InternalRel of F₁() holds
P₁[y] ) holds
P₁[x] and
A2: F₁() is well_founded

proof end;

:: Well-foundedness and recursive definitions

definition

let R be non empty RelStr ;
let V be non empty set ;
let H be Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V;
let F be Function;

pred F is_recursively_expressed_by H means :: WELLFND1:def 5
for x being Element of R holds F . x = H . (x,(F | ( the InternalRel of R -Seg x)));

end;

:: deftheorem defines is_recursively_expressed_by WELLFND1:def 5 :
for R being non empty RelStr
for V being non empty set
for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V
for F being Function holds
( F is_recursively_expressed_by H iff for x being Element of R holds F . x = H . (x,(F | ( the InternalRel of R -Seg x))) );

:: Well foundedness and existence

theorem :: WELLFND1:11

for R being non empty RelStr holds
( R is well_founded iff for V being non empty set
for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V ex F being Function of the carrier of R,V st F is_recursively_expressed_by H )

proof end;

:: Uniqueness implies well-foundedness

theorem :: WELLFND1:12

for R being non empty RelStr
for V being non trivial set st ( for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V
for F1, F2 being Function of the carrier of R,V st F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H holds
F1 = F2 ) holds
R is well_founded

proof end;

:: Well-foundedness implies uniqueness

theorem :: WELLFND1:13

for R being non empty well_founded RelStr
for V being non empty set
for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V
for F1, F2 being Function of the carrier of R,V st F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H holds
F1 = F2

proof end;

:: Well-foundedness and omega chains

definition

let R be RelStr ;
let f be sequence of R;

attr f is descending means :: WELLFND1:def 6
for n being Nat holds
( f . (n + 1) <> f . n & [(f . (n + 1)),(f . n)] in the InternalRel of R );

end;

:: deftheorem defines descending WELLFND1:def 6 :
for R being RelStr
for f being sequence of R holds
( f is descending iff for n being Nat holds
( f . (n + 1) <> f . n & [(f . (n + 1)),(f . n)] in the InternalRel of R ) );

:: omega chains

theorem :: WELLFND1:14

for R being non empty RelStr holds
( R is well_founded iff for f being sequence of R holds not f is descending )

proof end;