Class Note for CMPSCI 601 at UMass(41)
Class Note for CMPSCI 601 at UMass(41)
Popular in Course
Popular in Department
This 16 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 14 views.
Reviews for Class Note for CMPSCI 601 at UMass(41)
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 14 FirstOrder Proof Rule I l cp gttI l cp I l t Modus Ponens MP gt Elim FirstOrder Axioms all generalizations of the following O Tautologies on at most three boolean variables la tzt lb tlzt 1 tkt gtft1tkf 1t lc tlzt lA tkt k gt Rt1tk gtR 1t 2 WW gt W lt t 3 p gt Vacltp a not free in p 4 WW gt 2b gt WOW gt WW0 Prop 127 MP preserves truth validity and semantic implication Props 128 129 1210 1212 1214 1215 Every instance of every axiom from P is valid Soundness Theorem Every rstorder theorem is valid ie for all 2 and for all p E Z tww Furthermore rstorder proofs preserve truth and se mantic implication ie for all T g Z ifFlcp then 1190 Proof The axioms are valid and MP preserves validity A Prop 139 FOTHEOREMS 2 go I lcp E re Two Proof Systems The proof rules of Fitch preserve not only validity but provabz lz ly in P s system That is the existence of a Fitch proof proves the existence of a P proof We establish this fact by proving metatheorems 0 Generalization If F l ap and a does not occur freely in F then T l Valtp Deduction Ifl U 90 l zJ then T l ap gt 2 0 Proof By Contradiction If F U 90 l l then T l P 0 Add A Constant If i Elaltp and F ltpa lt c l 2 where c does not occur in F p or 2 then T l 2 Proposition 141 Fmez xzyAyzz gt 3222 Proof 1 aczyAyzzay Elim 2 azzyAyzzyz Elim 3 Fuzzy gtyza Lect 13s1 12 4 aczyAyzz yaz MP13 5 F zzz AXla 6 2yyz yxzz Intr045 7 F yazz gtyz gtacz Ach 8 2yyz F yz gtaz MP67 9 aczyAyzz az MP28 10 F ayyz gtaz gtIntr09 11 FVzayyz gtaz VIntr010 12 FVsz aczyAyzz gtaz VIntr011 13 FVmVsz azzyAyzz gtaz VIntro 12 De nition 142 F is consistent iff F lf i Q Already shown Soundness Th If F is satis able Then T is consistent Completeness Theorem If F is consistent then T is satis able Proof Let F g E be consistent We will build A such that A l T Idea Extend F to a maximally consistent set of formulas A A answers every question and thus de nes a model A Let c0 c1 Cg be new constant symbols Z ZuciieN 3239 900790179021H cn does not occur in 900901pn 11 2 F Tn Fn1 U 90m Ian1 U cpn cons1stent cpn otherwise U ZJCn I 3vzJvjust added Each new statement is either already forced to be true forced to be false or not yet forced In the last case we make it true If the new true statement says that an ele ment exists with a property 2 we make on that element Claim Each Tn is consistent Proof By induction on n Base case 1L1 consistent by assumption Inductive step Assume Fn1 consistent At least one of Fn1 U cpn Fn1 U man is consistent If Fn1 U EJvzJv consistent Then so is Fn1 U 3vzJv 2cn by El Elimination A A is consistent and complete and has the Hencm property that every provable El statement has a constant Witness Consistent Suppose A l l Since proofs are nite some I l l Complete for all cpn E E A l cpn or A l cpn Henkin if A l Elvzv then for some constant k A l Mk CMPSCI 601 Build A from A Lecture 14 De nition 143 Ci E cj iff A l ci 2 cj Q Claim E is an equivalence relation Proof l ci 2 Ci l ci 2 cj gt cj 2 Ci l ci2chcj2ck gtci2ck Q W M I iEN a 2 on stAl a2cn RA 2 mail own I A e Rm a w fA ltCi1 39 39 39 Cirf1gt I A F fltci17 39 39 39 acidf Ci f l Note fA is well de ned by Ale and RA is well de ned by Ach Claim 144 A i2 A Proof First Show tf 2 t 42 A t1 2 t2 by induction on ltll ltgl base case t1 2 u t2 2 v tf 2 cl t 2 02 Where A i t1 2 Chtg Z Cg F4 t ltgt 01 02 42 A i 01 2 Cg 42gt Ai tlztg 10 inductive case t1 2 sh 8a 3A i1a t Cg Z By inductive hypothesis A tg 2 62 Ai sizki i1a if t 4 41gt fAk1aaka 62 42gt Ai fk1ka262 42gt Ai f818a262 42gt Ai tlztg 11 Now by induction on p E Z show A l 90 42gt A l 0 Base case p Rt1 gimp Inductive case p ZJ Inductive case p 2 a Inductive case p 2 WokWu This completes the proof of Claim 144 Q This completes proof of the Completeness Theorem Q 12 Corollary 145 F 90 42gt F F 0 Proof Suppose F V p I mWi there exists A A k F U ip WW FOTHEOREM 2 FOVALID Ene Notation F p A p 13 CMPSCI601 Compactness Theorem Lecture 14 Theorem 146 Compactness Theorem Suppose every nite subset of F has a model Then T has a model Proof If F is inconsistent then some nite subset of F is inconsistent because proofs are nite N0 nite subset of F is inconsistent F is consistent F has a model 14 Compactness Applications CMPSCI 601 Lecture 14 TheoryN 2 90 E EN I N i 90 F 2 TheoryN U cgt0cgt1cgt2cgt3 Corollary 147 F has a model There is a countable model of TheoryN that is not iso morphic to N EN cannot uniquely characterize N Proof Every nite subset of F is satis able by N for 239 su iciently large By Compactness F is satis able Q 15 Corollary 148 Connectedness is not expressible m the rstorder language of graphs Eg Proof Suppose that X E I am connected F 2 x U DIST3tgt1DISTstgt 2 DIST0an gt n E n l V931 39 39 399371 1 V 932 i1 EWz 93241 2 Every nite subset of F is satis able By Compactness F is satis able 2gt Connectedness is not expressible in the rstorder lan guage of graphs Q 16
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'