# Proof, Truth, and Computation

*intuitionistic logic and the foundations of mathematics*

I gave a talk at CUMC over the summer, on intuitionistic logic and the foundations of mathematics. I spent quite a bit of time on it, and thought it went relatively well, so decided to upload the slides and transcript here!

Around the turn of the 20th century, mathematicians ran into a problem. A pretty
big problem. A crisis, if you will. They started caring about their *foundations*: their
justification for assuming the principles of mathematics they did. And when they
started looking closer, they discovered that things were not exactly as they seemed.
Little paradoxes and concerning, very weird statements began to pop up - most
famously Russell’s paradox. This led to a very real worry that if their foundations
weren’t solid, mathematics was building atop a house of cards - with total collapse
being inevitable. I’m going to talk about this a little more later. But this is the
backdrop of our story - intuitionism and subsequently intuitionistic logic came out
of this setting.

So - intuitionistic logic, which is what this talk is mostly about, is a formal system,
and I’m going to need to introduce some formal notation to sufficiently describe it.
This up here is an *inference* - you can think of it as vaguely analogous to natural
deduction. On the left hand side here we have $Γ$ - $Γ$ is a context, and can be thought of
as the set of arbitrary propositions. On the right hand side is $A$ - some proposition.
In the middle here, we have a single tack - annotated with a $c$. The $c$ stands for
classically - in the wild, the logical system is frequently implicit, but I want to be
very explicit in this talk about when we are talking about classical logic and
intuitionistic logic. As a whole, we pronounce this as Gamma *classically* entails A.

So the reason logicians do not simply re-use the standard implication arrow is -
aside from notational confusion - that there are actually two notions of validity, or
entailment, that are interesting to talk about! We have here, syntactic validity. This
corresponds to proof, or in philosophical terms, sense. We say that $A$ is *syntactically*
derived by $Γ$ when applying dumb rewrite rules to $Γ$ can yield us $A$.
Semantic validity, on the other hand, concerns itself with preserving *truth*. This
corresponds to a philosophical of meaning, or *denotation*. We say that $A$ is
*semantically entailed* by $Γ$ if $A$ is true only when $Γ$ is.

So, what kind of falls out of having separate notions of validity are equivalences
between them. This is soundness and completeness. If you’ve heard about a system
being sound, there is actually a formal definition of what *sound* means. We say that
a system is sound if every syntactically valid inference - every proof - is
semantically correct. This is very important! Unsound logics are… not great. We say
that a system is *complete* if every semantically valid inference - everything that is
true - is *provable*. It’s less common for people to talk about completeness, because a
lot of useful logics are incomplete - including, famously, second-order classical logic.
A guy named Gödel had interesting things to say about that - he showed that there
are true propositions that cannot be *proved*, in a sufficiently complex system with
finite axioms. (If you had infinite axioms, you could simply have an axiom for each
true proposition… so that’s cheating.)

Alright, so let’s go back to our foundational crisis. A major result of the crisis was
the creation of Hilbert’s program - David Hilbert is this guy by the way, mostly
known for his work in foundations and his cool hat - which aimed to provide a
*consistent* (or sound) and *complete* framework for mathematics, as a set of axioms.
Kind of subsequently, and we’ll talk about this a little bit later, he also wanted
mathematics to be *decidable* - for there to exist some algorithm that can spit out
true or false for any well-founded mathematical statement. This actually took some
time after Gödel to be resolved, but once again, it ended in decisive failure for
Hilbert’s program - both Church and Turing showed this with their work on the
*entscheidungsproblem* (“decision problem”) and the halting problem.

On the other hand - diametrically and vehemently opposed, lay Brouwer. LEJ
Brouwer was an extremely accomplished mathematician, most famously known for
his work in topology. He was also Dutch. The Dutch care about their logic. Separate
from his work in standard mathematics - he freely used classical logic - he also had
some interesting ideas about the philosophy of mathematics: he believed that
mathematics was a *pure* form of reasoning, making mental *constructions* -
“constructions” here is important - and could only be properly captured in the mind
of the mathematician. Writing it down as a formal system, then - Hilbert’s program -
was a fool’s game, and the two of them exchanged rather heated words over this
point. Brouwer had pretty good philosophical arguments for his side of things - one
being that the principle of excluded middle - that a proposition is either true or false -
doesn’t really, make sense? He held the excluded middle to be an *overused* axiom:
valid in some contexts, not valid in others or generally, yet *consistent* nonetheless.
This is an important point! Classical logic is not *wrong*! Classical logic is just
perhaps not the *best* foundation of mathematics.

