《FoundationsofLogic (4).pdf》由会员分享，可在线阅读，更多相关《FoundationsofLogic (4).pdf（33页珍藏版）》请在taowenge.com淘文阁网|工程机械CAD图纸|机械工程制图|CAD装配图下载|SolidWorks_CaTia_CAD_UG_PROE_设计图分享下载上搜索。
1、H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDOnline Course:Foundations of LogicDag Westerst ahlTsinghua LogicH:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDThis is Chapter 3.3The proof tre
2、es in Natural Deduction mirror natural ways ofreasoning,but are rather complicated syntactic objects:treesof sentences,with information about possibly dischargedassumptions.The classical idea of deduction is rather that of a linearsequence of sentences,each being an axiom or following fromearlier se
3、ntences,with no going back to earlier sentences andchanging things.This makes the proof itself a much simpler structure,althoughit can be less easy to find a proof.Such simplicity is helpful when you want to prove thingsabout a logic or a theory,as we do in this course,rather thanworking in the logi
4、c.1 of 32H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDH:languageThe inference system is called H(for Hilbert).The onlyconnectives in this system are and.As we know,the others can be defined in terms of them.For example,we could set =def and vi
5、ew as an abbreviation of .So when wewrite,for example,(p q)rthis is just shorthand for(p q)r2 of 32H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDH:axioms and ruleThere are three axioms(rather,axioms schemes)and one rule!(Ax1)()(Ax2)()()()(Ax3)(
6、)()(MP)From and ,follows.(Ax1)is a familiar tautology,and so is(Ax2).(Ax3)is a version of reductio:if we assume,and both and follow,i.e.if a contradiction follows,then weconclude.3 of 32H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDH:derivation
7、s(proofs)The system H is very economical,and the notion of aderivation(or proof)is extremely simple:DefinitionA derivation in H of from is a finite sequence of sentenceswhose last sentence is,and such that each sentence in thesequence is either(i)an assumption in,or(ii)an axiom of H,or(iii)follows f
8、rom earlier sentences in the sequence by means of arule in H.Also,1,.,nHmeans that there is a derivation in H of from 1,.,n.4 of 32H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDH:examplesWe havep,p q qbecause the following is a derivation in H
9、of q fromp,p q:p,p q,qAlso,the one sentence derivationpshows thatp Hp5 of 32H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDH:examplesThat was trivial.Recall that in ND,since p NDp(againtrivially),we directly conclude with the rule I thatNDp p.Bu
10、t there is no such rule in H!Still:H The derivation that shows this is not trivial.The trick is to use suitable instantiations of(Ax1)and(Ax2)with MP.(We could of course have added as a new axiom,butthen the system of axioms would not be independent.)6 of 32H:Propositional logicH:Deduction TheoremH:
11、quantifiersH:identityH:proof of Deduction TheoremH versus NDH:deriving We set up the derivation as follows:1 ()Ax12()()()Ax23()()MP from 1,24 ()Ax15 MP from 3,4Line 1 is(Ax1)with instead of.Line 2 is(Ax2)with instead of,and instead of.Thisgives line 3 with MP.Line 4 is(Ax1)with instead of.The desire
12、d conclusion followswith MP.7 of 32H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDH:annotating derivations1 ()Ax12()()()Ax23()()MP from 1,24 ()Ax15 MP from 3,4We write the derivations like this to see how each sentence followfrom previous ones.B
13、ut the actual derivation itself is just the sequence of fivesentences,without annotations.8 of 32H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDH:more examplesWe can use sentences we have already derived in new derivations.H()At step 2 we insert
14、 the derivation we already have for ,but we dont write again.The point is not to write down long derivations,but to show that aderivation of the desired kind exists.9 of 32H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDH:the Deduction TheoremIn
15、ND,the rule I takes us from,ND to ND .There is no such rule in H,but it is extremely useful!Fortunately,it is a derived rule in H:Fact(Deduction Theorem)If,H then H .We get back to the proof of this later;for now we see how itis used.Note that the other direction,IIf H then,H.follows from Modus Pone
16、ns.10 of 32H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDDeduction Theorem:examplesFor example,we trivially have H,hence H bythe Deduction Theorem.Consider:,H To show this,assume in addition,and derive:11 of 32H:Propositional logicH:Deduction T
17、heoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDMore examples(a)H By the Deduction Theorem,it is enough to show ,H12 of 32H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDMore examples(b)H ()By the Deduction Theorem,it is enoug
18、h to show(EFQ),H13 of 32H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDAnd one more()HWe use(a)and(b):14 of 32H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDQuantifier axioms and rule(x)has
19、at most x free,is a sentence,and t a closed term.(Ax4)x(x)(t)(Ax5)x(x)(x(x)(Ax6)(t)x(x)(Ax7)x(x)(x(x)(R)x(x)follows from(c),provided c does not occur in(x)or in any assumptions of the derivation that come before(c).Ax4 and Ax5 are unproblematic.Ax3,Ax5 reflect facts about distributing x,x in an impl
20、ication.R expresses a fact we showed last week:If|=(c)and c is new,then|=x(x).15 of 32H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDQuantifier examplesxPx HxPxWe did this in ND,and use a similar idea:choose a newconstant c,and derive Pc:NB c oc
21、curs in sentences preceding Pc,but not in assumptionspreceding Pc.16 of 32H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDQuantifier examplesThe following was shown to hold for|=in Chapter 2.IIf,(c)H,where c does not occur in,(x)or,then,x(x)H.Pro
22、of.17 of 32H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDObject language and metalanguage(1)p,p q Hq rThis is a(true)claim(in our metalanguage)about the system H:that a certain derivation exists.The following is a derivation in H,showing that(1
23、)is true:18 of 32H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDIdentity axiomsThe identity axioms are as expected:(Ax8)x x=x(Ax9)xy(x=y (x)(y)This completes the axioms and rules for the system H.19 of 32H:Propositional logicH:Deduction TheoremH
24、:quantifiersH:identityH:proof of Deduction TheoremH versus NDInduction on the length of proofsSuppose we want to show:IIf H,then has property P.This will follow if we can show:for all n,(An),where(An)If 0,.,nis a derivation in H of nfrom,then nhas property P.And“for all n,(An)”will follow if we can
25、show,for all n,(Bn)If(Ai)holds for all i n,then(An)holds.This is just a mathematical fact.NB(B0)is equivalent to(A0).20 of 32H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDProof of the Deduction Theorem 1Fact(Deduction Theorem)If,H,then H .In th
26、is case:(An)If 0,.,nis a proof of nfrom,then H n.So we must show that for every number n:(Bn)If(Ai)holds for all i n,then(An)holds.21 of 32H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDProof of the Deduction Theorem 2So,let n be any number,and
27、assume that for every i n we have:(Ai)If 0,.,iis a proof of ifrom,then H i.Our task is to show that then(An)also holds.To do this,suppose0,.,nis a proof of nfrom assumptions in .We must now show that H n.Depending on what the last step of the proof was(the step thatresulted in n),there are five case
28、s.22 of 32H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDProof of the Deduction Theorem,Case 1I0,.,nis a proof of nfrom assumptions in .Case 1:nis an assumption in.23 of 32H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of
29、 Deduction TheoremH versus NDProof of the Deduction Theorem,Case 2I0,.,nis a proof of nfrom assumptions in .Case 2:nis.24 of 32H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDProof of the Deduction Theorem,Case 3I0,.,nis a proof of nfrom assumpti
30、ons in .Case 3:nis a logical axiom.25 of 32H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDProof of the Deduction Theorem,Case 4I0,.,nis a proof of nfrom assumptions in .Case 4:nfollows from earlier sentences with MP.This meansthat there are i,j
31、n such that j=i n.26 of 32H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDProof of the Deduction Theorem,Case 5I0,.,nis a proof of nfrom assumptions in .Case 5:nfollows from earlier sentences with R.This means thatnhas the form x(x)and there is i
32、 n such that i=(c),where c is new.227 of 32H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDDeduction Theorem,important noteIt follows from our proof that the Deduction Theorem holdsfor any Hilbert style inference system,as long asI(Ax1),(Ax2),and
33、(Ax5)are provable(withoutassumptions)in the system;Ithe only rules are MP and R.For example,a system with the other connectives and aswell,and suitable axioms for them.28 of 32H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDND and H are equivalen
34、tThe systems ND and H are equivalent:for all sentences1,.,n,:Fact1,.,nND iff1,.,nHThis can be shown with induction on the length of proofs in Hin one direction,and on the length of ND style proof trees inthe other direction(see Chapter 3.3.3,but no need to gothrough the detailed proofs).29 of 32H:Pr
35、opositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus NDNext Monday:Chapter 430 of 32H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus ND31 of 32H:Propositional logicH:Deduction TheoremH:quantifiersH:identityH:proof of Deduction TheoremH versus ND32 of 32