Editing Heyting algebra (section)

==Universal constructions==

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

===Free Heyting algebra on an arbitrary set of generators===
In fact, the preceding construction can be carried out for any set of variables {''A''<sub>''i''</sub> : ''i''∈''I''} (possibly infinite). One obtains in this way the ''free'' Heyting algebra on the variables {''A''<sub>''i''</sub>}, which we will again denote by ''H''<sub>0</sub>. It is free in the sense that given any Heyting algebra ''H'' given together with a family of its elements 〈''a''<sub>''i''</sub>: ''i''∈''I'' 〉, there is a unique morphism ''f'':''H''<sub>0</sub>→''H'' satisfying ''f''([''A''<sub>''i''</sub>])=''a''<sub>''i''</sub>. The uniqueness of ''f'' is not difficult to see, and its existence results essentially from the metaimplication {{nowrap|1 ⇒ 2}} of the section "[[#Provable identities|Provable identities]]" above, in the form of its corollary that whenever ''F'' and ''G'' are provably equivalent formulas, ''F''(〈''a''<sub>''i''</sub>〉)=''G''(〈''a''<sub>''i''</sub>〉) for any family of elements 〈''a''<sub>''i''</sub>〉in ''H''.

===Heyting algebra of formulas equivalent with respect to a theory ''T''===
Given a set of formulas ''T'' in the variables {''A''<sub>''i''</sub>}, viewed as axioms, the same construction could have been carried out with respect to a relation ''F''≼''G'' defined on ''L'' to mean that ''G'' is a provable consequence of ''F'' and the set of axioms ''T''. Let us denote by ''H''<sub>''T''</sub> the Heyting algebra so obtained. Then ''H''<sub>''T''</sub> satisfies the same universal property as ''H''<sub>0</sub> above, but with respect to Heyting algebras ''H'' and families of elements 〈''a''<sub>''i''</sub>〉 satisfying the property that ''J''(〈''a''<sub>''i''</sub>〉)=1 for any axiom ''J''(〈''A''<sub>''i''</sub>〉) in ''T''. (Let us note that ''H''<sub>''T''</sub>, taken with the family of its elements 〈[''A''<sub>''i''</sub>]〉, itself satisfies this property.) The existence and uniqueness of the morphism is proved the same way as for ''H''<sub>0</sub>, except that one must modify the metaimplication {{nowrap|1 ⇒ 2}} in "[[#Provable identities|Provable identities]]" so that 1 reads "provably true ''from T''," and 2 reads "any elements ''a''<sub>1</sub>, ''a''<sub>2</sub>,..., ''a''<sub>''n''</sub> in ''H'' ''satisfying the formulas of T''."

The Heyting algebra ''H''<sub>''T''</sub> that we have just defined can be viewed as a quotient of the free Heyting algebra ''H''<sub>0</sub> on the same set of variables, by applying the universal property of ''H''<sub>0</sub> with respect to ''H''<sub>''T''</sub>, and the family of its elements 〈[''A''<sub>''i''</sub>]〉.

Every Heyting algebra is isomorphic to one of the form ''H''<sub>''T''</sub>. To see this, let ''H'' be any Heyting algebra, and let 〈''a''<sub>''i''</sub>: ''i''∈I〉 be a family of elements generating ''H'' (for example, any surjective family). Now consider the set ''T'' of formulas ''J''(〈''A''<sub>''i''</sub>〉) in the variables 〈''A''<sub>''i''</sub>: ''i''∈I〉 such that ''J''(〈''a''<sub>''i''</sub>〉)=1. Then we obtain a morphism ''f'':''H''<sub>''T''</sub>→''H'' by the universal property of ''H''<sub>''T''</sub>, which is clearly surjective. It is not difficult to show that ''f'' is injective.

===Comparison to Lindenbaum algebras===
The constructions we have just given play an entirely analogous role with respect to Heyting algebras to that of [[Lindenbaum algebra]]s with respect to [[Boolean algebra (structure)|Boolean algebras]]. In fact, The Lindenbaum algebra ''B''<sub>''T''</sub> in the variables {''A''<sub>''i''</sub>} with respect to the axioms ''T'' is just our ''H''<sub>''T''∪''T''<sub>1</sub></sub>, where ''T''<sub>1</sub> is the set of all formulas of the form ¬¬''F''→''F'', since the additional axioms of ''T''<sub>1</sub> are the only ones that need to be added in order to make all classical tautologies provable.