Heyting algebra is a bounded semi-lattice with implication which should satisfy the following law:

x ∧ a ≤ b ⇔ x ≤ (a ⇒ b)

We also require that a Heyting algebra is a distributive lattice, which means any of the two equivalent conditions holds:

a ∧ (b ∨ c) = a ∧ b ∨ a ∧ c

a ∨ (b ∧ c) = (a ∨ b) ∧ (a ∨ c)

This means a ⇒ b is an exponential object, which makes any Heyting algebra a cartesian closed category. This means that Curry isomorphism holds (which takes a form of an actual equality):

a ⇒ (b ⇒ c) = (a ∧ b) ⇒ c

Some other useful properties of Heyting algebras:

(a ⇒ b) ∧ a ≤ b

b ≤ a ⇒ a ∧ b

a ≤ b  iff a ⇒ b = ⊤

b ≤ b' then a ⇒ b ≤ a ⇒ b'

a'≤ a  then a' ⇒ b ≤ a ⇒ b

not (a ∧ b) = not (a ∨ b)

not (a ∨ b) = not a ∧ not b

implies is an alias for ==>

iff is an alias for <=>

Every Heyting algebra contains a Boolean algebra. toBoolean maps onto it; moreover it is a monad (Heyting algebra is a category as every poset is) which preserves finite infima.

Boolean algebra is a Heyting algebra which negation satisfies the law of excluded middle, i.e. either of the following:

not . not == not

or

x ∨ not x == top

Another characterisation of Boolean algebras is as complemented distributive lattices where the complement satisfies the following three properties:

(not a) ∧ a == bottom and (not a) ∨ a == top -- excluded middle law

not (not a) == a                             -- involution law

a ≤ b ⇒ not b ≤ not a                        -- order-reversing