complete Heyting algebra


A Heyting algebra that is also a complete latticeMathworldPlanetmath is called a complete Heyting algebra. In the following, we give a latticeMathworldPlanetmath characterizationMathworldPlanetmath of complete Heyting algebras without the relative pseudocomplementation operator .

Proposition 1.

Let H be a complete Heyting algebra, then

xy={zzxy}

for any x,yH, and

xA=(xA),

where xA:={xyyA}, for any xH, and any subset A of H.

Proof.

We first prove the identityPlanetmathPlanetmath xA=(xA). For any yH, we have xAy iff Axy iff axy for all aA iff xay for all aA iff (xA)y, hence xA=(xA).

Next, we show xy={zzxy}. For any aH, we have axy iff axy iff a{zzxy} iff a{zzxy}. ∎

The converseMathworldPlanetmath of the above is also true.

Proposition 2.

Let H be a complete lattice such that

xA=(xA),

where xA:={xyyA}, for any xH, and any subset A of H. Then for any x,yH, defining

xy:={zzxy}

turns H into a complete Heyting algebra.

Proof.

We want to show that axy iff axy for any aH: axy iff a{zzxy}. So xax{zzxy}={xzzxy}{y}=y

From this, one readily concludes that any finite distributive latticeMathworldPlanetmath is Heyting.

Remark. Since any complete lattice is bounded, a completePlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath Brouwerian lattice is a complete Heyting algebra. A complete Heyting algebra is also called a frame.

Title complete Heyting algebra
Canonical name CompleteHeytingAlgebra
Date of creation 2013-03-22 19:31:42
Last modified on 2013-03-22 19:31:42
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 10
Author CWoo (3771)
Entry type Definition
Classification msc 03G10
Classification msc 06D20
Related topic Locale