So this begins with an exercise on the additive version of the cut rule, or I should say, well,

an additive version of the cut rule, not because there are several ones, but because

it's more like a putative version of a cut rule that is not actually in the system.

So you will have noted that in the system that Tadeusz presented, there was only a multiplicative

cut rule, one where the two contexts that you get in these two premises here, well,

actually four of them, get concatenated in the conclusion.

And one could imagine an additive version where you have the same context in the premises

and the conclusion here.

That rule is not in the system, and this exercise is there to show that this is for good reason,

because it will prove this action here actually, well, this should be a normal or I think according

to a standard notation.

So this is just additive or additive disjunction.

And this is a bit right.

So the point of the exercise is to show a number of things.

A, this axiom is equivalent to this rule, basically, which means that if you add the

axiom to the system, you can derive the rule, and if you add the rule to the system, you

can derive the axiom.

One has to be a bit careful about what it means here to add an axiom, because there's,

well, there's a lot of subtleties in the system that aren't present in logistics as we've

known them so far.

And what this means is that if something is an axiom, it means you can insert it in any

sequence that you desire to prove on the left side.

So basically it says if you...

So that phi is an axiom basically means you have a rule like this.

If you want to prove a sequence, you may just as well prove the same sequence with the axiom

inserted on the left hand side.

So that's what it means for something to be an axiom.

Okay.

So you first show that basically the additive cut rule is equivalent to additive excluded

middle, if you will.

And you should then show or conclude from this that the additive cut rule is not admissible

because it proves things that weren't provable before.

Specifically it proves excluded middle.

So basically the next point of the exercise is to show that the additive excluded middle

formula is not provable.

Note the hint here, so of course if you try to prove unprovability of a formula in a system

that includes a cut rule, then you basically can have a lot of fun for the rest of your

life unless you're very cunning.

So you prove this by showing that the formula isn't provable in the cut free system, the

system without the multiplicative cut rule, and you're allowed to do that because we're

going to show that multiplicative cut is admissible.

So you can prove the same things with multiplicative cut as without multiplicative cut.

The next thing is an exercise in proving things in the system, again of course.

So basically we have these rules for the bank, specifically on the left, saying that on the

left we can contract and derelict the bank.

And the exercise here asks you to show that this is equivalent to adding this axiom here

to the system.

So basically this means we can either forget these rules here and instead add this as an

axiom.

In this case, well okay, so there are subtle differences.