Editing Heyting algebra (section)

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