Music

I've got the first sheet ready and we'll put it online later this afternoon.

And we'll talk about it tomorrow in the first tutorial.

So this will be an informal affair, of course, because we don't have any sheet to talk about, so we'll just, I mean, not solve one anyway.

So we'll just talk about the exercises of the current sheet, maybe give some examples, and generally see if everybody's happy.

Second point related, have you formed groups of at least two people?

No? No, you haven't. Okay, so let's maybe arrange this now. Who isn't in a group?

Oh, that's almost everyone. So I'll just lay back for a moment while you guys all get into groups.

We can leave it for the tutorial. Yeah, that's okay. So yeah, maybe you can pass this off line without us present, that's such a good idea.

I'll ask again tomorrow at the tutorial. So the guys that can't make it for the tutorial are at least for Tuesdays, are in groups already.

Good. Right, so now I should try to cover the material that is on the sheet.

So you can actually do it.

So this will be a new topic, although still in classical propositional logic, but one that hasn't been invoked,

namely the sequent calculus for classical propositional logic.

So this goes back to a journal logician who worked in the, well, actually the 20s, 30s of the early century, Gerhard Genssen.

I think it's a great achievement that makes this guy a famous guy. It's a bit of a two-sided thing because this guy died in 1945 in Henry Ford, Nazi.

Okay, so what is the idea of the sequent calculus? Well, you've seen natural deduction and gloic. Right, natural deduction has rules like this one, for instance,

the one for disjunction, just to pick the most complicated one, the elimination rule for disjunction. Hopefully some of you recall.

So this is an elimination rule, meaning I want to actually conclude something from a disjunction, say, a disjunction phi or epsilon.

So, of course, it's the very nature of the disjunction that I don't know which of these two things is true, phi or epsilon.

So, say, if I want to prove something chi under that assumption, thereby eliminating the disjunction symbol here, hence the name elimination rule.

And I have to show that on the first alternative I can derive my conclusion chi, and I have to show that I can derive it also on the second alternative psi.

If I manage that and I have the disjunction phi or psi, then I'm allowed to actually conclude chi.

So that's the elimination rule for disjunction in what's called natural deduction.

So there are two things to see here. One, a name called natural deduction for nothing.

So this is really the way we proceed in paper proofs, at least if we do it right.

So teaching people a natural deduction system or teaching students a natural deduction system at the same time tells them how to write correct proofs on paper.

If you are presented with a disjunction and you're supposed to prove something from it, then this is what you do.

You make a case distinction over which of the two disjunctions is true, and then you prove whatever you have to prove in each of the two cases.

So that's the upside. And the downside is that when you really look at what these proofs are, then natural deduction proofs are sort of complicated beasts.

So what you see here is not just a proof. It's a proof that has sub-proofs, which we see here.

And these sub-proofs come with extra assumptions that appear here in square brackets.

And these square brackets are short notation for, well, after I apply the rule, I actually discharge the assumptions.

So after applying the rule, they're no longer there.

Which is sort of something you can say, but which is not quite as easy to write down as the formal system when you really get down to it.

And because that's an actual technical difficulty, Genson came up with the idea of basically producing a slightly flatter version of these highly structured proofs.

So you would get a system that you would actually be able to handle, take.

And this system will talk about things that actually capture deductions.

So basically what you see here is you sort of get deductions in the rule premises. If I can deduce chi from 5, then.

So what you do is you actually come up with a symbol for deducibility.

And this symbol is going to be this. It's the one that we standardly use for deducibility.

It's distinguished from the very similar symbol that we've seen in the semantic definition last time by having only one vertical bar.

So one vertical bar means syntactic, two vertical bar means semantic.

And then you write things on the left and on the right of this chart here.

So these are then actual formulas. So you write formulas phi 1 up to phi m, say, on the left side, and

psi 1 up to psi m, not necessarily the same number on the right hand side.

And this captures a formal proof.

So basically it captures proving something from assumptions.

These are actually called.

So phi 1 up to phi m are the assumptions. So this captures things like the phi and psi in square brackets that you see up there in this rule.