Before learning how modern proof systems work, I wanted to embark on my own adventure to try to make one happen. It’s a project that’s been unfinished for quite a while now, so I thought I’d make a writeup about how it theoretically works, and the current stoppers, to refresh my memory.
Mathematical logic refresher
Before we can simulate mathematical logic, we have to have a good idea about it’s rules and constraints. People use logic every day in an informal way. Whether it’s from intuition, education, culture, whatever, we have a general sense of what makes arguments hold together. To go about symbolizing arguments, we have to think about what makes conclusions true or false.
If I say “If it rains where you live, you should own an umbrella”, and then I say “It rains where you live, therefore you should own an umbrella”, the particulars don’t actually matter that much if we’re talking about how the proof works. I could very well say “If A, B” and then say “A, therefore B”. Any argument of that form holds together, as long as qualifications are met:
- If A then B is true
- A is true Wherever there are qualifications that need to be met in order for an argument to ‘hold up’, we call them axioms. All arguments have axioms, since arguing itself implies you agree that there is such a thing as “true”, and that you agree that logic works, which are qualifications in order for any argument to ‘hold up’.
The mathematicians love giving symbols to things, and this is no exception. They have called for some conventions I will now go over for different kinds of statements:
- X is true is just, “X”. “Statement is true” does the same purpose as “statement”. I’ve heard some say this is the best definition you can give for truth before you run into a certain meta-problem outside the scope of this writing.
- X isn’t true or Not X is “¬X”. ”¬” is the symbol for “not”, and negates whatever it applies to.
- If A, then B is “A → B”. ”→” is the symbol for implication. More on this later.
- A and B is “A ∧ B”. ”∧” is the symbol for and, which can be memorized if you remember it looks like a little “A” :)
- A or B is “A ∨ B”, ”∨” is the symbol for or. It is identical to a “v” because it came from the latin word “vel” meaning the same thing. Note, this is inclusive, meaning that even if A and B is true, “A or B” is true.
- A, if and only if B is “A ↔ B”. Since A can only be true if B is true, we can deduce that if B is true, then A is true. and A is true if B is true. In other words, “A if and only if B” is like having “A → B” and “B → A”. It simply means that A and B have the same truth value (Either both false, or both true).
These are not the only symbols for these concepts, even in the field of mathematical logic. Outside the field for mathematical logic, the same ideas are expressed in many different ways, but the basic premise is the same: They are relationships between two things, which both have two options (In this case, true or false, in set theory, “in the set” or “out of the set”, etc)
One note on implication
this is the thing I said I’d talk about later, it has a feature some say is unintuitive. You see, normally when you talk about one thing implying another, the first thing is true, and you’re making a point about the second thing(The ‘implied’) to be also true. What happens to the statement “A implies B” when A is false? Well, the whole statement is presumed to be true.
This is often seen as strange to newcomers, but let’s look at the alternative: First of all, ‘A implies B’ is true if A and B are true, which is obvious enough. If two things imply eachother, it makes sense that they both be true at the same time. It is false if A is true and B is false, which also makes sense. If ‘A implies B’ is false when A is false regardless of B, congratulations, you have made a second “And”.
| A | B | A ∧ B (And) | A → B (implies) |
|---|---|---|---|
| False | False | False | True |
| False | True | False | True |
| True | False | False | False |
| True | True | True | True |
The truth is, when dealing with logic, A and B are unchanging. They may reveal themself to be true or false during your dealing with them, but their relationship is stationary. “A implies B” is a statement with one promise, “If you find A to be true, then it is certain that B is also true”. This is the only behavior that properly makes that promise.
Implication is not a statement about causal connectedness with regard to the kinds of things the argument discusses. It can often be applied to such cases, but it does not have to be. After all, in logic they could be statements about global politics just as much as they could be statements about tea-making, and logicians are not in the business to decide what is causally connected to what, only what is logically connected.
Back to business
These rules alone are enough to be able to translate most arguments into formal logic, although the axioms build up sometimes in unexpected ways. For instance, in the following argument: “All men are mortal, Socrates is a man, therefore Socrates is mortal”
We expect to be able to replicate it in 3 steps, but it is not so. It goes like this:
- A All men are mortal (Axiom)
- S Socrates is a man (Axiom)
- A ∧ S → M If all men are mortal, and Socrates is a man, then Socrates is mortal (Axiom)
- M Therefore, Socrates is mortal
The third step is not intuitive, but it arises as a result of the fact that we cannot say things about men(Or any other categories) in general with this language. When we say something of all men, it is it’s own statement, and when we say socrates is a man, it is entirely separate statement, not interacting with the categorical statement at all. We can do better.
First order predicate logic
When talking of categories in logic there are two typical qualifiers we use, symbolized like so:
- For all A, B ∀(a)(B)
- There exists some A such that B ∃(a)(B)
Another meaningful tool that ought to be introduced is a way to categorize things. If I say “John is a human”, I ought to say things about humans generally that will ‘automatically’ also apply to john. That is done like so:
- Hj - H for human, j for john.
One thing to note is the use of capital and non-capital letters. H represents a category. Another thing is that “a” in ∀(a) and ∃(a) represents everything / anything. If I wanted to limit the statement, say, to only human beings, I could do this:
- ∀(a)(Ha → Ea) For all things a, if a is a human, then a is edible (Yum)
Now, the Socrates syllogism looks like this:
- ∀(x)(Hx → Mx) For all x, if x is a man, x is mortal (H for human, since M is used for mortal) (Axiom)
- Hs Socrates is a man (Axiom)
- Ms Socrates is mortal
There, all is right with the universe, a syllogism is actually three steps. Neat!
Wait, what were we doing
So what?
So far, we’ve done a lot of translating sentences into logic, but we haven’t actually made clear how we go from axioms to conclusions, which is very important! Without it, there’s not really much of a purpose to what we’re doing, and it’s completely unclear how we’re supposed to make a program to do logic. to make logic more useful, we need to introduce rules of inference. These are tiny conclusions that apply to any piece of logic where they fit. For instance:
- Take, for granted, that if A implies B, and A is true, then B is true This is called the “Modus Ponens”. Now, with a given set of axioms, we can use it to draw conclusions:
- A → B A implies B (Axiom)
- A A (Axiom)
- B B (Conclusion, from Modus Ponens)
I cannot stress enough that a rule of inference is not just another axiom. If it were, it would require an inference rule of its own, ad infinitum, see What the tortoise said to achilles. No, it’s part of the logical system itself, similar to your agreement that there is such a thing as ‘true’.
There are quite a few other rules, such as DeMorgan’s laws:
- ¬(A ∨B) ↔ ¬A ∧ ¬B If it’s not true that “A or B is true”, then both A and B is false, and vice versa.
- ¬(A ∧ B) ↔ ¬A ∨¬B If it’s not true that “A and B is true”, then A or B is false, and vice versa. And to draw inferences from quantifiers, there are a couple things to consider
- ¬∀(a)(B) ↔ ∃(a)(¬B) If it’s not all the case that for all A, B is true, then there exists some A such that B is false.
- ¬∃(a)(B) ↔ ∀(a)(¬B) if there does not exist some A such that B is true, then for all A, B is false.
Finally, it’s important to consider this one, although it’s not so easy to notate it.
- In any universal statement ∀(x)(…), any x’s in (…) may be replaced with anything in particular, and the whole statement be true. This is what makes the Socrates syllogism’s conclusion possible.
How do we make this into a program?
So, the intuitive way to structure a program that does logic, then, might be to start with some axioms in a list of “true statements”, and see if those laws can be applied to them, and then whatever comes from that can also be added to the list of true statements.
This isn’t far from what I’ve actually come up with, but I wanted things to be a little bit more explicit (Not to mention a couple things that simplify the number of steps to get useful conclusions from a given statement). First of all, I wanted to make the steps to and from a given logical statement clear. Just adding a true statement to a list of true statements, it’s source is lost.
I also wanted to make things into a “map” of sorts, the end-goal being that I could use pathfinding to get short proofs from a set of axia to a goal conclusion. Not only will it find an argument, but it’ll find the /shortest/ (In whichever sense you are able to put a number on) argument.
The actual implementation
A small shortcut
There’s a problem with this theoretical implementation, which is simply that it takes so many steps to get things done. One way I found to eliminate a lot of the stepwise time is to do logic within the middle of statements. For instance, given the statement a ∧ b ∧ c, if b ∧ c implied something, and a ∧ (whatever b ∧ c implies) is a goal, then the only way to get to the goal would be to extract b ∧ c, probably using something like the two rules a ∧ b ↔ b ∧ a and a ∧ b → a. And on top of that, I’d have to finish off by remembering, and re-introducing a. Slow and tiring.
Whereas we know that if b ∧ c implies something, then the other thing can be put in it’s place. Meaning in a ∧ b ∧ c, we can deal with b ∧ c, do the substitution, and are left with a ∧ (whatever b ∧ c implies) right away.
Parsing?
Logical notation, like mathematical notation, is a little messy for computers to mess with. We’ve had memes like “6 / 2(1 + 2)” for a while, and even some calculators disagree on how it should be interpreted. Something a lot less messy for computers is Polish Notation. ”/ 6 (* 2 (+ 1 2))” isn’t so ambiguous, at least once you learn how to read it.
The neatest thing about polish notation for this project, though, is how it is so easy to deal with it in terms of a graph.
graph TD
a["2"]
b["2"]
star["＊"]
plus["＋"]
/-->6
/-->star
star-->a
star-->plus
plus-->1
plus-->b
(If you’re wondering why the addition and the multiplication symbols look a little funny, it’s because the mermaid dev’s need to get their shit together oh my lord)
In the process of dealing with the arithmetic, a node is either: A. The value written on the tin (If it’s 1, 2, etc) OR B. The value given by applying the operation to it’s children This leads to a simple recursive solution to getting the value of the whole statement.
In logic, it’ll look more like this:
graph TD
root["↔"]
childand_1["∧"]
childand_2["∧"]
ca_1["A"]
cb_1["B"]
ca_2["A"]
cb_2["B"]
root --> childand_1
root --> childand_2
childand_1 --> ca_1
childand_1 --> cb_1
childand_2 --> cb_2
childand_2 --> ca_2
This is the storage of a single statement, being (A ∧ B) ↔ (B ∧ A).
Another implementation detail to get out of the way before the big one is that there’s no need to store some big list of truths. We could make an interface to display and input things that way, but if I input all true things “A, B, C, D”, that is equivalent to having the single statement A ∧ B ∧ C ∧ D, and dealing with the single statement is a simpler ordeal.
How do we apply “rules” (Demorgans laws, etc)??
The method I came up with is substitution rules. For instance, say I want to express and test the rule that (A → B) ∧ A means B. This is done in steps. You walk through both the tested statement, and the rule, doing the following things:
(Non-variables, in this case, refers to ∧ and →)
- Checking the non-variables have the same number of children. If not, then you can’t apply the rule.
- Saving the variable to a list, both the rule and the non-rule in their own list, at the same index. At the end, check for repeat rule variables, and verify that they are also repeat in the tested statement.
- Checking that non-variables are exactly the same
Now, something to note, is that A can be a rather large statement of it’s own in the tested statement. It doesn’t have to be a single value. When checked that both “A”s are equal to each-other in the tested statement, you can check each node recursively.
Once a statement is verified to be following the “rule”, application is to simply walk through the statement and the rule again, and to use the list made earlier to change “B” In the second part of the rule (The rule being that (A → B) ∧ A means B ) to the equivalent from the tested statement.
That’s where I’m at. And it’s where I’m stuck. Because Although I’ve created all of this so far… Now I want to make it do some subset of second-order. And that’s tricky.
Thanks for reading :)