nm0930: last time we proved if i'm r-, i hope got it right we proved this 
sequent as you remember is one of the De Morgan Laws er i now want to as it 
were not immediately do another De Morgan Law although you will find several of 
them done in the book but to go on to something er directly from this to prove 
this sequent it's not the case that not-P and not-Q therefore if not-P then Q 
and so here we've got go from here to here and now we're going to 
prove from the conclusion of the previous argument the are going to prove 
another er conclusion so and let's do that on the centre board remember that 
this thing without any parentheses in it means a conditional that's the main 
connective a conditional in which the antecedent is not-P and the consequence 
is Q it's not it's not the negation of a conditional which we wanted to write 
the negation of a conditional we would write it like that so how are we going 
to prove this obviously as usual we assume what we're given right so it's not 
the case that not-P and not-Q remember you can't that you must respect all 
these m-, negation signs and the parentheses you can't just push the negation 
signs through or anything like that what have we got to prove well right let's 
before we even go that far let's say to ourselves what sort of a sentence 
is this it's a negation it's not only a negation it's what i usually refer to 
as a compound negation other words the negation of an already complicated 
sentence what can you do with the negation of an already complicated sentence 
actually not very much except and this is the the standard way of proceeding in 
these cases if you've got something like this is to try to build up what's 
inside the parentheses and get a contradiction so if you res-, if you get a 
compound negation try to construct whatever it is that is negated then you've 
got a contradiction and with a contradiction you can always deny something so 
you can always make some progress so don't people often ask what am i going do 
when i've got a negation sign outside a set of parentheses the only general 
advice i can give you is just what i have given you okay so we already know 
that we're going to head for R-A-A what have we got to prove well we've got 
prove a conditional we know how to prove conditionals we 
assume the antecedent that's we're going to discharge it in conditional proof 
we already know that er and it rests on itself now what have we got to prove 
we've reduced the problem they've put it before having assumed this we've 
reduced the problem now to proving Q how are we going to prove Q well again if 
you look at this and think how am i going to prove Q there's no obvious way of 
using this there's no obvious way of using this except to build up a 
contradiction so if nothing as it were stares you in face as to what you should 
do the best thing to do is to he-, try R-A-A so i want to prove Q how am i 
going to prove Q yes assume not the Q huh s-, so i assume in in th-, in this 
case i assume not-Q for R-A-A and now you can see it's suddenly all come out 
nicely because what we're doing we're in the middle of an R-A-A somewhere we're 
looking for a contradiction that's not difficult is it to get a contradiction 
out of that remember a contradiction is of form A and not-A this is a compound 
negation we can get the thing of which lose the negation formula which er which 
lose the negation by conjoining two and three and so we get not-P and not-Q two 
three and introduction and whe-, now moving fast towards this contradiction one 
two three this is going to rest on all of the the assumption which one and and 
er four rest on and now we've got to conjoin these and so we have to put in 
some more parentheses to make it quite unambiguous not-P and not-Q and it's not 
the case that not-P and not-Q sometimes these R-A-As you do find you get rather 
lengthy lines so er you m-, try not to start off from now onwards when you're 
writing out proofs don't don't put the assumption numbers too close to the er 
the as-, the annotations too close to the line numbers you may need quite a bit 
of space okay so here i do have something of the form A and not-A because if i 
take A and not-A and replace A by not-P and not-Q then i will get just that 
okay everybody happy with 
that that's contradiction and so i've done what i was goin-, said i was going 
to do here namely f-, find get hold of the sentence that is negated on line one 
and then from here i introduced not-Q for R-A-A i've got a contradiction er in 
the sense i have only to look back to see which assumption has got R-A-A 
against it to see what i expect to do at this stage it's three that i'm going 
to deny yes mm right no point denying one one or two normally it's three that 
i'm going to deny and so oh sorry i haven't filled this in yet have i er what 
do i need here i need a one four and introduction i tend to take n-, at this 
stage in the term tend to assume that an-, the and rules are so straightforward 
that i hardly need to mention them so we're going to deny three that means we 
discharge three in R-A-A leaving ourselves with just one and two as the 
assumptions denying three means what it means adding a negation sign to the 
front of three and the annotation is that 
the two lines namely the line that we've just denied that's line three and the 
contradiction that we used deny it to deny it in other words the absurdum ad 
which i can't get my Latin right the absurdum er er abs-, the absurdity to 
which we reduced it mm ad quem i suppose er so that is going to be three five R-
A-A three is what we have now discharged by denial five is the contradiction 
that allowed us to do that yes well we don't want not-not-Q what we're looking 
for of course is Q now again another pretty straightforward move if i think and 
don't need to rabbit on about very much er last doesn't go to not-not-Q to Q 
that's six double negation and now we've proved the consequent of the condition 
we're trying to prove using the antecedent yes so it's a straightforward 
conditional proof we now can discharge two in conditional proof drop it from 
the list of assumptions okay move it through into the antecedent position if 
not-P then Q and that's two seven C-P because two is the antecedent and seven 
is the consequent and 
that's what we were asked to prove now that's i th-, i think just a routine er 
R-A-A really don't think it's anyv-, anything particularly exciting or 
intriguing or interesting about it just a straightforward proof any no problems 
with this no cus yes everybody understands that i only did it because it's it's 
on the way to something else that i want to do everybody happy with that good 
now we've proved P-vel-Q arrow er sorry P P-vel-Q turnstile yields this and 
we've proved this yields this i now ask how we're going to prove the following 
sequence let's put it in a different colour P-vel-Q therefore not-P arrow Q now 
if you have any sense of what proofs were like in elementary mathematics or 
calculations and the like you know that you can put them together all right you 
can do a bit and then you do another bit mm and then you can put them together 
and the whole thing is still a valid proof or calculation or if you've remember 
at school geometry you may have 
started off with some postulates or axioms prove various theorems and then you 
call on theorems to prove other theorems mm so you don't have to do it all 
again from scratch this is it's what we call transitivity that proof is a 
transitive idea now you can see that in order to prove this from this w-, way 
one way we can do it would be first of all to write out the proof of this from 
this yes which was how many lines i eleven i think wasn't it yes something like 
that the one we did at the end last time and then to add on the end having got 
er line eleven to this mm then repeated this proof here so we would have got 
eighteen lines and then we'd have got to the conclusion if you don't believe me 
do it er you could write out a perfectly valid proof starting from here and 
let's say starting from here and ending up with here by going first to there 
and then from there to there that's that's all right isn't it i mean that's 
what you'd expect if this follows from this and this follows from this then 
this 
follows from this just by going through the the whole palaver still you 
wouldn't want to have to do that yes 
sf0931: is it despite the er multiplier in the brackets 'cause it's not 
nm0930: i'm sorry it's it's it's this that's wrong isn't it mm 
sf0931: yeah 
nm0930: yes 
sf0931: and then the next row it's not 
nm0930: it's this that should be be is is that the sh-, i'm sorry i didn't it's 
that should have been there from the start mm that was that was the sequent we 
proved last time thank you very much you're quite right i mean it's m-, er w-, 
what we have he-, now we do have now a case of going from here to here and then 
from here to here t-, what we need is a way of proving this by a short cut 
because we don't want to have to write the whole thing out every time when 
you've proved something somehow you've got it there why should you have to keep 
on proving it again and so we're going to have a new rule well let's first of 
all sketch how we might how we might do it and then introduce a new rule that's 
that's going to allow us to do this 
we start off on line one with P-vel-Q this is this is a just a sketch of what 
might happen and then we consider what was it was eleven lines wasn't it yes so 
at line eleven resting on line one we had er get it right this time okay and 
whatever the annotation was there it was a vel elimination i think wasn't it 
yes that's right something something something something something something 
vel elimination mm and now we do what we've just rubbed off the board another 
er seven lines to line eighteen resting on that we can get to and the since 
eleven rests on one then eighteen is going to rest on one and what was my last 
annotation it was two seven er C-P and therefore it's going to be twelve 
seventeen C-P that would be the full blood in proof mm just jamming the two 
together and what we want is a way of abbreviating this with a sort 
of plug-in effect what we need is a to re-, regard this as something like a 
modular system where you can take bits mm you just plug them in like little bit 
of circuitry that you push into into a circuit and it's all done for you and 
little bits of programs and so on and so we're going to repeat this proof let's 
do it on this board now we're going to re-, reduce it drastically by means of a 
rule called sequent introduction S-I actually sequent introduction has two 
forms let's do the simple form first actually it has in a way it has four forms 
er let's er let's do the th-, the the most straightforward one first and then 
we'll look at the others sequent introduction said if you have already this is 
just giving you an informal statement if you have proved a sequent a let's do 
write it rather generally A-zero through A-K-minus-one and therefore B okay so 
you prove a sequent with K premises and let's call it er what shall we call 
this er heart mm so that's on 
most keyboards these days so we call it heart if you've proved that sequent and 
in a proof you have A- zero A-K-minus-one on various lines i don't say separate 
lines because of course they may actually be the same but i mean in effect it's 
er er it doesn't make any difference if we say separate lines right so you've 
got all the premises of this sequent heart proved in your in your sequent right 
then you may proceed may write B on a separate line the assumption numbers are 
all the assumption numbers of the A-I in other words you've bundled together 
all the assumption numbers er and the annotation is [exclamation] how can we 
des-, describe it X-zero X- K- minus-one S-I where these are the line numbers 
of the A er er where X-I is the line number of A-I in other words when you call 
on this rule all you do is write down the line numbers of all the premises and 
then you go straight to the conclusion so 
it's a rule that's i mean this is rather a general statement you'll find a 
simpler statement in the workbook and in Lemon and i think we will learn it by 
example rather than trying to understand that mm so let us suppose that we've 
got we've now got the sequent P-vel-Q er therefore not if not-P and not-Q yes 
that's the one we proved last week so we'll call that diamond sorry we have to 
say here S-I this and then heart and then say you then give the name of the 
sequential calling them so we'll call this one diamond and then the one we 
proved this morning which we will call er club was was this mm diamond is what 
licenses the move from here to here and h-, club is what licenses the move from 
here to here and now we're going to turn the proof of this sequent which i 
suppose we'd better call spade since since er where we've got to namely P-vel-Q 
therefore if not-P then Q we're going to prove this sequent in three lines now 
mm 
effectively we don't have to do very much here except for renumber things and 
ignore the gaps line two of this new proof is going to be an application of 
sequent introduction to line one all right i've pr-, okay i've got i've got the 
premise of line one on a line na-, er sorry the premise of diamond on a line 
namely on line one i now can proceed immediately to the conclusion by saying 
one sequent introduction diamond and the l-, the line numbers are all the line 
numbers i need to get one and that's just one so what this rule says is in 
order to get from here to here i can do it via the sequent diamond all right if 
i wanted to i could fill in those lines there there's nine lines in between and 
i would get a straightforward proof using the primary rules this is just a 
short cut rule it doesn't add any strength to the system it doesn't do anything 
new it just saves time and effort okay and then line three is done in the same 
way still rests on one and now it's two sequent introduction club er because 
it's 
club now that licenses the move from it's not the case that not-P and not-Q to 
if not-P then Q er and there we have a proof of spade using er which is just 
three lines long though if you unpack it of course it's going to be whatever it 
was er eighteen lines long now you never need to use this rule say it's it's a 
it's just an additional rule that will save you time and effort and it's a very 
valuable rule for that are there any questions about whole thing well when i 
said there were various versions of this rule let's ha-, just mention one to 
start with the rule of theorem introduction which is indeed just a special case 
of this rule where the number of premises is zero a theorem you'll remember is 
a sequent with no premises and so since sequent introduction said if you've got 
all the premises on line on various lines then you can go to the conclusion 
theorem introduction says you just go to the conclusion so it just says you can 
introduce a theorem wherever you like mm simply introduce it 
wherever you feel like it so you can just a-, on any line you like you can 
introduce for example the theorem we that we proved last time it's not the case 
that P and not-P o-, you can just it's a [sigh] in old-fashioned er er sense 
you might say it's a like an axiom it's just something that you're it's it's 
not part of the premises of the sequent er sequent you're being given but it's 
just something you're given because it's already been proved you can just use 
it whenever you like so let's have a very simple example er well perhaps it's 
not so very simple after all no let's we'll go go on a little bit and then 
we'll come back to a simple example using that a-, actually i can state 
something for example sort of thing i ask you to prove that sequent it's not 
the case that not-P and not-not-P now if you understand what a substitution for 
a instance of a sequent is you will see that this is really the same sequent as 
this with not-P replacing P throughout er all right that if i if i take P er 
wherever it occurs and replace it by 
not-P then i'm just going to get this and you can it's the sort of thing that 
wordprocessors expected to be able to do very quickly to do replacements of 
this sort okay therefore any proof of this is really a-, a-, also a proof of 
this because you would just go through the proof changing P to not-P throughout 
and it wouldn't make any difference in other words if i've proved this i've 
really proved this already all right i mean i've done all the work that's 
needed to prove this if i've proved this so this gives us actually a a variant 
of the rule of theorem introduction that we can look at now theorem 
introduction substitution which is T-I- S rather ugly notation what this rule 
says if you've got a theorem then you can introduce on to a line not any line 
not just that theorem but any substitutions and swap it yes so here's a one 
line proof of this of this s-, this theorem let's call what shall we call this 
dollar mm so that's the thing that we've proved 
last time and so i now ask you to prove it's not the case that not-P and not-
not-P and you prove it in one line as follows theorem introduction substitution 
dollar in other words you you er as you if you'd like to use these this jargon 
you justify how you got there by saying that i obtained it from a theorem that 
i've already proved by substitution the theorem i've already proved is called 
i've just ad hoc called it dollar and the substitution is the result of 
replacing P by not-P since it's a theorem it rests on nothing at all and so we 
just put that over there so not only theorems can be introduced wherever you 
like but also any substitution instance of a theorem of course a substitution 
instance of a theorem is itself a theorem mm but you may not have proved it the 
thing is that you can't just introduce anything you like all the time in a 
sense the requirement is that you've already proved it and in an 
examination typically for example you might be told that you may use in a 
question any sequent or theorem that you've already proved mm if you were 
allowed to introduce any theorem then of course everything can be reduced to 
one line and that would be too easy er so let's have a there's also of course i 
e-, i expect you can guess there's also a sequent introduction substitution S-I-
S that is also sometimes useful and let's see how we might er use that for 
example to prove the following sequent we'll call pound sterling i want to 
prove a sequent that is rather like spade but is rather unlike it too mm this 
one has a disjunction and from it you prove a conditional whose antecedent is 
the negation of the left disjunct and this one also has a disjunction as a 
premise but here you prove a conditional whose antecedent's negation is the 
left disjunct mm a proof of thi-, this is not pound i hope is clear is not a 
substitution instance of spade right you can't go through spade replacing Ps 
and Qs uniformly by 
anything and end up with with pound you could of course replace P by not-P 
throughout spade but this would give you not-not-P here and not just P mm so 
it's not a substitution instance so we can't just call on one of these short 
cut rules to prove it we've got to do some work and i hope that we'll find that 
we can do s-, we can do it satisfactorily we are going to call on a short cut 
rule but not too much so pound is not-P or Q these names by the way are just 
for for today don't take them seriously the only two names that i will continue 
to use and not only now but in the examinati-, in the may may use in the 
examination er i shall tell you what they mean if i do use them there are star 
and dagger mm well there's one other er theorem that we're going to prove i 
hope before the end of the hour but all these other things go-, er spades and 
er hearts and dollars and so on are just ad hoc names anybody like to suggest 
how we might prove this any ideas don't do y-, do too much work that's my 
advice here how 
can you do this as quickly as possible or as slickly as possible any 
suggestions using of course the short cut rules if necessary yeah okay well 
there let me show you how you can do it and you'll kick yourselves mm not-P vel 
Q okay on line resting on line one i'm now going to go to if not-not-P then Q 
and that is going to be one sequent introduction substitution spade it's what i 
get from spade by replacing P by not-P so i'm just automatically using the 
substitution rule for sequents here on the assumption that you've already 
internalized this which perhaps is a bit unfair but nonetheless is er er i 
think it's a straightforward idea that if you have a proof as we have of spade 
and as we've already done that then you could just run through the proof 
replacing P in every pla-, place it occurs by not-P and you would get a proof 
of this yes that's that's i hope that this is obvious er just by replacing it 
by s-, you could replace it by the rain in Spain s-, stays mainly in the plane 
throughout and you'd still have a valid proof 
be t-, tiresomely long and would look a bit odd with the combination of words 
and symbols but it would still be valid you could replace it by the whole of 
the er Declaration of inde-, well perhaps Declaration of Independence contains 
imperatives the whole of some some text in the indicative mood w-, be the same 
so the the the proof goes through like that now what have we got to prove we've 
got to prove P arrow Q so i assume P for conditional proof that's how i prove 
conditionals the only way i know how to prove conditionals except trivial ones 
er so i assume P can you now see what i'm going to do yes now clear is this not 
that i'm trying to get Q after all because that's the consequent of the 
conditional i've assumed P can i use these two to get Q surely i can yes 
because in order to use this one this is er conditional i would expect to use 
modus ponens that means i want to get the antecedent the antecedent is not-not-
P that's a double negation how do i get a double negation 
by taking getting the sentence of which it is the double negation that's P have 
i how do i get P [click] all done yes in other words from P i can go to not-not-
P by three D-N and now i've got the antecedent of line two and therefore from 
one and three to one and three i can imply modus ponens gives me not-not-P and 
if not-not-P then Q that gives me Q what did i say two four modus ponens 
resting on lines one and three that's what i wanted that's the consequent of 
the conditional i'm er trying to prove it rests on line three which is the 
antecedent of the conditional i want to prove and therefore conditional proof 
that allows me to prove if P then Q three bec-, which is antecedent five which 
is the consequent C-P mm and therefore from not-P or Q i've proved if P then Q 
now the advantage of these sequent introduction rules and theorem introduction 
rules is that they enable you to break the job down into small parts that you 
can tackle i gave the 
analogy last time of making a long journey i don't know you're driving to 
[sigh] Budapest mm you you're not going to do that er in one day you're going 
to have to stop one si-, without stopping so you break the journey down into 
manageable bits that you can see how you're going to do it mm Coventry to i 
don't know Dover Dover to to o-, Ostend Ostend to Cologne or whatever i don't 
know what rou-, what the route would be mm and then you can see how to do it so 
typically when you've got a g-, more complicated proof what you do is try and 
break it down into little bits each of which you can see how to do and then you 
can put them altogether by sequent introduction if you want to though sometimes 
it's just as easy to write the proof out but sequent introduction is very 
helpful when you've got some rather long modules already any questions about 
this this rule and how it works there are some exercises this week for you to 
try involving this rule one of which it's just slightly puzzling mm just 
slightly puzzling i don't know why 
it's slightly puzzling but somehow it always it always er er leaves people 
wondering whether that can be right and yes it it is all right any questions 
there no everybody can do that 
sm0932: sequent introduction i'm not happy with it 
nm0930: you're not happy with it 
sm0932: no i'm not 
nm0930: w-, 
sm0932: why is it not-not-P when you use S-I-S 
nm0930: er because if i take this sequent which i'm given yes and everywhere 
replace P by not-P sorry i shouldn't have ri-, rubbed out that everywhere 
replace P by not-P then i get this 
sm0932: right 
nm0930: yes it's a it's a substitution instance of perhaps i could have done 
that in in er in different colours what's in pink there er is simply a re-, way 
of replacing uniformly what was in green before and then with a P mm so this is 
just a substitution instance and proofs of substitutions instances follow the s-
, exactly the same pattern as the proof of the original i mean if th-, you're 
not persuaded by that just write out a proof some proof of say half a dozen 
lines and then take a substitution 
instance and write out the proof of the substitution instance and and about 
halfway through you'll say why am i doing this mm what's the point of doing 
this again it's obviously the same proof er sometimes it's it's actually 
existentional absorption into the task does convince you in a way that no 
amount of theory would mm yes 
sm0933: can you substitute it with anything 
nm0930: you can substi-, provided you substitute uniformly for letters 
sm0933: could you put Q 
nm0930: yes you could put Q yes indeed you could if you put if you put let's 
choose another colour if you put Q shall we shall we go back to the the the 
original version i can replace P by Q that would give me Q-vel-Q therefore if 
not-Q then Q yes and indeed that is a sequent that in effect we have now proved 
because we've proved spade and this is a substitution instance mm or we could 
have replaced it by not-Q and then or rather we er let well we could replace Q 
by not-P here and that would give us P vel not-P therefore if not-P then not-P 
well that is perhaps is not a very interesting sequent because that 
conclusion is itself provable nonetheless all these se-, these substitutions 
are possible the two things i stress i str-, i stress again first of all it 
must be uniform yes you must replace every occurrence by the same thing and 
secondly you can only substitute for letters you can't s-, i mean i-, if in 
this formula i can't replace not-Q by P that wouldn't be a substitution 
instance i can only replace Q or any other letter by a formula but not er but 
not er er a compound formula because this formula has to be something that is a 
conditional whose antecedent is a negation if i were allowed to replace this 
well let's say by R i would have now gone to a case that wasn't necessarily a 
negation so i would have e-, actually gone to something more general rather 
than to something more specific which is what substitution is okay it's the 
same exactly the same in algebra it's exactly the same thing that if you have 
an algebraic formula X-plus-Y-all-squared equals X-squared plus two-X-Y plus Y-
squared 
you can replace X and Y by anything you like yes for example you can replace 
them both by zero or both by minus-one or both by X or both by Z right well i 
think we've got since we we came across this formula here i think it's now time 
to prove this formula as a theorem mm this one is a theorem and in fact this se-
, this implication this er er derivation goes in the other direction but rather 
than try to do all that i'll just con-, finish with the proof of P or not-P 
because P or not-P is a it's a it's a characteristic of a type of proof that is 
has the reaches the level of sophistication that i think is essential to 
succeed in this course you do you understand how to do this there are more 
difficult proofs there's no question but this is the the s-, the sort of level 
i would say if you n-, if you know and understand how to do proofs like this 
then you've you got the idea mm okay P or not-P is called the law of excluded 
middle and that's a that's of course a an old name it's also the its medieval 
Latin name tertium non datur it means the third is not given so it's an anti-
Blairite 
er type er type of er [laugh] of theorem it says either P no-, or not-P but no 
third possibility yes there's nothing additional to P and its negation yes and 
it's it was regarded along with the law of non-contradiction which i mentioned 
last time which may even still be on the board somewhere well yes here yes and 
the law of identity as it was sometimes called if P then P these were regarded 
as the fundamental laws of logic this was in a b-, b-, before logic was 
properly developed but nonetheless they do contain a lot of the important facts 
about it and the question is how are we going to prove this theorem you can see 
i've got six minutes to do this in so i'd better get my skates on here right 
what do you do when you've got to prove a sequent you first of all write down 
what you're given that's all right done that then look at what we've got to 
prove what sort of a sentence have we got to prove a disjunction how do you 
prove a disjunction well the rule that allows you to prove a disjunction is vel 
introduction how do you 
prove how do you use vel introduction you've got to get one of the disjuncts 
first can we get P or not-P well obviously not very straightforwardly mm i 
can't i mean i just get P out of nowhere if i could prove P from nothing at all 
then that would be logic over mm you can prove everything from nothing at all 
and we could all go home and forget about it mm fortunately for us it's not as 
easy as that mm so what do we do we can't look at our premises and get some 
clues from them because there aren't any premises the conclusion doesn't isn't 
at all helpful it just tells us to prove a disjunction even though actually we 
can't prove either of the disjuncts well what do i say you should do when you 
there's nothing else to do reductio ad absurdum you've just got to somehow go 
for a contradiction so this is how this this proof goes er i think there's room 
on this board line one we assume it's not the case that P or not-P and this is 
an assumption that well the only way we know how to get rid of it is by R-A-A 
we're not quite 
sure how we're going to do that yet but that's the the beauty of R-A-A you can 
as it were set out on that journey without having a very any very clear idea 
about how you're going to get to the terminus mm well now what sort of a 
sentence have we got on line one what i called earlier today a compound 
negation what do what was my advice in this when you've got a compound negation 
try to construct the formula in the insides that's P or not-P how do i 
construct a disjunction by getting one of the disjuncts we seem to have gone 
round in a circle but not quite because if i try to construct this there's no 
reason why i shouldn't just assume P this is also an assumption for R-A-A see 
that's the other beauty of R-A-A that you can make all these assumptions and as 
long as you get a contradiction you can start knocking them down again so here 
i've got an assumption P now i can construct the sentence that is denied on 
line one by vel introduction P vel not-P so lines one and three contradict each 
other and so from lines one and two i've i have P vel not-P and it's not the 
case that P vel not-P mind your parentheses mm make sure you understand what 
you're writing down get the parentheses right so that's one and three and 
introduction that's a contradiction i can deny therefore either one or two now 
if you think about it it's pointless to deny one at this stage mm you would 
actually find you'd got back where you s-, in effect to where you started but 
we can deny two at this stage this you can change your colour to show how 
important it is and resting on one we now get not-P er two four R-A-A now we've 
made a tremendous advance here at this stage we had one of the disjuncts of 
what we're trying to prove assumed we had to assume it but at this stage we've 
proved it from from one that's mu-, that's much less commitment on our part and 
we can now repeat this process exactly the same way we now introduce not-P on 
er P on the left i'm sorry five vel introduction so that gives us and now we 
can do another reductio ad absurdum resting on one we get P or not-P and it's 
not the case 
that P or not-P all right that's a conjunction of one and six another 
contradiction now we can there's only one thing we can deny now and that's one 
itself and so we can eliminate the function one by denying it now it's very 
important here that you remember that you must write not-not-P or not-P er one 
seven R-A-A and then on the final line we can get rid of those negation signs 
and we get P or not-P eight D-N now that proof certainly repays study mm it's 
theorem forty-four in Lemon i often refer to it as theorem forty-four for 
example in the workbook you could refer to it as the law of excluded middle L-E-
M if you liked or T-N-D er provided you know what you're doing mm it happens to 
be along with star and dagger something that is often useful to call on when 
you're doing proofs and through with sequent introduction and theorem 
introduction well next time we'll say a little bit more about this and show how 
we can generalize it mm to prove other other sequents with disjunctive 
conclusions well that was fairly hard work this morning mm thank you very much