Skip to main content

pslct033

<?xml version="1.0"?>

<!DOCTYPE TEI.2 SYSTEM "base.dtd">

<TEI.2><teiHeader>

<fileDesc>

<titleStmt>

<title>Formal Logic</title></titleStmt>

<publicationStmt><distributor>BASE and Oxford Text Archive</distributor>

<idno>pslct033</idno>

<availability><p>The British Academic Spoken English (BASE) corpus was developed at the

Universities of Warwick and Reading, under the directorship of Hilary Nesi

(Centre for English Language Teacher Education, Warwick) and Paul Thompson

(Department of Applied Linguistics, Reading), with funding from BALEAP,

EURALEX, the British Academy and the Arts and Humanities Research Board. The

original recordings are held at the Universities of Warwick and Reading, and

at the Oxford Text Archive and may be consulted by bona fide researchers

upon written application to any of the holding bodies.

The BASE corpus is freely available to researchers who agree to the

following conditions:</p>

<p>1. The recordings and transcriptions should not be modified in any

way</p>

<p>2. The recordings and transcriptions should be used for research purposes

only; they should not be reproduced in teaching materials</p>

<p>3. The recordings and transcriptions should not be reproduced in full for

a wider audience/readership, although researchers are free to quote short

passages of text (up to 200 running words from any given speech event)</p>

<p>4. The corpus developers should be informed of all presentations or

publications arising from analysis of the corpus</p><p>

Researchers should acknowledge their use of the corpus using the following

form of words:

The recordings and transcriptions used in this study come from the British

Academic Spoken English (BASE) corpus, which was developed at the

Universities of Warwick and Reading under the directorship of Hilary Nesi

(Warwick) and Paul Thompson (Reading). Corpus development was assisted by

funding from the Universities of Warwick and Reading, BALEAP, EURALEX, the

British Academy and the Arts and Humanities Research Board. </p></availability>

</publicationStmt>

<sourceDesc>

<recordingStmt>

<recording dur="00:49:53" n="6687">

<date>05/11/1998</date><equipment><p>video</p></equipment>

<respStmt><name>BASE team</name>

</respStmt></recording></recordingStmt></sourceDesc></fileDesc>

<profileDesc>

<langUsage><language id="en">English</language>

<language id="la">Latin</language>

</langUsage>

<particDesc>

<person id="nm0930" role="main speaker" n="n" sex="m"><p>nm0930, main speaker, non-student, male</p></person>

<person id="sf0931" role="participant" n="s" sex="f"><p>sf0931, participant, student, female</p></person>

<person id="sm0932" role="participant" n="s" sex="m"><p>sm0932, participant, student, male</p></person>

<person id="sm0933" role="participant" n="s" sex="m"><p>sm0933, participant, student, male</p></person>

<personGrp id="ss" role="audience" size="m"><p>ss, audience, medium group </p></personGrp>

<personGrp id="sl" role="all" size="m"><p>sl, all, medium group</p></personGrp>

<personGrp role="speakers" size="6"><p>number of speakers: 6</p></personGrp>

</particDesc>

<textClass>

<keywords>

<list>

<item n="speechevent">Lecture</item>

<item n="acaddept">Philosophy</item>

<item n="acaddiv">ps</item>

<item n="partlevel">UG</item>

<item n="module">unknown</item>

</list></keywords>

</textClass>

</profileDesc></teiHeader>

<text><body>

<u who="nm0930"> last time <pause dur="0.2"/> we proved if i'm <trunc>r</trunc> <pause dur="0.3"/> i hope <pause dur="0.2"/> got it right <pause dur="6.4"/><kinesic desc="writes on board" iterated="y" dur="14"/> we proved this sequent as you remember <pause dur="0.3"/> is one of the De Morgan Laws <pause dur="7.1"/> # <pause dur="0.8"/> i now want to <pause dur="0.2"/> as it were <pause dur="0.2"/> not <pause dur="0.4"/> immediately do another De Morgan Law <pause dur="0.8"/> although you will find <pause dur="0.2"/> several of them done in the book <pause dur="1.3"/> but to go on to something <pause dur="0.4"/> # <pause dur="0.5"/> directly from this <pause dur="5.3"/> <kinesic desc="writes on board" iterated="y" dur="6"/> to prove <kinesic desc="indicates point on board" iterated="n"/> this sequent <pause dur="1.3"/> it's not the case that <pause dur="0.4"/> not-P and not-Q <pause dur="0.8"/> therefore <pause dur="0.6"/><kinesic desc="writes on board" iterated="y" dur="3"/> if not-P then Q <pause dur="3.1"/> and so <pause dur="0.3"/> here we've got <pause dur="0.2"/> go from <kinesic desc="indicates point on board" iterated="n"/> here to <kinesic desc="indicates point on board" iterated="n"/> here <pause dur="0.4"/> and now we're going to

prove from <pause dur="1.5"/> the conclusion of the previous argument <pause dur="0.5"/> the <pause dur="0.7"/> are going to prove another <pause dur="0.6"/> # conclusion <pause dur="0.5"/> so and let's do that on the centre board <pause dur="10.3"/> <kinesic desc="writes on board" iterated="y" dur="10"/> remember <pause dur="0.3"/> that <pause dur="0.7"/><kinesic desc="indicates point on board" iterated="n"/> this <pause dur="0.2"/> thing without any parentheses in it means a conditional <pause dur="0.4"/><kinesic desc="indicates point on board" iterated="n"/> that's the main connective a conditional <pause dur="0.3"/> in which the antecedent is not-P <pause dur="0.4"/> and the consequence is Q it's not <pause dur="2.7"/><kinesic desc="writes on board" iterated="y" dur="5"/> it's not the negation of a conditional <pause dur="0.8"/> which we wanted to write the negation of a conditional we would write it like that <pause dur="1.9"/> so <pause dur="0.6"/> how are we going to prove this <pause dur="5.4"/><kinesic desc="writes on board" iterated="y" dur="7"/> obviously <pause dur="0.4"/> as usual we assume what we're given <pause dur="1.5"/> right so it's not the case that <pause dur="0.4"/> not-P and not-Q <pause dur="0.5"/> remember you can't <pause dur="0.6"/> that <pause dur="0.3"/> you must respect all these <trunc>m</trunc> negation signs and the parentheses <pause dur="0.9"/> you can't just push the negation signs through or anything like that <pause dur="1.1"/> what have we got to prove <pause dur="0.2"/> well <pause dur="0.4"/> right let's before we even go that far let's say to ourselves what sort of a sentence <kinesic desc="indicates point on board" iterated="n"/>

is this it's a negation it's not only a negation <pause dur="0.3"/> it's what <pause dur="0.3"/><kinesic desc="writes on board" iterated="y" dur="5"/> i usually refer to as a compound negation <pause dur="2.8"/> other words the negation <pause dur="0.2"/> of <pause dur="0.2"/> an already complicated sentence <pause dur="1.3"/> what can you do <pause dur="0.2"/> with the negation of an already complicated sentence <pause dur="0.3"/> actually not very much except <pause dur="1.1"/> and this is the the standard way of proceeding in these cases if you've got something <kinesic desc="indicates point on board" iterated="n"/> like this <pause dur="0.5"/> is to try to build up what's inside <pause dur="1.0"/> the parentheses <pause dur="1.0"/> and get a contradiction <pause dur="1.0"/> so if you <trunc>res</trunc> if you get a compound negation <pause dur="0.3"/> try to construct <pause dur="0.2"/> whatever it is that is negated <pause dur="0.5"/> then you've got a contradiction <pause dur="0.3"/> and with a contradiction you can always deny something so you can always make some progress <pause dur="0.6"/> so don't <pause dur="0.6"/> people often ask what am i going do when i've got a negation sign outside a set of parentheses <pause dur="0.3"/> the only <pause dur="0.3"/> general advice i can give you is just what i have given you <pause dur="0.9"/> okay <pause dur="0.4"/> so <pause dur="0.6"/> we already know <pause dur="0.4"/> that we're going to head for R-A-A <pause dur="3.3"/> what have we got to prove <kinesic desc="writes on board" iterated="y" dur="1"/><pause dur="0.6"/> well <pause dur="0.4"/> we've got prove a conditional <pause dur="0.9"/> we know how to prove conditionals <pause dur="1.6"/><kinesic desc="writes on board" iterated="y" dur="4"/> we

assume the antecedent <pause dur="0.5"/> that's <pause dur="1.4"/> we're going to discharge it in conditional proof we already know that <pause dur="1.3"/> # <pause dur="0.4"/> and it rests on itself <pause dur="5.0"/> now what have we got to prove <pause dur="0.5"/> we've reduced the problem <pause dur="0.4"/> <unclear>they've put it before</unclear> <pause dur="0.3"/> having assumed <kinesic desc="indicates point on board" iterated="n"/> this we've reduced the problem now to proving Q <pause dur="1.3"/> how are we going to prove Q <pause dur="0.9"/> well <pause dur="1.5"/> again <pause dur="0.8"/> if you look at <kinesic desc="indicates point on board" iterated="n"/> this and think how am i going to prove Q <pause dur="0.7"/> there's no <pause dur="0.3"/> obvious way of using <kinesic desc="indicates point on board" iterated="n"/> this <pause dur="0.2"/> there's no obvious way of using <kinesic desc="indicates point on board" iterated="n"/> this except to build up a contradiction <pause dur="0.6"/> so <pause dur="1.2"/> if nothing <pause dur="0.3"/> as it were stares you in face as to what you should do <pause dur="0.4"/> the best thing to do <pause dur="0.2"/> is to <trunc>he</trunc> <pause dur="0.5"/> try R-A-A <pause dur="0.6"/> so i want to prove Q <pause dur="0.2"/> how am i going to prove Q <pause dur="1.3"/> yes <pause dur="1.5"/> assume <pause dur="0.9"/><kinesic desc="writes on board" iterated="y" dur="10"/> not the Q <pause dur="0.3"/> huh <trunc>s</trunc> <pause dur="1.0"/> so i assume in <pause dur="0.2"/> in <trunc>th</trunc> in this case <pause dur="0.2"/> i assume not-Q <pause dur="1.1"/> for R-A-A <pause dur="3.5"/> and now you can see it's suddenly <pause dur="0.4"/> all <pause dur="0.4"/> come out nicely <pause dur="0.3"/> because <pause dur="0.4"/> what we're doing we're in the middle of an R-A-A somewhere <pause dur="0.2"/> we're looking for a contradiction <pause dur="1.9"/> that's not difficult is it to get a contradiction out of that <pause dur="0.3"/> remember a contradiction is of form A and not-A <pause dur="0.9"/><kinesic desc="indicates point on board" iterated="n"/> this is a compound

