Editing Heyting algebra (section)

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