:: On same equivalents of well-foundedness
:: by Piotr Rudnicki and Andrzej Trybulec
::
:: Received February 25, 1997
:: Copyright (c) 1997-2016 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 FUNCT_1, PARTFUN1, TARSKI, RELAT_1, SUBSET_1, CARD_1, XBOOLE_0,
CARD_5, ORDINAL2, ORDERS_2, WELLORD1, STRUCT_0, WAYBEL_0, XXREAL_0,
ZFMISC_1, SETFAM_1, ORDINAL1, CARD_2, FINSET_1, FUNCOP_1, FUNCT_4, NAT_1,
ARYTM_3, NUMBERS, WELLFND1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
RELAT_1, FUNCT_1, BINOP_1, SETFAM_1, DOMAIN_1, XCMPLX_0, NAT_1, STRUCT_0,
RELSET_1, PARTFUN1, FUNCT_2, FUNCT_4, FUNCOP_1, WELLORD1, ORDINAL2,
FINSET_1, CARD_2, ORDERS_2, CARD_5, RFUNCT_3, WAYBEL_0;
constructors SETFAM_1, WELLORD1, BINOP_1, FUNCT_4, ORDINAL2, CARD_2, REALSET1,
CARD_5, RFUNCT_3, WAYBEL_0, RELSET_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCOP_1,
CARD_1, CARD_5, STRUCT_0, WAYBEL_0, FUNCT_1, ZFMISC_1, XCMPLX_0, NAT_1;
requirements NUMERALS, SUBSET, BOOLE;
begin :: Preliminaries
:: General preliminaries
theorem :: 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;
scheme :: WELLFND1:sch 1
PFSeparation {X, Y() -> set, P[set]}: ex PFS being Subset of PFuncs(X(), Y()
) st for pfs being PartFunc of X(), Y() holds pfs in PFS iff P[pfs];
:: Cardinals
registration
let X be set;
cluster nextcard X -> non empty;
end;
registration
cluster regular for Aleph;
end;
theorem :: WELLFND1:2
for M being regular Aleph, X being set st X c= M & card X in M
holds sup X in M;
:: Relational structures
theorem :: WELLFND1:3
for R being RelStr, x being set holds (the InternalRel of R)-Seg
x c= the carrier of R;
definition
let R be RelStr, X be Subset of R;
redefine attr X is lower means
:: WELLFND1:def 1
for x, y being object st x in X & [y, x] in the InternalRel of R
holds y in X;
end;
theorem :: WELLFND1:4
for R being RelStr, X being Subset of R, x being set st X is
lower & x in X holds (the InternalRel of R)-Seg x c= X;
theorem :: WELLFND1:5
for R being RelStr, X being lower Subset of R, Y being Subset of
R, x being set st Y = X \/ {x} & (the InternalRel of R)-Seg x c= X holds Y is
lower;
begin :: Well-founded relational structures
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;
registration
cluster non empty well_founded for RelStr;
end;
definition
let R be RelStr, X be Subset of R;
attr X is well_founded means
:: WELLFND1:def 3
the InternalRel of R is_well_founded_in X;
end;
registration
let R be RelStr;
cluster well_founded for Subset of R;
end;
definition
let R be RelStr;
func well_founded-Part R -> Subset of R means
:: WELLFND1:def 4
it = union {S where S is Subset of R : S is well_founded lower};
end;
registration
let R be RelStr;
cluster well_founded-Part R -> lower well_founded;
end;
theorem :: WELLFND1:6
for R being non empty RelStr, x be Element of R holds {x} is
well_founded Subset of R;
theorem :: WELLFND1:7
for R being RelStr, X, Y being well_founded Subset of R st X is
lower holds X \/ Y is well_founded Subset of R;
theorem :: WELLFND1:8
for R being RelStr holds R is well_founded iff well_founded-Part
R = the carrier of R;
theorem :: WELLFND1:9
for R being non empty RelStr, x being Element of R st (the
InternalRel of R)-Seg x c= well_founded-Part R holds x in well_founded-Part R
;
:: Well-founded induction
scheme :: WELLFND1:sch 2
WFMin {R() -> non empty RelStr, x() -> Element of R(), P[set]}: ex x being
Element of R() st P[x] & not ex y being Element of R() st x <> y & P[y] & [y,x]
in the InternalRel of R()
provided
P[x()] and
R() is well_founded;
:: WF iff WFInduction
theorem :: 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;
scheme :: WELLFND1:sch 3
WFInduction {R() -> non empty RelStr, P[set]}: for x being Element of R()
holds P[x]
provided
for x being Element of R() st for y being Element of R() st y <> x &
[y,x] in the InternalRel of R() holds P[y] holds P[x] and
R() is well_founded;
:: Well-foundedness and recursive definitions
definition
let R be non empty RelStr, V be non empty set, H be Function of [:the
carrier of R, PFuncs(the carrier of R, V):], V, 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;
:: 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, 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;
:: Uniqueness implies well-foundedness
theorem :: WELLFND1:12
for R being non empty RelStr, V being non trivial set st for H being
Function of [:the carrier of R, PFuncs(the carrier of R, V):], V, 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;
:: Well-foundedness implies uniqueness
theorem :: WELLFND1:13
for R being non empty well_founded RelStr, V being non empty set, H
being Function of [:the carrier of R, PFuncs(the carrier of R, V):], V, 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;
:: Well-foundedness and omega chains
definition
let R be RelStr, 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;
:: omega chains
theorem :: WELLFND1:14
for R being non empty RelStr holds R is well_founded iff not ex f
being sequence of R st f is descending;