negation <pause dur="0.3"/> we can get the thing of which lose the negation formula which # which lose the negation <pause dur="0.3"/> by conjoining two and three <pause dur="1.2"/><kinesic desc="writes on board" iterated="y" dur="10"/> and so we get <pause dur="1.8"/> not-P <pause dur="0.2"/> and not-Q <pause dur="1.6"/> two three and introduction <pause dur="1.7"/> and <pause dur="0.2"/> <trunc>whe</trunc> now moving fast towards this contradiction <pause dur="6.9"/><kinesic desc="writes on board" iterated="y" dur="3"/> one two three <pause dur="0.4"/> this is going to rest on all of the the assumption which one and <pause dur="0.6"/> and # four rest on <pause dur="0.3"/> and now we've got to conjoin these <pause dur="1.1"/> and so <kinesic desc="writes on board" iterated="y" dur="10"/> we have to put in some more parentheses to make it quite unambiguous <pause dur="1.3"/> not-P and not-Q <pause dur="0.2"/> and <pause dur="0.2"/> it's not the case that <pause dur="0.3"/> not-P and not-Q <pause dur="2.0"/> sometimes these <pause dur="0.2"/> R-A-As you do find you get rather lengthy lines <pause dur="0.3"/> so <pause dur="0.2"/> # you <trunc>m</trunc> <pause dur="0.6"/> try not to <pause dur="0.2"/> start off <pause dur="0.3"/> from now onwards <pause dur="0.2"/> when you're writing out proofs <pause dur="0.2"/> don't don't <pause dur="0.5"/> put the assumption numbers too close <pause dur="0.3"/> to the <pause dur="0.5"/> # the <trunc>as</trunc> the annotations too close to the line numbers you may need quite a bit of space <pause dur="1.0"/> okay <pause dur="1.8"/> so <kinesic desc="indicates point on board" iterated="n"/> here i do have something of the form A and not-A because if i take A and not-A and replace A by <pause dur="0.8"/> not-P and not-Q <pause dur="0.4"/> then i will get <pause dur="0.6"/> just that <kinesic desc="indicates point on board" iterated="n"/> <pause dur="0.5"/> okay <pause dur="0.5"/> everybody happy with

that <pause dur="0.7"/><kinesic desc="indicates point on board" iterated="n"/> that's contradiction <pause dur="2.8"/> and so <pause dur="0.4"/> i've done what i was <trunc>goin</trunc> said i was going to do <kinesic desc="indicates point on board" iterated="n"/> here namely <trunc>f</trunc> <pause dur="0.3"/> find get hold of the sentence that is negated on line one <pause dur="1.8"/> and then <kinesic desc="indicates point on board" iterated="n"/> from here i introduced not-Q for R-A-A i've got a contradiction <pause dur="0.9"/> # <pause dur="0.2"/> in the sense i have only to look back to see which assumption has got R-A-A against it to see <pause dur="0.7"/> what i expect to do at this stage it's three that i'm going to deny <pause dur="0.6"/> yes <pause dur="1.4"/> mm <pause dur="0.2"/> right <pause dur="0.3"/> no point denying one <pause dur="0.3"/> one or two normally <pause dur="0.2"/> it's three that i'm going to deny <pause dur="0.9"/> and so <pause dur="0.6"/> oh sorry i haven't filled this in yet have i <pause dur="0.7"/> # what do i need here <pause dur="0.6"/> i need <pause dur="0.4"/> a one four <kinesic desc="writes on board" iterated="y" dur="3"/> and introduction <pause dur="4.4"/> i tend to take <trunc>n</trunc> at this stage in the term <pause dur="0.5"/> tend to assume that <trunc>an</trunc> the and rules are so straightforward that i hardly need to <pause dur="0.6"/> mention them <pause dur="2.9"/><kinesic desc="writes on board" iterated="y" dur="4"/> so we're going to deny three that means we discharge three in R-A-A <pause dur="0.4"/> leaving ourselves <pause dur="0.3"/> with just one and two as the assumptions <pause dur="0.4"/> denying three means what <pause dur="0.2"/> it means <pause dur="2.0"/> adding a negation sign to the front of three <pause dur="5.7"/><kinesic desc="writes on board" iterated="y" dur="2"/> and the annotation is that <pause dur="0.9"/>

the two lines namely <pause dur="0.5"/> the line that we've just denied that's line three <pause dur="0.5"/> and the contradiction that we used deny it to deny it in other words <pause dur="0.3"/> the <pause dur="0.9"/> <distinct lang="la">absurdum</distinct> <pause dur="0.6"/> <distinct lang="la">ad</distinct> which i can't get my Latin right <pause dur="0.4"/> the <distinct lang="la">absurdum</distinct> # # <trunc>abs</trunc> the absurdity to which we reduced it <pause dur="0.3"/> mm <pause dur="0.3"/> <distinct lang="la">ad quem</distinct> i suppose <pause dur="1.9"/> # so <pause dur="0.5"/> that is going to be <kinesic desc="writes on board" iterated="y" dur="4"/> three <pause dur="0.2"/> five R-A-A <pause dur="1.0"/> three is what we have now discharged by denial <pause dur="0.3"/> five is the contradiction that allowed us to do that <pause dur="0.9"/> yes <pause dur="3.7"/> well we don't want not-not-Q <pause dur="0.4"/> what we're looking for of course is Q <pause dur="1.7"/> now again another <pause dur="0.8"/><kinesic desc="writes on board" iterated="y" dur="3"/> pretty straightforward move <pause dur="0.2"/> <unclear>if i think</unclear> <pause dur="0.3"/> and don't need to <pause dur="0.8"/> rabbit on about very much <pause dur="1.3"/> # last doesn't go to not-not-Q to Q <pause dur="0.2"/> that's <kinesic desc="writes on board" iterated="y" dur="1"/> six double negation <pause dur="4.3"/> and now <pause dur="0.7"/> we've proved the consequent of the condition we're trying to prove <pause dur="0.3"/> using the antecedent <pause dur="1.4"/> yes <pause dur="0.4"/> so it's a straightforward conditional proof <pause dur="0.4"/> we now <pause dur="0.2"/> can discharge two <pause dur="0.7"/> in conditional proof <pause dur="0.5"/><kinesic desc="writes on board" iterated="y" dur="2"/> drop it from the list of assumptions <pause dur="1.1"/> okay <pause dur="0.3"/> move it through into the antecedent position <pause dur="0.5"/><kinesic desc="writes on board" iterated="y" dur="8"/> if not-P then Q <pause dur="2.2"/> and that's two seven C-P because two is the antecedent <pause dur="0.4"/> and seven is the consequent <pause dur="2.1"/> and

that's what we were <pause dur="0.4"/> asked to prove <pause dur="2.4"/> now <pause dur="0.2"/> that's <pause dur="0.4"/> i <trunc>th</trunc> i think just a routine # <pause dur="0.2"/> R-A-A really <pause dur="0.5"/> don't think it's <trunc>anyv</trunc> anything particularly exciting <pause dur="0.3"/> or <pause dur="0.2"/> intriguing or <pause dur="0.3"/> interesting about it <pause dur="0.2"/> just a straightforward proof any <pause dur="0.3"/> no problems with this <pause dur="0.2"/> no <unclear><trunc>cus</trunc></unclear> <pause dur="0.4"/> yes everybody understands that <pause dur="0.9"/> i only did it <pause dur="0.3"/> because <pause dur="0.7"/> it's <pause dur="0.7"/> it's <pause dur="1.2"/> on the way to something else that i want to do <pause dur="3.1"/> everybody happy with that <pause dur="0.9"/> good <pause dur="3.2"/> now <pause dur="0.2"/> we've proved <pause dur="0.7"/> P-vel-Q <pause dur="1.0"/> arrow <pause dur="1.2"/> # sorry <pause dur="0.3"/> P P-vel-Q turnstile <pause dur="0.6"/> yields <pause dur="0.7"/><kinesic desc="indicates point on board" iterated="n"/> this <pause dur="0.2"/> and we've proved <kinesic desc="indicates point on board" iterated="n"/> this yields <kinesic desc="indicates point on board" iterated="n"/> this i now ask <pause dur="0.6"/> how we're going to prove the following sequence let's put it in a <kinesic desc="writes on board" iterated="y" dur="6"/> different colour <pause dur="0.6"/> P-vel-Q <pause dur="0.3"/> therefore <pause dur="1.0"/> not-P <pause dur="2.1"/> arrow Q <pause dur="6.1"/> now <pause dur="1.1"/> if you have any sense of what proofs were like in <pause dur="0.2"/> elementary mathematics or calculations and the like <pause dur="0.3"/> you know <pause dur="0.2"/> that you can put them together <pause dur="0.6"/> all right you can do a bit <pause dur="0.3"/> and then you do another bit <pause dur="0.4"/> mm <pause dur="0.3"/> and then you can put them together <pause dur="0.3"/> and the whole thing is still a valid proof or calculation <pause dur="1.6"/> or if you've remember at school geometry you may have

