Editing Intuitionistic logic (section)

==Semantics==
The semantics are rather more complicated than for the classical case. A [[model theory]] can be given by [[Heyting algebra|Heyting algebras]] or, equivalently, by [[Kripke semantics]]. In 2014, a [[Semantic theory of truth|Tarski-like model theory]] was proved complete by [[Robert Lee Constable|Bob Constable]], but with a different notion of completeness than classically.{{sfn|Constable|Bickford|2014}}

Unproved statements in intuitionistic logic are not given a intermediate or third truth value (as is sometimes mistakenly asserted). One can prove that such statements have no third truth value, a result dating back to [[Valery Glivenko|Glivenko]] in 1928.{{sfn|Van Atten|2022}} Instead they remain of unknown truth value, until they are either proved or disproved. Statements are disproved by deducing a contradiction from them.

A consequence of this point of view is that intuitionistic logic has no interpretation as a two-valued logic, nor even as a finite-valued logic, in the familiar sense. Although intuitionistic logic retains the trivial propositions <math>\{\top, \bot\}</math> from classical logic, each ''proof'' of a propositional formula is considered a valid propositional value, thus by [[Brouwer-Heyting-Kolmogorov|Heyting's]] notion of propositions-as-sets, propositional formulae are (potentially non-finite) sets of their proofs.

===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}}

===Kripke semantics===
{{Main|Kripke semantics}}

Building upon his work on semantics of [[modal logic]], [[Saul Kripke]] created another semantics for intuitionistic logic, known as Kripke semantics or relational semantics.{{sfn|Kripke|1965}}{{sfn|Moschovakis|2022}}{{sfn|Bezhanishvili|De Jongh|page=8}}

===Tarski-like semantics===
It was discovered that Tarski-like semantics for intuitionistic logic were not possible to prove complete. However, [[Robert Lee Constable|Robert Constable]] has shown that a weaker notion of completeness still holds for intuitionistic logic under a Tarski-like model. In this notion of completeness we are concerned not with all of the statements that are true of every model, but with the statements that are true ''in the same way'' in every model. That is, a single proof that the model judges a formula to be true must be valid for every model. In this case, there is not only a proof of completeness, but one that is valid according to intuitionistic logic.{{sfn|Constable|Bickford|2014}}