Editing Heyting algebra (section)

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