#
*
Intuiting Constructivism
*

This post goes over the philosophy of constructivism in mathematics, in particular, the intuitionist variant of constructivism.

This is meant to be an introduction to constructive logic and type theory and more posts will hopefully follow, in the future. Please, enjoy.

### Table of Contents

# Making sense of logic

If you've ever had a dive into some formal mathematical logic, you might have felt somewhat swamped by all
of the seemingly arbitrary definitions, the weird tree-like diagrams, the weird names such as
* Axiom K*,

*,*

**System F***(which all could be tracks on a metal album), and formulas which you do not understand, such as:*

**The Undefinability of Truth**$$ \begin{align*} P &\implies \Box \Diamond P \cr \Box P &\implies \Box \Box P \end{align*} $$

And **what for?**

Of course, there's a reason for all of this formalism and these systems.
What many people tend to forget is that we did not invent all of logic, and * then* math.

Diving head first into a piece of formal logic without understanding the rationale behind its creation.

I'll be writing about a subset of logic called **Intuitionist logic**, which embodies the **Constructivist**
philosophy of mathematics.
Let's start to unpack that, shall we?

# Constructing answers

Here's a funny question: **Are there two irrational numbers $a$ and $b$ such that $a^b$ is a rational number?**

Feel free to think about it. Try to come up with an answer.

Meanwhile, I'll present a solution myself:

Take for instance the number $\sqrt{2}^{\sqrt{2}}$. This number is either rational or irrational.

* If it is rational*, well, then we can have $a = b = \sqrt{2}$, and we're done, since $\sqrt{2}^{\sqrt{2}}$ is

*.*

**rational*** If it is irrational*, then have $a = \sqrt{2}^{\sqrt{2}}$ and $b = \sqrt{2}$. This way we have that:

$$ a^b = \left( {\sqrt{2}^{\sqrt{2}}} \right) ^ {\sqrt{2}} = \sqrt{2} ^ {\sqrt{2} \sqrt{2}} = {\sqrt{2}} ^ 2 = 2 $$

Which is * rational*.

So there are indeed some irrational $a$ and $b$ such that $a^b$ is rational! Which $a$ and $b$? **I don't know!**, it could be either of the two cases.
What I do know is that the answer to the question is **yes**.

Think about that for a moment. The question that I asked above accepts a simple yes or no. You don't need to tell me what the $a$ and $b$ are.

Now, in your attempt, did you try to * find* two irrational numbers $a$ and $b$ and then checked if $a^b$ was rational?
Did you

**feel**the need to find that $a$ and $b$?

If you did, then my proof was very unsatisfactory. Notice, that I have not stated that the proof is * wrong* or is

*somehow. No. It is perfectly valid. I have split the proof into two cases, and in each of those cases I have reached the conclusion that there is*

**cheating****some**pair of rationals in that case which when exponentiated give a rational, and that is logically valid.

Now, I'm not going to let this tease you any further. I'll give you * two actual numbers* that answer this question

**directly**.

Take $a = \sqrt{2}$ and $b = \log_2{9}$.
Both are irrational and if we work it out, then:
$$
a ^ b = (\sqrt{2}) ^ {(\log_2{9})} = \sqrt{ 2 ^ {(\log_2{9})}} = \sqrt{9} = 3
$$
which is **rational**.

This feels somewhat more satisfactory (to me at least).
I have given you two numbers and you can verify they they satisfy the requirements of the question.
I have **constructed** a solution, not just giving a yes/no answer (hence the name * Constructivism*).

I hope you can appreciate the * aesthetic* or the

*reason for why many might prefer the*

**philosophical***proof, as opposed to the*

**constructive***proof.*

**classical**But this seeming pedantry can actually be **useful** (* *gasps**).

Forgive me the contrived example, but imagine that at some point in your life, you require two irrational numbers
that when exponentiated give a rational number.
You might need this because you are writing a far more complicated proof, and you need these two numbers.
Maybe you're working on some cryptographic algorithm or proof, and you * need* these two numbers.

Well, the classical proof will tell you that there does exist such a pair of numbers, and at least you know your search isn't
futile, but the **constructive proof will straight up****give you the numbers**.

You get a real benefit of being able to * compose* proofs into constructions.
I concede, you can compose classical proofs too, but, critically, if at some point you require a concrete construction,
and you have composed classical proofs into your other constructive proofs, you are not guaranteed to be able to extract a construction.

The moment you introduce a proof with some **non-constructive element**, you are not able to then extract the constructed solution.

In the classical example above, the * non-constructive element* that was used was

*that a number is either*

**splitting the proof into cases***or*

**rational***, which isn't*

**irrational***, because we didn't actually show which of the cases was true.*

**constructively valid**(If you are curious, $\sqrt{2}^{\sqrt{2}}$ is irrational, see the Gelfond–Schneider theorem for details. Using this fact we can turn the previous classical proof into a constructive one.)

That might feel a little odd, since * irrational numbers are the non-rational reals*, so it seems cut and dry that a number is either rational or irrational,
but constructively, we have to

