We're building a model of how humans argue.

In math.

Okay.

But that's really what we wanted to do.

Now, if you ever try proving stuff in natural deduction, and many of you have done that in glowing,

then you'll see the following happen.

The theorem is here.

You have a couple of assumptions here.

And then you make a step, maybe another step, and another step, and step.

And then you prove the theorem.

Hooray! I can submit.

Wonderful.

Except that this is not how it happens.

Actually, what happens is, you start from your assumptions.

You do your proving.

And you miss the target.

Well, you can try again.

And if you're lucky, at some point you come back and prove it there.

Or at least that's how proving feels to me.

The problem here is one we've encountered before.

The problem here is that we're lacking a sense of direction.

We don't really have a good heuristic.

Oh, this theorem is here. Let's go there. Ha ha ha.

We don't have a good sense of direction.

Think about implementing the natural deduction is that we actually do breadth-first search or iterative deepening search,

which is essentially the same.

We'll try to look at the space of all proofs and then do it level by level.

And after a couple of gazillion of years, we actually hit the theorem invariably by enumerating all proofs.

Okay? Not very efficient.

We need a sense of direction.

The problem with the sense of direction is that we often have the same assumptions,

say the assumptions of group theory, but the theorems are all over the place.

And if I have this heuristic that says, oh, go to the right, you'll find it.

Keep somewhere in the middle of the blackboard.

Well, doesn't work very well if your theorem is here.

Okay? So if we want to implement, we do something completely different.

What we do is that instead of thinking positively and saying I'm starting from the axioms or my assumptions or my observations

and go towards the theory, we just turn it on its head.

We say, what can we do to get not T?

How can I actually, actually what I ask myself, how can I actually make sure I'm never going to be able to prove not T?

And then when you're doing not, everything changes direction.

So instead of going from the axioms to the theorem, we go from the negated theorems to elementary contradictions.

And elementary contradictions are wonderful, something of the form A and not A.

Now, A and not A is always in the same place.

So we have a sense of direction.

We start out from not T and directly go there.

And it turns out that this idea, and we're calling that a test calculus,

we're testing whether not T can actually be achieved, is better to implement.

So we have a third kind of calculus.

This is what we call a machine-oriented calculus, is one that is good to implement.