Editing Heyting algebra (section)

===The De Morgan laws in a Heyting algebra===
One of the two [[De Morgan laws]] is satisfied in every Heyting algebra, namely

:<math>\forall x,y \in H: \qquad \lnot(x \vee y)=\lnot x \wedge \lnot y.</math>

However, the other De Morgan law does not always hold. We have instead a weak de Morgan law:

:<math>\forall x,y \in H: \qquad \lnot(x \wedge y)= \lnot \lnot (\lnot x \vee \lnot y).</math>

The following statements are equivalent for all Heyting algebras ''H'':
#''H'' satisfies both De Morgan laws,
#<math>\lnot(x \wedge y)=\lnot x \vee \lnot y \mbox{ for all } x, y \in H,</math>
#<math>\lnot(x \wedge y)=\lnot x \vee \lnot y \mbox{ for all regular } x, y \in H,</math>
#<math>\lnot\lnot (x \vee y) = \lnot\lnot x \vee \lnot\lnot y \mbox{ for all } x, y \in H,</math>
#<math>\lnot\lnot (x \vee y) = x \vee y \mbox{ for all regular } x, y \in H,</math>
#<math>\lnot(\lnot x \wedge \lnot y) = x \vee y \mbox{ for all regular } x, y \in H,</math>
#<math>\lnot x \vee \lnot\lnot x = 1 \mbox{ for all } x \in H.</math>
Condition 2 is the other De Morgan law. Condition 6 says that the join operation ∨<sub>reg</sub> on the Boolean algebra ''H''<sub>reg</sub> of regular elements of ''H'' coincides with the operation ∨ of ''H''. Condition 7 states that every regular element is complemented, i.e., ''H''<sub>reg</sub> = ''H''<sub>comp</sub>.

We prove the equivalence. Clearly the metaimplications {{nowrap|1 ⇒ 2,}} {{nowrap|2 ⇒ 3}} and {{nowrap|4 ⇒ 5}} are trivial. Furthermore, {{nowrap|3 ⇔ 4}} and {{nowrap|5 ⇔ 6}} result simply from the first De Morgan law and the definition of regular elements. We show that {{nowrap|6 ⇒ 7}} by taking ¬''x'' and ¬¬''x'' in place of ''x'' and ''y'' in 6 and using the identity {{nowrap|''a'' &and; ¬''a'' {{=}} 0.}} Notice that {{nowrap|2 ⇒ 1}} follows from the first De Morgan law, and {{nowrap|7 ⇒ 6}} results from the fact that the join operation  ∨ on the subalgebra ''H''<sub>comp</sub> is just the restriction of ∨ to ''H''<sub>comp</sub>, taking into account the characterizations we have given of conditions 6 and 7. The metaimplication {{nowrap|5 ⇒ 2}} is a trivial consequence of the weak De Morgan law, taking ¬''x'' and ¬''y'' in place of ''x'' and ''y'' in 5.

Heyting algebras satisfying the above properties are related to [[Intermediate logic|De Morgan logic]] in the same way Heyting algebras in general are related to intuitionist logic.