started off with some postulates or axioms <pause dur="0.6"/> prove various theorems and then you call on theorems <pause dur="0.5"/> to prove other theorems <pause dur="0.6"/> mm so you don't have to do it all again from scratch <pause dur="0.7"/> this is <pause dur="0.3"/> it's what we call transitivity that proof is a transitive idea <pause dur="2.1"/> now you can see that in order to prove <pause dur="0.3"/> <kinesic desc="indicates point on board" iterated="n"/> this from <kinesic desc="indicates point on board" iterated="n"/> this <pause dur="0.4"/> <trunc>w</trunc> way one way we can do it would be <pause dur="0.2"/> first of all to write out <pause dur="0.3"/> the proof <pause dur="0.2"/> of <kinesic desc="indicates point on board" iterated="n"/> this from <kinesic desc="indicates point on board" iterated="n"/> this <pause dur="1.0"/> yes <pause dur="0.7"/> which was <pause dur="0.7"/> how many lines i eleven i think wasn't it <pause dur="0.8"/> yes <pause dur="0.2"/> something like that the one we did at the end last time <pause dur="0.7"/> and then <pause dur="0.4"/> to add on the end <pause dur="0.5"/> having got # line eleven to <kinesic desc="indicates point on board" iterated="n"/> this <pause dur="0.4"/> mm <pause dur="0.3"/> then <pause dur="0.4"/> repeated <kinesic desc="indicates point on board" iterated="n"/> this proof here <pause dur="0.4"/> so we would have got <pause dur="0.4"/> eighteen lines and then we'd have got to the conclusion <pause dur="1.4"/> if you don't believe me do it <pause dur="0.6"/> # you could write out <pause dur="0.2"/> a perfectly valid proof <pause dur="0.7"/> starting from <kinesic desc="indicates point on board" iterated="n"/> here <pause dur="0.2"/> <gap reason="inaudible" extent="1 sec"/> and let's say starting from here <kinesic desc="indicates point on board" iterated="n"/> <pause dur="0.3"/> and ending up with here <pause dur="0.5"/> by going first to there <kinesic desc="indicates point on board" iterated="n"/> <pause dur="0.6"/> and then <kinesic desc="indicates point on board" iterated="n"/> from there <kinesic desc="indicates point on board" iterated="n"/> to there <pause dur="0.9"/> that's <pause dur="0.3"/> that's all right isn't it i mean that's <pause dur="0.4"/> what you'd expect if <kinesic desc="indicates point on board" iterated="n"/> this <pause dur="0.3"/> follows from <kinesic desc="indicates point on board" iterated="n"/> this <pause dur="0.2"/> and <kinesic desc="indicates point on board" iterated="n"/> this follows from <kinesic desc="indicates point on board" iterated="n"/> this then <kinesic desc="indicates point on board" iterated="n"/> this

follows from <kinesic desc="indicates point on board" iterated="n"/> this just by <pause dur="0.6"/> going through the <pause dur="0.2"/> the whole palaver <pause dur="2.5"/> still <pause dur="0.2"/> you wouldn't want to have to do that yes </u><pause dur="0.2"/> <u who="sf0931" trans="pause"> is it despite the # <unclear>multiplier</unclear> in the brackets <pause dur="1.7"/> 'cause it's not </u><pause dur="1.0"/> <u who="nm0930" trans="pause"> i'm sorry <pause dur="0.5"/> it's it's it's <kinesic desc="indicates point on board" iterated="n"/> this that's wrong isn't it mm </u><pause dur="0.3"/> <u who="sf0931" trans="pause"> yeah </u><u who="nm0930" trans="overlap"> yes </u><u who="sf0931" trans="overlap"> and then the next row it's not </u><pause dur="0.5"/> <u who="nm0930" trans="pause"> it's <kinesic desc="indicates point on board" iterated="n"/> this that should be be is is that the <trunc>sh</trunc> i'm sorry i didn't <pause dur="0.8"/><kinesic desc="writes on board" iterated="y" dur="1"/> it's that should have been there from the start mm <pause dur="1.5"/><kinesic desc="indicates point on board" iterated="n"/> that was that was the sequent we proved last time <pause dur="1.1"/> thank you very much <pause dur="0.4"/> you're quite right i mean it's <trunc>m</trunc> <pause dur="0.7"/> # <pause dur="0.5"/> <trunc>w</trunc> what we have <trunc>he</trunc> now we do have now <pause dur="1.1"/> a case of going from <kinesic desc="indicates point on board" iterated="n"/> here to <kinesic desc="indicates point on board" iterated="n"/> here <pause dur="0.2"/> and then from <kinesic desc="indicates point on board" iterated="n"/> here to <kinesic desc="indicates point on board" iterated="n"/> here <pause dur="0.8"/> <trunc>t</trunc> what we need <pause dur="0.3"/> is a way of proving this by a short cut <pause dur="1.6"/> because we don't want to have to write the whole thing out every time <pause dur="0.5"/> when you've proved something <pause dur="0.4"/> somehow you've got it <pause dur="0.2"/> there <pause dur="0.4"/> why should you have to keep on proving it again <pause dur="2.9"/> and so we're going to have a new rule <pause dur="0.3"/> well let's first of all sketch how we might <pause dur="0.5"/> how we might do it <pause dur="1.2"/> and then <pause dur="0.2"/> introduce a new rule <pause dur="0.3"/> that's <pause dur="0.2"/> <gap reason="inaudible" extent="1 sec"/> that's going to allow us to do this <pause dur="13.4"/><kinesic desc="writes on board" iterated="y" dur="24"/>

we start off on line one with P-vel-Q <pause dur="0.7"/> this is <pause dur="0.3"/> this is a just a sketch of what might happen <pause dur="1.1"/> and then we consider <pause dur="1.0"/> what was it was eleven lines wasn't it <pause dur="0.5"/> yes <pause dur="0.5"/> so <pause dur="0.2"/> at line eleven <pause dur="0.2"/> resting on line one <pause dur="0.3"/> we had <pause dur="0.8"/> # <pause dur="0.2"/> get it right this time <pause dur="6.3"/> okay and whatever the annotation was there <pause dur="1.6"/> it was a vel elimination i think wasn't it <pause dur="0.3"/> yes <pause dur="2.2"/> that's right <pause dur="0.3"/> something <pause dur="0.5"/><kinesic desc="writes on board" iterated="y" dur="3"/> something something something something something <pause dur="0.2"/> vel elimination <pause dur="0.7"/> mm <pause dur="2.4"/> and now <pause dur="0.3"/> we do what we've just rubbed off the board <pause dur="0.7"/><kinesic desc="writes on board" iterated="y" dur="4"/> another <pause dur="0.3"/> # seven lines to line <pause dur="0.2"/> eighteen <pause dur="0.7"/> resting on <kinesic desc="indicates point on board" iterated="n"/> that we can get to <pause dur="3.6"/><kinesic desc="writes on board" iterated="y" dur="2"/> and the since eleven rests on one <pause dur="0.4"/> then eighteen <kinesic desc="writes on board" iterated="y" dur="1"/> is going to rest on one <pause dur="0.8"/> and what was my last annotation it was two <pause dur="0.4"/> seven <pause dur="0.5"/> # <pause dur="1.1"/> C-P and therefore it's going to be twelve seventeen C-P <kinesic desc="writes on board" iterated="y" dur="2"/><pause dur="1.6"/> that would be the full blood in proof <pause dur="0.2"/> mm <pause dur="0.3"/> just jamming the two together <pause dur="5.8"/> and what we want is a way of <pause dur="0.4"/> abbreviating this <pause dur="1.2"/> with a sort

of plug-in <pause dur="0.3"/> effect <pause dur="0.6"/> what we need is a <pause dur="0.7"/> to <trunc>re</trunc> <pause dur="0.3"/> regard this as something like a modular system where you can <pause dur="0.9"/> take bits <pause dur="0.2"/> mm you just plug them in <pause dur="0.2"/> like little bit of circuitry that you <pause dur="0.7"/> push into <pause dur="0.4"/> into a circuit <pause dur="0.4"/> and <pause dur="0.5"/> it's all done for you <pause dur="0.5"/> and little bits of programs and so on <pause dur="2.3"/> and so we're going to repeat this proof let's do it on <kinesic desc="indicates board" iterated="n"/> this board <pause dur="1.7"/> now <pause dur="0.4"/> we're going to <pause dur="1.0"/> <trunc>re</trunc> reduce it drastically by means of a rule called <pause dur="0.3"/> sequent introduction <pause dur="10.0"/><kinesic desc="writes on board" iterated="y" dur="10"/> S-I <pause dur="1.4"/> actually sequent introduction has two forms <pause dur="0.7"/> let's do the simple form first <pause dur="0.8"/> actually it has <pause dur="0.3"/> in a way it has four forms <pause dur="0.6"/> # <pause dur="0.3"/> let's # let's do the <trunc>th</trunc> the the most straightforward one first and then we'll look at the others <pause dur="1.6"/> sequent introduction said <pause dur="0.2"/> if you have already <pause dur="0.2"/><kinesic desc="writes on board" iterated="y" dur="16"/> this is just giving you an informal statement <pause dur="0.3"/> if you have <pause dur="1.9"/> proved <pause dur="1.4"/> a sequent <pause dur="2.7"/> a <pause dur="0.3"/> let's do write it rather generally <pause dur="0.4"/> A-zero through A-K-minus-one and therefore B <pause dur="0.6"/> okay so you prove <pause dur="0.6"/> a sequent with K premises <pause dur="4.0"/> and let's call it <pause dur="0.4"/> # <kinesic desc="writes on board" iterated="y" dur="3"/> what shall we call this <pause dur="0.2"/> # heart <pause dur="0.6"/> mm <pause dur="1.8"/> so that's on

