Logic And Proof
Computer proof assistants have been a hot button issue, at least in my mind, for some years now. I’m sure you can understand why the idea of a program that could automatically check your proofs for correctness would be an appealing prospect for an undergraduate maths student. I was enchanted by the idea that I’d be able to leverage my knowledge of programming to get perfect marks in my maths homework, however, as is often the case, the reality was much crueller than the dream. Over my undergrad years, I made a handful of attempts to learn a proof assistant but was rebuffed by a general lack of educational material. I settled on Lean as my assistant of choice since it at least offered some kind of onboarding pathway, unlike something like Coq which remains totally impenetrable to me. My progress through the Lean learning material was limited however, I found that the suggested book, Theorem Proving in Lean, far too difficult to follow as a newcomer to the topic. But things were different this iteration of the cycle as I also dug into some of the secondary book recommendations, including the titular Logic and Proof. This book has proven not only to be a great introduction to Lean, but also a great introduction to the underlying topic of mathematical logic. This project will chronicle my endeavours to work through the book and complete all (read most) the relevant exercises.
With this project, I’m going to be trying a different format for the website. Instead of waiting until I’ve finished the project, which let’s be honest is ambitious, before doing the writeup à la Rlox, I’m going to try to give written project updates as they happen. Hopefully, this will make it easier for me to get content out to you, my loving audience, and also help make the projects meaningfully distinct from my blog posts.
30/05/2021
This first progress update will cover the first 5 chapters of the book and the exercises from chapter 3. I’ve already gone a bit off the rails and rushed into doing all the chapter 3 exercises in Lean instead of writing out the proofs in natural deduction. My initial plan was to embed some LaTeX rendering in the page and display the natural deduction proofs in the page alongside the proof in Lean. After doing some research on MathJax, KaTeX, and natural deduction packages for LaTeX, I decided that wasn’t going to work very well, look very nice, and would essentially require me to program every proof twice. Luckily for you, all the proofs are available on Github and are significantly easier to follow than the natural deduction equivalents anyway.
Even though I’m only just beginning, I have encountered a little bit of the frustration of having to make my proofs completely rigorous that you often hear about with proof assistants. In particular, not being able to use some of my common tools, such as proof by cases, has been difficult, although I hope the book will build up to those as it goes on. At this point, it is difficult to picture how more complex proofs will come together, I know Lean has an extensive library of proofs but it is just hard to imagine how something like undergrad Linear Algebra could be expressed in Lean. Not that I don’t believe it’s possible but more that I’m eager to start proving more substantial results.
08/06/2021
In the time since the last progress update, I have read ahead to chapter 9 and completed the exercises up to chapter 6. In conceptual terms, this has taken us from intuitionistic logic to classical logic, and from propositional logic to first-order logic.
To make things a bit more understandable for those who haven’t been reading along or who aren’t particularly maths savvy, I’m going to try and give an elevator pitch definition for these concepts. In general, a system of logic is a set of rules that let us reason about the implications of facts. An example of this is the reasoning, if we know that vehicles can be blue and we know a car is a vehicle, then it follows that cars can be blue. In other words, logic allows us to manipulate and solve equations of facts, rather than equations of numbers. Different systems of logic offer us different tools for performing these manipulations.
Classical logic is the system that you’re probably familiar with if you’re only passingly familiar with logic. On the other hand, Intuitionistic logic is a weaker form of classical logic, which notably doesn’t include the law of excluded middle, or equivalently double negation elimination. In practical terms, this means that you can’t use proof by contradiction, as it depends on the law of excluded middle. This is appealing in a romantic sense, it means it’s not enough to prove that something cannot possibly be false to prove that it’s true(which may not always be the case), for example, if you want to show that a certain object you have to be able to produce an example of it. This is certainly more satisfying, however, after doing all the exercises I can tell you it’s much more difficult and many very fundamental identities like De Morgans’ laws depend on classical arguments.
Moving onto propositional vs first-order logic, propositional logic, as the name might suggest, operates on propositions. In this context, a proposition is like the statements of facts we discussed earlier, and these can be combined into more complex propositions by using the logical operations: and, or, not, implication, bi-implication. For example, a car being red implies that it goes faster or it goes the same speed and looks cool. First-order logic instead operates on some universe of objects that we are free to choose, so long as we can evaluate equality for those objects, such as numbers. First-order logic also adds, predicates, which take some number of our objects and gives us back a proposition about them, such as one being less than the other, and functions, which take some of our objects and transforms them into a new object from our universe. Finally, first-order logic gives us the universal and existential quantifiers, which allows us to reason about all of the objects in our universe or some arbitrary object with certain properties, respectively.
With first-order logic we have enough power, at least logically speaking, to start establishing some non-trivial proofs. Lean itself is built around type theory which, as I understand it, is a more powerful system again. Going from the contents of the book, however, we spend a couple more chapters learning how to use our new toys before taking a tour of different fields of maths, using first-order logic in production, so to speak. At the moment I’m just rushing to gather enough working knowledge that I can start catching up on exercises and hopefully solidify my slightly fuzzy understanding of first-order logic up to this point.
19/06/2021
For today’s update, I’m going to keep things a bit less theoretical. Since last time I’ve worked through the exercises for chapters seven, eight, and nine. While I was working through these exercises, I spent a lot of time thinking about my workflow for “written” exercises and thought I’d share some of my conclusions. I say written in quotation marks because these are still maths exercises that involve manipulating equations and drawing up tables rather than actual prose. Essentially, I think of everything that doesn’t require a proof in Lean as a written exercise. At first, I used LaTex to do all these exercises however the process was excruciating. LaTex is certainly great for typesetting long-form technical pieces of writing, but that’s also why I found it so difficult to use. I found that I had to write so much boilerplate just to put together a simple truth table with some math symbols in it. Then I had to wrestle with the formatting just to make it look presentable. Worst of all, I had to do it all in a separate application and only after installing thousands of other packages.
Since then, I had been avoiding doing any written exercises and searching for a solution. I was looking for a format that was easy to write in, supported rendering math symbols, and could integrate with the website as a stretch goal. It was then when I stumbled across Stefan Gössner’s article Web Publications - LaTex Style, that I saw the light. Gössner has written a VS Code extension Markdown+Math which uses KaTex to provide a WYSIWYG editing flow for Markdown with support for math rendering. Additionally, it supports HTML rendering and custom CSS which makes it appealing on the off chance I ever wanted to integrate it with my site. Although, I have taken a leaf from its book and added KaTex to the site so now we can have nicely rendered equations like \(e^{i\pi} = -1\). KaTex is somewhat more limited than LaTex, you couldn’t write natural deduction proofs in it for example, but I still refuse to write natural deduction proofs, so this seems like a fine tradeoff to me. This also inspired me to rewrite the content on the site in pure Markdown rather than mostly HTML in an md file. The next big workflow improvement I have my eye out for is a nice way to add keyboard shortcuts for maths symbols. In particular, having quick access to the single french quotes would be life-changing, as far as writing Lean is concerned. So keep an ear out for that update, it’s sure to be entertaining.
24/07/2021
It’s finally happened, my regular update cadence has fallen victim to the rigours of adult life. In the more than a month since my last update, I’ve worked all the way through to chapter 16. These 7 chapters cover sets, relations, and functions and how to use them in Lean. In my mind, these three topics constitute everything you need to get started on the real maths. Up until this point, the exercises and proofs in the book have focused on basic results in logic. Most programming languages have logic like this as a basic construct, so it’s not particularly difficult to imagine how these proofs work in Lean. What makes these chapters interesting is that they start to bridge the gap towards the language of practical maths.
In particular, I’ve been curious how Lean would be able to handle functions as they are so core to advanced proofs. Confusingly the word function often means something different in the context of maths versus the context of programming. To make the difference clear I’ll call them maths functions and beep-boop functions, respectively. Maths functions map one object to another, this mapping can be arbitrary but often is given by a formula i.e \(f(x) = x^2\). To write proofs about a math function we can either reason about its definition, for example by rearranging it, and its result, by evaluating it. However, not all maths functions can be easily defined or evaluated. Beep-boop functions, however, generally represent some behaviour, they describe what the computer should do, step by step. These functions can map one object to another, but they can also perform other changes inside the program called side effects. These side effects can’t be modelled very well by a maths function, and are sometimes called impure. Lean is a purely functional language, and while the strict definition of “purely functional” is hotly debated, it’s generally agreed that it means all beep-boop functions in that language are pure. So for simplicity, I’m only going to talk about pure beep-boop functions here. We can generally always evaluate beep-boop functions, just by running them and seeing what they output, they may not always return something but that’s a different problem. It’s very difficult to reason about the definition of a beep-boop function, in a maths sense, even though we have access to the algorithmic definition, doing so runs into the same problem again. So it would seem that maths functions and beep-boop functions would be at odds with each other, but as a language, Lean needs to be able to represent them both. From what I can tell, Lean achieves this by treating functions both symbolically and as executable code by default. Then using the noncomputable keyword you can signal to Lean that a function is purely symbolic and that it shouldn’t attempt to compile it. This keyword means that Lean can represent maths functions that can’t be translated to beep boop functions because they can’t be defined algorithmically. Then when writing a proof about a function, or any other object, Lean can automatically substitute in its symbolic definition and you can write proofs about it as normal.
To cleanse the palate after that big block of theory I’m gonna close off this update with some quickfire observations, which I might expand on in future updates. Now that the written exercises involve writing long-form proofs I find that writing proofs in Lean is much less laborious. I think this is because Lean is much less verbose, and I think it might be interesting in future to investigate programming language “density” compared to ease of writing and understanding that language. Second, the documentation on Lean continues to be awful. It wasn’t so much of an issue before, but now I’ve started to encounter more bugs and the explanations in the book have become more fast and loose. On the bright side, this does encourage self-directed learning and I wonder if removing friction from the learning process can be to the detriment of deeper understanding.