Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000 Association of Mizar Users

The Incompleteness of the Lattice of Substitutions


Adam Grabowski
University of Bialystok

Summary.

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].

MML Identifier: HEYTING3

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

Contents (PDF format)

  1. Preliminaries
  2. Poset of Substitutions
  3. The Incompleteness

Bibliography

[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.

Received July 17, 2000

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