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

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.