'T' is for Theorem-proving

'T' is for Theorem-proving

So, you've been theorem-proving all your life.

Let's just get that one out there.

When you're given a math problem that says:

"Solve x + 1 = 2 (for x) (of course)"

And you say, "Why, x is 1, of course," quick as thinking, you've just proved a theorem.

Here, let me show you:

x + 1 = 2 (basis)

     -1 = -1 (reflexive)

x + 0 = 1 (addition)

x       = 1 (identity)

Q.E.D. ('cause you rock)

So, yeah. Theorem proving is this, correction: theorem proving is simply this: going from step 1, to step 2 to step 3 until you've got to where you want to be.

How do you go from step 1 to step 2, etc? The same way you do everything! You follow the rules you're given.

Let's prove a theorem, right now.

So, in classical logic, we have a theorem that says

p → p

That is, if you've got a p, that implies (that you've got a) p.

Toughie!

But proving that? How do we go about doing that?

Well, in classical logic, you're given three basic axioms (thanks to sigfpe for his article "Adventures in Classic Land"):

1. p → (q → p)

2. (p → (q → r)) → ((p → q) → (p → r))

3. ¬¬p → p

So, p → p. How do we get there? Let's start with axiom 1 above.

1. p → ((p → p) → p)

axiom 1 (where q = (p → p))

2. (p → ((p → p) → p) → ((p → (p → p)) → (p → p))

axiom 2 (where q = (p → p) and r = p)

3. (p → (p → p)) → (p → p)

modus ponens

4. p → (p → p)

axiom 1 (where q = p)

5. p → p

modus ponens

Q.E.D. (a.k.a. whew!)

I used something called modus ponens in the above proof. It says, basically, that if you've proved something that you're depending on, you can drop it. Or, logically:

p → q, p

       ∴ q

Or, we have "p implies q" we've proved p, so now we can just use q.

Now, there's been a lot of thought put into theory, coming up with theorems and proving them, and this has been over a long time, from Aristotle up to now. The big question for a long time was that ...

Well, theorem proving is a lot of hard work. Is there any way to automate it?

So there's been this quest to make theorem proving mechanical.

But to make theorem-proving mechanical, you have to mechanize everything, the axioms, the rules, and the process. Up until recent history, theory has been a lot of great minds spouting truths, and 'oh, here's a new way to look at the world!'

And that has been great (it has), but it hasn't helped mechanize things.

Then along came Frege. What Frege did was to give us a set of symbols that represented logical connectives and then symbols that represented things.

And there you had it: when you have objects and their relations, you have an ontology, a knowledge-base. Frege provided the tools to represent knowledge as discreet things that could be manipulated by following the rules of the (symbolized) relations.

He gave abstraction to knowledge and an uniform way of manipulating those abstractions, so, regardless of the underlying knowledge be it about money or chickens or knowledge, itself, it could be represented and then manipulated.

That way you could go from step 1 to step 2 to step 3, etc, until you arrived at your conclusion, or, just as importantly, arrived at a conclusion (including one that might possibly say what you were trying to prove was inadmissible).

Since Frege, there has been (a lot of) refinement to his system, but we've been using his system since because it works so well. He was the one who came up with the concept of types ('T' is for Types) and from that we've improved logic to be able to deliver this blog post to you on a laptop that is, at base, a pile of sand that constantly proving theorems in a descendent of Frege's logic.

Let's take a look at one such mechanized system. It's a Logic Framework, and is called tweLF. The first example proof from the Princeton team that uses this system is 'implies true,' and it goes like this:

imp_true: pf B -> pf (A imp B) = ...

That's the declaration. It's saying: the proof of B, or pf B, implies the proof of A implies B, or pf (A imp B).

How can you claim such a thing?

Well, you prove it.

imp_true: pf B -> pf (A imp B) =

[p1: pf B]            % you have the proof of B

% ... but now what? for we don't have the proof that A implies B

.

So the 'now what' is our theorem-proving adventure. Mechanized.

We don't have the proof that A implies B, but we have a logical loop-hole (called a hole) that a proof some something that's true is its proof:

hole: {C} pf C.

Which says, mechanized what I just said in words, so with that:

imp_true: pf B -> pf (A imp B) =

[p1: pf B]

(hole (A imp B)).

And there you go.

... that is, if you're fine with a big, gaping loophole in your proof of such a thing.

If you are satisfied, then, well, here, sit on this rusty nail until you get unsatisfied.

So there.

Okay, so we have an implication, but we need to prove that.

So we introduce the implication into the proof, which is defined as:

imp_i: (pf A -> pf B) -> pf (A imp B)

SO! we have that, and can use it:

imp_true: pf B -> pf (A imp B) =

[p1 : pf B]

(imp_i ([p2: pf A] (hole B))).

So, we have the proof of A and that leads to B. But wait! We already have B, don't we? It's p1 (that is [p1 : pf B])

BAM!

imp_true: pf B -> pf (A imp B) =

[p1 : pf B]

(imp_i ([p2 : pf A] p1)).

DONE!

This is what theorem-proving is: you start with what you want, e.g.:

imp_true: pf B -> pf (A imp B)

which is "implies-true is that if you have B proved, then you have the proof that (A implies B) is true, too."

Then you take what you've got:

pf B

And give it a value:

[p1 : pf B]

Then you apply your rules (in this case, implication introduction, or 'imp_i') to fill the holes in your proof, to get:

[p1: pf B] (imp_i [p2: pf A] p1)

Which is the demonstration of your proof, and that's why we say 'Q.E.D.' or 'quod est demonstratum.' 'Thus it is demonstrated.'

Ta-dah! Now you have all the tools you need to prove theorems.

Now go prove Fermat's Last Theorem.

eheh.

(I am so mean!)

Okay, okay, so maybe Fermat's Last Theorem is a bit much, but if you want to try your hand at proving some theorems, there's a list of some simple theorems to prove.