most keyboards these days <pause dur="0.8"/> so we call it heart if you've proved that sequent <kinesic desc="writes on board" iterated="y" dur="16"/> and <pause dur="0.6"/> in <pause dur="0.4"/> a proof <pause dur="1.5"/> you <pause dur="0.7"/> have <pause dur="0.9"/> A-<pause dur="0.3"/>zero <pause dur="0.8"/> A-K-minus-one <pause dur="0.7"/> on <pause dur="1.1"/> various lines <pause dur="2.4"/> i don't say separate lines because of course they may actually be the same <pause dur="0.9"/> but <pause dur="0.3"/> i mean in effect it's # # it doesn't make any difference if we say separate lines <pause dur="0.9"/> right so <pause dur="0.3"/> you've got all the premises of this sequent heart <pause dur="0.5"/> proved in your in your sequent <pause dur="0.2"/> right <pause dur="0.6"/> then you may proceed <pause dur="3.2"/><kinesic desc="writes on board" iterated="y" dur="12"/> may <pause dur="0.5"/> write <pause dur="1.8"/> B <pause dur="0.3"/> on <pause dur="0.3"/> a separate line <pause dur="8.1"/><kinesic desc="writes on board" iterated="y" dur="21"/> the assumption numbers <pause dur="6.8"/> are <pause dur="0.3"/> all the assumption numbers <pause dur="4.8"/> of the A-I <pause dur="5.7"/> in other words you've bundled together all the assumption numbers <pause dur="0.6"/><kinesic desc="writes on board" iterated="y" dur="6"/> # <pause dur="3.0"/> and <pause dur="0.6"/> the <pause dur="0.2"/> annotation <pause dur="2.8"/> is <vocal desc="exclamation" iterated="n"/> how can we <trunc>des</trunc> describe it <pause dur="1.2"/><kinesic desc="writes on board" iterated="y" dur="5"/> X-zero <pause dur="0.6"/> X-<pause dur="0.8"/>K-<pause dur="0.2"/>minus-one <pause dur="0.4"/> S-I <pause dur="0.5"/> where <pause dur="0.4"/><kinesic desc="indicates point on board" iterated="n"/> these are the line numbers <pause dur="0.2"/> of the <pause dur="0.4"/> A # <pause dur="0.4"/> # <pause dur="0.2"/><kinesic desc="writes on board" iterated="y" dur="10"/> where X-I is the line number <pause dur="6.9"/> of <pause dur="0.2"/> A-I <pause dur="1.3"/> in other words <pause dur="0.3"/> when you call on <kinesic desc="indicates point on board" iterated="n"/> this rule <pause dur="0.3"/> all you do <pause dur="0.2"/> is write down the line numbers of all the premises <pause dur="0.5"/> and then <pause dur="0.2"/> you go straight to the conclusion <pause dur="1.3"/> so <pause dur="0.2"/>

it's a rule <pause dur="0.3"/> that's i mean this is rather a general statement you'll find a simpler statement in the workbook and in Lemon <pause dur="0.6"/> and <pause dur="0.5"/> i think we will learn it by example rather than trying to understand that <pause dur="1.0"/> mm <pause dur="3.4"/> so <pause dur="1.5"/> let us suppose <pause dur="0.4"/> that we've got <pause dur="0.4"/> we've now got the <kinesic desc="writes on board" iterated="y" dur="12"/> sequent P-vel-Q <pause dur="0.7"/> # therefore not <pause dur="0.5"/> if not-P and not-Q <pause dur="1.0"/> yes that's the one we proved last week <pause dur="0.4"/> so we'll call that <pause dur="1.6"/> diamond <pause dur="1.9"/> sorry we have to say here <pause dur="0.4"/> S-I this <pause dur="0.4"/> and then heart <pause dur="0.6"/><kinesic desc="writes on board" iterated="y" dur="1"/> and then say <pause dur="0.5"/> you then <pause dur="0.4"/> give the name of the sequential calling them <pause dur="2.2"/> so we'll call this one diamond <pause dur="0.8"/> and then the one we proved this morning <pause dur="0.3"/> which we will call # <pause dur="3.4"/><kinesic desc="writes on board" iterated="y" dur="14"/> club <pause dur="1.5"/> was <pause dur="9.0"/> was this <pause dur="0.8"/> mm <pause dur="4.2"/> diamond is what licenses the move from <kinesic desc="indicates point on board" iterated="n"/> here to here <pause dur="0.4"/> and <trunc>h</trunc> club is what licenses <kinesic desc="indicates point on board" iterated="n"/> the move from here to here <pause dur="0.6"/> and now we're going to turn the proof of <kinesic desc="indicates point on board" iterated="n"/> this sequent <pause dur="1.0"/> which i suppose we'd better call <kinesic desc="writes on board" iterated="y" dur="4"/> spade since since # where we've got to <pause dur="5.8"/> namely <pause dur="0.6"/><kinesic desc="writes on board" iterated="y" dur="4"/> P-vel-Q <pause dur="0.3"/> therefore if not-P then Q <pause dur="5.5"/> we're going to prove this sequent in three lines now <pause dur="0.7"/> mm <pause dur="1.0"/>

effectively <pause dur="0.2"/> we don't have to <pause dur="0.9"/> do very much here except for <pause dur="0.4"/> renumber things and <pause dur="0.9"/> ignore the gaps <pause dur="4.0"/><kinesic desc="writes on board" iterated="y" dur="3"/> line two of this new proof <pause dur="1.6"/> is going to <pause dur="0.7"/> be an application of sequent introduction to line one <pause dur="1.4"/> all right i've <trunc>pr</trunc> <pause dur="0.6"/> okay i've got <pause dur="0.7"/> i've got the premise of line one on a line <trunc>na</trunc> # sorry the premise of diamond on a line <pause dur="0.2"/> namely on line one <pause dur="0.6"/> i now can proceed immediately to the conclusion <pause dur="0.7"/> by <pause dur="0.2"/> saying <pause dur="0.3"/> one <pause dur="0.2"/><kinesic desc="writes on board" iterated="y" dur="1"/> sequent introduction <pause dur="3.2"/> diamond <pause dur="5.1"/><kinesic desc="writes on board" iterated="y" dur="2"/> and the <trunc>l</trunc> the line numbers are all the line numbers i need to get one and that's just one <pause dur="3.7"/> so what this rule says is <pause dur="2.7"/> in order to get from <kinesic desc="indicates point on board" iterated="n"/> here to <kinesic desc="indicates point on board" iterated="n"/> here <pause dur="1.5"/> i can do it via the sequent <pause dur="0.7"/> diamond <pause dur="0.5"/> all right if i wanted to <pause dur="0.2"/> i could fill in <kinesic desc="indicates point on board" iterated="n"/> <pause dur="0.2"/> those lines there <pause dur="0.4"/> there's nine lines in between <pause dur="0.3"/> and i would get a straightforward proof using the primary rules <pause dur="0.6"/> this is just a short cut rule it doesn't add any strength to the system it doesn't do anything new <pause dur="0.4"/> it just saves time and effort <pause dur="1.3"/> okay <pause dur="1.4"/> and then line three is done in the same way <pause dur="2.6"/><kinesic desc="writes on board" iterated="y" dur="2"/> still rests on one <pause dur="1.5"/> and now <pause dur="0.2"/> it's two <pause dur="0.9"/><kinesic desc="writes on board" iterated="y" dur="6"/> sequent introduction <pause dur="1.0"/> club <pause dur="6.2"/> # <pause dur="0.5"/> because it's

club now <pause dur="0.2"/> that licenses <pause dur="0.8"/> the move from it's not the case <pause dur="0.2"/> that not-P and not-Q <pause dur="0.4"/> to if not-P then Q <pause dur="3.0"/> # <pause dur="0.5"/> and there we have a proof of <pause dur="0.5"/> spade <pause dur="1.2"/> using <pause dur="0.3"/> # which is just three lines long <pause dur="0.7"/> though <pause dur="0.6"/> if you unpack it of course <pause dur="0.7"/> it's going to be whatever it was <pause dur="0.8"/> # eighteen lines long <pause dur="1.9"/> now <pause dur="0.4"/> you never need to use this rule <pause dur="1.6"/> say it's <pause dur="0.4"/> it's a it's just an additional rule <pause dur="0.2"/> that will save you time and effort <pause dur="1.7"/> and it's a very valuable rule for that <pause dur="4.5"/> <unclear>are there</unclear> any questions about <pause dur="0.5"/> whole thing <pause dur="2.2"/> well when i said there were various versions of this rule <pause dur="3.8"/> let's <trunc>ha</trunc> just mention one <pause dur="8.6"/> to start with <pause dur="1.9"/> the rule of <kinesic desc="writes on board" iterated="y" dur="11"/> theorem introduction <pause dur="5.4"/> which is <pause dur="0.5"/> indeed <pause dur="0.4"/> just a special case of this rule <pause dur="0.4"/> where the number of premises is zero <pause dur="0.6"/> a theorem you'll remember <pause dur="0.2"/> is a sequent with no premises <pause dur="1.4"/> and so <pause dur="0.7"/> since sequent introduction said if you've got all the premises on line on various lines then you can go to the conclusion <pause dur="0.4"/> theorem introduction says <pause dur="1.4"/> you just go to the conclusion <pause dur="0.5"/> so it just says you can introduce a theorem wherever you like <pause dur="1.0"/> mm <pause dur="1.9"/> simply introduce it

wherever you feel like it <pause dur="0.3"/> so <pause dur="0.2"/> you can just <trunc>a</trunc> <pause dur="0.3"/> on any line you like <pause dur="0.2"/> you can introduce for example <pause dur="0.6"/> the theorem <pause dur="0.3"/><kinesic desc="writes on board" iterated="y" dur="5"/> we that we proved last time <pause dur="0.3"/> it's not the case that P and not-P <pause dur="4.8"/> <trunc>o</trunc> <pause dur="0.9"/> you can just <pause dur="1.0"/> it's a <pause dur="0.5"/> <vocal desc="sigh" iterated="n"/><pause dur="1.1"/> in old-fashioned # # sense you might say it's a like an axiom it's just something that you're it's <pause dur="0.3"/> it's not <pause dur="0.2"/> part of the premises of the sequent # sequent you're being given but it's just something you're given <pause dur="0.7"/> because it's already been proved you can just use it whenever you like <pause dur="0.4"/> so let's have a very simple example <pause dur="1.2"/> # well perhaps it's not so very simple after all <pause dur="0.4"/> no <pause dur="0.3"/> let's we'll go go on a little bit and then we'll come back to a simple example using that <pause dur="4.6"/> <trunc>a</trunc> <pause dur="0.4"/> actually i can state something for example <pause dur="0.2"/><kinesic desc="writes on board" iterated="y" dur="7"/> sort of thing i ask you to prove <pause dur="6.7"/> that sequent <pause dur="3.8"/> it's not the case that <pause dur="0.3"/> not-P <pause dur="0.4"/> and not-not-P <pause dur="3.4"/> now <pause dur="0.9"/> if you understand what a substitution for a <pause dur="0.2"/> instance of a sequent is <pause dur="1.2"/> you will see that <kinesic desc="indicates point on board" iterated="n"/> this <pause dur="0.3"/> is really the same sequent as <kinesic desc="indicates point on board" iterated="n"/> this <pause dur="0.5"/> with <pause dur="0.3"/> not-P <pause dur="0.2"/> replacing P throughout <pause dur="0.6"/> # <pause dur="0.4"/> all right <pause dur="0.8"/> that if i <pause dur="0.4"/> if i take <pause dur="0.4"/><kinesic desc="writes on board" iterated="y" dur="2"/> P <pause dur="0.3"/> # wherever it occurs <pause dur="0.2"/> and replace it by

