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.

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, The Undefinability of Truth (which all could be tracks on a metal album), and formulas which you do not understand, such as:

\begin{aligned} 𝑃 & \Rightarrow □ ◇ 𝑃 \\ □ 𝑃 & \Rightarrow □ □ 𝑃 \end{aligned}

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 $𝑎$ and $𝑏$ such that $𝑎^{𝑏}$ 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 $𝑎 = 𝑏 = \sqrt{2}$ , and we’re done, since ${\sqrt{2}}^{\sqrt{2}}$ is rational, and $\sqrt{2}$ is irrational. If it is irrational, then have $𝑎 = {\sqrt{2}}^{\sqrt{2}}$ and $𝑏 = \sqrt{2}$ . This way we have that:

𝑎^{𝑏} = {({\sqrt{2}}^{\sqrt{2}})}^{\sqrt{2}} = {\sqrt{2}}^{\sqrt{2} \sqrt{2}} = {\sqrt{2}}^{2} = 2

Which is rational.

So there are indeed some irrational $𝑎$ and $𝑏$ such that $𝑎^{𝑏}$ is rational! Which $𝑎$ and $𝑏$ ? 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 $𝑎$ and $𝑏$ are.

Now, in your attempt, did you try to find two irrational numbers $𝑎$ and $𝑏$ and then checked if $𝑎^{𝑏}$ was rational? Did you feel the need to find that $𝑎$ and $𝑏$ ?

If you did, then my proof was very unsatisfactory. Notice, that I have not stated that the proof is wrong or is cheating 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 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 $𝑎 = \sqrt{2}$ and $𝑏 = lg (9)$ (where $lg$ is the binary logarithm). Both are irrational and if we work it out, then:

