《FoundationsofLogic (3).pdf》由会员分享，可在线阅读，更多相关《FoundationsofLogic (3).pdf（34页珍藏版）》请在taowenge.com淘文阁网|工程机械CAD图纸|机械工程制图|CAD装配图下载|SolidWorks_CaTia_CAD_UG_PROE_设计图分享下载上搜索。
1、ND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules for identityParametersOnline Course:Foundations of LogicDag Westerst ahlTsinghua LogicND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules for identityParametersThis is Chapter 3.12This week we w
2、ill be occupied with the syntactic aspects oflogical consequence.We will say that a conclusion follows from premises in=1,.,n if there is a derivation of from1,.,n,in some inference system S.In symbols:1,.,nSWhat a derivation looks like depends on the system S.We will take a quick look at two such s
3、ystems:NaturalDeduction(ND)and(next time)a Hilbert type system(H).1 of 33ND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules for identityParametersNatural Deduction:the ideaA derivation in ND starts from assumptions.Some assumptions are temporary,and get discharged duringt
4、he derivation;others(the premises)remain when thederivation is finished.The inference rules come in pairs:an introduction rule and anelimination rule for each logical constant.The derivation has a tree form,with the assumptions asleaves and the conclusion as the root.2 of 33ND:the ideaND:rules for c
5、onnectivesND:negationND:rules for quantifiersND:rules for identityParametersRules for We write the rules for coinjunction rules like this:(I)(E)The correctness of these rules is obvious.3 of 33ND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules for identityParametersHow to
6、 read the rulesConsider again the rule I.(I).Suppose we have a derivation ending with,and a derivationending with.The rules says we can join these two derivations,adding as a new root,to form a new derivation.The new derivation depends on the assumptions that the twogiven derivations depend on.4 of
7、33ND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules for identityParametersAn assumption ruleInstead of derivation,we often say proof tree.All derivations in ND start from assumptions.So we have an Assumption Rule:(A)Any sentence may be introduced as an assumption.That is
8、,the tree consisting of a single sentence occurrence is a prooftree(with as both assumption/premise and conclusion).The sentences in branches with an assumption at the topdepend on unless has been discharged.5 of 33ND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules for id
9、entityParametersRules for:(I)(E)I says:assume and derive (possibly with otherassumptions as well).Then we can write on the nextline,at the same time discharging the assumption.We mark discharged assumptions with .Sentences below nolonger depend on them.E is the familar rule Modus Ponens.6 of 33ND:th
10、e ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules for identityParametersInference dynamics7 of 33ND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules for identityParametersDerivations in NDDefinition1,.,nNDif there is a proof tree(a derivation)built
11、with the ND rules,ending with,and whose undischarged assumptions are among1,.,n.8 of 33ND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules for identityParametersDerivations in ND:first examplesWe show thatND ()that is,that ()is derivable in ND withoutassumptions:21I I1 ()I
12、2 ()Note how the numbering of rules and discharged assumptionshelps us keep track!9 of 33ND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules for identityParametersDerivations in ND:first examplesNext,show thatND ()The first application of I looks odd:was not needed toderiv
13、e,so there is nothing to discharge,but we can stillconclude .But this is in accordance with the rule I,and it is correct:if is true,then must be true.10 of 33ND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules for identityParametersRules for The introduction rules are obvi
14、ous,but how to eliminate?We use reasoning by cases:if derives,and also derives,then derives.(I):(E)11 of 33ND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules for identityParametersThe rules in actionShow,ND()()12 of 33ND:the ideaND:rules for connectivesND:negationND:rules
15、 for quantifiersND:rules for identityParametersRules for negationIn ND is it practical to assume the PL language has a falsumsymbol ,standing for a contradiction.Then we can define in terms of:=def Now the following rules become special cases of I and E:(I)(E)These rules are very useful,but not suff
16、icient for negation.13 of 33ND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules for identityParametersReductio Ad AbsurdumWhat more do we need?One possibility is to add a reductio rule:if you can derive acontradiction from,then conclude:(RAA)Note the difference from I.14 o
17、f 33ND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules for identityParametersDNE implies RAAIf we had a rule of Double Negation Elimination,then RAAfollows:(DNE)15 of 33ND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules for identityParametersRA
18、A and DNE 2Conversely,DNE follows from RAA:This is a typical use of RAA:we assume and derive from it,andpossibly other assumptions,a contradiction.Then we may conclude and discharge the assumption,but of course the otherassumptions remain.16 of 33ND:the ideaND:rules for connectivesND:negationND:rule
19、s for quantifiersND:rules for identityParametersEx Falso Quodlibet 1Everything follows from a contradiction.This has a well-known medieval name,EFQ;and is also calledthe Law of Explosion:(EFQ)It can be derived with RAA(or DNE).In fact,it is an instance of RAA!17 of 33ND:the ideaND:rules for connecti
20、vesND:negationND:rules for quantifiersND:rules for identityParametersEx Falso Quodlibet 2EFQ allows us to prove many facts about negation,such asDisjunctive Syllogism:,NDBut EFQ does not suffice to show,for example,ND which requires RAA(or DNE).18 of 33ND:the ideaND:rules for connectivesND:negationN
21、D:rules for quantifiersND:rules for identityParametersLaw of Excluded Middle(LEM)ND The proof tree for this is a little less obvious:19 of 33ND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules for identityParametersLEM+EFQ implies RAAThis is not so trivial either.We are as
22、suming:and must derive while discharging.Since LEM is adisjunction we must somehow get the result with E.20 of 33ND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules for identityParameters21 of 33ND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules
23、 for identityParametersClassical and intuitionistic logicIntuitionistic Propositional Logic(IPL)is the rule system for,just presented,with defined as ,plus the rule EFQ.Classical Propositional Logic(CPL)is obtained by instead addingRAA(or DNE,or LEM).We will see that CPLexactly matches|=(in Chapter
24、4).Exactly matching IPL requires a different kind of semantics,onethat does not make e.g.p p valid!Very roughly:IPL formalizes warranted assertibility,not truth.There are interesting connections between derivability in IPL and inCPL;see Exercises 3.1.47 and 3.3.10.For example:If CPL,then IPL.!22 of
25、33ND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules for identityParametersRules for:(c)(I)x(x)x(x)(E)(t)(x)has at most x free.t can be any closed term(no variables).But c in I must be new:cannot occur in(x)or in anyundischarged assumptions in the derivation of(c).The ide
26、a:if we can derive(c)for an arbitrary c,then we haveshown that(x)holds for all x.(Remember:if|=(c)where c is new,then|=x(x).)23 of 33ND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules for identityParametersRules for(t)(I)x(x)x(x)(c):(E)I is unproblematic.Again,in E,c must
27、 be new:cannot occur in(x),or in thesentence,or in any undischarged assumptions in the derivation of,except in the assumption(c).The idea:We want to conclude some sentence from x(x).Sothere is some x such that(x);call it c!If we can derive from(c),we are done.(Remember:if,(c)|=where c is new,then,x(
28、x)|=.)24 of 33ND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules for identityParametersExamplesShowNDx(Px Px)Idea:Derive(Pc Pc)(with no assumptions),then use I.25 of 33ND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules for identityParametersMor
29、e examplesShowxPx NDxPxIdea:Derive Pc for a new c.This should work if we assumePc,which yields xPx,which contradicts our assumption.Note that RAA is not used,not even EFQ.26 of 33ND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules for identityParametersMore examplesShowxPx
30、 NDxPxThis is harder,and requires RAA.Idea:We must derive a contradiction from xPx(and then useRAA).To do this,we derive a contradiction from Pc,which yieldsPc,which gives xPx,and we have our contradiction.27 of 33ND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules for ide
31、ntityParametersRules for=(=)1t=ts=t(s)(=)2(t)t=s(s)(t)Here(t)results from(s)by replacing some occurrences ofthe closed term s with the closed term t.For example:NDxy(x=y y=x)(For the derivation,see textbook p.57!)28 of 33ND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules
32、for identityParametersOne more(easy)exampleShowPc,Pd NDxy x 6=y29 of 33ND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules for identityParametersIndividual constants as parametersTo apply the quantifier rules,we need a supply(in fact,aninfinite supply)of individual constan
33、ts.These constants dont appear in the premises or theconclusions we want to obtain.But they are used during the derivations,as parameters.So in what follows well assume that such an infinite supply ofindividual constants is always available.(An alternative would be to use free variables instead,andt
34、hus allow formulas with free variables in derivations.)30 of 33ND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules for identityParametersNext Thursday:Chapter 3.331 of 33ND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules for identityParameters32 of 33ND:the ideaND:rules for connectivesND:negationND:rules for quantifiersND:rules for identityParameters33 of 33