Editing Heyting algebra (section)

===Provable identities===
Given a formula <math>F(A_1, A_2,\ldots, A_n)</math> of propositional calculus (using, in addition to the variables, the connectives <math>\land, \lor, \lnot, \to</math>, and the constants 0 and 1), it is a fact, proved early on in any study of Heyting algebras, that the following two conditions are equivalent:
# The formula ''F'' is provably true in intuitionist propositional calculus.
# The identity <math>F(a_1, a_2,\ldots, a_n) = 1</math> is true for any Heyting algebra ''H'' and any elements <math>a_1, a_2,\ldots, a_n \in H</math>.
The metaimplication {{nowrap|1 ⇒ 2}} is extremely useful and is the principal practical method for proving identities in Heyting algebras. In practice, one frequently uses the [[deduction theorem]] in such proofs.

Since for any ''a'' and ''b'' in a Heyting algebra ''H'' we have <math>a \le b</math> if and only if ''a''→''b'' = 1, it follows from {{nowrap|1 ⇒ 2}} that whenever a formula ''F''→''G'' is provably true, we have <math>F(a_1, a_2,\ldots, a_n) \le G(a_1, a_2,\ldots, a_n)</math> for any Heyting algebra ''H'', and any elements <math>a_1, a_2,\ldots, a_n \in H</math>. (It follows from the deduction theorem that ''F''→''G'' is provable (unconditionally) if and only if ''G'' is provable from ''F'', that is, if ''G'' is a provable consequence of ''F''.) In particular, if ''F'' and ''G'' are provably equivalent, then <math>F(a_1, a_2,\ldots, a_n) = G(a_1, a_2,\ldots, a_n)</math>, since ≤ is an order relation.

1 ⇒ 2 can be proved by examining the logical axioms of the system of proof and verifying that their value is 1 in any Heyting algebra, and then verifying that the application of the rules of inference to expressions with value 1 in a Heyting algebra results in expressions with value 1. For example, let us choose the system of proof having [[modus ponens]] as its sole rule of inference, and whose axioms are the Hilbert-style ones given at [[Intuitionistic logic#Axiomatization]]. Then the facts to be verified follow immediately from the axiom-like definition of Heyting algebras given above.

1 ⇒ 2 also provides a method for proving that certain propositional formulas, though [[tautology (logic)|tautologies]] in classical logic, ''cannot'' be proved in intuitionist propositional logic. In order to prove that some formula <math>F(A_1, A_2,\ldots, A_n)</math> is not provable, it is enough to exhibit a Heyting algebra ''H'' and elements <math>a_1, a_2,\ldots, a_n \in H</math> such that <math>F(a_1, a_2,\ldots, a_n) \ne 1</math>.

If one wishes to avoid mention of logic, then in practice it becomes necessary to prove as a lemma a version of the deduction theorem valid for Heyting algebras: for any elements ''a'', ''b'' and ''c'' of a Heyting algebra ''H'', we have <math>(a \land b) \to c = a \to (b \to c)</math>.

For more on the metaimplication 2 ⇒ 1, see the section "[[#Universal constructions|Universal constructions]]" below.