Editing Heyting algebra (section)

==Heyting algebras as applied to intuitionistic logic==
If one interprets the axioms of the intuitionistic propositional logic as terms of a Heyting algebra, then they will evaluate to the largest element, 1, in ''any'' Heyting algebra under any assignment of values to the formula's variables. For instance, (''P''∧''Q'')→''P'' is, by definition of the pseudo-complement, the largest element ''x'' such that <math>P \land Q \land x \le P</math>. This inequation is satisfied for any ''x'', so the largest such ''x'' is 1.

Furthermore, the rule of [[modus ponens]] allows us to derive the formula ''Q'' from the formulas ''P'' and ''P''→''Q''. But in any Heyting algebra, if ''P'' has the value 1, and ''P''→''Q'' has the value 1, then it means that <math>P \land 1 \le Q</math>, and so <math>1 \land 1 \le Q</math>; it can only be that ''Q'' has the value 1.

This means that if a formula is deducible from the laws of intuitionistic logic, being derived from its axioms by way of the rule of modus ponens, then it will always have the value 1 in all Heyting algebras under any assignment of values to the formula's variables. However one can construct a Heyting algebra in which the value of [[Peirce's law]] is not always 1. Consider the 3-element algebra {0,{{sfrac|1|2}},1} as given above. If we assign {{sfrac|1|2}} to ''P'' and 0 to ''Q'', then the value of Peirce's law ((''P''→''Q'')→''P'')→''P'' is {{sfrac|1|2}}. It follows that Peirce's law cannot be intuitionistically derived. See [[Curry&ndash;Howard isomorphism]] for the general context of what this implies in [[type theory]].

The converse can be proven as well: if a formula always has the value 1, then it is deducible from the laws of intuitionistic logic, so the ''intuitionistically valid'' formulas are exactly those that always have a value of 1. This is similar to the notion that ''classically valid'' formulas are those formulas that have a value of 1 in the [[two-element Boolean algebra]] under any possible assignment of true and false to the formula's variables&mdash;that is, they are formulas that are tautologies in the usual truth-table sense. A Heyting algebra, from the logical standpoint, is then a generalization of the usual system of truth values, and its largest element 1 is analogous to 'true'. The usual two-valued logic system is a special case of a Heyting algebra, and the smallest non-trivial one, in which the only elements of the algebra are 1 (true) and 0 (false).