not-P <pause dur="0.4"/> then i'm just going to get this <kinesic desc="indicates point on board" iterated="n"/> <pause dur="0.4"/> and you can <pause dur="0.5"/> it's the sort of thing that wordprocessors <pause dur="0.4"/> expected to be able to do <pause dur="0.5"/> very quickly to <pause dur="0.4"/> do replacements of this sort <pause dur="0.2"/> okay <pause dur="1.5"/> therefore <pause dur="0.4"/> any proof of <kinesic desc="indicates point on board" iterated="n"/> this <pause dur="0.8"/><kinesic desc="indicates point on board" iterated="n"/> is really <trunc>a</trunc> <trunc>a</trunc> also a proof of this <pause dur="1.1"/> because you would just go through the proof <pause dur="0.3"/> changing <pause dur="0.5"/> P to not-P throughout and it wouldn't make any difference <pause dur="1.1"/> in other words if i've proved <kinesic desc="indicates point on board" iterated="n"/> this i've really proved <kinesic desc="indicates point on board" iterated="n"/> this already <pause dur="1.8"/> all right <pause dur="1.4"/> i mean i've done all the work that's needed <pause dur="0.4"/> to prove <kinesic desc="indicates point on board" iterated="n"/> this if i've proved <kinesic desc="indicates point on board" iterated="n"/> this <pause dur="1.6"/> so <pause dur="0.3"/> this gives us <pause dur="0.5"/> actually a a variant of the rule of theorem <kinesic desc="writes on board" iterated="y" dur="16"/> introduction <pause dur="0.2"/> that we can look at now <pause dur="0.3"/> theorem introduction <pause dur="2.7"/> substitution <pause dur="6.5"/> which is <pause dur="0.3"/> T-I-<pause dur="0.7"/>S <pause dur="2.8"/> rather ugly notation <pause dur="2.5"/> what this rule says if you've got a theorem <pause dur="0.9"/> then you can introduce on to a line not any line not just that theorem <pause dur="0.6"/> but any substitutions and <unclear>swap it</unclear> <pause dur="1.3"/> yes <pause dur="1.5"/> so <pause dur="0.2"/> here's a one line proof <pause dur="0.4"/> of this <kinesic desc="indicates point on board" iterated="n"/> <pause dur="3.3"/> of <pause dur="0.3"/> this <trunc>s</trunc> this theorem <pause dur="5.0"/> let's call what shall we call this <pause dur="2.2"/><kinesic desc="writes on board" iterated="y" dur="2"/> dollar <pause dur="0.5"/> mm <pause dur="1.3"/> so <kinesic desc="indicates point on board" iterated="n"/> that's the thing that we've proved

last time <pause dur="0.5"/> and so i now ask you to prove <pause dur="0.5"/><kinesic desc="writes on board" iterated="y" dur="18"/> it's not the case that not-P and <pause dur="0.3"/> not-not-P <pause dur="0.3"/> and you prove it in one line as follows <pause dur="4.9"/> theorem <pause dur="0.9"/> introduction <pause dur="0.3"/> substitution <pause dur="0.6"/> dollar <pause dur="1.9"/> in other words you <pause dur="0.4"/> you # as you if you'd like to use these this jargon <pause dur="0.2"/> you justify <pause dur="0.8"/> how you got there by saying that i obtained it <pause dur="0.2"/> from a theorem that i've already proved <pause dur="1.3"/> by substitution the theorem i've already proved is called <pause dur="0.2"/> i've just <pause dur="0.4"/> ad hoc called it dollar <pause dur="0.6"/> and the substitution is <pause dur="0.2"/> the result of replacing <pause dur="1.3"/> P by not-P <pause dur="0.9"/> since it's a theorem <pause dur="0.3"/><kinesic desc="writes on board" iterated="y" dur="1"/> it rests on nothing at all <pause dur="1.3"/> and so we just put that over there <pause dur="6.1"/> so not only theorems <pause dur="0.2"/> can be introduced wherever you like <pause dur="0.2"/> but also <pause dur="0.6"/> any substitution instance of a theorem of course a substitution instance of a theorem is itself a theorem <pause dur="0.8"/> mm but you may not have proved it <pause dur="0.7"/> the thing is that <pause dur="0.4"/> you can't just introduce anything you like <pause dur="0.3"/> all the time in a sense the requirement is that you've already proved it <pause dur="0.8"/> and <pause dur="0.3"/> in an

examination <pause dur="0.2"/> typically for example <pause dur="0.3"/> you <pause dur="0.2"/> might be told that you may use in a question <pause dur="1.0"/> any sequent or theorem that you've already proved <pause dur="0.6"/> mm <pause dur="0.6"/> if you were allowed to introduce any theorem then of course <pause dur="0.4"/> everything can be reduced to one line <pause dur="1.3"/> and that would be too easy # <pause dur="3.4"/> so let's have a <pause dur="0.3"/> there's also of course i <trunc>e</trunc> i expect you can guess there's also <pause dur="0.8"/><kinesic desc="writes on board" iterated="y" dur="6"/> a sequent introduction substitution <pause dur="0.7"/> S-I-S <pause dur="1.9"/> that is also sometimes useful <pause dur="0.5"/> and let's see how we might <pause dur="1.1"/> # <pause dur="1.5"/> use that <pause dur="5.2"/> for example to prove the following <pause dur="0.4"/><kinesic desc="writes on board" iterated="y" dur="2"/> sequent <pause dur="0.4"/> we'll call pound <pause dur="0.2"/> sterling <pause dur="10.7"/> <kinesic desc="writes on board" iterated="y" dur="6"/> i want to prove <pause dur="1.6"/> a sequent that is rather like <pause dur="0.6"/> spade <pause dur="0.8"/> but is rather unlike it too <pause dur="1.1"/> mm <pause dur="0.5"/><kinesic desc="indicates point on board" iterated="n"/> this one has a disjunction <pause dur="0.7"/> and from it you prove a conditional whose antecedent is the negation of the left disjunct <pause dur="0.8"/> and <kinesic desc="indicates point on board" iterated="n"/> this one also has a disjunction as a premise <pause dur="0.4"/> but <kinesic desc="indicates point on board" iterated="n"/> here you prove a conditional <pause dur="0.2"/> whose antecedent's negation <pause dur="0.2"/> is the left disjunct <pause dur="1.8"/> mm <pause dur="1.2"/> a proof of <trunc>thi</trunc> <pause dur="0.2"/><kinesic desc="indicates point on board" iterated="n"/> this is not <pause dur="0.7"/> pound i hope is clear is not a substitution instance of spade <pause dur="1.1"/> right <pause dur="2.2"/> you can't <pause dur="0.3"/> go through spade <pause dur="0.3"/> replacing <pause dur="0.2"/> Ps and Qs <pause dur="0.2"/> uniformly by

anything <pause dur="0.2"/> and end up <pause dur="0.4"/> with <pause dur="0.7"/> with pound <pause dur="0.7"/> you could of course replace P <pause dur="0.2"/> by not-P throughout spade <pause dur="0.2"/> but this would give you <pause dur="0.4"/><kinesic desc="indicates point on board" iterated="n"/> not-not-P here <pause dur="0.7"/> and not just P <pause dur="0.6"/> mm <pause dur="0.3"/> so it's not a substitution instance <pause dur="0.2"/> so <pause dur="0.5"/> we can't <pause dur="0.2"/> just call on one of these <pause dur="0.2"/> short cut rules to prove it we've got to do some work <pause dur="1.7"/> and i hope <pause dur="0.5"/> that <pause dur="0.4"/> we'll find that we can do <trunc>s</trunc> we can <pause dur="0.2"/> do it satisfactorily <pause dur="5.6"/> we are going to call on a short cut rule <pause dur="0.7"/> but <pause dur="0.7"/> not too much <pause dur="0.9"/> so <pause dur="0.7"/> pound is <kinesic desc="writes on board" iterated="y" dur="6"/> not-P <pause dur="0.2"/> or Q these names by the way are just for <pause dur="0.6"/> for today don't <pause dur="0.3"/> take them seriously the only <pause dur="0.3"/> two names that i will continue to use <pause dur="0.8"/> and not only now but in the <trunc>examinati</trunc> in the may may use in the examination # i shall tell you what they mean if i do use them there <pause dur="0.2"/> are star and dagger <pause dur="0.9"/> mm <pause dur="0.2"/> well <pause dur="0.3"/> there's one other <pause dur="0.5"/> # theorem that we're going to prove i hope before the end of the hour <pause dur="1.2"/> but <pause dur="0.4"/> all these other things <pause dur="0.2"/> <trunc>go</trunc> <pause dur="0.6"/> # spades and # hearts and dollars and so on are just ad hoc names <pause dur="1.7"/><kinesic desc="writes on board" iterated="y" dur="11"/> anybody like to suggest how we might prove this <pause dur="5.8"/> any ideas <pause dur="13.2"/> don't <pause dur="1.1"/> do <trunc>y</trunc> <pause dur="0.7"/> do too much work <pause dur="0.3"/> that's my <pause dur="0.2"/> advice here <pause dur="0.4"/> how

