Editing Heyting algebra

{{Short description|Algebraic structure used in logic}}
In [[mathematics]], a '''Heyting algebra''' (also known as '''pseudo-Boolean algebra'''<ref>{{Cite web|url=https://www.encyclopediaofmath.org/index.php/Pseudo-Boolean_algebra|title = Pseudo-Boolean algebra - Encyclopedia of Mathematics}}</ref>) is a [[Lattice (order)#Bounded lattice|bounded lattice]] (with join and meet operations written ∨ and ∧ and with least element 0 and greatest element 1) equipped with a binary operation ''a'' → ''b'' called ''implication'' such that (''c'' ∧ ''a'') ≤ ''b'' is equivalent to ''c'' ≤ (''a'' → ''b''). From a logical standpoint, ''A'' → ''B'' is by this definition the weakest proposition for which [[modus ponens]], the inference rule ''A'' → ''B'', ''A'' ⊢ ''B'', is [[Soundness#Logical systems|sound]].  Like [[Boolean algebra (structure)|Boolean algebras]], Heyting algebras form a [[Variety (universal algebra)|variety]] axiomatizable with finitely many equations. Heyting algebras were introduced in 1930 by [[Arend Heyting]] to formalize [[intuitionistic logic]]. <ref name="Heyting1930">{{citation|last=Heyting|first= A.
|title=Die formalen Regeln der intuitionistischen Logik. I, II, III|jfm= 56.0823.01
|journal=Sitzungsberichte Akad. Berlin |year=1930|pages= 42–56, 57–71, 158–169 }}</ref>

Heyting algebras are [[distributive lattice|distributive lattices]].  Every Boolean algebra is a Heyting algebra when ''a'' → ''b'' is defined as ¬''a'' ∨ ''b'', as is every [[Completeness (order theory)|complete]] [[distributive lattice]] satisfying a one-sided [[Distributivity (order theory)#Distributivity laws for complete lattices|infinite distributive law]] when ''a'' → ''b'' is taken to be the [[supremum]] of the set of all ''c'' for which ''c'' ∧ ''a'' ≤ ''b''.  In the finite case, every nonempty distributive lattice, in particular every nonempty finite [[Total order#Chains|chain]], is automatically complete and completely distributive, and hence a Heyting algebra.

It follows from the definition that 1 ≤ 0 → ''a'', corresponding to the intuition that any proposition ''a'' is implied by a contradiction 0.  Although the negation operation ¬''a'' is not part of the definition, it is definable as ''a'' → 0.  The intuitive content of ¬''a'' is the proposition that to assume ''a'' would lead to a contradiction. The definition implies that ''a'' ∧ ¬''a'' = 0.  It can further be shown that ''a'' ≤ ¬¬''a'', although the converse, ¬¬''a'' ≤ ''a'', is not true in general, that is, [[double negation elimination]] does not hold in general in a Heyting algebra.

Heyting algebras generalize Boolean algebras in the sense that Boolean algebras are precisely the Heyting algebras satisfying ''a'' ∨ ¬''a'' = 1 ([[excluded middle]]), equivalently ¬¬''a'' = ''a''. Those elements of a Heyting algebra ''H'' of the form ¬''a'' comprise a Boolean lattice, but in general this is not a [[subalgebra]] of ''H'' (see [[#Regular and complemented elements|below]]).

Heyting algebras serve as the algebraic models of propositional [[intuitionistic logic]] in the same way Boolean algebras model propositional [[classical logic]].<ref name="MacLane1994">{{cite book | vauthors=((Mac Lane, S.)), ((Moerdijk, I.)) | date= 1994 | title=Sheaves in Geometry and Logic | series= Universitext | publisher=Springer New York | url=http://dx.doi.org/10.1007/978-1-4612-0927-0 | pages=48 | doi=10.1007/978-1-4612-0927-0| isbn= 978-0-387-97710-2 }}</ref> The internal logic of an [[elementary topos]] is based on the Heyting algebra of [[subobject]]s of the [[terminal object]] 1 ordered by inclusion, equivalently the morphisms from 1 to the [[subobject classifier]] Ω.

The [[open set]]s of any [[topological space]] form a [[complete Heyting algebra]]. Complete Heyting algebras thus become a central object of study in [[pointless topology]].  

Every Heyting algebra whose set of non-greatest elements has a greatest element (and forms another Heyting algebra) is [[Subdirectly irreducible algebra|subdirectly irreducible]], whence every Heyting algebra can be made subdirectly irreducible by adjoining a new greatest element.  It follows that even among the finite Heyting algebras there exist infinitely many that are subdirectly irreducible, no two of which have the same [[equational theory]].  Hence no finite set of finite Heyting algebras can supply all the counterexamples to non-laws of Heyting algebra.  This is in sharp contrast to Boolean algebras, whose only subdirectly irreducible one is the two-element one, which on its own therefore suffices for all counterexamples to non-laws of Boolean algebra, the basis for the simple [[truth table]] decision method.  Nevertheless, it is [[Decidability (logic)|decidable]] whether an equation holds of all Heyting algebras.<ref name="Kripke63">Kripke, S. A.: 1965, 'Semantical analysis of intuitionistic logic I'. In: J. N. Crossley and M. A. E. Dummett (eds.): Formal Systems and Recursive Functions. Amsterdam: North-Holland, pp. 92–130.</ref>

Heyting algebras are less often called '''pseudo-Boolean algebras''',<ref name="Rasiowa-Sikorski">{{cite book|author1=Helena Rasiowa|author2=Roman Sikorski|title=The Mathematics of Metamathematics|year=1963 |publisher=Państwowe Wydawnictwo Naukowe (PWN)|pages=54–62, 93–95, 123–130}}</ref> or even '''Brouwer lattices''',<ref name="KusraevKutateladze1999">{{cite book|author1=A. G. Kusraev|author2=Samson Semenovich Kutateladze|title=Boolean valued analysis|url=https://books.google.com/books?id=MzVXq3LRHOYC&pg=PA12 |year=1999 |publisher=Springer|isbn=978-0-7923-5921-0|page=12}}</ref> although the latter term may denote the dual definition,<ref>{{springer | title=Brouwer lattice  | id= b/b017660  | last= Yankov  | first= V.A.}}</ref> or have a slightly more general meaning.<ref name="Blyth2005">{{cite book|author=Thomas Scott Blyth|title=Lattices and ordered algebraic structures|url=https://books.google.com/books?id=WgROkcmTxG4C&pg=PA151 |year=2005 |publisher=Springer |isbn=978-1-85233-905-0|page=151}}</ref>

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

==Alternative definitions==
===Category-theoretic definition===
A Heyting algebra <math>H</math> is a bounded lattice that has all [[exponential object]]s.

The lattice <math>H</math> is regarded as a [[category (mathematics)|category]] where 
meet, <math>\wedge</math>, is the [[product (category theory)|product]]. The exponential condition means that for any objects <math>Y</math> and <math>Z</math> in <math>H</math> an exponential <math>Z^Y</math> uniquely exists as an object in <math>H</math>.

A Heyting implication (often written using <math>\Rightarrow</math> or <math>\multimap</math> to avoid confusions such as the use of <math>\to</math> to indicate a [[functor]]) is just an exponential: <math>Y \Rightarrow Z</math> is an alternative notation for <math>Z^Y</math>. From the definition of exponentials we have that implication (<math>\Rightarrow : H \times H \to H</math>) is [[right adjoint]] to meet (<math>\wedge : H \times H \to H</math>). This adjunction can be written as <math>(- \wedge Y) \dashv (Y \Rightarrow -)</math> or more fully as:
<math display="block">(- \wedge Y): H \stackrel {\longrightarrow} {\underset {\longleftarrow}{\top}} H: (Y \Rightarrow -)</math>

===Lattice-theoretic definitions===
An equivalent definition of Heyting algebras can be given by considering the mappings:

:<math>\begin{cases} f_a \colon H \to H \\ f_a(x)=a\wedge x \end{cases}</math>

for some fixed ''a'' in ''H''. A bounded lattice ''H'' is a Heyting algebra [[if and only if]] every mapping ''f<sub>a</sub>'' is the lower adjoint of a monotone [[Galois connection]]. In this case the respective upper adjoint ''g<sub>a</sub>'' is given by ''g<sub>a</sub>''(''x'') = ''a''→''x'', where → is defined as above.

Yet another definition is as a [[residuated lattice]] whose monoid operation is ∧. The monoid unit must then be the top element 1. Commutativity of this monoid implies that the two residuals coincide as ''a''→''b''.

===Bounded lattice with an implication operation===
Given a bounded lattice ''A'' with largest and smallest elements 1 and 0, and a binary operation →, these together form a Heyting algebra if and only if the following hold:
#<math>a\to a = 1</math>
#<math>a\wedge(a\to b)=a\wedge b</math>
#<math>b\wedge(a\to b)= b</math>
#<math>a\to (b\wedge c)= (a\to b)\wedge (a\to c)</math>
where equation 4 is the distributive law for →.

===Characterization using the axioms of intuitionistic logic===
This characterization of Heyting algebras makes the proof of the basic facts concerning the relationship between intuitionist propositional calculus and Heyting algebras immediate. (For these facts, see the sections "[[#Provable identities|Provable identities]]" and "[[#Universal constructions|Universal constructions]]".) One should think of the element <math>\top</math> as meaning, intuitively, "provably true". Compare with the axioms at [[Intuitionistic_logic#Syntax|Intuitionistic logic]].

Given a set ''A'' with three binary operations →, ∧ and ∨, and two distinguished elements <math>\bot</math> and <math>\top</math>, then ''A'' is a Heyting algebra for these operations (and the relation ≤ defined by the condition that <math>a \le b</math> when ''a''→''b'' = <math>\top</math>) if and only if the following conditions hold for any elements ''x'', ''y'' and ''z'' of ''A'':

#<math>\mbox{If } x \le y  \mbox{ and } y \le x  \mbox{ then } x = y ,</math>
#<math>\mbox{If } \top \le y , \mbox{ then } y = \top ,</math>
#<math>x \le y \to x  ,</math>
#<math> x \to (y \to z) \le (x \to y) \to (x \to z)  ,</math>
#<math> x \land y \le x  ,</math>
#<math> x \land y \le y ,</math>
#<math> x \le y \to (x \land y)  ,</math>
#<math> x \le x \lor y ,</math>
#<math> y \le x \lor y  ,</math>
#<math> x \to z \le (y \to z) \to (x \lor y \to z)  ,</math>
#<math> \bot \le x  .</math>
Finally, we define ¬''x'' to be ''x''→ <math>\bot</math>.

Condition 1 says that equivalent formulas should be identified. Condition&nbsp;2 says that provably true formulas are closed under [[modus ponens]]. Conditions&nbsp;3 and 4 are ''then'' conditions. Conditions&nbsp;5, 6 and 7 are ''and'' conditions. Conditions&nbsp;8, 9 and 10 are ''or'' conditions. Condition&nbsp;11 is a ''false'' condition.

Of course, if a different set of axioms were chosen for logic, we could modify ours accordingly.

== Examples ==
[[File:Rieger-Nishimura.svg|thumb|right|280px|The [[free object|free]] Heyting algebra over one generator (aka Rieger–Nishimura lattice)]]

<ul>
<li> Every [[Boolean algebra (structure)|Boolean algebra]] is a Heyting algebra, with ''p''→''q'' given by ¬''p''∨''q''.</li>
<li> Every [[total order|totally ordered set]] that has a least element 0 and a greatest element 1 is a Heyting algebra (if viewed as a lattice). In this case ''p''→''q'' equals to 1 when ''p≤q'', and ''q'' otherwise.</li>
<li> The simplest Heyting algebra that is not already a Boolean algebra is the totally ordered set {0, {{sfrac|1|2}}, 1} (viewed as a lattice), yielding the operations:
{|
|-style="vertical-align:bottom"
|
<div>
{| class="wikitable"
|+ <math>a \land b</math>
|-
! {{diagonal split header|''a''|''b''}}
| bgcolor="white" width="30" align="center" | 0
| bgcolor="white" width="30" align="center" | {{sfrac|1|2}}
| bgcolor="white" width="30" align="center" | 1
|-
| bgcolor="white" align="center" | 0
| align="center" | 0
| align="center" | 0
| align="center" | 0
|-
| bgcolor="white" align="center" | {{sfrac|1|2}}
| align="center" | 0
| align="center" | {{sfrac|1|2}}
| align="center" | {{sfrac|1|2}}
|-
| bgcolor="white" align="center" | 1
| align="center" | 0
| align="center" | {{sfrac|1|2}}
| align="center" | 1
|}
</div>
| width="30" | 
|
<div>
{| class="wikitable"
|+ <math>a \lor b</math>
|-
! {{diagonal split header|''a''|''b''}}
| bgcolor="white" width="30" align="center" | 0
| bgcolor="white" width="30" align="center" | {{sfrac|1|2}}
| bgcolor="white" width="30" align="center" | 1
|-
| bgcolor="white" align="center" | 0
| align="center" | 0
| align="center" | {{sfrac|1|2}}
| align="center" | 1
|-
| bgcolor="white" align="center" | {{sfrac|1|2}}
| align="center" | {{sfrac|1|2}}
| align="center" | {{sfrac|1|2}}
| align="center" | 1
|-
| bgcolor="white" align="center" | 1
| align="center" | 1
| align="center" | 1
| align="center" | 1
|}
</div>
| width="30" | 
|
<div>
{| class="wikitable"
|+ {{nobold|{{math|''a''→''b''}}}}
|-
! {{diagonal split header|''a''|''b''}}
| bgcolor="white" width="30" align="center" | 0
| bgcolor="white" width="30" align="center" | {{sfrac|1|2}}
| bgcolor="white" width="30" align="center" | 1
|-
| bgcolor="white" align="center" | 0
| align="center" | 1
| align="center" | 1
| align="center" | 1
|-
| bgcolor="white" align="center" | {{sfrac|1|2}}
| align="center" | 0
| align="center" | 1
| align="center" | 1
|-
| bgcolor="white" align="center" | 1
| align="center" | 0
| align="center" | {{sfrac|1|2}}
| align="center" | 1
|}
</div>
| width="30" | 
|
<div>
{| class="wikitable"
| width="50" align="center" | ''a''
| width="50" align="center" | ¬''a''
|-
| bgcolor="white" align="center" | 0
| align="center" | 1
|-
| bgcolor="white" align="center" | {{sfrac|1|2}}
| align="center" | 0
|-
| bgcolor="white" align="center" | 1
| align="center" | 0
|}
</div>
|}
In this example, note that {{math|size=100%|1= {{sfrac|1|2}}&or;¬{{sfrac|1|2}} = {{sfrac|1|2}}&or;({{sfrac|1|2}} → 0) = {{sfrac|1|2}}&or;0 = {{sfrac|1|2}}}} falsifies the law of excluded middle.

<li> Every [[topology]] provides a complete Heyting algebra in the form of its [[open set]] lattice. In this case, the element ''A''→''B'' is the [[interior (topology)|interior]] of the union of ''A<sup>c</sup>'' and ''B'', where ''A<sup>c</sup>'' denotes the [[Complement (set theory)|complement]] of the [[open set]] ''A''. Not all complete Heyting algebras are of this form. These issues are studied in [[pointless topology]], where complete Heyting algebras are also called '''frames''' or '''locales'''.
<li> Every [[interior algebra]] provides a Heyting algebra in the form of its lattice of open elements. Every Heyting algebra is of this form as a Heyting algebra can be completed to a Boolean algebra by taking its free Boolean extension as a bounded distributive lattice and then treating it as a [[generalized topology]] in this Boolean algebra.
<li> The [[Lindenbaum algebra]] of propositional [[intuitionistic logic]] is a Heyting algebra.</li>
<li> The [[global element]]s of the [[subobject classifier]] Ω of an [[elementary topos]] form a Heyting algebra; it is the Heyting algebra of [[truth value]]s of the intuitionistic higher-order logic induced by the topos. More generally, the set of [[Subobject|subobjects]] of any object ''X'' in a topos forms a Heyting algebra.</li>
<li> [[Łukasiewicz–Moisil algebra]]s (LM<sub>''n''</sub>) are also Heyting algebras for any ''n''<ref>{{Cite journal | doi = 10.1007/s10516-005-4145-6| title = N-Valued Logics and Łukasiewicz–Moisil Algebras| journal = Axiomathes| volume = 16| pages = 123–136| year = 2006| last1 = Georgescu | first1 = G. | issue = 1–2| s2cid = 121264473}}, Theorem 3.6</ref> (but they are not [[MV-algebras]] for ''n'' ≥ 5<ref>Iorgulescu, A.: Connections between MV<sub>''n''</sub>-algebras and ''n''-valued Łukasiewicz–Moisil algebras—I. Discrete Math. 181, 155–177 (1998) {{doi|10.1016/S0012-365X(97)00052-6}}</ref>).
</ul>

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

==Heyting algebra morphisms==

===Definition===
Given two Heyting algebras ''H''<sub>1</sub> and ''H''<sub>2</sub> and a mapping {{nowrap|1=''f'' : ''H''<sub>1</sub> → ''H''<sub>2</sub>,}} we say that ''ƒ'' is a '''[[morphism]]''' of Heyting algebras if, for any elements ''x'' and ''y'' in ''H''<sub>1</sub>, we have:
#<math>f(0) = 0,</math>
#<math>f(x \land y) = f(x) \land f(y),</math>
#<math>f(x \lor y) = f(x) \lor f(y),</math>
#<math>f(x \to y) = f(x) \to f(y),</math>

It follows from any of the last three conditions (2, 3, or 4) that ''f'' is an increasing function, that is, that {{nowrap|1=''f''(''x'') ≤ ''f''(''y'')}} whenever {{nowrap|1=''x'' ≤ ''y''}}.

Assume ''H''<sub>1</sub> and ''H''<sub>2</sub> are structures with operations →, ∧, ∨ (and possibly ¬) and constants 0 and 1, and ''f'' is a surjective mapping from ''H''<sub>1</sub> to ''H''<sub>2</sub> with properties 1 through 4 above. Then if ''H''<sub>1</sub> is a Heyting algebra, so too is ''H''<sub>2</sub>. This follows from the characterization of Heyting algebras as bounded lattices (thought of as algebraic structures rather than partially ordered sets) with an operation → satisfying certain identities.

===Properties===
The identity map {{nowrap|1=''f''(''x'') = ''x''}} from any Heyting algebra to itself is a morphism, and the composite {{nowrap|1=''g'' ∘ ''f''}} of any two morphisms ''f'' and ''g'' is a morphism. Hence Heyting algebras form a [[Category (mathematics)|category]].

===Examples===
Given a Heyting algebra ''H'' and any subalgebra ''H''<sub>1</sub>, the inclusion mapping {{nowrap|1=''i'' : ''H''<sub>1</sub> → ''H''}} is a morphism.

For any Heyting algebra ''H'', the map {{nowrap|1=''x'' ↦ ¬¬''x''}} defines a morphism from ''H'' onto the Boolean algebra of its regular elements ''H''<sub>reg</sub>. This is ''not'' in general a morphism from ''H'' to itself, since the join operation of ''H''<sub>reg</sub> may be different from that of ''H''.

==Quotients==
Let ''H'' be a Heyting algebra, and let {{nowrap|1=''F'' ⊆ ''H''.}} We call ''F'' a '''filter''' on ''H'' if it satisfies the following properties:
#<math>1 \in F,</math>
#<math> \mbox{If } x,y \in F \mbox{ then } x \land y \in F,</math>
#<math> \mbox{If } x \in F, \ y \in H, \ \mbox{and } x \le y \mbox{ then } y \in F.</math>

The intersection of any set of filters on ''H'' is again a filter. Therefore, given any subset ''S'' of ''H'' there is a smallest filter containing ''S''. We call it the filter '''generated''' by ''S''. If ''S'' is empty, {{nowrap|1=''F'' = {1}.}} Otherwise, ''F'' is equal to the set of ''x'' in ''H'' such that there exist {{nowrap|1=''y''<sub>1</sub>, ''y''<sub>2</sub>, ..., ''y''<sub>''n''</sub> ∈ ''S''}} with {{nowrap|1=''y''<sub>1</sub> ∧ ''y''<sub>2</sub> ∧ ... ∧ ''y''<sub>''n''</sub> ≤ ''x''.}}

If ''H'' is a Heyting algebra and ''F'' is a filter on ''H'', we define a relation ~ on ''H'' as follows: we write {{nowrap|1=''x'' ~ ''y''}} whenever {{nowrap|1=''x'' → ''y''}} and {{nowrap|1=''y'' → ''x''}} both belong to ''F''. Then ~ is an [[equivalence relation]]; we write {{nowrap|1=''H''/''F''}} for the [[quotient set]]. There is a unique Heyting algebra structure on {{nowrap|1=''H''/''F''}} such that the canonical surjection {{nowrap|1=''p''<sub>''F''</sub> : ''H'' → ''H''/''F''}} becomes a Heyting algebra morphism. We call the Heyting algebra {{nowrap|1=''H''/''F''}} the '''quotient''' of ''H'' by ''F''.

Let ''S'' be a subset of a Heyting algebra ''H'' and let ''F'' be the filter generated by ''S''. Then ''H''/''F'' satisfies the following universal property:
:Given any morphism of Heyting algebras {{nowrap|1=''f'' : ''H'' → ''{{prime|H}}''}} satisfying {{nowrap|1=''f''(''y'') = 1}} for every {{nowrap|1=''y'' ∈ ''S'',}} ''f'' factors uniquely through the canonical surjection {{nowrap|1=''p''<sub>''F''</sub> : ''H'' → ''H''/''F''.}} That is, there is a unique morphism {{nowrap|1=''{{prime|f}}'' : ''H''/''F'' → ''{{prime|H}}''}} satisfying {{nowrap|1=''{{prime|f}}p''<sub>''F''</sub> = ''f''.}} The morphism ''{{prime|f}}'' is said to be ''induced'' by ''f''.

Let {{nowrap|1=''f'' : ''H''<sub>1</sub> → ''H''<sub>2</sub>}} be a morphism of Heyting algebras. The '''kernel''' of ''f'', written ker ''f'', is the set {{nowrap|1=''f''<sup>−1</sup>[{1}].}} It is a filter on ''H''<sub>1</sub>. (Care should be taken because this definition, if applied to a morphism of Boolean algebras, is dual to what would be called the kernel of the morphism viewed as a morphism of rings.) By the foregoing, ''f'' induces a morphism {{nowrap|1=''{{prime|f}}'' : ''H''<sub>1</sub>/(ker ''f'') → ''H''<sub>2</sub>.}} It is an isomorphism of {{nowrap|1=''H''<sub>1</sub>/(ker ''f'')}} onto the subalgebra ''f''[''H''<sub>1</sub>] of ''H''<sub>2</sub>.

==Universal constructions==

===Heyting algebra of propositional formulas in ''n'' variables up to intuitionist equivalence===
The metaimplication {{nowrap|2 ⇒ 1}} in the section "[[#Provable identities|Provable identities]]" is proved by showing that the result of the following construction is itself a Heyting algebra:
#Consider the set ''L'' of propositional formulas in the variables ''A''<sub>1</sub>, ''A''<sub>2</sub>,..., ''A''<sub>''n''</sub>.
# Endow ''L'' with a preorder ≼ by defining ''F''≼''G'' if ''G'' is an (intuitionist) [[logical consequence]] of ''F'', that is, if ''G'' is provable from ''F''. It is immediate that ≼ is a preorder.
# Consider the equivalence relation ''F''~''G'' induced by the preorder F≼G. (It is defined by ''F''~''G'' if and only if ''F''≼''G'' and ''G''≼''F''. In fact, ~ is the relation of (intuitionist) logical equivalence.)
# Let ''H''<sub>0</sub> be the quotient set ''L''/~. This will be the desired Heyting algebra.
# We write [''F''] for the equivalence class of a formula ''F''. Operations →, ∧, ∨ and ¬ are defined in an obvious way on ''L''. Verify that given formulas ''F'' and ''G'', the equivalence classes [''F''→''G''], [''F''∧''G''], [''F''∨''G''] and [¬''F''] depend only on [''F''] and [''G'']. This defines operations →, ∧, ∨ and ¬ on the quotient set ''H''<sub>0</sub>=''L''/~. Further define 1 to be the class of provably true statements, and set 0=[⊥].
# Verify that ''H''<sub>0</sub>, together with these operations, is a Heyting algebra. We do this using the axiom-like definition of Heyting algebras. ''H''<sub>0</sub> satisfies conditions THEN-1 through FALSE because all formulas of the given forms are axioms of intuitionist logic. MODUS-PONENS follows from the fact that if a formula ⊤→''F'' is provably true, where ⊤ is provably true, then ''F'' is provably true (by application of the rule of inference modus ponens). Finally, EQUIV results from the fact that if ''F''→''G'' and ''G''→''F'' are both provably true, then ''F'' and ''G'' are provable from each other (by application of the rule of inference modus ponens), hence [''F'']=[''G''].

As always under the axiom-like definition of Heyting algebras, we define ≤ on ''H''<sub>0</sub> by the condition that ''x''≤''y'' if and only if ''x''→''y''=1. Since, by the [[deduction theorem]], a formula ''F''→''G'' is provably true if and only if ''G'' is provable from ''F'', it follows that [''F'']≤[''G''] if and only if  F≼G. In other words, ≤ is the order relation on ''L''/~ induced by the preorder ≼ on ''L''.

===Free Heyting algebra on an arbitrary set of generators===
In fact, the preceding construction can be carried out for any set of variables {''A''<sub>''i''</sub> : ''i''∈''I''} (possibly infinite). One obtains in this way the ''free'' Heyting algebra on the variables {''A''<sub>''i''</sub>}, which we will again denote by ''H''<sub>0</sub>. It is free in the sense that given any Heyting algebra ''H'' given together with a family of its elements 〈''a''<sub>''i''</sub>: ''i''∈''I'' 〉, there is a unique morphism ''f'':''H''<sub>0</sub>→''H'' satisfying ''f''([''A''<sub>''i''</sub>])=''a''<sub>''i''</sub>. The uniqueness of ''f'' is not difficult to see, and its existence results essentially from the metaimplication {{nowrap|1 ⇒ 2}} of the section "[[#Provable identities|Provable identities]]" above, in the form of its corollary that whenever ''F'' and ''G'' are provably equivalent formulas, ''F''(〈''a''<sub>''i''</sub>〉)=''G''(〈''a''<sub>''i''</sub>〉) for any family of elements 〈''a''<sub>''i''</sub>〉in ''H''.

===Heyting algebra of formulas equivalent with respect to a theory ''T''===
Given a set of formulas ''T'' in the variables {''A''<sub>''i''</sub>}, viewed as axioms, the same construction could have been carried out with respect to a relation ''F''≼''G'' defined on ''L'' to mean that ''G'' is a provable consequence of ''F'' and the set of axioms ''T''. Let us denote by ''H''<sub>''T''</sub> the Heyting algebra so obtained. Then ''H''<sub>''T''</sub> satisfies the same universal property as ''H''<sub>0</sub> above, but with respect to Heyting algebras ''H'' and families of elements 〈''a''<sub>''i''</sub>〉 satisfying the property that ''J''(〈''a''<sub>''i''</sub>〉)=1 for any axiom ''J''(〈''A''<sub>''i''</sub>〉) in ''T''. (Let us note that ''H''<sub>''T''</sub>, taken with the family of its elements 〈[''A''<sub>''i''</sub>]〉, itself satisfies this property.) The existence and uniqueness of the morphism is proved the same way as for ''H''<sub>0</sub>, except that one must modify the metaimplication {{nowrap|1 ⇒ 2}} in "[[#Provable identities|Provable identities]]" so that 1 reads "provably true ''from T''," and 2 reads "any elements ''a''<sub>1</sub>, ''a''<sub>2</sub>,..., ''a''<sub>''n''</sub> in ''H'' ''satisfying the formulas of T''."

The Heyting algebra ''H''<sub>''T''</sub> that we have just defined can be viewed as a quotient of the free Heyting algebra ''H''<sub>0</sub> on the same set of variables, by applying the universal property of ''H''<sub>0</sub> with respect to ''H''<sub>''T''</sub>, and the family of its elements 〈[''A''<sub>''i''</sub>]〉.

Every Heyting algebra is isomorphic to one of the form ''H''<sub>''T''</sub>. To see this, let ''H'' be any Heyting algebra, and let 〈''a''<sub>''i''</sub>: ''i''∈I〉 be a family of elements generating ''H'' (for example, any surjective family). Now consider the set ''T'' of formulas ''J''(〈''A''<sub>''i''</sub>〉) in the variables 〈''A''<sub>''i''</sub>: ''i''∈I〉 such that ''J''(〈''a''<sub>''i''</sub>〉)=1. Then we obtain a morphism ''f'':''H''<sub>''T''</sub>→''H'' by the universal property of ''H''<sub>''T''</sub>, which is clearly surjective. It is not difficult to show that ''f'' is injective.

===Comparison to Lindenbaum algebras===
The constructions we have just given play an entirely analogous role with respect to Heyting algebras to that of [[Lindenbaum algebra]]s with respect to [[Boolean algebra (structure)|Boolean algebras]]. In fact, The Lindenbaum algebra ''B''<sub>''T''</sub> in the variables {''A''<sub>''i''</sub>} with respect to the axioms ''T'' is just our ''H''<sub>''T''∪''T''<sub>1</sub></sub>, where ''T''<sub>1</sub> is the set of all formulas of the form ¬¬''F''→''F'', since the additional axioms of ''T''<sub>1</sub> are the only ones that need to be added in order to make all classical tautologies provable.

==Heyting algebras as applied to intuitionistic logic==
If one interprets the axioms of the intuitionistic propositional logic as terms of a Heyting algebra, then they will evaluate to the largest element, 1, in ''any'' Heyting algebra under any assignment of values to the formula's variables. For instance, (''P''∧''Q'')→''P'' is, by definition of the pseudo-complement, the largest element ''x'' such that <math>P \land Q \land x \le P</math>. This inequation is satisfied for any ''x'', so the largest such ''x'' is 1.

Furthermore, the rule of [[modus ponens]] allows us to derive the formula ''Q'' from the formulas ''P'' and ''P''→''Q''. But in any Heyting algebra, if ''P'' has the value 1, and ''P''→''Q'' has the value 1, then it means that <math>P \land 1 \le Q</math>, and so <math>1 \land 1 \le Q</math>; it can only be that ''Q'' has the value 1.

This means that if a formula is deducible from the laws of intuitionistic logic, being derived from its axioms by way of the rule of modus ponens, then it will always have the value 1 in all Heyting algebras under any assignment of values to the formula's variables. However one can construct a Heyting algebra in which the value of [[Peirce's law]] is not always 1. Consider the 3-element algebra {0,{{sfrac|1|2}},1} as given above. If we assign {{sfrac|1|2}} to ''P'' and 0 to ''Q'', then the value of Peirce's law ((''P''→''Q'')→''P'')→''P'' is {{sfrac|1|2}}. It follows that Peirce's law cannot be intuitionistically derived. See [[Curry&ndash;Howard isomorphism]] for the general context of what this implies in [[type theory]].

The converse can be proven as well: if a formula always has the value 1, then it is deducible from the laws of intuitionistic logic, so the ''intuitionistically valid'' formulas are exactly those that always have a value of 1. This is similar to the notion that ''classically valid'' formulas are those formulas that have a value of 1 in the [[two-element Boolean algebra]] under any possible assignment of true and false to the formula's variables&mdash;that is, they are formulas that are tautologies in the usual truth-table sense. A Heyting algebra, from the logical standpoint, is then a generalization of the usual system of truth values, and its largest element 1 is analogous to 'true'. The usual two-valued logic system is a special case of a Heyting algebra, and the smallest non-trivial one, in which the only elements of the algebra are 1 (true) and 0 (false).

==Decision problems==
The problem of whether a given equation holds in every Heyting algebra was shown to be decidable by [[Saul Kripke]] in 1965.<ref name="Kripke63" /> The precise [[Computational complexity theory|computational complexity]] of the problem was established by [[Richard Statman]] in 1979, who showed it was [[PSPACE-complete]]<ref>{{cite journal | last1 = Statman | first1 = R. | year = 1979 | title = Intuitionistic propositional logic is polynomial-space complete | journal = Theoretical Comput. Sci. | volume = 9 | pages = 67–72 | doi=10.1016/0304-3975(79)90006-9| hdl = 2027.42/23534 | hdl-access = free }}</ref> and hence at least as hard as [[Boolean satisfiability problem|deciding equations of Boolean algebra]] (shown coNP-complete in 1971 by [[Stephen Cook]])<ref name="Cook71">{{Cite conference|last = Cook  | first = S.A. | author-link = Stephen A. Cook  | title = The complexity of theorem proving procedures
 | book-title = Proceedings, Third Annual ACM Symposium on the Theory of Computing, ACM, New York | year = 1971 | pages = 151–158 | doi = 10.1145/800157.805047| doi-access = free}}</ref> and conjectured to be considerably harder.  The elementary or first-order theory of Heyting algebras is undecidable.<ref>{{cite journal | last1 = Grzegorczyk | first1 = Andrzej | author-link = Andrzej Grzegorczyk | year = 1951 | title = Undecidability of some topological theories | url =https://www.impan.pl/shop/publication/transaction/download/product/93826?download.pdf | journal = Fundamenta Mathematicae | volume = 38 | pages = 137–52 | doi = 10.4064/fm-38-1-137-152 }}</ref> It remains open whether the [[universal Horn theory]] of Heyting algebras, or [[word problem (mathematics)|word problem]], is decidable.<ref>Peter T. Johnstone, ''Stone Spaces'', (1982) Cambridge University Press, Cambridge, {{ISBN|0-521-23893-5}}. ''(See paragraph 4.11)''</ref>  Regarding the word problem it is known that Heyting algebras are not locally finite (no Heyting algebra generated by a finite nonempty set is finite), in contrast to Boolean algebras, which are locally finite and whose word problem is decidable. 

== Topological representation and duality theory==
Every Heyting algebra {{math|''H''}} is naturally isomorphic to a bounded sublattice {{math|''L''}} of open sets of a topological space {{math|''X''}}, where the implication <math>U\to V</math> of {{math|''L''}} is given by the interior of <math>(X\setminus U)\cup V</math>. 
More precisely, {{math|''X''}} is the [[spectral space]] of prime [[ideal (order theory)|ideals]] of the bounded lattice {{math|''H''}} and {{math|''L''}} is the lattice of open and quasi-compact subsets of {{math|''X''}}.

More generally, the category of Heyting algebras 
is dually equivalent to the category of Heyting spaces.<ref>see section 8.3 in * {{cite book | last1=Dickmann | first1=Max | last2=Schwartz | first2= Niels | last3=Tressl | first3= Marcus | title=Spectral Spaces| doi=10.1017/9781316543870 | year=2019 | publisher=[[Cambridge University Press]] | series=New Mathematical Monographs | volume=35 | location=Cambridge | isbn=9781107146723 | s2cid=201542298 }} </ref> 
This duality can be seen as restriction of the classical [[Stone duality]] of bounded distributive lattices to the (non-full) subcategory of Heyting algebras.

Alternatively,  the category of Heyting algebras is dually equivalent to the category of [[Esakia space]]s. This is called [[Esakia duality]].

==Notes==
{{Reflist}}

==See also==
* [[Alexandrov topology]]
* [[Intermediate logic|Superintuitionistic (aka intermediate) logic]]s
* [[List of Boolean algebra topics]]
* [[Ockham algebra]]

==References==
* {{cite book | first = Daniel Edwin | last = Rutherford | year = 1965 | title = Introduction to Lattice Theory | publisher = Oliver and Boyd | oclc = 224572 }}
* F. Borceux, ''Handbook of Categorical Algebra 3'', In ''Encyclopedia of Mathematics and its Applications'', Vol. 53, Cambridge University Press, 1994. {{ISBN|0-521-44180-3}} {{OCLC|52238554}}
* G. Gierz, K.H. Hoffmann, K. Keimel, J. D. Lawson, M. Mislove and [[Dana Scott|D. S. Scott]], ''Continuous Lattices and Domains'', In ''Encyclopedia of Mathematics and its Applications'', Vol. 93, Cambridge University Press, 2003.
* S. Ghilardi. ''Free Heyting algebras as bi-Heyting algebras'', Math. Rep. Acad. Sci. Canada XVI., 6:240–244, 1992.
*{{citation|last=Heyting|first= A.
|title=Die formalen Regeln der intuitionistischen Logik. I, II, III|jfm= 56.0823.01
|journal=Sitzungsberichte Akad. Berlin |year=1930|pages= 42–56, 57–71, 158–169 }}
* {{cite book | vauthors=((Mac Lane, S.)), ((Moerdijk, I.)) | date= 1994 | title=Sheaves in Geometry and Logic | series= Universitext | publisher=Springer New York | url=http://dx.doi.org/10.1007/978-1-4612-0927-0 | doi=10.1007/978-1-4612-0927-0| isbn= 978-0-387-97710-2 }}
* {{cite book | last1=Dickmann | first1=Max | last2=Schwartz | first2= Niels | last3=Tressl | first3= Marcus | title=Spectral Spaces| doi=10.1017/9781316543870 | year=2019 | publisher=[[Cambridge University Press]] | series=New Mathematical Monographs | volume=35 | location=Cambridge | isbn=9781107146723 | s2cid=201542298 }}

==External links==

* {{PlanetMath|urlname=heytingalgebra|title=Heyting algebra}}

{{Order theory}}
{{DEFAULTSORT:Heyting Algebra}}

[[Category:Algebraic logic]]
[[Category:Constructivism (mathematics)]]
[[Category:Lattice theory]]