Journal of Formalized Mathematics
Volume 9, 1997
University of Bialystok
Copyright (c) 1997 Association of Mizar Users

## Birkhoff Theorem for Many Sorted Algebras

Artur Kornilowicz
Warsaw University, Bialystok

### Summary.

\newcommand \pred{${\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 .

#### MML Identifier: BIRKHOFF

The terminology and notation used in this paper have been introduced in the following articles                      

Contents (PDF format)

#### Bibliography

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