% part: intuitionistic-logic
% chapter: introduction
% section: constructive-reasoning

\documentclass[../../../include/open-logic-chapter]{subfiles}

\begin{document}

\olfileid{int}{int}{cr}

\section{Constructive Reasoning}

In contrast to extensions of classical logic by modal operators or
second-order quantifiers, intuitionistic logic is ``non-classical'' in
that it restricts classical logic.  Classical logic is
\emph{non-constructive} in various ways. Intuitionistic logic is
intended to capture a more ``constructive'' kind of reasoning
characteristic of a kind of constructive mathematics. The following
examples may serve to illustrate some of the underlying motivations.

Suppose someone claimed that they had determined a natural number~$n$
with the property that if $n$ is even, the Riemann hypothesis is
true, and if $n$ is odd, 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 they seem to have reduced the
problem to one of calculation, that is, to the determination of
whether a specific number is even or not.

What is the magic value of~$n$? They describe it as follows: $n$ is
the natural number that is equal to $2$ if the Riemann hypothesis is
true, and $3$ otherwise.

Angrily, you demand your money back. From a classical point of view,
the description above does in fact determine a unique value of $n$;
but what you really want is a value of $n$ that is given
\emph{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 \emph{irrational} power, and get a
rational result. The following theorem answers this in the
affirmative:

\begin{thm}
There are irrational numbers $a$ and $b$ such that $a^b$ is rational.
\end{thm}

\begin{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,
\]
which is rational. So, in this case, let $a$ be
$\sqrt{2}^{\sqrt{2}}$, and let $b$ be~$\sqrt 2$.
\end{proof}

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 \emph{which} pair of numbers it
is.  It is possible to prove the same result, but in such a way that
the pair $a$, $b$ \emph{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,
\]
since $3^{\log_3 x} = x$.

Intuitionistic logic is designed to capture 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 logic is what you get if
you restrict !!a{derivation} system for classical logic in a certain
way. From the mathematical point of view, these are
just formal deductive systems, but, as already noted, they are
intended to capture 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.

\end{document}