2.7.5: Intuitionistic Logic

\(\def\Assign#1#2{ { #1^{\Struct{#2}} } }\)
\(\def\Atom#1#2{ { \mathord{#1}(#2) } }\)
\(\def\Bin{ {\mathbb{B}} }\)
\(\def\cardeq#1#2{ { #1 \approx #2 } }\)
\(\def\cardle#1#2{ { #1 \preceq #2 } }\)
\(\def\cardless#1#2{ { #1 \prec #2 } }\)
\(\def\cardneq#1#2{ { #1 \not\approx #2 } }\)
\(\def\comp#1#2{ { #2 \circ #1 } }\)
\(\def\concat{ { \;\frown\; } }\)
\(\def\Cut{ { \text{Cut} } }\)
\(\def\Discharge#1#2{ { [#1]^#2 } }\)
\(\def\DischargeRule#1#2{ { \RightLabel{#1}\LeftLabel{\scriptsize{#2} } } }\)
\(\def\dom#1{ {\operatorname{dom}(#1)} }\)
\(\def\Domain#1{ {\left| \Struct{#1} \right|} }\)
\(\def\Elim#1{ { {#1}\mathrm{Elim} } }\)
\(\newcommand{\Entails}{\vDash}\)
\(\newcommand{\EntailsN}{\nvDash}\)
\(\def\eq[#1][#2]{ { #1 = #2 } }\)
\(\def\eqN[#1][#2]{ { #1 \neq #2 } }\)
\(\def\equivclass#1#2{ { #1/_{#2} } }\)
\(\def\equivrep#1#2{ { [#1]_{#2} } }\)
\(\def\Exchange{ { \text{X} } }\)
\(\def\False{ { \mathbb{F} } }\)
\(\def\FalseCl{ { \lfalse_C } }\)
\(\def\FalseInt{ { \lfalse_I } }\)
\(\def\fCenter{ { \,\Sequent\, } }\)
\(\def\fdefined{ { \;\downarrow } }\)
\(\def\fn#1{ { \operatorname{#1} } }\)
\(\def\Frm[#1]{ {\operatorname{Frm}(\Lang #1)} }\)
\(\def\fundefined{ { \;\uparrow } }\)
\(\def\funimage#1#2{ { #1[#2] } }\)
\(\def\funrestrictionto#1#2{ { #1 \restriction_{#2} } }\)
\(\newcommand{\ident}{\equiv}\)
\(\newcommand{\indcase}[2]{#1 \ident #2\text{:}}\)
\(\newcommand{\indcaseA}[2]{#1 \text{ is atomic:}}\)
\(\def\indfrm{ { A } }\)
\(\def\indfrmp{ { A } }\)
\(\def\joinrel{\mathrel{\mkern-3mu}}\)
\(\def\lambd[#1][#2]{\lambda #1 . #2}\)
\(\def\Lang#1{ { \mathcal{#1} } }\)
\(\def\LeftR#1{ { {#1}\mathrm{L} } }\)
\(\def\len#1{ {\operatorname{len}(#1)} }\)
\(\def\lexists#1#2{ { \exists #1\, #2 } }\)
\(\def\lfalse{ {\bot} }\)
\(\def\lforall#1#2{ { \forall#1\, #2 } }\)
\(\newcommand{\lif}{\rightarrow}\)
\(\newcommand{\liff}{\leftrightarrow}\)
\(\def\Log#1{ { \mathbf{#1} } }\)
\(\def\ltrue{ {\top} }\)
\(\def\Id#1{ {\operatorname{Id}_#1} }\)
\(\def\Int{ {\mathbb{Z}} }\)
\(\def\Intro#1{ { {#1}\mathrm{Intro} } }\)
\(\def\mModel#1{ { \mathfrak{#1} } }\)
\(\newcommand{\mSat}[3][{}]{\mModel{#2}{#1}\Vdash{#3}}\)
\(\newcommand{\mSatN}[3][{}]{\mModel{#2}{#1}\nVdash{#3}}\)
\(\def\Nat{ {\mathbb{N}} }\)
\(\def\nicefrac#1#2{ {{}^#1/_#2} }\)
\(\def\num#1{ { \overline{#1} } }\)

\(\def\ran#1{ {\operatorname{ran}(#1)} }\)
\(\newcommand{\Obj}[1]{\mathsf{#1}}\)
\(\def\Rat{ {\mathbb{Q}} }\)
\(\def\Real{ {\mathbb{R}} }\)
\(\def\RightR#1{ { {#1}\mathrm{R} } }\)
\(\def\Part#1#2{ { \Atom{\Obj P}{#1, #2} } }\)
\(\def\pto{ { \hspace{0.1 cm}\to\hspace{-0.44 cm}\vcenter{\tiny{\hbox{|}}}\hspace{0.35 cm} } }\)
\(\def\PosInt{ {\mathbb{Z}^+} }\)
\(\def\Pow#1{ {\wp(#1)} }\)
\(\newcommand{\Proves}{\vdash}\)
\(\newcommand{\ProvesN}{\nvdash}\)
\(\def\Relbar{\mathrel{=}}\)
\(\newcommand{\Sat}[3][{}]{\Struct{#2}{#1}\vDash{#3}}\)
\(\newcommand{\SatN}[3][{}]{\Struct{#2}{#1}\nvDash{#3}}\)
\(\newcommand{\Sequent}{\Rightarrow}\)
\(\def\Setabs#1#2{ { \{#1:#2\} } }\)
\(\newcommand{\sFmla}[2]{#1\,#2}\)
\(\def\Struct#1{ {#1} }\)
\(\def\subst#1#2{ { #1/#2 } }\)
\(\def\Subst#1#2#3{ { #1[\subst{#2}{#3}] } }\)
\(\def\TMblank{ { 0 } }\)
\(\newcommand{\TMendtape}{\triangleright}\)
\(\def\TMleft{ { L } }\)
\(\def\TMright{ { R } }\)
\(\def\TMstay{ { N } }\)
\(\def\TMstroke{ { 1 } }\)
\(\def\TMtrans#1#2#3{ { #1,#2,#3 } }\)
\(\def\Trm[#1]{ {\operatorname{Trm}(\Lang #1)} }\)
\(\def\True{ { \mathbb{T} } }\)
\(\newcommand{\TRule}[2]{#2#1}\)
\(\def\tuple#1{ {\langle #1 \rangle} }\)
\(\newcommand{\Value}[3][\,]{\mathrm{Val}_{#1}^{#3}(#2)}\)
\(\def\Var{ { \mathrm{Var} } }\)
\(\newcommand{\varAssign}[3]{#1 \sim_{#3} #2}\)
\(\def\Weakening{ { \text{W} } }\)

In constrast to second-order and higher-order logic, intuitionistic first-order logic represents a restriction of the classical version, intended to model a more “constructive” kind of reasoning. The following examples may serve to illustrate some of the underlying motivations.

Suppose someone came up to you one day and announced that they had determined a natural number \(x\), with the property that if \(x\) is prime, the Riemann hypothesis is true, and if \(x\) is composite, the Riemann hypothesis is false. Great news! Whether the Riemann hypothesis is true or not is one of the big open questions of mathematics, and here they seem to have reduced the problem to one of calculation, that is, to the determination of whether a specific number is prime or not.

What is the magic value of \(x\)? They describe it as follows: \(x\) is the natural number that is equal to \(7\) if the Riemann hypothesis is true, and \(9\) otherwise.

Angrily, you demand your money back. From a classical point of view, the description above does in fact determine a unique value of \(x\); but what you really want is a value of \(x\) that is given explicitly.

To take another, perhaps less contrived example, consider the following question. We know that it is possible to raise an irrational number to a rational power, and get a rational result. For example, \(\sqrt{2}^2 = 2\). What is less clear is whether or not it is possible to raise an irrational number to an irrational power, and get a rational result. The following theorem answers this in the affirmative:

Theorem \(\PageIndex{1}\)

There are irrational numbers \(a\) and \(b\) such that \(a^b\) is rational.

Proof. Consider \(\sqrt{2}^{\sqrt{2}}\). If this is rational, we are done: we can let \(a = b = \sqrt{2}\). Otherwise, it is irrational. Then we have \[(\sqrt{2}^{\sqrt{2}})^{\sqrt{2}} = \sqrt{2}^{\sqrt{2} \cdot \sqrt{2}} = \sqrt{2}^2 = 2,\nonumber\] which is certainly rational. So, in this case, let \(a\) be \(\sqrt{2}^{\sqrt{2}}\), and let \(b\) be \(\sqrt 2\). ◻

Does this constitute a valid proof? Most mathematicians feel that it does. But again, there is something a little bit unsatisfying here: we have proved the existence of a pair of real numbers with a certain property, without being able to say which pair of numbers it is. It is possible to prove the same result, but in such a way that the pair \(a\), \(b\) is given in the proof: take \(a = \sqrt{3}\) and \(b = \log_3 4\). Then \[a^b = \sqrt{3}^{\log_3 4} = 3^{1/2 \cdot \log_3 4} = (3^{\log_3 4})^{1/2} = 4^{1/2}= 2,\nonumber\] since \(3^{\log_3 x} = x\).

Intuitionistic logic is designed to model a kind of reasoning where moves like the one in the first proof are disallowed. Proving the existence of an \(x\) satisfying \(A(x)\) means that you have to give a specific \(x\), and a proof that it satisfies \(A\), like in the second proof. Proving that \(A\) or \(B\) holds requires that you can prove one or the other.

Formally speaking, intuitionistic first-order logic is what you get if you omit restrict a proof system for first-order logic in a certain way. Similarly, there are intuitionistic versions of second-order or higher-order logic. From the mathematical point of view, these are just formal deductive systems, but, as already noted, they are intended to model a kind of mathematical reasoning. One can take this to be the kind of reasoning that is justified on a certain philosophical view of mathematics (such as Brouwer’s intuitionism); one can take it to be a kind of mathematical reasoning which is more “concrete” and satisfying (along the lines of Bishop’s constructivism); and one can argue about whether or not the formal description captures the informal motivation. But whatever philosophical positions we may hold, we can study intuitionistic logic as a formally presented logic; and for whatever reasons, many mathematical logicians find it interesting to do so.

There is an informal constructive interpretation of the intuitionist connectives, usually known as the BHK interpretation (named after Brouwer, Heyting, and Kolmogorov). It runs as follows: a proof of \(A \land B\) consists of a proof of \(A\) paired with a proof of \(B\); a proof of \(A \lor B\) consists of either a proof of \(A\), or a proof of \(B\), where we have explicit information as to which is the case; a proof of \(A \lif B\) consists of a procedure, which transforms a proof of \(A\) to a proof of \(B\); a proof of \(\lforall{x}{A(x)}\) consists of a procedure which returns a proof of \(A(x)\) for any value of \(x\); and a proof of \(\lexists{x}{A(x)}\) consists of a value of \(x\), together with a proof that this value satisfies \(A\). One can describe the interpretation in computational terms known as the “Curry-Howard isomorphism” or the “formulas-as-types paradigm”: think of a formula as specifying a certain kind of data type, and proofs as computational objects of these data types that enable us to see that the corresponding formula is true.

Intuitionistic logic is often thought of as being classical logic “minus” the law of the excluded middle. This following theorem makes this more precise.

Theorem \(\PageIndex{2}\)

Intuitionistically, the following axiom schemata are equivalent:

1. \((A \lif \lfalse) \lif \lnot A\).
2. \(A \lor \lnot A\)
3. \(\lnot \lnot A \lif A\)

Obtaining instances of one schema from either of the others is a good exercise in intuitionistic logic.

The first deductive systems for intuitionistic propositional logic, put forth as formalizations of Brouwer’s intuitionism, are due, independently, to Kolmogorov, Glivenko, and Heyting. The first formalization of intuitionistic first-order logic (and parts of intuitionist mathematics) is due to Heyting. Though a number of classically valid schemata are not intuitionistically valid, many are.

The double-negation translation describes an important relationship between classical and intuitionist logic. It is defined inductively follows (think of \(A^N\) as the “intuitionist” translation of the classical formula \(A\)): \[\begin{aligned} A^N & \ident \lnot\lnot A \quad \text{for atomic formulas $A$} \\ (A \land B)^N & \ident (A^N \land B^N) \\ (A \lor B)^N & \ident \lnot\lnot (A^N \lor B^N) \\ (A \lif B)^N & \ident (A^N \lif B^N) \\ (\lforall{x}{A})^N & \ident \lforall{x}{A^N} \\ (\lexists{x}{A})^N & \ident \lnot\lnot\lexists{x}{A^N}\end{aligned}\] Kolmogorov and Glivenko had versions of this translation for propositional logic; for predicate logic, it is due to Gödel and Gentzen, independently. We have

Theorem \(\PageIndex{3}\)

1. \(A \liff A^N\) is provable classically
2. If \(A\) is provable classically, then \(A^N\) is provable intuitionistically.

We can now envision the following dialogue. Classical mathematician: “I’ve proved \(A\)!” Intuitionist mathematician: “Your proof isn’t valid. What you’ve really proved is \(A^N\).” Classical mathematician: “Fine by me!” As far as the classical mathematician is concerned, the intuitionist is just splitting hairs, since the two are equivalent. But the intuitionist insists there is a difference.

Note that the above translation concerns pure logic only; it does not address the question as to what the appropriate nonlogical axioms are for classical and intuitionistic mathematics, or what the relationship is between them. But the following slight extension of the theorem above provides some useful information:

Theorem \(\PageIndex{4}\)

If \(\Gamma\) proves \(A\) classically, \(\Gamma^N\) proves \(A^N\) intuitionistically.

In other words, if \(A\) is provable from some hypotheses classically, then \(A^N\) is provable from their double-negation translations.

To show that a sentence or propositional formula is intuitionistically valid, all you have to do is provide a proof. But how can you show that it is not valid? For that purpose, we need a semantics that is sound, and preferrably complete. A semantics due to Kripke nicely fits the bill.

We can play the same game we did for classical logic: define the semantics, and prove soundness and completeness. It is worthwhile, however, to note the following distinction. In the case of classical logic, the semantics was the “obvious” one, in a sense implicit in the meaning of the connectives. Though one can provide some intuitive motivation for Kripke semantics, the latter does not offer the same feeling of inevitability. In addition, the notion of a classical structure is a natural mathematical one, so we can either take the notion of a structure to be a tool for studying classical first-order logic, or take classical first-order logic to be a tool for studying mathematical structures. In contrast, Kripke structures can only be viewed as a logical construct; they don’t seem to have independent mathematical interest.

A Kripke structure \(\mModel M = \tuple{W, R, V}\) for a propositional language consists of a set \(W\), partial order \(R\) on \(W\) with a least element, and an “monotone” assignment of propositional variables to the elements of \(W\). The intuition is that the elements of \(W\) represent “worlds,” or “states of knowledge”; an element \(v \geq u\) represents a “possible future state” of \(u\); and the propositional variables assigned to \(u\) are the propositions that are known to be true in state \(u\). The forcing relation \(\mSat[,w]{M}{A}\) then extends this relationship to arbitrary formulas in the language; read \(\mSat[,w]{M}{A}\) as “\(A\) is true in state \(w\).” The relationship is defined inductively, as follows:

1. \(\mSat[,w]{M}{\Obj p_i}\) iff \(\Obj p_i\) is one of the propositional variables assigned to \(w\).
2. \(\mSatN[,w]{M}{\lfalse}\).
3. \(\mSat[,w]{M}{(A \land B)}\) iff \(\mSat[,w]{M}{A}\) and \(\mSat[,w]{M}{B}\).
4. \(\mSat[,w]{M}{(A \lor B)}\) iff \(\mSat[,w]{M}{A}\) or \(\mSat[,w]{M}{B}\).
5. \(\mSat[,w]{M}{(A \lif B)}\) iff, whenever \(w' \geq w\) and \(\mSat[,w']{M}{A}\), then \(\mSat[,w']{M}{B}\).

It is a good exercise to try to show that \(\lnot (p \land q) \lif (\lnot p \lor \lnot q)\) is not intuitionistically valid, by cooking up a Kripke structure that provides a counterexample.