𝑎^{𝑏} = {(\sqrt{2})}^{lg (9)} = \sqrt{2^{log (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 philosophical reason for why many might prefer the constructive proof, as opposed to the classical proof. 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 splitting the proof into cases that a number is either rational or irrational, which isn’t constructively valid, because we didn’t actually show which of the cases was true.

(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 actually show that the number is either rational or irrational, which isn’t possible in the general sense, because the real numbers are very, very, very weird in the constructive world. The best we can do is show that a number is not rational. However, there are some alternate definitions of the irrational numbers 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.

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 $𝑓$ is continuous, and defined on the interval $[𝑎, 𝑏]$ , then it takes on every value between $𝑓 (𝑎)$ and $𝑓 (𝑏)$ in that interval.

The IVT doesn’t state where those exact values are taken. For example, if the interval is $[0, 1]$ and $𝑓 (0) = - 1$ and $𝑓 (1) = 1$ , then there is some $𝑥$ in $[0, 1]$ where $𝑓 (𝑥) = 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 impossible to prove that a real number is equal to $0$ . It is somewhat akin to checking that every digit in the infinite expansion of $0.00000000 \dots$ is actually $0$ . At any point, a $1$ could pop up, so it will take infinite time to check if the number is indeed zero. In fact, being able to check real equality for $0$ can solve the Halting Problem (you might start seeing inklings of the connection between constructivism and computability).

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 $𝑃 \land 𝑄$ is a pair $(𝑎, 𝑏)$ where $𝑎$ is a proof of $𝑃$ and $𝑏$ is a proof of $𝑄$ .
A proof of $𝑃 \lor 𝑄$ is either a pair $(0, 𝑎)$ where $𝑎$ is a proof of $𝑃$ or a pair $(1, 𝑏)$ where $𝑏$ is a proof of $𝑄$ .
A proof of $𝑃 \Rightarrow 𝑄$ is a function that converts a proof of $𝑃$ into a proof of $𝑄$ .
A proof of $(\exists 𝑥 \in 𝑆) (𝑃 (𝑥))$ is a pair $(𝑥, 𝑝)$ where $𝑥$ is in $𝑆$ and $𝑝$ is a proof of $𝑃 (𝑥)$ .
A proof of $(\forall 𝑥 \in 𝑆) (𝑃 (𝑥))$ is a function that converts elements $𝑥$ in $𝑆$ into a proof of $𝑃 (𝑥)$ .
There are no proofs of $⊥$ (which encodes falsehood or imposibility).
$\neg 𝑃$ is defined as $𝑃 \Rightarrow ⊥$ .

I’d like to highlight three things here:

The proof of $𝑃 \land 𝑄$ maintains the proof of both statements separately, so that no information is lost.
Likewise, $𝑃 \lor 𝑄$ states which of the statements is true, 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 impossible to have $\neg 𝑃$ when there is no proof of $𝑃$ , thanks to Gödel (the biggest party pooper, ever).

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 $𝑎$ and $𝑏$ such that $𝑎^{𝑏}$ is a rational number.

Turning it into a logical formula, we’d get something like this:

(\exists (𝑎, 𝑏) \in {(ℝ - ℚ)}^{2}) (𝑎^{𝑏} \in ℚ)

We can see that this formula is an existential formula, in other words, of the type $(\exists 𝑥 \in 𝑆) (𝑃 (𝑥))$ , with $𝑥$ being $(𝑎, 𝑏)$ , $𝑆$ being ${(ℝ - ℚ)}^{2}$ and $𝑃 (𝑥)$ being $𝑎^{𝑏} \in 𝑄$ .

A proof of this formula would then be a pair $((𝑎, 𝑏), 𝑝)$ where $(𝑎, 𝑏)$ is in ${(ℝ - ℚ)}^{2}$ and $𝑝$ is a proof of $𝑎^{𝑏} \in ℚ$ .

Its somewhat clear that if we’re translating our previous constructive proof, then $𝑎 = \sqrt{2}$ and $𝑏 = lg (9)$ , but $𝑝$ is somewhat trickier to find. We’d need to encode the fact that $𝑎^{𝑏} \in ℚ$ , which ultimately ends up being $3 \in ℚ$ 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, Kleene’s Realizability Theory, etc.

For simplicity’s sake, let’s say that we reduce values via arithmetic and that the way to encode that $𝑥 \in ℚ$ is by providing a pair $(𝑛, 𝑑) \in ℤ^{2}$ such that $\frac{𝑛}{𝑑} = 𝑥$ . In this way, we could encode $𝑝$ as $(3, 1)$ , since $\frac{3}{1} = 3$ .

Therefore, our whole constructive proof of the formula

(\exists (𝑎, 𝑏) \in {(ℝ - ℚ)}^{2}) (𝑎^{𝑏} \in ℚ)

could be written as $((\sqrt{2}, lg (9)), (3, 1))$ .

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 tangible mathematical objects, such as pairs and functions. And beyond that, we can now construct new proofs from other proofs, by composing them in pairs, and passing them around 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 have our cake and eat it right? (Unless you know about the Banach–Tarski paradox, which actually relies on the Axiom of Choice, which in itself is non-constructive).

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 𝑃, 𝑃 \lor \neg 𝑃

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 𝑃, \neg \neg 𝑃 \equiv 𝑃

Classical contraposition is then not valid because double negation isn’t valid:

\forall 𝑃, 𝑄, (\neg 𝑃 \Rightarrow \neg 𝑄) \Rightarrow (𝑄 \Rightarrow 𝑃)

Reductio ad Absurdum is equivalent to LEM and therefore not valid

\forall 𝑃, 𝑄, (\neg 𝑃 \Rightarrow 𝑄) \land (\neg 𝑃 \Rightarrow \neg 𝑄) \Rightarrow 𝑃

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 (𝑃 \lor \neg 𝑃) 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 real numbers have a lot of issues when it comes to computability, which goes hand in hand with constructivism.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 nicheSo, if constructivism has so many handicaps, then why am I even talking about it ? Well, as I’ve hinted as I’ve gone along, there are some deep connections with computability and computers .Constructive logics are the kind of logic that can be encoded in typed programming languages and type theories, such as the previously mentioned 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. ⊥ corresponds to the empty type 0 . The existential quantifier \exists corresponds to the Σ type constructor The universal quantifier \forall corresponds to the Π type constructorAll 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 upI 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/.❖