Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991 Association of Mizar Users

## Algebra of Normal Forms Is a Heyting Algebra

Andrzej Trybulec
Warsaw University, Bialystok

### Summary.

We prove that the lattice of normal forms over an arbitrary set, introduced in [12], is an implicative lattice. The relative pseudo-complement $\alpha\Rightarrow\beta$ is defined as $\bigsqcup_{\alpha_1\cup\alpha_2=\alpha}-\alpha_1\sqcap \alpha_2\rightarrowtail\beta$, where $-\alpha$ is the pseudo-complement of $\alpha$ and $\alpha\rightarrowtail\beta$ is a rather strong implication introduced in this paper.

Partially supported by RPBP.III-24.B1.

#### MML Identifier: HEYTING1

The terminology and notation used in this paper have been introduced in the following articles [10] [6] [16] [17] [4] [5] [2] [11] [3] [7] [15] [8] [18] [13] [14] [9] [12] [1]

Contents (PDF format)

#### Bibliography

[1] Grzegorz Bancerek. Filters --- part I. Journal of Formalized Mathematics, 2, 1990.
[2] Czeslaw Bylinski. Basic functions and operations on functions. Journal of Formalized Mathematics, 1, 1989.
[3] Czeslaw Bylinski. Binary operations. Journal of Formalized Mathematics, 1, 1989.
[4] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[5] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[6] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[7] Andrzej Trybulec. Binary operations applied to functions. Journal of Formalized Mathematics, 1, 1989.
[8] Andrzej Trybulec. Domains and their Cartesian products. Journal of Formalized Mathematics, 1, 1989.
[9] Andrzej Trybulec. Semilattice operations on finite subsets. Journal of Formalized Mathematics, 1, 1989.
[10] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[11] Andrzej Trybulec. Tuples, projections and Cartesian products. Journal of Formalized Mathematics, 1, 1989.
[12] Andrzej Trybulec. Algebra of normal forms. Journal of Formalized Mathematics, 2, 1990.
[13] Andrzej Trybulec. Finite join and finite meet, and dual lattices. Journal of Formalized Mathematics, 2, 1990.
[14] Andrzej Trybulec. Function domains and Fr\aenkel operator. Journal of Formalized Mathematics, 2, 1990.
[15] Andrzej Trybulec and Agata Darmochwal. Boolean domains. Journal of Formalized Mathematics, 1, 1989.
[16] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[17] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[18] Stanislaw Zukowski. Introduction to lattice theory. Journal of Formalized Mathematics, 1, 1989.