Class Note for CMPSCI 601 at UMass(52)
Class Note for CMPSCI 601 at UMass(52)
Popular in Course
Popular in Department
This 22 page Class Notes was uploaded by an elite notetaker on Friday February 6, 2015. The Class Notes belongs to a course at University of Massachusetts taught by a professor in Fall. Since its upload, it has received 15 views.
Reviews for Class Note for CMPSCI 601 at UMass(52)
Report this Material
What is Karma?
Karma is the currency of StudySoup.
You can buy or earn more Karma at anytime and redeem it for class notes, study guides, flashcards, and more!
Date Created: 02/06/15
CMPSCI 601 Recall From Last Time Lecture 13 Th 121 For any vocabulary E W E STRUCE 99 6 ME in the game where A asserts and B denies that W 99 W l cp ltigt A has a winning strategy W b cp ltigt B has a winning strategy Question If 99 is a tautology and A asserts 9 A has a winning strategy in the game But must A win no matter what he does Answer No if A plays su iciently badly he can lose For example suppose 99 E Teta 1Teta A must choose which disjunct he thinks is true A wrong choice here will lose the game even though Teta 1Teta is a tautology CMPSCI 601 The FirstOrder Proof Rule Lecture 13 Notation For T g E cp E E F l cp is read F proves cp and means There is a rstorder proof of cp assuming F Modus Ponens MP F l a F l Prop 127 Modus Ponens preserves truth validity and semantic implication ie ifAltp gtgbandllcp thenAgD ifl ltp gtgbandl ltp thenFlzzb If p is a rstorder formula then Valtp is called a gen eralization of cp Prop 128 If 9 then Valtp CMPSCI 601 FirstOrder Axioms Lecture 13 all generalizations of the following AXO Tautologies on at most three boolean variables with rstorder formula substituted for the variables 131 gt 131 131 gt 131 V 132 3131 V 13131 bPJNH 31 gt 1921 gt 322 Vu lvEuv gt Vu lvEuv Vzz lt z z gt lt z z lt ElzRz 1ElzRz prime17 gt 1prime17 gt 0 0 999 Proposition 131 All members ofAXO are valid Equality Axioms all generalizations of the following AXlat 2 t for any terrnt t1 2 t 1 quot39tk 2 t2 39 fltt1tk 2 f 1t forterrnst1 fEltlgtrfk AXlC t1 2 t 1 quot39tk 2 t2 gt Rt1tk R 1t fortermst1 GWREILMR PVL Proposition 132 Every instance ofAX is valid 77 Proof Because A is interpreted as identically equal De nition 133 Term t is substitutable for variable a in p iff no free occurrence of a in 99 is Within the scope of a quanti er for a variable z occurring in t cpa lt t is the result of substituting t for all free occur rences of a in cp We never use this expression unless t is substitutable for a in 9 Q ll 06 oalt z1 II 043 lt fu v H 01 z 1 u u u v are substitutable for a in 0 y y 1 are not substitutable for a in 0 04 E a is not the least element 043 lt z 1 z 1 is not the least element ll Instantiation Axioms all generalizations of the following AX2 Valtp gt cpa lt t a a variable t a term t substitutable for a in 9 Proposition 134 Every instance 0fAX2 is valid Proof Let Valtp gt cpa lt t E AXZ Replacing Bound Variables Lemma 135 Let A A be identical except for now they interpret some variables not free in 9 Then AIM9 e Wimp Proof By induction on cp Base case p E Rt1 tk Inductive case 1 cp E nib Inductive case 2 99 E a 8 Inductive case 3 cp E WSW Generalization Axioms all generalizations of the following AX3 99 gt Valtp where a does not occur freely in cp Proposition 136 Every instance 0fAX3 is valid Proof Let 99 gt Valtp E AX3 Let A E STRUCE be arbitrary Suppose A cp Wan i V5601 ltgt for all a E lAleAW w i 99 By Lemma 135 A i Valtp One Last Set of Axioms all generalizations of the following AX4 Valtp gt w gt Valtp gt Vazw Proposition 137 Every instance 0fAX4 is valid Proof Valtp gt w gt Valtp gtVazb E AX4 Suppose A Valtp gt w nish on Whiteboard CMPSCI 601 Theorems and Proofs Lecture 13 De nition 138 Let T Q E Aproofm F0 logic from F is a nite sequence of formulas 0517 0527 a3 quot39 an such that for each 05 1 0 is an axiom or 2 0 E F or 3 3339 k lt 0 follows from 04 oz by MP If 9 is in a proof from F write T t 9 If9 is in a proof from 0 write t 9 9 is a theorem FOTheorems 2 9 I t 9 10 Proposition 139 FOTheorems E re Proof 1fori1tooo 2 for each string 539 of length 239 3 if S is a correct FO proof 4 then output LastLineS 5 11 CMPSCI601 An Example of an F0 Theorem Lecture 13 Proposition 1310 1 a 2 y gt y 2 as T his formula holds in any structure containing an assign ment to a and y We know it s true because a 2 3 means that Mac 2 My tn the structure But we want to prove it in P s formal system Proof 1 x2yaz2a gtac2az gty2az Ach 23923 AXla x2ac gt 3 x2yAac2ac gtaz2az gty2ac gt AXO wy2y 4 x2yAaz2ac gtac2az gty2az gt MP273 wy2y 5x2y gty2a MP14 ampa2 mmwmewrww 12 Theorem 1311 Soundness Theorem If l ap then i p FOTHEOREMS g FOVALID Proof The axioms are valid and MP preserves validity A Soundness is also called consistency It says every thing provable is true while completeness says every thing true is provable Corollary 1312 IfI l cp Then T l 9 Proof The axioms are valid and MP preserves truth ie lfI lzgoandI cp gtzb ThenI izzb Thus by induction on the length of a proof from F every line is true in every model of T Q 13 Two Proof Systems The main text P uses the system we have just described with one proof rule Modus Ponens and lots of axioms The LPL book uses the system F or Fitch which has no axioms but lots of proof rules We ve now seen all the P axioms and proved that they are valid they only prove true statements But we d rather do our proofs in Fitch because it more closely follows our informal processes and because we have software to help us with it So we need to show that Fitch s rules only prove things that are provable in P s system It s also true that Fitch can prove all of P s axioms and it has MP as a rule rightarrow Elim so they prove the same statements 14 Generalization MetaTheorem 2 V Intro If F l 99 and a does not occur freely anywhere in P Then T l Valtp Proof By induction on the length of the proof of p from F Base case n 2 1 99 E AXIOMS Valtp E AXIOMS Base case n 2 1 cp E F 99 gt Valtp E AX3 since a not free in cp 9 given Valtp MP 15 Inductive case Assume true for all proofs of length less than n 041 042 ozn1 9 is a prooffrom F By induction T l Vaa 1 g i g n 1 9 follows from 05 oz by MP ij lt n 013 Z 04239 gt 99 2 Vaa gt 9 Vaa gt 9 gt WXai gt WM 4 Vaa gt Va9 MP 23 AX4 5 WW MP 14 16 CMPSCI 601 The Deduction Metatheorem Lecture 13 The Deduction MetaTheorem 2 gt Intro If F Ultp1 gb Then Pkg Mb Proof By induction on n the length of the proof of w from F U Base case n 2 1 99 2 w w gt w E AXO Base case n 2 1 w E F U AXIOMS 1 w zb E F U AXIOMS 2 w gt 99 gt w AXO 3 9 gt w MP12 17 Inductive case Assume true for all proofs of length less than n 04104204n17b is a proof from F U By induction T F 9 gt 0251 32 g n 1 w follows from 052 043 by MP ij lt n 043 Cw Mb 199 gt04i Ff cp ozz 299 gt04i gtzb IWp ozj 3 70 gt39 05239 gt 99 gt 011 W gt 99 gt W 4 9 gt 042 gt w gt 9 gt w MP13 AXO 5 99 gt MR 2 4 18 Proof by Contradiction MetaTheorem 2 1 Intro If F U 99 i L Then T mp Proof Suppose F U 99 i i By the Deduction MetaTheorem F cp gt L 1 9 gt i 2 99 gt i gt 1ltp AXO 3 mp MP12 Exercise IfI U 199 i L Then T i 9 19 Change Bound Variable Lemma If 3 does not occur freely in 99 and if y is substitutable for a in p then P WW H WWW lt 31 Proof Show Valtp l cpa lt y l Valtp l Valtp Assumption 2 Valtp l Valtp gt 99h lt y AXZ 3 Valtp l cpa lt y MP 12 4 Valtp l Vyltpa lt V Intro 3 5 l Valtp gt Vyltpa lt gt Intro 4 The converse is similar Q 20 Add a Constant MetaTheorem 2 El Elim IfI i 3330p and F 99h lt e i w where c does not occur in 1399 or w Then T i w Proof F 99h lt e i w T i cpa lt c gt w gt Intro F i gb gt mph lt c AXO MP F gb i 1lt9a lt e F gb 1ltpa lt z z new Lemma F gb i Vz1ltpa lt V Intro F gb Va1ltp Change Bound Variable F zb Va1ltp given 13w i i F gb Proof by Contradiction A Lemma 1313 IfA i oa lt c where neither z nor 0 occurs in A or 04 then A i oa lt z Proof By induction on length of proof of A i oa lt c A 21 Proposition 1314 F Vacyz a 2 y y 2 z gt a 2 239 Proof 1 x2yy2zx2y Elim 2 x2yy2zy2z Elim 3 Faz2y gty2ac Lect 13s1 12 4 x2yy2z y2a MP13 5 F z2z AXla 6 2yy2z y2a z2z Intr045 7 F y2az2z gty2z gtac2z Ach 8 x2yy2z F y2z gta2z MP67 9 x2yy2z x2z MP28 10 F x2yy2z gta 2z gtIntr09 11 FVza2yy2z gtaz2z VIntro 10 12 FVszac2yy2z gta2z VIntr011 13 FVxVszaz2yy2z gta2z VIntro 12 22
Are you sure you want to buy this material for
You're already Subscribed!
Looks like you've already subscribed to StudySoup, you won't need to purchase another subscription to get this material. To access this material simply click 'View Full Document'