can you <pause dur="0.4"/> do this as quickly as possible <pause dur="1.2"/> or <pause dur="0.4"/> as slickly as possible <pause dur="1.9"/> any suggestions <pause dur="2.8"/> using of course the short cut rules if necessary <pause dur="4.2"/> yeah <pause dur="0.8"/> okay well there let me show you how you can do it <pause dur="0.9"/> and <pause dur="0.4"/> you'll kick yourselves <pause dur="0.8"/> mm <pause dur="5.5"/><kinesic desc="writes on board" iterated="y" dur="1"/> not-P vel Q <pause dur="1.4"/> okay <pause dur="0.3"/> on line <pause dur="0.2"/><kinesic desc="writes on board" iterated="y" dur="1"/> resting on line one <pause dur="0.5"/> i'm now going to go to <pause dur="3.3"/><kinesic desc="writes on board" iterated="y" dur="2"/> if not-not-P then Q <pause dur="2.0"/> and that is going to be <pause dur="0.2"/><kinesic desc="writes on board" iterated="y" dur="8"/> one sequent introduction <pause dur="0.2"/> substitution <pause dur="0.9"/> spade <pause dur="5.4"/> it's what i get <pause dur="0.6"/> from <pause dur="0.2"/> 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 <pause dur="1.0"/> but nonetheless is # <pause dur="0.6"/> # <pause dur="0.5"/> i think it's a straightforward idea <pause dur="0.2"/> that <pause dur="0.6"/> if you have a proof <pause dur="0.3"/> as we have of spade <pause dur="1.2"/> and as we've already done that <pause dur="0.3"/> then <pause dur="0.2"/> you could just run through the proof replacing P in every <trunc>pla</trunc> place it occurs by not-P <pause dur="0.2"/> and you would get a proof <kinesic desc="indicates point on board" iterated="n"/> of this <pause dur="0.6"/> yes <pause dur="1.0"/> that's that's i hope that this is obvious # <pause dur="0.5"/> just by replacing it by <trunc>s</trunc> you could replace it by <pause dur="0.3"/> the rain in Spain <trunc>s</trunc> stays mainly in the plane throughout and you'd still have a valid proof <pause dur="1.0"/>

be <trunc>t</trunc> <pause dur="0.4"/> tiresomely long and would look a bit odd with the combination of words and symbols but it would still be valid <pause dur="0.9"/> you could replace it by <pause dur="0.6"/> the whole of the <pause dur="1.2"/> # Declaration of <trunc>inde</trunc> well perhaps Declaration of Independence contains imperatives <pause dur="0.9"/> the whole of some <pause dur="0.2"/> some <pause dur="0.3"/> text in the indicative mood <pause dur="0.7"/> <trunc>w</trunc> <pause dur="0.2"/> be the same <pause dur="0.7"/> so <pause dur="0.5"/> the the the proof goes through like that <pause dur="0.6"/> now what have we got to prove <pause dur="0.2"/> we've got to prove P arrow Q <pause dur="1.6"/><kinesic desc="writes on board" iterated="y" dur="2"/> so i assume P <pause dur="1.3"/> for conditional proof <pause dur="0.6"/> that's how i prove conditionals the only way i know <kinesic desc="writes on board" iterated="y" dur="1"/> how to prove conditionals <pause dur="0.7"/> except trivial ones <pause dur="1.2"/> # <pause dur="0.9"/> so i assume P <pause dur="0.2"/><kinesic desc="writes on board" iterated="y" dur="1"/> can you now see what i'm going to do <pause dur="2.2"/> yes <pause dur="1.3"/> now clear is this not <pause dur="0.7"/> that <pause dur="0.4"/> i'm trying to get Q after all <pause dur="0.4"/> because that's the consequent of the conditional <pause dur="0.3"/> i've assumed P <pause dur="0.9"/><kinesic desc="indicates point on board" iterated="n"/> can i use these two to get Q <pause dur="0.2"/> surely i can <pause dur="0.3"/> yes because in order to use <kinesic desc="indicates point on board" iterated="n"/> this one <pause dur="0.9"/> this is # conditional <pause dur="0.2"/> i would expect to use modus ponens <pause dur="0.2"/> that means i want to get the antecedent <pause dur="0.2"/> the antecedent is not-not-P that's a double negation <pause dur="0.2"/> how do i get a double negation <pause dur="0.9"/>

by taking getting the sentence of which it is the double negation that's P <pause dur="0.3"/> have i how do i get P <pause dur="1.7"/> <vocal desc="click" iterated="n"/><kinesic desc="gestures stop with hands" iterated="n"/> <pause dur="0.7"/> all done <pause dur="0.3"/> yes <pause dur="2.3"/><kinesic desc="writes on board" iterated="y" dur="10"/> in other words <pause dur="0.8"/> from P <pause dur="0.2"/> i can go to not-not-P <pause dur="1.5"/> by <pause dur="1.0"/> three D-N <pause dur="10.4"/> and now i've got the antecedent of line two <pause dur="2.1"/><kinesic desc="writes on board" iterated="y" dur="3"/> and therefore from one and three to one and three i can imply modus ponens <pause dur="0.6"/> gives me not-not-P <pause dur="0.3"/> and if not-not-P then Q <kinesic desc="writes on board" iterated="y" dur="1"/><pause dur="0.5"/> that gives me Q <pause dur="2.7"/> what did i say <kinesic desc="writes on board" iterated="y" dur="3"/> two four modus ponens <pause dur="2.6"/> resting on lines one and three <pause dur="3.4"/> that's what i wanted <kinesic desc="indicates point on board" iterated="n"/> that's the consequent of the conditional i'm # trying to prove <pause dur="0.3"/> it rests on <pause dur="0.3"/> line three <pause dur="0.2"/> which is the antecedent of the conditional i <pause dur="0.2"/> want to prove <pause dur="0.4"/> and therefore <pause dur="0.2"/> conditional proof <kinesic desc="writes on board" iterated="y" dur="4"/><pause dur="1.0"/> that allows me to prove <pause dur="0.4"/> if P then Q <pause dur="2.2"/> three <pause dur="0.5"/><kinesic desc="writes on board" iterated="y" dur="3"/> <trunc>bec</trunc> which is antecedent five which is the consequent <pause dur="0.5"/> C-P <pause dur="3.7"/> mm <pause dur="3.0"/> and therefore <pause dur="0.4"/> from <pause dur="0.2"/> not-P or Q i've proved <pause dur="0.2"/> if P then Q <pause dur="0.8"/> now <pause dur="2.5"/> the advantage of these sequent introduction <pause dur="1.3"/> rules and theorem introduction rules is that they enable you to break <pause dur="0.3"/> the job down into small parts that you can tackle <pause dur="0.5"/> i gave the

analogy <pause dur="0.3"/> last time of making a long journey <pause dur="0.6"/> i don't know you're driving to <vocal desc="sigh" iterated="n"/> Budapest <pause dur="0.4"/> mm <pause dur="0.8"/> you you're not going to do that <pause dur="1.2"/> # in one day you're going to have to stop one <trunc>si</trunc> without stopping <pause dur="0.8"/> so you break the journey down into manageable bits that you can see <pause dur="0.2"/> how you're going to do it <pause dur="0.4"/> mm <pause dur="3.2"/> Coventry to <pause dur="0.6"/> i don't know <pause dur="1.4"/> Dover <pause dur="1.0"/> Dover to <pause dur="0.4"/> to <trunc>o</trunc> <pause dur="0.9"/> Ostend <pause dur="0.5"/> Ostend to <pause dur="0.6"/> Cologne or whatever i don't know what <trunc>rou</trunc> what the route would be <pause dur="0.2"/> mm <pause dur="0.5"/> and <pause dur="0.2"/> then you can see how to do it so typically when you've got a <trunc>g</trunc> more complicated proof what you do is try and break it down into little bits <pause dur="0.4"/> each of which you can see how to do <pause dur="0.2"/> and then you can put them altogether by sequent introduction if you want to <pause dur="0.6"/> though <pause dur="0.3"/> sometimes it's just as easy to write the proof out <pause dur="0.3"/> but sequent introduction is very helpful <pause dur="0.2"/> when you've got <pause dur="0.6"/> some rather long <pause dur="0.3"/> modules already <pause dur="2.2"/> any questions about this <pause dur="0.4"/> this rule and how it works <pause dur="1.6"/> there are some exercises this week for you to try <pause dur="0.7"/> involving this rule <pause dur="0.8"/> one of which <pause dur="0.6"/> it's just slightly puzzling <pause dur="2.3"/> mm <pause dur="0.8"/> just slightly puzzling i don't know why

