Editing Heyting algebra (section)

== Properties ==

===General properties===
The ordering <math>\le</math> on a Heyting algebra ''H'' can be recovered from the operation → as follows: for any elements ''a'', ''b'' of ''H'', <math>a \le b</math> if and only if ''a''→''b'' = 1.

In contrast to some [[many-valued logic]]s, Heyting algebras share the following property with Boolean algebras: if negation has a [[fixed point (mathematics)|fixed point]] (i.e. ¬''a'' = ''a'' for some ''a''), then the Heyting algebra is the trivial one-element Heyting algebra.

===Provable identities===
Given a formula <math>F(A_1, A_2,\ldots, A_n)</math> of propositional calculus (using, in addition to the variables, the connectives <math>\land, \lor, \lnot, \to</math>, and the constants 0 and 1), it is a fact, proved early on in any study of Heyting algebras, that the following two conditions are equivalent:
# The formula ''F'' is provably true in intuitionist propositional calculus.
# The identity <math>F(a_1, a_2,\ldots, a_n) = 1</math> is true for any Heyting algebra ''H'' and any elements <math>a_1, a_2,\ldots, a_n \in H</math>.
The metaimplication {{nowrap|1 ⇒ 2}} is extremely useful and is the principal practical method for proving identities in Heyting algebras. In practice, one frequently uses the [[deduction theorem]] in such proofs.

Since for any ''a'' and ''b'' in a Heyting algebra ''H'' we have <math>a \le b</math> if and only if ''a''→''b'' = 1, it follows from {{nowrap|1 ⇒ 2}} that whenever a formula ''F''→''G'' is provably true, we have <math>F(a_1, a_2,\ldots, a_n) \le G(a_1, a_2,\ldots, a_n)</math> for any Heyting algebra ''H'', and any elements <math>a_1, a_2,\ldots, a_n \in H</math>. (It follows from the deduction theorem that ''F''→''G'' is provable (unconditionally) if and only if ''G'' is provable from ''F'', that is, if ''G'' is a provable consequence of ''F''.) In particular, if ''F'' and ''G'' are provably equivalent, then <math>F(a_1, a_2,\ldots, a_n) = G(a_1, a_2,\ldots, a_n)</math>, since ≤ is an order relation.

1 ⇒ 2 can be proved by examining the logical axioms of the system of proof and verifying that their value is 1 in any Heyting algebra, and then verifying that the application of the rules of inference to expressions with value 1 in a Heyting algebra results in expressions with value 1. For example, let us choose the system of proof having [[modus ponens]] as its sole rule of inference, and whose axioms are the Hilbert-style ones given at [[Intuitionistic logic#Axiomatization]]. Then the facts to be verified follow immediately from the axiom-like definition of Heyting algebras given above.

1 ⇒ 2 also provides a method for proving that certain propositional formulas, though [[tautology (logic)|tautologies]] in classical logic, ''cannot'' be proved in intuitionist propositional logic. In order to prove that some formula <math>F(A_1, A_2,\ldots, A_n)</math> is not provable, it is enough to exhibit a Heyting algebra ''H'' and elements <math>a_1, a_2,\ldots, a_n \in H</math> such that <math>F(a_1, a_2,\ldots, a_n) \ne 1</math>.

If one wishes to avoid mention of logic, then in practice it becomes necessary to prove as a lemma a version of the deduction theorem valid for Heyting algebras: for any elements ''a'', ''b'' and ''c'' of a Heyting algebra ''H'', we have <math>(a \land b) \to c = a \to (b \to c)</math>.

For more on the metaimplication 2 ⇒ 1, see the section "[[#Universal constructions|Universal constructions]]" below.

===Distributivity===
Heyting algebras are always [[distributivity (order theory)|distributive]]. Specifically, we always have the identities
#<math>a \wedge (b \vee c) = (a \wedge b) \vee (a \wedge c)</math>
#<math>a \vee (b \wedge c) = (a \vee b) \wedge (a \vee c)</math>

The distributive law is sometimes stated as an axiom, but in fact it follows from the existence of relative pseudo-complements. The reason is that, being the lower adjoint of a [[Galois connection]], <math>\wedge</math> preserves all existing [[suprema]]. Distributivity in turn is just the preservation of binary suprema by <math>\wedge</math>.

By a similar argument, the following [[infinite distributive law]] holds in any complete Heyting algebra:

:<math>x\wedge\bigvee Y = \bigvee \{x\wedge y \mid y \in Y\}</math>

for any element ''x'' in ''H'' and any subset ''Y'' of ''H''. Conversely, any complete lattice satisfying the above infinite distributive law is a complete Heyting algebra, with
:<math>a\to b=\bigvee\{c\mid a\land c\le b\}</math>
being its relative pseudo-complement operation.

===Regular and complemented elements===
An element ''x'' of a Heyting algebra ''H'' is called '''regular''' if either of the following equivalent conditions hold:
#''x'' =  ¬¬''x''.
#''x'' =  ¬''y'' for some ''y'' in ''H''.
The equivalence of these conditions can be restated simply as the identity ¬¬¬''x'' = ¬''x'', valid for all ''x'' in ''H''.

Elements ''x'' and ''y'' of a Heyting algebra ''H'' are called '''complements''' to each other if ''x''∧''y'' = 0 and ''x''∨''y'' = 1. If it exists, any such ''y'' is unique and must in fact be equal to ¬''x''. We call an element ''x'' '''complemented''' if it admits a complement. It is true that ''if'' ''x'' is complemented, then so is ¬''x'', and then ''x'' and ¬''x'' are complements to each other. However, confusingly, even if ''x'' is not complemented, ¬''x'' may nonetheless have a complement (not equal to ''x''). In any Heyting algebra, the elements 0 and 1 are complements to each other. For instance, it is possible that ¬''x'' is 0 for every ''x'' different from 0, and 1 if ''x'' = 0, in which case 0 and 1 are the only regular elements.

Any complemented element of a Heyting algebra is regular, though the converse is not true in general. In particular, 0 and 1 are always regular.

For any Heyting algebra ''H'', the following conditions are equivalent:
# ''H'' is a [[Boolean algebra (structure)|Boolean algebra]];
# every ''x'' in ''H'' is regular;<ref>Rutherford (1965), Th.26.2 p.78.</ref>
# every ''x'' in ''H'' is complemented.<ref>Rutherford (1965), Th.26.1 p.78.</ref>
In this case, the element {{nowrap|1=''a''→''b''}} is equal to {{nowrap|1=¬''a'' ∨ ''b''.}}

The regular (respectively complemented) elements of any Heyting algebra ''H'' constitute a Boolean algebra ''H''<sub>reg</sub> (respectively ''H''<sub>comp</sub>), in which the operations ∧, ¬ and →, as well as the constants 0 and 1, coincide with those of ''H''. In the case of ''H''<sub>comp</sub>, the operation ∨ is also the same, hence ''H''<sub>comp</sub> is a subalgebra of ''H''. In general however, ''H''<sub>reg</sub> will not be a subalgebra of ''H'', because its join operation ∨<sub>reg</sub> may be different from ∨. For {{nowrap|1=''x'', ''y'' ∈ ''H''<sub>reg</sub>,}} we have {{nowrap|1=''x'' ∨<sub>reg</sub> ''y'' = ¬(¬''x'' ∧ ¬''y'').}} See below for necessary and sufficient conditions in order for ∨<sub>reg</sub> to coincide with ∨.

===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.