Editing Heyting algebra (section)

== Formal definition ==
A Heyting algebra ''H'' is a [[lattice (order)#As partially ordered set|bounded lattice]] such that for all ''a'' and ''b'' in ''H'' there is a greatest element ''x'' of ''H'' such that

:<math> a \wedge x \le b.</math>

This element is the '''relative pseudo-complement''' of ''a'' with respect to ''b'', and is denoted ''a''→''b''. We write 1 and 0 for the largest and the smallest element of ''H'', respectively.

In any Heyting algebra, one defines the '''[[pseudo-complement]]''' ¬''a'' of any element ''a'' by setting  ¬''a'' = (''a''→0). By definition, <math>a\wedge \lnot a = 0</math>, and ¬''a'' is the largest element having this property. However, it is not in general true that <math>a\vee\lnot a=1</math>, thus ¬ is only a pseudo-complement, not a true [[complement (set theory)|complement]], as would be the case in a Boolean algebra.

A '''[[complete Heyting algebra]]''' is a Heyting algebra that is a [[complete lattice]].

A '''subalgebra''' of a Heyting algebra ''H'' is a subset ''H''<sub>1</sub> of ''H'' containing 0 and 1 and closed under the operations ∧, ∨ and →. It follows that it is also closed under ¬. A subalgebra is made into a Heyting algebra by the induced operations.