it's slightly puzzling but somehow it always <pause dur="0.4"/> it always # <pause dur="0.5"/> # leaves people wondering whether that can be right and yes it it is all right <pause dur="0.8"/> any questions there <pause dur="1.7"/> no <pause dur="0.9"/> everybody can do that </u><pause dur="0.8"/> <u who="sm0932" trans="pause"> sequent introduction i'm not happy with it </u><pause dur="0.4"/> <u who="nm0930" trans="pause"> you're not happy with it </u><u who="sm0932" trans="latching"> no i'm not </u><u who="nm0930" trans="latching"> <trunc>w</trunc> </u><u who="sm0932" trans="overlap"> why is it not-not-P when you use S-I-S </u><pause dur="0.7"/> <u who="nm0930" trans="pause"> # because <pause dur="0.4"/> if i take <pause dur="0.3"/> this sequent <kinesic desc="indicates point on board" iterated="n"/> <pause dur="0.3"/> which i'm given yes <pause dur="0.9"/> and everywhere <pause dur="0.2"/> replace P <pause dur="0.3"/> by not-P <pause dur="0.3"/> sorry i shouldn't have <trunc>ri</trunc> rubbed out that <pause dur="0.6"/><kinesic desc="writes on board" iterated="y" dur="5"/> everywhere replace P by not-P <pause dur="2.3"/> then i get this </u><pause dur="0.5"/> <u who="sm0932" trans="pause"> right </u><pause dur="0.3"/> <u who="nm0930" trans="pause"> yes <pause dur="0.6"/> it's a <pause dur="0.3"/> it's a substitution instance <pause dur="0.2"/> of <pause dur="0.6"/> perhaps i could have done that in <pause dur="0.4"/> in # <pause dur="0.3"/> in different colours <pause dur="5.7"/><kinesic desc="writes on board" iterated="y" dur="3"/> what's in pink there <pause dur="1.4"/> # <pause dur="1.0"/> is simply a <trunc>re</trunc> way of replacing uniformly what was in green before and then with a P <pause dur="0.3"/> mm <pause dur="0.2"/> so this is just a substitution instance and <pause dur="0.4"/> proofs <pause dur="0.3"/> of substitutions instances follow the <trunc>s</trunc> exactly the same pattern as the proof of the original i mean <pause dur="0.4"/> if <trunc>th</trunc> you're not persuaded by that <pause dur="0.2"/> just write out <pause dur="1.3"/> a proof <pause dur="0.6"/> some proof of say half a dozen lines and then take a substitution

instance and write out the proof <pause dur="0.3"/> of the substitution instance and and <pause dur="0.3"/> about halfway through you'll say <pause dur="0.2"/> why am i doing this <pause dur="0.7"/> mm <pause dur="0.4"/> what's the point of doing this again <pause dur="0.2"/> it's obviously the same proof <pause dur="0.5"/> # <pause dur="0.9"/> sometimes it's <pause dur="0.5"/> it's actually existentional <pause dur="0.5"/> absorption into the task does convince you in a way that no amount of theory would <pause dur="0.4"/> mm <pause dur="0.5"/> yes </u><pause dur="0.3"/> <u who="sm0933" trans="pause"> can you substitute it with anything </u><pause dur="0.5"/> <u who="nm0930" trans="pause"> you can <trunc>substi</trunc> <pause dur="0.2"/> provided you substitute uniformly for letters </u><pause dur="0.8"/> <u who="sm0933" trans="pause"> could you put Q </u><pause dur="0.4"/> <u who="nm0930" trans="pause"> yes you could put Q <pause dur="0.3"/> yes <pause dur="0.3"/> indeed you could <pause dur="2.6"/> if you put <pause dur="0.2"/> if you put let's choose another colour <pause dur="0.4"/> if you put Q <pause dur="0.5"/> shall we <pause dur="0.2"/> shall we go back to the <pause dur="0.6"/> the the original version <pause dur="4.2"/><kinesic desc="writes on board" iterated="y" dur="4"/> i can replace P by Q that would give me <pause dur="1.1"/><kinesic desc="writes on board" iterated="y" dur="5"/> Q-vel-Q <pause dur="0.3"/> therefore <pause dur="0.6"/> if not-Q then Q <pause dur="2.9"/> yes <pause dur="2.3"/> and indeed <pause dur="0.4"/><kinesic desc="indicates point on board" iterated="n"/> that <pause dur="0.3"/> is a sequent that <pause dur="0.3"/> in effect we have now proved because we've proved spade <pause dur="0.4"/> and <kinesic desc="indicates point on board" iterated="n"/> this is a substitution instance <gap reason="inaudible" extent="1 sec"/> <pause dur="2.8"/> mm <pause dur="0.4"/> or we could have replaced it by not-Q <pause dur="2.1"/> and then <pause dur="0.9"/> or rather we # let well we could replace Q by not-P <kinesic desc="indicates point on board" iterated="n"/> here and that would <kinesic desc="writes on board" iterated="y" dur="7"/> give us <pause dur="0.4"/> P vel not-P <pause dur="0.9"/> therefore <pause dur="0.4"/> if not-P <pause dur="0.2"/> then not-P <pause dur="3.9"/> well <pause dur="0.4"/> that is perhaps is not a very interesting sequent because <kinesic desc="indicates point on board" iterated="n"/> that

conclusion <pause dur="0.6"/> is itself <pause dur="0.2"/> provable <pause dur="2.1"/> nonetheless <pause dur="0.2"/> all these <trunc>se</trunc> these substitutions are possible <pause dur="0.5"/> the two things i stress i <trunc>str</trunc> i stress again <pause dur="0.2"/> first of all it must be uniform <pause dur="0.8"/> yes you must replace every occurrence <pause dur="0.5"/> by the same thing and secondly you can only <pause dur="0.3"/> substitute for letters <pause dur="1.3"/> you can't <trunc>s</trunc> <pause dur="0.3"/> i mean <pause dur="0.2"/> <trunc>i</trunc> if <pause dur="1.2"/> in <kinesic desc="indicates point on board" iterated="n"/> this formula i can't replace not-Q by P <pause dur="1.9"/> that wouldn't be a substitution instance <pause dur="1.9"/> i can only replace Q <pause dur="1.0"/> or any other letter by a formula but not <pause dur="0.5"/> # but not # <pause dur="0.6"/> # a compound formula <pause dur="1.3"/> because <pause dur="0.7"/><kinesic desc="indicates point on board" iterated="n"/> this formula has to be something that is a conditional <pause dur="0.6"/> whose antecedent is a negation <pause dur="0.3"/> if i were <kinesic desc="writes on board" iterated="y" dur="1"/> allowed to replace this well let's say by R <pause dur="1.1"/> i would have now <pause dur="0.4"/> gone to a case that wasn't necessarily a negation <pause dur="0.8"/> so i would have <trunc>e</trunc> <pause dur="0.2"/> actually <pause dur="0.3"/> gone to something more general <pause dur="0.3"/> rather than to something more specific which is what substitution is <pause dur="1.0"/> okay <pause dur="1.4"/> it's the same <pause dur="0.2"/> exactly the same in algebra <pause dur="2.4"/> it's exactly the same <pause dur="0.5"/> thing that if you have an algebraic formula <pause dur="1.8"/><kinesic desc="writes on board" iterated="y" dur="7"/> X-plus-Y-all-squared <pause dur="0.3"/> equals X-squared <pause dur="0.4"/> plus two-X-Y <pause dur="0.7"/> plus Y-squared <pause dur="0.4"/>

you can replace X and Y <pause dur="0.5"/> by anything you like <pause dur="1.3"/> yes <pause dur="0.2"/> for example you can replace them both by <pause dur="1.4"/> zero or <pause dur="0.4"/> both by <pause dur="0.4"/> minus-one or <pause dur="1.0"/> both by X or both by Z <pause dur="2.8"/> right well i think we've got <pause dur="0.3"/> since we we came across this <pause dur="2.1"/><kinesic desc="indicates point on board" iterated="n"/> formula here <pause dur="2.5"/><kinesic desc="writes on board" iterated="y" dur="1"/> i think <pause dur="1.0"/> it's now time to prove <pause dur="0.5"/> this <pause dur="0.5"/> formula as a theorem <pause dur="0.7"/> mm <pause dur="0.3"/> <kinesic desc="indicates point on board" iterated="n"/> this one is a theorem and in fact <kinesic desc="indicates point on board" iterated="n"/> this <trunc>se</trunc> this <pause dur="0.2"/> implication this # <pause dur="0.6"/> # derivation goes in the other direction <pause dur="1.0"/> but <pause dur="1.5"/> rather than try to do all that i'll just <pause dur="0.4"/> <trunc>con</trunc> <pause dur="0.4"/> finish with the proof <pause dur="0.6"/> of <pause dur="0.4"/> P or not-P <pause dur="0.2"/> because <pause dur="1.0"/> P or not-P <pause dur="0.4"/> is a it's a <pause dur="0.3"/> it's a characteristic of a type of proof <pause dur="0.5"/> that is <pause dur="0.4"/> has the <pause dur="0.4"/> reaches the level of sophistication that i think is <pause dur="0.7"/> essential to <pause dur="0.6"/> succeed in this course <pause dur="0.6"/> you do you understand how to do this <pause dur="0.2"/> there are more difficult proofs <pause dur="0.2"/> there's no question <pause dur="0.3"/> but <pause dur="0.4"/> this is the the <trunc>s</trunc> the sort of level i would say if you <trunc>n</trunc> if you know and understand how to do proofs like this <pause dur="0.7"/> then you've <pause dur="0.3"/> you got the idea <pause dur="0.3"/> mm <pause dur="0.7"/> okay <pause dur="1.2"/> P or not-P <pause dur="0.2"/> is called <pause dur="2.3"/><kinesic desc="writes on board" iterated="y" dur="20"/> the law of excluded middle <pause dur="3.8"/> and that's a <pause dur="0.6"/> that's of course a <pause dur="0.5"/> an old name <pause dur="0.4"/> it's also the its medieval Latin name <pause dur="1.1"/> <distinct lang="la">tertium</distinct> <pause dur="0.5"/> <distinct lang="la">non</distinct> <pause dur="0.8"/> <distinct lang="la">datur</distinct> <pause dur="3.6"/> it means the third is not given <pause dur="2.4"/> so it's an anti-Blairite <pause dur="0.9"/>

