@MISC{WELLFND1.MIZ,
  AUTHOR = {Rudnicki, Piotr and Trybulec, Andrzej},
  TITLE = {On Same Equivalents of Well-foundedness},
  NOTE = {This work was partially supported by NSERC Grant OGP9207
		  and NATO CRG 951368.},
  SECTION1 = {Preliminaries},
  SECTION2 = {Well Founded Relational Structures},
  DAY = {25},
  MONTH = {February},
  YEAR = {1997},
  ADDRESS1 = {University of Alberta\\Edmonton},
  ADDRESS2 = {Warsaw University\\Bia{\l}ystok},
  SUMMARY = {Four statements equivalent to well-foundedness 
    (well-founded induction,
    existence of recursively defined functions,
    uniqueness of recursively defined functions, and
    absence of descending $\omega$-chains)
have been proved in Mizar and the proofs were mechanically checked for 
correctness.
It seems not to be widely known that the existence (without the uniqueness
assumption) of recursively defined functions implies well-foundedness.
In the proof we used regular cardinals, a fairly advanced notion
of set theory.
This work was inspired by T.~Franzen's paper ~\cite{tor96}.
Franzen's proofs were written by a mathematician having an argument
with a computer scientist.  We were curious about the effort needed to
formalize Franzen's proofs given the state of the Mizar Mathematical 
Library at that time (July 1996).
The formalization went quite smoothly once the mathematics was sorted out.}}

