This post assumes some familiarity with typed functional programming, Lisp, and formal logic.
Today we will attempt to write a truth oracle in Lisp. By "truth oracle," I mean a program that can determine whether arbitrary mathematical statements are true or false. This might sound impossible, due to first-order logic being undecidable, but let's try anyway.
Before that, though, we need to go over some required concepts.
Extracting information from proofs
First, sometimes, we can extract information from proofs themselves, beyond just the facts that they prove.
Imagine you want to prove a statement of the form “\(A\) or \(B\).” If you can prove either \(A\) or \(B\), then you can prove “\(A\) or \(B\)” by the or-introduction rule. Let’s say you have a proof of this form, and you want to figure out which of \(A\) or \(B\) is the one that’s true. This is pretty easy. You can just look at the last step of the proof, and see if it’s left-or-introduction or right-or-introduction. For example, if you have a proof that a number is either divisible by three or by five, you can look at the last step of the proof to see which it’s divisible by.
The same principle applies for proofs of existence. If you want to prove “there exists \(x\) such that \(P(x)\),” you can use the existential introduction rule. In other words, you can give the specific value \(x\) satisfying \(P(x)\), and then prove \(P(x)\) with that value. Then if you have a proof of this form that there exists a number \(x\) such that there is a string of digits “123456789” starting at the \(x\)th digit of \(\pi\), you can look at the existential introduction rule of the proof to see where in \(\pi\) you can find the digit string “123456789.”
In other words, for proofs of “or” statements, we can look at the proof to see which individual statement is true, and for proofs of existence we can look at the proof to see the value that exists.
The Curry-Howard correspondence
The next concept is a relationship between proofs and programs called the Curry-Howard correspondence. This topic has a lot of depth and I’m not going to go into the full details, but the basics aren’t too complicated. The core idea is that formal logic proofs can be thought of as expressions in a typed functional programming language, and vice versa. Similarly, the types of expressions can be thought of as propositions, or statements, that the expressions prove. I’ll describe some examples below.
... continue reading