# type # type of # <vocal desc="laugh" iterated="n"/><pause dur="0.3"/> of theorem it says <pause dur="0.2"/> either P <trunc>no</trunc> or not-P but <pause dur="0.4"/> no third possibility <pause dur="0.6"/> yes <pause dur="1.8"/> there's nothing additional to P and its negation <pause dur="2.2"/> yes <pause dur="0.2"/> and it's <pause dur="0.3"/> it was regarded along with the law of non-contradiction which i mentioned last time <pause dur="0.2"/> which may even still be on the board somewhere <pause dur="0.5"/> well <pause dur="0.2"/> yes <kinesic desc="indicates point on board" iterated="n"/> here <pause dur="0.4"/> yes <pause dur="0.9"/> and the law of identity as it was sometimes called if P then P <pause dur="0.3"/> these were regarded as <pause dur="0.2"/> the fundamental laws of logic this was in a <trunc>b</trunc> <trunc>b</trunc> before logic was properly developed but nonetheless <pause dur="0.3"/> they do contain a lot of the important <pause dur="0.3"/> facts about it <pause dur="0.9"/> and the question is <pause dur="0.7"/><kinesic desc="writes on board" iterated="y" dur="3"/> how are we going to prove this theorem <pause dur="3.0"/> you can see i've got six minutes to do this in <pause dur="0.6"/> so <pause dur="0.6"/> i'd better get my skates on here <pause dur="3.6"/> right what do you do when you've got to prove a sequent <pause dur="0.7"/> you first of all <pause dur="0.3"/> write down what you're given <pause dur="2.2"/> that's all right done that <pause dur="2.1"/> then look at what we've got to prove <pause dur="1.7"/> what sort of a sentence have we got to prove <pause dur="1.0"/> a disjunction <pause dur="0.3"/> how do you prove a disjunction <pause dur="1.2"/> well the rule that allows you to prove a disjunction is vel introduction <pause dur="0.3"/> how do you

prove <pause dur="0.3"/> how do you use vel introduction <pause dur="0.2"/> you've got to get one of the disjuncts first <pause dur="0.8"/> can we get P <pause dur="0.4"/> or not-P <pause dur="1.5"/> well <pause dur="1.5"/> obviously not very straightforwardly <pause dur="1.0"/> mm i can't i mean i just get P out of nowhere <pause dur="0.8"/> if i could prove P from nothing at all <pause dur="0.5"/> then that would be logic over <pause dur="0.8"/> mm <pause dur="0.6"/> you can prove everything <pause dur="0.7"/> from nothing at all and we could all go home and forget about it <pause dur="0.5"/> mm <pause dur="2.1"/> fortunately for us <pause dur="0.7"/> it's not as easy as that <pause dur="0.8"/> mm <pause dur="0.6"/> so <pause dur="0.4"/> what do we do <pause dur="1.0"/> we can't look at our premises and <pause dur="0.2"/> get some clues from them because there aren't any premises <pause dur="2.4"/> the conclusion doesn't <pause dur="0.2"/> isn't at all helpful it just tells us to prove a disjunction even though actually we can't prove either of the disjuncts <pause dur="2.1"/> well <pause dur="0.5"/> what do i say you should do when you there's nothing else to do <pause dur="1.5"/> <distinct lang="la">reductio ad absurdum</distinct> you've just got to <pause dur="0.4"/> somehow <pause dur="0.3"/> go for a contradiction <pause dur="0.9"/> so <pause dur="0.2"/> this is how this this proof goes <pause dur="1.0"/> # <pause dur="0.2"/><kinesic desc="writes on board" iterated="y" dur="10"/> i think there's room on this board <pause dur="0.3"/> line one <pause dur="0.3"/> we assume <pause dur="0.2"/> it's not the case that P or not-P <pause dur="1.9"/> and this is an assumption <pause dur="0.3"/> that <pause dur="0.3"/> well the only way we know how to get rid of it is by R-A-A <pause dur="1.2"/> we're not quite

sure how we're going to do that yet <pause dur="0.3"/> but that's the the beauty of R-A-A you can as it were <pause dur="0.2"/> set out on that journey <pause dur="0.3"/> without having a very any <pause dur="0.2"/> very clear idea about how you're going to get to the terminus <pause dur="0.7"/> mm <pause dur="1.9"/> well <pause dur="0.2"/> now what sort of a sentence have we got on line one <pause dur="1.3"/> what i called earlier today a compound negation <pause dur="1.0"/> what do what was my advice in this when you've got a compound negation <pause dur="0.6"/> try <pause dur="0.3"/> to construct <pause dur="0.6"/> the formula <pause dur="0.3"/> in the insides <pause dur="0.9"/> that's P or not-P <pause dur="0.6"/> how do i construct a disjunction <pause dur="1.9"/> by getting one of the disjuncts <pause dur="0.2"/> we seem to have gone round in a circle <pause dur="0.6"/> but not quite because <pause dur="0.6"/> if i try to construct <kinesic desc="indicates point on board" iterated="n"/> this <pause dur="0.3"/> there's no reason why i shouldn't <kinesic desc="writes on board" iterated="y" dur="9"/> just assume P <pause dur="4.4"/> this is also an assumption for R-A-A <pause dur="1.5"/> see that's the other beauty of R-A-A that you can make all these assumptions <pause dur="0.7"/> and <pause dur="1.3"/> as long as you get a contradiction you can start knocking them down again <pause dur="1.1"/> so <pause dur="0.2"/> here <pause dur="0.6"/> i've got an assumption P <pause dur="3.4"/><kinesic desc="writes on board" iterated="y" dur="10"/> now i can construct the sentence <pause dur="0.3"/> that is denied on line one <pause dur="1.2"/> by vel introduction <pause dur="3.6"/> P vel not-P <pause dur="3.0"/><kinesic desc="writes on board" iterated="y" dur="10"/> so <pause dur="0.2"/> lines one and three contradict each

other and so from lines one and two i've <pause dur="0.2"/> i have P vel not-P <pause dur="0.8"/> and it's not the case that P vel not-P mind your parentheses <pause dur="1.9"/> mm <pause dur="1.4"/> make sure you understand what you're writing down get the parentheses right <pause dur="1.0"/> so that's one and three and introduction <pause dur="3.7"/><kinesic desc="writes on board" iterated="y" dur="2"/> that's a contradiction <pause dur="3.1"/> i can deny therefore either one or two <pause dur="1.1"/> now <pause dur="0.5"/> if you think about it <pause dur="0.4"/> it's pointless to deny one at this stage <pause dur="1.7"/> mm you would actually find you'd got back where you <trunc>s</trunc> in effect to where you started <pause dur="0.5"/> but we can deny two at this stage <pause dur="0.9"/> <unclear>this</unclear> you can change your colour to show how important it is <pause dur="0.5"/><kinesic desc="writes on board" iterated="y" dur="10"/> and resting on one <pause dur="0.2"/> we now get <pause dur="0.2"/> not-P <pause dur="2.2"/> # two four R-A-A <pause dur="6.5"/> now <pause dur="0.8"/> we've made a tremendous advance here <pause dur="0.3"/> at <kinesic desc="indicates point on board" iterated="n"/> this stage we had one of the disjuncts of what we're trying to prove <pause dur="0.2"/> assumed <pause dur="0.7"/> we had to assume it <pause dur="0.5"/> but at <kinesic desc="indicates point on board" iterated="n"/> this stage <pause dur="0.2"/> we've proved it from <pause dur="0.2"/> from one <pause dur="1.1"/> that's <trunc>mu</trunc> that's much less commitment on our part <pause dur="0.8"/> and we can now repeat this <kinesic desc="writes on board" iterated="y" dur="10"/> process <pause dur="0.6"/> exactly the same way <pause dur="0.4"/> we now <pause dur="0.2"/> introduce not-P on # P on the left i'm sorry <pause dur="0.3"/> five vel introduction <pause dur="1.5"/> so that gives us <pause dur="0.5"/> and now we can <pause dur="0.4"/> do another <distinct lang="la">reductio ad absurdum</distinct> <pause dur="1.7"/><kinesic desc="writes on board" iterated="y" dur="9"/> resting on one <pause dur="0.3"/> we get P or not-P <pause dur="0.8"/> and it's not the case

that P or not-P <pause dur="2.0"/> all right <kinesic desc="indicates point on board" iterated="n"/> that's a conjunction <pause dur="0.3"/> of one <pause dur="0.3"/> and six <pause dur="6.1"/><kinesic desc="writes on board" iterated="y" dur="2"/> another contradiction <pause dur="0.6"/> now we can <pause dur="0.3"/> there's only one thing we can deny now <pause dur="0.4"/> and that's one itself <pause dur="0.6"/> and so <pause dur="3.2"/><kinesic desc="writes on board" iterated="y" dur="2"/> we can <pause dur="0.4"/> eliminate <pause dur="0.5"/> the function one <pause dur="0.7"/> by denying it <pause dur="0.4"/> now it's <kinesic desc="writes on board" iterated="y" dur="3"/> very important here that you remember that <pause dur="0.4"/> you must write <pause dur="0.3"/> not-not-P or not-P <pause dur="2.0"/> # <pause dur="1.4"/> one seven <kinesic desc="writes on board" iterated="y" dur="3"/> R-A-A <pause dur="2.0"/> and then on the final <pause dur="0.6"/> line <kinesic desc="writes on board" iterated="y" dur="8"/> we can get rid of those negation signs <pause dur="0.8"/> and we get P or not-P <pause dur="1.5"/> eight D-N <pause dur="4.8"/> now that <pause dur="0.3"/> proof certainly repays study <pause dur="2.2"/> mm <pause dur="2.9"/> it's theorem forty-four in <kinesic desc="writes on board" iterated="y" dur="2"/> Lemon <pause dur="1.7"/> i often refer to it as theorem forty-four for example in the workbook <pause dur="0.8"/> you could refer to it as the law of excluded middle L-E-M <pause dur="0.3"/> if you liked or <pause dur="0.3"/> T-N-D <pause dur="0.7"/> # provided you know what you're doing <pause dur="0.7"/> mm <pause dur="0.5"/> it happens to be along with star and dagger <pause dur="0.3"/> something that is often useful to call on <pause dur="0.2"/> when you're doing proofs <pause dur="0.6"/> and <pause dur="0.2"/> through with sequent introduction and theorem introduction <pause dur="1.1"/> well <pause dur="0.5"/> next time <pause dur="0.4"/> we'll say a little bit more about this and show how we can generalize it <pause dur="0.6"/> mm <pause dur="0.7"/> to prove other <pause dur="0.6"/> other sequents with disjunctive conclusions <pause dur="1.7"/> well that was fairly <pause dur="0.2"/> hard work this morning <pause dur="0.4"/> mm <pause dur="1.4"/> thank you very much

</u></body>

</text></TEI.2>