Volume 12, 2000

University of Bialystok

Copyright (c) 2000 Association of Mizar Users

**Adam Grabowski**- University of Bialystok

- In [12] we proved that the lattice of substitutions, as defined in [10], is a Heyting lattice (i.e. it is pseudo-complemented and it has the zero element). We show that the lattice needs not to be complete. Obviously, the example has to be infinite, namely we can take the set of natural numbers as variables and a singleton as a set of constants. The incompleteness has been shown for lattices of substitutions defined in terms of [23] and relational structures [20].

- Preliminaries
- Poset of Substitutions
- The Incompleteness

- [1]
Grzegorz Bancerek.
The fundamental properties of natural numbers.
*Journal of Formalized Mathematics*, 1, 1989. - [2]
Grzegorz Bancerek.
Curried and uncurried functions.
*Journal of Formalized Mathematics*, 2, 1990. - [3]
Grzegorz Bancerek.
Complete lattices.
*Journal of Formalized Mathematics*, 4, 1992. - [4]
Grzegorz Bancerek.
Bounds in posets and relational substructures.
*Journal of Formalized Mathematics*, 8, 1996. - [5]
Grzegorz Bancerek and Krzysztof Hryniewiecki.
Segments of natural numbers and finite sequences.
*Journal of Formalized Mathematics*, 1, 1989. - [6]
Czeslaw Bylinski.
Functions and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [7]
Czeslaw Bylinski.
Partial functions.
*Journal of Formalized Mathematics*, 1, 1989. - [8]
Czeslaw Bylinski.
Some basic properties of sets.
*Journal of Formalized Mathematics*, 1, 1989. - [9]
Agata Darmochwal.
Finite sets.
*Journal of Formalized Mathematics*, 1, 1989. - [10]
Adam Grabowski.
Lattice of substitutions.
*Journal of Formalized Mathematics*, 9, 1997. - [11]
Adam Grabowski.
Lattice of substitutions is a Heyting algebra.
*Journal of Formalized Mathematics*, 10, 1998. - [12]
Adam Grabowski.
The incompleteness of the lattice of substitutions.
*Journal of Formalized Mathematics*, 12, 2000. - [13]
Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto.
Preliminaries to circuits, I.
*Journal of Formalized Mathematics*, 6, 1994. - [14]
Piotr Rudnicki and Andrzej Trybulec.
Abian's fixed point theorem.
*Journal of Formalized Mathematics*, 9, 1997. - [15]
Andrzej Trybulec.
Domains and their Cartesian products.
*Journal of Formalized Mathematics*, 1, 1989. - [16]
Andrzej Trybulec.
Tarski Grothendieck set theory.
*Journal of Formalized Mathematics*, Axiomatics, 1989. - [17]
Andrzej Trybulec.
Tuples, projections and Cartesian products.
*Journal of Formalized Mathematics*, 1, 1989. - [18]
Andrzej Trybulec.
Subsets of real numbers.
*Journal of Formalized Mathematics*, Addenda, 2003. - [19]
Andrzej Trybulec and Agata Darmochwal.
Boolean domains.
*Journal of Formalized Mathematics*, 1, 1989. - [20]
Wojciech A. Trybulec.
Partially ordered sets.
*Journal of Formalized Mathematics*, 1, 1989. - [21]
Zinaida Trybulec.
Properties of subsets.
*Journal of Formalized Mathematics*, 1, 1989. - [22]
Edmund Woronowicz.
Relations and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [23]
Stanislaw Zukowski.
Introduction to lattice theory.
*Journal of Formalized Mathematics*, 1, 1989.

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