Editing Intuitionistic logic (section)

===Heyting algebra semantics===
In classical logic, we often discuss the [[truth value]]s that a formula can take. The values are usually chosen as the members of a [[Boolean algebra (structure)|Boolean algebra]].  The [[Join and meet|meet and join]] operations in the Boolean algebra are identified with the ∧ and ∨ logical connectives, so that the value of a formula of the form ''A'' ∧ ''B'' is the meet of the value of ''A'' and the value of ''B'' in the Boolean algebra.  Then we have the useful theorem that a formula is a valid proposition of classical logic if and only if its value is 1 for every [[valuation (logic)|valuation]]—that is, for any assignment of values to its variables.

A corresponding theorem is true for intuitionistic logic, but instead of assigning each formula a value from  a Boolean algebra, one uses values from a [[Heyting algebra]], of which Boolean algebras are a special case. A formula is valid in intuitionistic logic if and only if it receives the value of the top element for any valuation on any Heyting algebra.

It can be shown that to recognize valid formulas, it is sufficient to consider a single Heyting algebra whose elements are the open subsets of the real line '''R'''.{{sfn|Sørensen|Urzyczyn|2006|page=42}} In this algebra we have:

:<math>\begin{align}
\text{Value}[\bot] &=\emptyset \\
\text{Value}[\top] &= \mathbf{R} \\
\text{Value}[A \land B] &= \text{Value}[A] \cap \text{Value}[B] \\
\text{Value}[A \lor B]  &= \text{Value}[A] \cup \text{Value}[B] \\
\text{Value}[A \to B] &= \text{int} \left ( \text{Value}[A]^\complement \cup \text{Value}[B] \right )
\end{align}</math>

where int(''X'') is the [[interior (topology)|interior]] of ''X'' and  ''X''<sup>∁</sup> its [[complement (set theory)|complement]].

The last identity concerning ''A'' → ''B'' allows us to calculate the value of ¬''A'':

:<math>\begin{align}
\text{Value}[\neg A] &= \text{Value}[A \to \bot] \\
&=  \text{int} \left ( \text{Value}[A]^\complement \cup \text{Value}[\bot] \right ) \\
&= \text{int} \left ( \text{Value}[A]^\complement \cup \emptyset \right ) \\
&=  \text{int} \left ( \text{Value}[A]^\complement \right )
\end{align}</math>

With these assignments, intuitionistically valid formulas are precisely those that are assigned the value of the entire line.{{sfn|Sørensen|Urzyczyn|2006|page=42}} For example, the formula ¬(''A'' ∧ ¬''A'') is valid, because no matter what set ''X'' is chosen as the value of the formula ''A'', the value of ¬(''A'' ∧ ¬''A'') can be shown to be the entire line:

:<math>\begin{align}
\text{Value}[\neg(A \land \neg A)] &= \text{int} \left ( \text{Value} [A \land \neg A]^\complement   \right )  && \text{Value}[\neg B] = \text{int}\left ( \text{Value}[B]^\complement \right) \\
&= \text{int} \left ( \left (\text{Value}[A] \cap \text{Value}[\neg A] \right )^\complement \right )\\
&= \text{int} \left ( \left (\text{Value}[A]  \cap \text{int} \left (\text{Value}[A]^\complement \right ) \right )^\complement \right )  \\
&= \text{int} \left ( \left (X  \cap \text{int} \left (X^\complement \right ) \right )^\complement \right ) \\
&= \text{int} \left (\emptyset^\complement \right ) && \text{int} \left (X^\complement \right ) \subseteq X^\complement \\
&= \text{int} (\mathbf{R}) \\
&= \mathbf{R}
\end{align}</math>

So the valuation of this formula is true, and indeed the formula is valid. But the law of the excluded middle, ''A'' ∨ ¬''A'', can be shown to be ''invalid'' by using a specific value of the set of positive real numbers for ''A'':

:<math>\begin{align}
\text{Value}[A \lor \neg A] &=  \text{Value}[A] \cup \text{Value}[\neg A] \\
&=  \text{Value}[A] \cup \text{int} \left (  \text{Value}[A]^\complement \right) && \text{Value}[\neg B] = \text{int}\left ( \text{Value}[B]^\complement \right) \\
&=  \{ x > 0\} \cup \text{int} \left (  \{x > 0\}^\complement \right ) \\
&= \{ x > 0\} \cup \text{int} \left (  \{x \leqslant 0 \} \right) \\
&= \{ x > 0\} \cup  \{x < 0 \} \\
&=\{ x \neq 0 \} \\
&\neq \mathbf{R}
\end{align}</math>

The [[interpretation (logic)|interpretation]] of any intuitionistically valid formula in the infinite Heyting algebra described above results in the top element, representing true, as the valuation of the formula, regardless of what values from the algebra are assigned to the variables of the formula.{{sfn|Sørensen|Urzyczyn|2006|page=42}} Conversely, for every invalid formula, there is an assignment of values to the variables that yields a valuation that differs from the top element.{{sfn|Tarski|1938}}{{sfn|Rasiowa|Sikorski|1963|pages=385-386}} No finite Heyting algebra has the second of these two properties.{{sfn|Sørensen|Urzyczyn|2006|page=42}}