Alright. So Hilbert wants a formal system for all of mathematics, Brouwer believes
it can be done only in the mind. Enter Heyting. Heyting was Brouwer’s student:
firmly an intuitionist. What he did is quite funny: he took Brouwer’s philosophy of
mind, his anti-syntactic intuitionism: and wrote down syntax for it! Brouwer was
not too happy about this. But uh, I am. You might notice that these are called
Heyting *semantics*, but they are using this single-tack symbol that we said earlier
was *syntactic*: this is Heyting’s somewhat brilliant idea. *No longer* are we modelling
truth. We are modelling *proof*. We say that $A$ means that there is a *proof* of $A$,
$A ∧ B$ means that there is both a proof of $A$ and a proof of $B$, $A ∨ B$ means that there is
either a proof of $A$ or a proof of $B$. $A$ implies $B$ means that one can *construct* - again,
“construct” is important - a proof of $B$ from $A$. The negation says that there is a
proof that there is *no proof* of $A$. Not that $A$ is false!

Here in the corner I’ve snuck a very important result of these rules - the excluded middle
does not hold in intuitionistic logic! It is not a *tautology*. It can still be true, in certain
conditions, but reading it: we say “A proof of $A$ or a proof there is *no proof* of $A$”.
This is not always true! What if we simply had no proof of $A$? What about, say, the twin
primes conjecture? On the other hand, what if we had a proof *there is no proof* of $A$?
What about the continuum hypothesis?

I do not have time to go into the last two, but these inspired the field of *dependent*
type theory. The talk following this is going to go over a profound connection
between intuitionistic logic and dependent type theory - well, between propositions
and types as a whole, but dependent type theory is where it gets interesting. So
stick around for that. Propositions as types is, far and away the most beautiful and
interesting singular thing that I’ve ever learned about, I think. And I’m very sad
that I don’t have time to talk about it here.

Okay, back on topic. This is intuitionistic logic: it is separate from intuitionism. So
why do we do this? What does this give us? Well, for one, this perhaps more
accurately models what mathematics really is! There *are* propositions neither true
nor false: because we have not proven them yet, or because there is no proof. There
are a lot more technical details baked up in this, but I’m going to have to move on.

I’ve explicitly mentioned “construction” a number of times: we typically *construct* a
proof, for example. There are some proofs that intuitionists would consider
*nonconstructive*: for example, pulling an object out of an existential proposition -
this subtly uses proof by contradiction, which does not hold in intuitionistic logic.

Actually, a *lot* of things do not hold in intuitionistic logic. The principle of the
excluded middle is not valid. The axiom of choice actually implies the principle of
the excluded middle, in an intuitionistic system, and so it also does not hold. Again,
this is “hold” as a *tautology* - as propositions, they can be true, in some cases.
Something that is straight-up *false*, though, is the intermediate value theorem! The
intermediate value theorem says that if $f$ is continuous over an interval $[a, b]$ it
takes on all values between $a$ and $b$ at *some* point. That “some” is not constructive!

So why would you do this? Why would you ever want to work with an intuitionistic
system, when you lose so much of mathematics? First, intuitionistic logic provides
for a more intuitive notion of proof, as we talked about earlier. Second, intuitionistic
logic is amenable to *computational* interpretations, which we’ll talk more about in a
minute. But most importantly - you can *still do nonconstructive mathematics*! You
can simply assume the principle of the excluded middle as an axiom. And having a
way to do constructive mathematics is useful! For example, while classical analysis
does not hold in an intuitionistic system - without additional axioms, that is -
*constructive* analysis (which is a little bit more difficult - weaker) will *give* you
concrete mathematical objects! Which, for the constructive intermediate value
theorem, takes the form of an algorithm for arbitrarily precise approximations!

This principle of the excluded middle really can be considered a principle, or axiom,
of *decidability*: it lets us assume that we either have a proof of $A$ or a proof there is
no proof of $A$. Which is exactly decidability! And I really want to emphasize again
that this principle is not *false* - it is just sometimes very helpful to treat it like an
independent axiom of your logical system, for *constructive*, *computational* reasons.

