On Same Equivalents of Well-foundedness

Piotr Rudnicki

University of Alberta, Edmonton

Andrzej Trybulec

Warsaw University, Bialystok

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 ~[14]. 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.

This work was partially supported by NSERC Grant OGP9207 and NATO CRG 951368.

MML Identifier: WELLFND1

Contents (PDF format)

1. Preliminaries
2. Well Founded Relational Structures

Bibliography

[1] Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.

[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.

[3] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.

[4] Grzegorz Bancerek. Sequences of ordinal numbers. Journal of Formalized Mathematics, 1, 1989.

[5] Grzegorz Bancerek. The well ordering relations. Journal of Formalized Mathematics, 1, 1989.

[6] Grzegorz Bancerek. On powers of cardinals. Journal of Formalized Mathematics, 4, 1992.

[7] Grzegorz Bancerek. Directed sets, nets, ideals, filters, and maps. Journal of Formalized Mathematics, 8, 1996.

[8] Jozef Bialas. Group and field definitions. Journal of Formalized Mathematics, 1, 1989.

[9] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[10] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.

[11] Czeslaw Bylinski. Partial functions. Journal of Formalized Mathematics, 1, 1989.

[12] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.

[13] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.

[14] T. Franzen. Teaching mathematics through formalism: a few caveats. In D. Gries, editor, \em Proceedings of the DIMACS Symposium on Teaching Logic. DIMACS, 1996. On WWW: \tt http://dimacs.rutgers.edu/Workshops/Logic/program.html.

[15] Jaroslaw Kotowicz and Yuji Sakai. Properties of partial functions from a domain to the set of real numbers. Journal of Formalized Mathematics, 5, 1993.

[16] Beata Padlewska. Families of sets. Journal of Formalized Mathematics, 1, 1989.

[17] Jan Popiolek. Real normed space. Journal of Formalized Mathematics, 2, 1990.

[18] Andrzej Trybulec. Binary operations applied to functions. Journal of Formalized Mathematics, 1, 1989.

[19] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[20] Andrzej Trybulec. Function domains and Fr\aenkel operator. Journal of Formalized Mathematics, 2, 1990.

[21] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

[22] Wojciech A. Trybulec. Partially ordered sets. Journal of Formalized Mathematics, 1, 1989.

[23] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

[24] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[25] Edmund Woronowicz. Relations defined on sets. Journal of Formalized Mathematics, 1, 1989.