Okay, so we were talking last time about the Gensens system for intuitionistic propositional

logic. I won't repeat the entire system now because hopefully everybody's got it and most

of the rules look as expected anyway with two exceptions and I'm going to write those down

because we're going to need their exact format all the time and on top of that I copied one of them

wrong from my notes last time so well we did have it right in the end but so let's just recall these

two one of them was the right rule for implication which looked like this. Ah, recall that we changed

the notation for the sequent right have the double arrow in between instead of the turnstile. Okay,

so we have an implication to the right hand side of the double arrow now and we wish to prove that

so what we do is we move the antecedent to the left of the double arrow keep the psi on the right

and drop the context drop the context on the right only keeping it on the left and this rule

was the key one that disabled proofs of certain classical facts that now are no longer provable

in intuitionistic logic and then there was the left rule so in this case we had the implication

to the left of the double arrow and this rule has two premises one where we keep the psi on the left

of the arrow and retain the implication thereby making the rule actually stronger and a second

premise that looks as in the classical case we move the antecedent to the right of the turnstile

so this is actually the only rule that shunts things across the double arrow right all the

other rules keep everything to the same side of the double arrow this is the only one that will

ever remove a formula from in this case from the left to the right yes is it wrong again wait a

moment no ah so the part of the rule that retains the implication is the other one damn it yeah as

in my notes correctly so the one that retains the implication to the left of the arrow is the one

that moves the antecedent to the right correctly and the one that keeps the psi on the left hand

side is the one that actually drops the implication and we will see why the rules are designed that

way so because we're going to see a completeness proof today and a soundness proof so the soundness

proof of so in the soundness proof we would prove we will see why this rule has been designed as

it stands in particular we will see why it drops the context and in the completeness proof we will

see why the handling of the implication is as it is here so kept in the left premise dropped in the

right so the first thing we want to do is soundness so in the sense that we want to show that all the

rules preserve validity within one model and we've already done one trivial case I believe the what's

the disjunction rule on the left right yeah and so the more interesting rules remain so let's start

with which one with the right implication rule so this is continued okay right implication rule

is this one so we assume a model that satisfies the press so we assume M models the premise gamma

comma phi implies psi in a sense that we've defined last time so basically what we do is we

really insert conjunctions here well no just junction here in this case because it's only

one formula and replace the double arrow by a single arrow okay what do we have to show

well we have to show that the model also satisfies the conclusion and for that of course we show that

a an arbitrary state of that model satisfies the conclusion so we have to show that given some W

a state in the model M and W satisfy the conclusion that is phi implies gamma well gamma and double

implies phi implies psi comma Delta okay now we have to keep in mind this our our reading of the

double error is the same as that of the error that is we have to check satisfaction of an

intuition mystic implication so that is we have to give ourselves an arbitrary successor state of

W assume that it satisfies what's on the left and show that it satisfies what's on the right so

so we assume that we have a successor V of W and we assume that V satisfies gamma well I'll

omit the conjunction in the hope that this will be clear okay what do we have to show in this case

well we have to show that V satisfies the right hand side of the double arrow that is the disjunction

of this whole bit here the implication that's the principle formula or the big disjunction of the

Delta right and to that end it will suffice to show that V satisfies the implication

and I mean if anything is right then this should follow from this premise here because

this premise here will clearly I mean just by basically a jointness of conjunction with

implication right if V satisfies gamma then V should satisfy this thing here and indeed

that is easy to check so now of course we again have to check and implement satisfaction of an