FoundationsofLogic (4).pdf
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 trees 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 sentences,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 logic.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 view 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)()()(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:derivations(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 from 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 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.But 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: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 desired 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.But 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 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 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 Ponens.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 TheoremH: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 enough 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 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 implication.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 occurs 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.Proof.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)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: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 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 this 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 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 cases.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 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 assumptions 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 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 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(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 equivalentThe 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:Propositional 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
