Volume 9, 1997

University of Bialystok

Copyright (c) 1997 Association of Mizar Users

**Artur Kornilowicz**- Warsaw University, Bialystok

- \newcommand \pred[1]{${\cal P} #1$} In this article Birkhoff Variety Theorem for many sorted algebras is proved. A class of algebras is represented by predicate \pred{}. Notation \pred{[A]}, where $A$ is an algebra, means that $A$ is in class \pred{}. All algebras in our class are many sorted over many sorted signature $S$. The properties of varieties: \begin{itemize} \itemsep-3pt \item a class \pred{ } of algebras is abstract \item a class \pred{ } of algebras is closed under subalgebras \item a class \pred{ } of algebras is closed under congruences \item a class \pred{ } of algebras is closed under products \end{itemize} are published in this paper as: \begin{itemize} \itemsep-3pt \item for all non-empty algebras $A$, $B$ over $S$ such that $A$ and $B$ are\_isomorphic and \pred{[A]} holds \pred{[B]} \item for every non-empty algebra $A$ over $S$ and for strict non-empty subalgebra $B$ of $A$ such that \pred{[A]} holds \pred{[B]} \item for every non-empty algebra $A$ over $S$ and for every congruence $R$ of $A$ such that \pred{[A]} holds \pred{[A\slash R]} \item Let $I$ be a set and $F$ be an algebra family of $I$ over ${\cal A}.$ Suppose that for every set $i$ such that $i \in I$ there exists an algebra $A$ over ${\cal A}$ such that $A = F(i)$ and ${\cal P}[A]$. Then${\cal P}[\prod F]$. \end{itemize} This paper is formalization of parts of [21].

Contents (PDF format)

- [1]
Grzegorz Bancerek.
K\"onig's theorem.
*Journal of Formalized Mathematics*, 2, 1990. - [2]
Ewa Burakowska.
Subalgebras of many sorted algebra. Lattice of subalgebras.
*Journal of Formalized Mathematics*, 6, 1994. - [3]
Czeslaw Bylinski.
Functions and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [4]
Czeslaw Bylinski.
Functions from a set to a set.
*Journal of Formalized Mathematics*, 1, 1989. - [5]
Czeslaw Bylinski.
Some basic properties of sets.
*Journal of Formalized Mathematics*, 1, 1989. - [6]
Artur Kornilowicz.
Extensions of mappings on generator set.
*Journal of Formalized Mathematics*, 7, 1995. - [7]
Artur Kornilowicz.
Equations in many sorted algebras.
*Journal of Formalized Mathematics*, 9, 1997. - [8]
Malgorzata Korolkiewicz.
Homomorphisms of many sorted algebras.
*Journal of Formalized Mathematics*, 6, 1994. - [9]
Malgorzata Korolkiewicz.
Many sorted quotient algebra.
*Journal of Formalized Mathematics*, 6, 1994. - [10]
Beata Madras.
Product of family of universal algebras.
*Journal of Formalized Mathematics*, 5, 1993. - [11]
Beata Madras.
Products of many sorted algebras.
*Journal of Formalized Mathematics*, 6, 1994. - [12]
Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto.
Preliminaries to circuits, I.
*Journal of Formalized Mathematics*, 6, 1994. - [13]
Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto.
Preliminaries to circuits, II.
*Journal of Formalized Mathematics*, 6, 1994. - [14]
Beata Padlewska.
Families of sets.
*Journal of Formalized Mathematics*, 1, 1989. - [15]
Beata Perkowska.
Free many sorted universal algebra.
*Journal of Formalized Mathematics*, 6, 1994. - [16]
Andrzej Trybulec.
Tarski Grothendieck set theory.
*Journal of Formalized Mathematics*, Axiomatics, 1989. - [17]
Andrzej Trybulec.
Many-sorted sets.
*Journal of Formalized Mathematics*, 5, 1993. - [18]
Andrzej Trybulec.
Many sorted algebras.
*Journal of Formalized Mathematics*, 6, 1994. - [19]
Andrzej Trybulec.
Subsets of real numbers.
*Journal of Formalized Mathematics*, Addenda, 2003. - [20]
Zinaida Trybulec.
Properties of subsets.
*Journal of Formalized Mathematics*, 1, 1989. - [21] Wolfgang Wechler. \em Universal Algebra for Computer Scientists, volume 25 of \em EATCS Monographs on TCS. Springer--Verlag, 1992.
- [22]
Edmund Woronowicz.
Relations and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [23]
Edmund Woronowicz.
Relations defined on sets.
*Journal of Formalized Mathematics*, 1, 1989.

[ Download a postscript version, MML identifier index, Mizar home page]