So today we're going to get started on the sequent calculus for intuitionistic propositional logic.

The standard reference for this kind of thing is the proof theory book by Trulstra and Schlichtenberg.

Now these sequent calculi for intuitionistic logic like sequent calculi in general actually come in a variety of different flavors as we have already noticed early in the lecture.

So we will continue to use the version of the calculus that absorbs the structural rules.

That is you don't need weakening or contraction as explicit separate rules in their own right.

We build the calculus in such a way that these rules are admissible.

In the book these calculators are designated G3 and then something depending on what the logic is in this case G3i as an intuitionistic variance of this RC for classical and M for minimum.

And in order to better match this with what we've done before we'll use the variant that is multi-conclusion.

That is the variant that like the one that we've used so far will allow you to have arbitrarily many formulas both to the left and to the right of the turnstile.

The standard version of G3i actually allows only one formula to the right hand side of the turnstile.

And this is actually generally regarded as sort of the main distinctive feature between intuitionistic and classical logic.

Only one formula to the right of the turnstile.

But never the less these multi-conclusion systems exist and work perfectly well.

Yeah, yeah, I will.

Right.

I mean the name of this is MG3i.

The disadvantage of this with regard to literature is that we're maneuvering ourselves into a sort of corner case here.

So when I say the book mentions this I mean that the book has a sort of hand wavy paragraph about this that tells you how the rules look and sort of tells you that all the other things work more or less as expected or suitably adapted.

So let's hope we get this all right.

I mean this is the most encyclopedic book that's available on the subject so what they don't have we won't find elsewhere or only by digging in original literature.

So let's hope for the best.

Because we are now starting to use this book more seriously I would like to introduce a notational change that will make life easier in many respects.

A new symbol in place of the turnstile.

We agree on this change of notational policy we write a double arrow in place of what was hither to the turnstile so we separate the left and the right hand side of a two sided sequence by a double arrow.

The main advantage besides sticking to the notation used in Trulsrandt-Richtenberg's book will be to free the turnstile again for its normal use.

So is everybody fine with that?

First of all the system.

Parts of the system look very much as they did up to now.

For instance the axiom rule.

So this is the axiom rule same as it was before.

I wanted to use the arrow, yeah of course.

And painstakingly corrected this two times forwards and backwards in my notes.

Okay so that's the new form of the axiom rule and I'll just say that the rules for conjunction remain entirely unchanged.

Also unchanged the rule for bottom.

And there's only one rule for bottom evidently we would never want to introduce bottom on the right. Of course it is perfectly sensible to introduce bottom on the left.

We haven't done this explicitly so far but let's do it now.

Let's put it to the right.

So basically any sequence is derivable that contains bottom on the left.

Ah yeah thanks. I will get used to it in the course of the lecture I guess.

Right so these are the unsurprising rules and then there are some more new but unsurprising rules.

Such as the rules for disjunction which in fact you have already derived on one of the sheets and they look exactly like the ones that you derived.

Let me make it explicit nonetheless.

So now I managed for the first time to actually use the symbol at the first attempt.

So this thing here is more or less dual to the rule for disjunction.

In the case of conjunction the right rule was branching.

In the case of disjunction the left rule is branching. That is in order to derive this we have to show two things.

First of all that under gamma and phi we can derive.

Oh that's total nonsense.

We can derive delta and secondly under gamma and psi we can conclude delta.

Which basically amounts to a proof by case distinction.