Characterization using the axioms of intuitionistic logic

Statement

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" and "Universal constructions".) One should think of the element $\top$ as meaning, intuitively, "provably true". Compare with the axioms at Intuitionistic logic.

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

1. \mbox{If } x \le y \mbox{ and } y \le x \mbox{ then } x = y ,
2. \mbox{If } \top \le y , \mbox{ then } y = \top ,
3. $$x \le y \to x ,$$
4. $$x \to (y \to z) \le (x \to y) \to (x \to z) ,$$
5. $$x \land y \le x ,$$
6. $$x \land y \le y ,$$
7. $$x \le y \to (x \land y) ,$$
8. $$x \le x \lor y ,$$
9. $$y \le x \lor y ,$$
10. $$x \to z \le (y \to z) \to (x \lor y \to z) ,$$
11. $$\bot \le x .$$

Finally, we define ¬x to be x→ $\bot$.

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

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