Many-sorted Sets

Andrzej Trybulec

Warsaw University, Bialystok

Summary.

The article deals with parameterized families of sets. When treated in a similar way as sets (due to systematic overloading notation used for sets) they are called many sorted sets. For instance, if $x$ and $X$ are two many-sorted sets (with the same set of indices $I$) then relation $x \in X$ is defined as $\forall_{i \in I} x_i \in X_i$.\par I was prompted by a remark in a paper by Tarlecki and Wirsing: ``Throughout the paper we deal with many-sorted sets, functions, relations etc. ... We feel free to use any standard set-theoretic notation without explicit use of indices'' [6, p. 97]. The aim of this work was to check the feasibility of such approach in Mizar. It works.\par Let us observe some peculiarities: \begin{itemize} \item[-] empty set (i.e. the many sorted set with empty set of indices) belongs to itself (theorem 133), \item[-] we get two different inclusions $X \subseteq Y$ iff $\forall_{i \in I} X_i \subseteq Y_i$ and $X \sqsubseteq Y$ iff $\forall_x x \in X \Rightarrow x \in Y$ equivalent only for sets that yield non empty values. \end{itemize} Therefore the care is advised.

MML Identifier: PBOOLE

Contents (PDF format)

1. Preliminaries
2. Lattice Properties of Many Sorted Sets
3. The Empty Many Sorted Set
4. The Difference and the Symmetric Difference
5. Meeting and Overlapping
6. The Second Inclusion
7. Non empty set of sorts
8. Non Empty and Non-empty Many Sorted Sets

Bibliography

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

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

[3] Czeslaw Bylinski. A classical first order language. Journal of Formalized Mathematics, 2, 1990.

[4] Katarzyna Jankowska. Matrices. Abelian group of matrices. Journal of Formalized Mathematics, 3, 1991.

[5] Yatsuka Nakamura and Andrzej Trybulec. A mathematical model of CPU. Journal of Formalized Mathematics, 4, 1992.

[6] Andrzej Tarlecki and Martin Wirsing. Continuous abstract data types. \em Fundamenta Informaticae, 9(1):95--125, 1986.

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

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

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

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