I am very low on time, so I am going to rush through the rest of this, which I kind of
designed to be rushed through. First off - there are these things called proof
assistants. There are different types of proof assistants - the most successful ones
building atop *dependent type theory*, which is related to the beautiful intuitionistic
propositions-as-types correspondence I mentioned earlier. They are an embodiment
of this constructive, computable, way of mathematics that intuitionism and
intuitionistic logic set the stage for. Even though these proof assistants are
intuitionistic - they can admit classical reasoning, too, you just lose *some* of your
computational interpretation. This here is the standard representation of the
natural numbers in a proof assistant, I put this here because I wanted to make a
point that I no longer have time to make.

Anyway. Here is a split-second overview of the correspondence between propositions
and types - you can see that each of our propositional symbols, our logical
connectives, have a corresponding *type* constructor. You’ll see more of this in the
next talk though!

But we’ve talked about why intuitionistic logic is useful - why are proof assistants
useful? They’re useful for a number of reasons - there are many, many stories of
people outside of the mathematical community or without or without access to a
standard background in mathematics who pick up a proof assistant, and able to
reason in a system that does not admit errors, learn *mathematics*. But they are also
useful because math is hard! In an ideal world, we have peer review to catch
mistakes in proof, and mathematics builds atop a solid, concrete, justifiable
foundation. But in the real world, we have proofs like Wiles’ proof of Fermat’s Last
Theorem spanning over a hundred pages, taking years to verify, and other proofs,
disputed for their complexity, like the possible proof of the ABC conjecture!

A more recent example is a proof mechanized by Sky Winshaw that New
Foundations - an alternative foundations of mathematics - is consistent with respect
to ZFC! You can’t really prove that it is consistent relative to itself because - Gödel -
but this is just here to emphasize that proof assistants work for complicated proofs.
And provide a stronger notion of validity! Another example comes from the field of
*condensed mathematics*, actually: one Peter Scholze was having some trouble
believing his proof. He turned to the Lean community, started up a mechanization
project, and as it turned out: mechanization both gave justification to the proof, and
simplified it by the way of encouraging constructivism!

And I want to talk about exactly what they give you, real fast, because it’s useful to
talk about this notion of validity and where it can go wrong. There are not a lot of
places where you can make mistakes, when you are using a proof assistant! You can
accidentally use an *escape hatch* - for example, `sorry`

provides a proof of whatever in
Lean - but this is something trivially catchable. Just search your codebase for the
word “sorry”. And I think Lean will yell at you, too. You can have mistakes in the
theoretical model - the specific form of logic underpinning the proof assistant. But
this is very well studied. You can have mistakes in the implementation of the proof
assistant - but what most proof assistants do is they have a kernel, a small core core
of the language that everything else is built atop. And these kernels, in turn, are
very well studied. And you can have a mistake in the type - the proposition - of a
theorem, where you write down and accidentally prove the wrong thing. But this is
unlikely and the very act of mechanizing your proof invites closer scrutiny. And I
want to emphasize that - bugs in the proof *will* be caught! With these exceptions,
the actual reasoning of the proof - must be sound!

My main takeaway from all of this is that these systems are cool, and also sometimes useful, and make us think deeply about what we are really doing. I like foundations for the sake of foundations - I just think they’re neat!

So I hope I’ve at least interested some of you in exploring this further. If you’re a mathematician newly-interested in this, I would recommend checking out proof assistants! I think Lean is quite cool as a system: design-wise it has learned from the last two decades of theorem provers, and it seems to attract mathematicians otherwise not interested in foundations fairly well. The Coq theorem prover - soon to be Rocq, it is being renamed for… obvious reasons, is also a very good language despite its age, and the next talk is going to go into some examples of working through proofs in it. Another popular one is Agda, which category theory people seem to like. And there are various other proof assistants, most commonly used for software verification.

Question: So can you work with classical logic in these intuitionistic-based systems?

Answer: Yes! In these proof assistant systems, you can freely - but explicitly -
assume classical axioms. This breaks some computational interpretation - in
particular, “extracting” programs from proofs (which I didn’t get into) no longer
holds, but checking proofs is unaffected.