*, which isn't possible in the general sense, because the real numbers are very,*

**actually show that the number is either rational or irrational***,*

**very****very**weird in the constructive world. The best we can do is show that a number is

*. However, there are some*

**not rational***that do allow for this case, such as being a positive distance from every rational numbers, which are constructively valid, but that's beyond the scope of this text.*

**alternate definitions of the irrational numbers**## Which Intermediate Value, though?

A classic (* pun intended*) example of a non-constructive theorem is the Intermediate Value Theorem.

Essentially the IVT states that if a real function $f$ is continuous, and defined on the interval $[a,b]$, then it takes on every value between $f(a)$ and $f(b)$ in that interval.

The IVT doesn't state where those exact values are taken. For example, if the interval is $[0,1]$ and $f(0) = -1$ and $f(1) = 1$, then there is some $x$ in $[0,1]$ where $f(x) = 0$, but
we don't know * which one*.

It turns out, the IVT, in constructive mathematics is just, **wholly, and completely****false**. Yep, it is * not true*.

The reason why the IVT isn't constructive is because it relies on * case analysis*, once again. It splits into a case where we a real number is either less than $0$, equal to $0$, or greater
than $0$.
Unfortunately, in constructive mathematics, is

*. It is somewhat akin to checking that every digit in the infinite expansion of $0.00000000...$ is actually $0$. At any point, a $1$ could pop up, so it will take*

**impossible to prove that a real number is equal to $0$***. In fact, being able to check real equality for $0$ can*

**infinite time to check if the number is indeed zero***(you might start seeing inklings of the connection between constructivism and computability).*

**solve the Halting Problem**There is actually a special, albeit weaker, version of IVT for constructive mathematics, which, by being constructive does specify the value in the interval.

# BKH Interpretation of Intuitionism

Alright, I've given you a somewhat crude introduction as to what constructivism should be about, now its time to act like logicians and codify some rules.

I am going to show the now standard interpretation of intuitionist logic: the Brouwer–Heyting–Kolmogorov (BKH) interpretation.

The BKH interpretation states what exactly a proof of a formula **is**, and a proof roughly corresponds with the idea of * constructing* an object.

- A proof of $P \land Q$ is a pair $(a,b)$ where $a$ is a proof of $P$ and $b$ is a proof of $Q$.
- A proof of $P \lor Q$ is either a pair $(0,a)$ where $a$ is a proof of $P$ or a pair $(1,b)$ where $b$ is a proof of $Q$.
- A proof of $P \implies Q$ is a function that converts a proof of $P$ into a proof of $Q$.
- A proof of $(\exists x \in S)(P(x))$ is a pair $(x, p)$ where $x$ is in $S$ and $p$ is a proof of $P(x)$.
- A proof of $(\forall x \in S)(P(x))$ is a function that converts elements $x$ in $S$ into a proof of $P(x)$.
- There are no proofs of $\bot$ (which encodes falsehood or imposibility).
- $\neg P$ is defined as $P \implies \bot$.

I'd like to highlight three things here:

- The proof of $P \land Q$ maintains the proof of both statements separately, so that
.**no information is lost** - Likewise, $P \lor Q$ states
of the statements is true,**which****and**provides the proof of the statement. This deals with the problem of case analysis in our previous classical proofs. - The somewhat weird definition of negation is necessary because it is
to have $\neg P$ when there is no proof of $P$, thanks to Gödel (the biggest party pooper, ever).**impossible**

Let's take a look at our previous question regarding irrational numbers, and try to encode its proof in BKH.

Here's the statement: **There are two irrational numbers $a$ and $b$ such that $a^b$ is a rational number.**

Turning it into a logical formula, we'd get something like this: $ (\exists (a,b) \in (\R - \mathbb{Q})^2) (a^b \in \mathbb{Q}) $

We can see that this formula is an existential formula, in other words, of the type $(\exists x \in S)(P(x))$, with $x$ being $(a,b)$, $S$ being $(\R - \mathbb{Q})^2$ and $P(x)$ being $a^b \in \mathbb{Q}$.

A proof of this formula would then be a pair $((a,b), p)$ where $(a,b)$ is in $(\R - \mathbb{Q})^2$ and $p$ is a proof of $a^b \in \mathbb{Q}$.

Its somewhat clear that if we're translating our previous constructive proof, then $a = \sqrt{2}$ and $b = \log_2{9}$, but $p$ is somewhat trickier to find. We'd need to encode the fact that $a^b \in \mathbb{Q}$, which ultimately ends up being $3 \in \mathbb{Q}$ after some arithmetic.

The way in which to encode these more fundamental proofs, such as equality, and functions, is * somewhat contentious*.
Different opinions give rise to different encodings and systems of constructivism, such as

*,*

**Martin-Löf type theory***, etc.*

**Kleene's Realizability Theory**For simplicity's sake, let's say that we reduce values via arithmetic and that the way to encode that $x \in \mathbb{Q}$ is by providing a pair $(n,d) \in \Z^2$ such that $\frac{n}{d} = x$. In this way, we could encode $p$ as $(3,1)$, since $\frac{3}{1} = 3$.

