The thing I want to talk about now is, was there anybody of you who liked this calculus?

I thought so.

I hate it, okay, because it's not the way any decent agent would reason about the world.

I've never seen anybody who does that.

So we need better calculus.

Sorry David, bad calculus.

We want to, and we always take math as kind of the example because they're reasoning.

Reasoning also happens outside of math, but in math it's easier to grasp.

So a guy called Gerhard Genson, who was a PhD student of David Hilbert, said, hey David,

probably Mr., Professor Hilbert, you're doing it all wrong.

And I have a better suggestion.

And that was what he came up with.

He said, well, we should really look at how mathematicians do math and make a calculus

that may not be as small as yours, Professor, but which actually maps what people do.

And Genson being a student to the god of gods of mathematics kind of called this calculus

natural deduction.

Okay, it was kind of quite a land grab, which probably was okay because it's much more natural.

And that's really what I want to show you.

Okay, we'll write down a couple of rules here.

Okay, remember we have these vertical, these horizontal lines and they say if you believe

the stuff that's on top, you can also believe what's below.

If you believe that A holds and that B holds, you can believe that A and B holds.

Okay, natural.

Conversely, if you believe that A and B holds, you can believe that A holds and by the same

token that B holds.

Okay, if you believe that A implies B holds and A holds, then B holds.

And read A implies B as if A then B. If it doesn't rain, we're going to have a barbecue

party.

Oh, it doesn't rain.

Okay, you do it all the time.

There's one axiom in this calculus according to Genson, which is A or not A. Hard to argue

with that, very natural.

And now comes the rule, that's the only one that's interesting in it, is how do you prove

A implies B or if A then B?

What you do in math is let's assume A, and so on B. Okay, so you kind of derive B from

the assumption that A holds.

And if that is the case, then you say, so A implies B. Okay, that's what you do all

the time as well.

There's a little glitch in here.

You have to make sure that the assumption of A is independent of everything else.

You have to be a little bit careful there.

And afterwards, down here in the proof, when you kind of go on and do stuff, you're not

allowed to use A anymore because you've already used it to make A implies B. Okay?

That was the analysis of Gerhard Genson.

And he said, that's natural.

Okay?

I can model what mathematicians are doing.

And also this has very nice logical properties.

Look at this.

Once you start making names, you can see that this rule here has an and below and no and