---
tag: 69SBK65SC5
kind: statement
role: proposition
name: Characterization using the axioms of intuitionistic logic
sources:
  - wikipedia: en:309343@r1371256451
    locator: Heyting algebra, section Alternative definitions > Characterization using the axioms of intuitionistic logic
    note: adopted
    mention: wikipedia://en/309343#OT57
    sections: [Statement]
inventory: [JF33P1MSS0]
---

## 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 ,$$
1. $$\mbox{If } \top \le y , \mbox{ then } y = \top ,$$
1. $$x \le y \to x ,$$
1. $$x \to (y \to z) \le (x \to y) \to (x \to z) ,$$
1. $$x \land y \le x ,$$
1. $$x \land y \le y ,$$
1. $$x \le y \to (x \land y) ,$$
1. $$x \le x \lor y ,$$
1. $$y \le x \lor y ,$$
1. $$x \to z \le (y \to z) \to (x \lor y \to z) ,$$
1. $$\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|0Y0MQYST0M]]. 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.