Therefore, our * whole constructive proof* of the

*$ (\exists (a,b) \in (\R - \mathbb{Q})^2) (a^b \in \mathbb{Q}) $*

**formula***as $((\sqrt{2},\log_2{9}),(3,1))$.*

**could be written**## Working with proofs

I'd like to take a moment to address the fact that we have made a * subtle* yet

**major**shift in our treatment of proofs.

We are no longer considering a proof to be some words that we read that convince us, by adhering to some agreed upon rules, that a given statement is true or false.

We are now * treating proofs* themselves as

*, such as*

**tangible mathematical objects***and*

**pairs***. And beyond that, we can now construct new proofs from other proofs, by composing them in pairs, and passing them around functions.*

**functions**Given a particular formula, we can very much **construct** an object which **proves** the formula.
If there is any takeaway that I'd wish for you to retain from this post, is that in mathematical logic, we aren't just * using logic to encode math*, we are

**using math to encode logic**. This can come off as circular and, well, it's because it is, but we'll get to that later, when we discuss meta-languages.

# Against Constructivism

Alright, I've been somewhat praising constructivism, but * there has to be a catch*, right?
We can't

*and*

**have our cake***right? (Unless you know about the Banach–Tarski paradox, which actually relies on the Axiom of Choice, which in itself is non-constructive).*

**eat it**Well, we have already found some issues as we have gone along, mainly with case analysis and real numbers.

So I'll just dump it on you cold: we **can't use the Law of Excluded Middle** (in its general form).

What is * Excluded Middle* you ask? (

*)*

**If you didn't, uhm, sorry?**$$ \forall P, P \lor \neg P $$

Essentially, a statement is either true, or its negation is.

Getting rid of the Law of Excluded Middle * (LEM)* upset a lot of people and was generally considered a bad move at the time..

From * Constance Reid's "Hilbert"* a biography of the mathematician of the same name:

"Taking the Principle of the Excluded Middle from the mathematician," Hilbert said, "is the same as […] prohibiting the boxer the use of his fists."

So yeah, * it got pretty heated*.

*"But it doesn't seem that bad"* you say, mysterious reader.

* Oh, just you wait*.

LEM is equivalent to a lot of things. First of all, * double negation elimination*.

$$ \forall P, \neg \neg P \equiv P $$

* Classical contraposition* is then not valid because double negation isn't valid:
$$
\forall P, Q, (\neg P \implies \neg Q) \implies (Q \implies P)
$$

* Reductio ad Absurdum* is equivalent to LEM and therefore not valid
$$
\forall P, Q, (\neg P \implies Q) \land (\neg P \implies \neg Q) \implies P
$$

And, oh, yeah, **The Axiom of Choice** is inconsistent with not having LEM, since * Choice implies LEM*.
These are big blows. We prohibited the boxer from using his fists and he just kicked us instead.

*Funnily enough
$
\neg\neg(P\vee \neg P)
$
is actually constructively valid.*

A lot of * real analysis* also somewhat goes

**out of the window**. At least with the standard definitions. This mostly stems from the fact that the

*, which goes hand in hand with constructivism.*

**real numbers have a lot of issues when it comes to computability**The fact that * equality is not decidable* is big hindrance, even if inequality is semi-decidable.

* Exclusive Middle isn't completely lost* though, in the sense that decidable relations still obey LEM.
For example, the integers have decidable equality so we can always known/show that two integers are equal or they are not.

# Constructivist niche

So, if constructivism has * so many handicaps*, then

*? Well, as I've hinted as I've gone along, there are some*

**why am I even talking about it***with*

**deep connections***.*

**computability and computers*** Constructive logics* are the kind of logic that can be

*in typed programming languages and*

**encoded***, such as the previously mentioned*

**type theories***.*

**Martin-Löf type theory**Martin-Löf type theory encodes the principle of constructivism of building constructions, sometimes called witnesses of proof.

The general encoding is the following:

- Implication in the logic are functions in the type theory.
- $\bot$ corresponds to the empty type $\mathbf{0}$.
- The existential quantifier $\exists$ corresponds to the $\Sigma$ type constructor
- The universal quantifier $\forall$ corresponds to the $\Pi$ type constructor

All of this to say, since Martin-Löf type theory * encodes constructivist logic*, any programming language implementing it
can make use of constructive logic, even going so far as

**proving theorems**in the programming language!

In later posts, I will go over Martin-Löf type theories and other constructivist type theories, for that would be too much to handle in one post.

# Wrapping up

I hope I have shed some light into how constructivism can be a useful working in mathematics, despite its quirks. Especially, I wish you have gained some understanding of how it is possible to encode truths in a logical system into tangible objects, that can be manipulated and constructed, and even programmed in, in certain typed programming languages.

In the future, I will be diving in **deep** into those type theories, but as of now, I leave you here.
* I hope you have enjoyed reading*.

Bye, o/.