−Table of Contents
Lattices
Abbreviation: Lat
Definition
A \emph{lattice} is a structure L=⟨L,∨,∧⟩, where ∨ and ∧ are infix binary operations called the \emph{join} and \emph{meet}, such that
∨,∧ are associative: (x∨y)∨z=x∨(y∨z), (x∧y)∧z=x∧(y∧z)
∨,∧ are commutative: x∨y=y∨x, x∧y=y∧x
∨,∧ are absorbtive: (x∨y)∧x=x, (x∧y)∨x=x.
Remark: It follows that ∨ and ∧ are idempotent: x∨x=x, x∧x=x.
This definition shows that lattices form a variety.
A partial order ≤ is definable in any lattice by x≤y⟺x∧y=x, or equivalently by x≤y⟺x∨y=y.
Morphisms
Let L and M be lattices. A morphism from L to M is a function h:L→M that is a homomorphism:
h(x∨y)=h(x)∨h(y), h(x∧y)=h(x)∧h(y)
Definition
A \emph{lattice} is a structure L=⟨L,∨,∧⟩ of type ⟨2,2⟩ such that
⟨L,∨⟩ and ⟨L,∧⟩ are semilattices, and
∨,∧ are absorbtive: (x∨y)∧x=x, (x∧y)∨x=x
Definition
A \emph{lattice} is a structure L=⟨L,≤⟩ that is a partially ordered set in which all elements x,y∈L have a
least upper bound: z=x∨y⟺x≤z, y≤z and ∀w (x≤w, y≤w⟹z≤w) and a
greatest lower bound: z=x∧y⟺z≤x, z≤y and ∀w (w≤x, w≤y⟹w≤z)
Definition
A \emph{lattice} is a structure L=⟨L,∨,∧,≤⟩ such that ⟨L,≤⟩ is a partially ordered set and the following quasiequations hold:
∨-left: x≤z and y≤z ⟹x∨y≤z
∨-right: z≤x⟹z≤x∨y, z≤y⟹z≤x∨y
∧-right: z≤x and z≤y⟹z≤x∧y
∧-left: x≤z⟹x∧y≤z, y≤z⟹x∧y≤z
Remark: These quasiequations give a cut-free Gentzen system to decide the equational theory of lattices.
Examples
Example 1: ⟨P(S),∪,∩,⊆⟩, the collection of subsets of a sets S, ordered by inclusion.
Basic results
Properties
Classtype | variety |
---|---|
Equational theory | decidable in polynomial time |
Quasiequational theory | decidable |
First-order theory | undecidable |
Locally finite | no |
Residual size | unbounded |
Congruence distributive | yes 1) |
Congruence modular | yes |
Congruence n-permutable | no |
Congruence regular | no |
Congruence uniform | no |
Congruence extension property | no |
Definable principal congruences | no |
Equationally def. pr. cong. | no |
Amalgamation property | yes |
Strong amalgamation property | yes 2) |
Epimorphisms are surjective | yes |
Finite members
f(1)=1f(2)=1f(3)=1f(4)=2f(5)=5f(6)=15f(7)=53f(8)=222f(9)=1078f(10)=5994f(11)=37622f(12)=262776f(13)=2018305f(14)=16873364f(15)=152233518f(16)=1471613387f(17)=15150569446f(18)=165269824761f(19)=19019106255783)4)