Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

## Algebra of Normal Forms

Andrzej Trybulec
Warsaw University, Bialystok

### Summary.

We mean by a normal form a finite set of ordered pairs of subsets of a fixed set that fulfils two conditions: elements of it consist of disjoint sets and element of it are incomparable w.r.t. inclusion. The underlying set corresponds to a set of propositional variables but it is arbitrary. The correspondents to a normal form of a formula, e.g. a disjunctive normal form is as follows. The normal form is the set of disjuncts and a disjunct is an ordered pair consisting of the sets of propositional variables that occur in the disjunct non-negated and negated. The requirement that the element of a normal form consists of disjoint sets means that contradictory disjuncts have been removed and the second condition means that the absorption law has been used to shorten the normal form. We construct a lattice $\langle {\Bbb N},\sqcup,\sqcap \rangle$, where $a \sqcup b = \mu (a \cup b)$ and $a \sqcap b = \mu c$, $c$ being set of all pairs $\langle X_1 \cup Y_1, X_2 \cup Y_2 \rangle$, $\langle X_1, X_2 \rangle \in a$ and $\langle Y_1,Y_2 \rangle \in b$, which consist of disjoiny sets. $\mu a$ denotes here the set of all minimal, w.r.t. inclusion, elements of $a$. We prove that the lattice of normal forms over a set defined in this way is distributive and that $\emptyset$ is the minimal element of it.

#### MML Identifier: NORMFORM

The terminology and notation used in this paper have been introduced in the following articles [6] [3] [9] [7] [10] [2] [1] [4] [8] [5] [11]

Contents (PDF format)

#### Bibliography

[1] Czeslaw Bylinski. Binary operations. Journal of Formalized Mathematics, 1, 1989.
[2] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[3] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[4] Andrzej Trybulec. Domains and their Cartesian products. Journal of Formalized Mathematics, 1, 1989.
[5] Andrzej Trybulec. Semilattice operations on finite subsets. Journal of Formalized Mathematics, 1, 1989.
[6] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[7] Andrzej Trybulec. Tuples, projections and Cartesian products. Journal of Formalized Mathematics, 1, 1989.
[8] Andrzej Trybulec and Agata Darmochwal. Boolean domains. Journal of Formalized Mathematics, 1, 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.
[11] Stanislaw Zukowski. Introduction to lattice theory. Journal of Formalized Mathematics, 1, 1989.