Class Note for CMPSCI 601 at UMass(7)
Class Note for CMPSCI 601 at UMass(7)
Popular in Course
Popular in Department
This 27 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 17 views.
Reviews for Class Note for CMPSCI 601 at UMass(7)
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 The Course So Far We ve de ned various models of computation in which we can study what problems can and can t be solved and what resources the solvable problems require The most important model has been the Turing machine which might or might not halt on a given input Re cursive sets are decided by alwayshalting TM s recur sively enumerable sets have TM s that accept strings in them and fail to halt on the others Similarly total re cursive functions are computed by alwayshalting TM s and partial recursive function by general TM s Some sets and functions are provably not recursive 0 The busybeaver function 0 HALT 2 M x M halts on input 2 0 K 2 n n 6 Wm 0 any nontrivial property of machines ZCFL We showed busybeaver and K to be nonrecursive by direct arguments For the others we used reductions if A g B and A is not recursive then B is not recursive A set is rec0mplete if it is re and all re languages re duce to it No recomplete language is recursive But a language can be nonrecursive Without being recomplete K is corecomplete and thus not re and there are languages that are neither re nor core at all Other Formal Models of Computation Formal Language Theory Regular languages DFA s NFA s or regular ex pressions Contextfree languages grammars or pushdown automata Boolean Compute on boolean values with AND OR NOT Boolean expressions compute boolean functions Straightline boolean programs Fitch proof system sound and complete 0 FirstOrder Logic El V starting today Recursive Function Theory Primitive Recursive Bloop computable General Recursive Floop computable partial re cursive Abstract RAM Can simulate TM vice versa poly time blowup CMPSCI 601 FirstOrder Logic With Equality Lecture 13 In propositional logic we reason about some set of state ments the atomic formulas each of which is either true or false Firstorder logic with equality FOL is a more complex logical system in which we deal with the fact that the atomic formulas are statements about ob jects To set up an FOL system we need a domain D the set of objects in question which may be nite or in nite We then need a vocabulary a formal de nition of what atomic statements we may make about the objects We then will be able to say 0 that two objects are the same 0 that an object exists with some property or that 0 all objects in D have some property Formal De nition of a Vocabulary A vocabulary Z is formally made up of three elements 0 The set I of function symbols each representing a function from Dk to D for some k 1 includes the constant symbols of the vocabulary which are thought of as function symbols with k 2 0 0 The set U of predicate symbols each representing a relation on D a function from Dk to 0 1 for some k The equality sign is included in H as a binary relation written in its usual in X form e g s 2 t 0 The arity function 7 which assigns the number of arguments k to each symbol in I and H Examples of FOL Vocabularies Number Theory EN 2 DN UN TN EN 2 0 039 X 7 N0 2 07 N0 2 174N 7 Ngtlt 2 TNT 2 2 EN 2 2 lt 74N2 2 7 Nlt 2 2 Graph Theory 2G 2 D9 Hgv 7 9 D9 Svtv 7493 2 749 Z 0 Hg 2 7 E 749 T9E 2 Binary String Theory 2W 2 110 Hwarg Du 2 0 H10 2 2 lt1 7302 2 rwlt 2 2rw1 21 Tarski s World ET 2 CDT7 HT 7 1 ET avbvcvdvevf HT 2 Tet Cube Dodec Small Medium Large SameSize SameShape Larger Smaller SameCol SameRow Adjoins LeftOf RightOf FrontOf BackOf Between rTet 2 rCube 2 rD0dec 2 rSmall 2 TMedium 2 rLarge 2 1 rSameSize 2 rSameShape 2 rLarger 2 rSmaller 2 rSameC01 2 rSameR0w 2 rAdj0ins 2 rLeftOf 2 rRightOf 2 rBackOf 2 2 rBetween 2 3 Inductive De nition of FOL Formulas Once we x a vocabulary Z we have a set MS of well formed formulas Entities within formulas have two types object and boolean We de ne valid formu las by induction Variables We have an in nite set V 2 13 y z why1 21 Terms A term is a variable or a function applied to the correct number of terms A constant is a special case of the latter Formulas A string is a wellformed formula if it is 0 An atomic formula which is a predicate symbol ap plied to the correct number of terms or the special atomic formula 3 2 t where s and t are terms 0 A boolean operator applied to the correct number of formulas or 0 3x P or Vx P where 1 is a variable and P is a formula CMPSCI601 Some Formulas 0f ZN Lecture 13 Abbreviations tlgtg C gtt1t2t1ltt2 1 C gt 00 2 C gt 01 3 C gt 02 t11t2 C gt 3xt1 X a 2 t2 primet1 C gt 1 lt t1 Vxxt1 gt a 1V 1 t1 CMPSCI601 Some Formulas 0f lt29 Lecture 13 1 WyXEway gt Etcax 2 wx mmn 3 WXEyXEWay V Eta 3 4W bEW D 5 3yzy 7A 2 Em y Em 2 6 Vyly2y3Exa 31 EW 92 EW 33 gt 31 y2Vyl y3Vy2 293 10 CMPSCI601 Free and Bound Variables Lecture 13 An occurrence of a variable a is bound iff it occurs within the scope of a quanti er Vx or Otherwise the occurrence is free Examples Which Variables are Free Eyzlly 7 Z Elxa y Elxa 2 V2 2 1 2 z 1 2 3 ViXer 1 y 4 Vxxxx 5567 3yyltx ll What Do Variables and Sentences Mean Bound variables are dummy variables you can change their names without affecting the meaning of the formula A rstorder formula says something about its free vari ables in the context of a particular structure of objects predicates and functions You cannot determine the mean ing of the formula without knowing the values of the free variables A sentence a formula with no free variables says some thing about the entire structure of objects predicates and functions Thus a sentence of ET talks about a particular blocks world a sentence of 2G talks about a particular graph and EN talks about a particular set of numbers with addition and multiplication de ned This is true even though there is no syntactic reference to the graph G in a 2G sentence or to the string 21 in a Spy sentence In 2G we talk about a vertex as a vari able or constant and an edge as a relation that holds for two vertices In 2W we talk about a position in the input as a variable and the letter a position contains as unary relation on the position 12 CMPSCI 601 FirstOrder Structures Lecture 13 A structure also called a model of a vocabulary Z 2 Cl 117 is a pair A 2 U n such that UNN M V gt U x gt 23 4 M 2 CD gt total functions on U 01 urfwf wmoy M I H gt relations on U0 V RHHWQWW l3 How s That Again In propositional logic we could decide whether an arbi trary compound formula was true or false once we had a model an assignment of a truth value to every atomic formula In FOL the model must be more complicated We need to know what the objects are and what the relation and function symbols mean If the universe or domain is nite we can specify this information by nite lookup ta bles for each function and relation To evaluate a formula with free variables we also need an assignment of an element of the domain to each variable 14 FOL Formulas as Propositional Formulas Suppose that we know that the domain is nite and has n elements We can think of a sentence of FOL as im plicitly describing a propositional formula where the atomic formulas are particular values of the evaluation function it For example Treat functions as relations adding wellde nedness for mulas Proposition 131 Any xed FOL sentence on a universe of size n is equivalent to a propositional formula of size 01 71 Proof Carry out the above process noting that the size is only multiplied by 001 for each quanti er in the for mula A 15 Example Any world W for Tarski s World is is struc ture of vocabulary 2T ie W E STRUCZT Example of Graph Structures G VG 1 3 EG e STRUCZg VG 0 1 2 3 4 EG 172v3v0v 3v1v3v27374v 40 is a structure of vocabulary 29 consisting of a directed graph with two speci ed vertices s and t G has ve ver tices and siX edges See the gure below which shows G as well as another graph H that is isomorphic but not equal to G S 16 Example of a Binary String Structure Let 11 be the string 01101 Aw 0 1 4 lt124 e STRUCZS 2s vvltvSvltv2gtvltltv2gtvltSv1gt lt2731 1 EnyXy S a 3amp0 2 lt yA Sx Sy gt lt z lt 17 CMPSCI 601 A Relational Database Lecture 13 Egan F17P2v32 30 U07F07P07 30 6 STRUCden U0 2 Abraham Isaac Rebekah Sarah F0 2 Sarah Rebekah P0 2 Abrahaszaac SarahIsaac SO 2 AbrahamSarah IsaacRebekah W5iblingltxvy E 7g 3 A f 7g m A 1308 PO 9 13071735 PM 11 pummel y E 3p3Ppv y A Wsibling jv 8 A s 2 a Sxs 18 It is perfectly reasonable to have two different models of the same vocabulary in which different things are true N 2 N 0 0 X T lt the standard model of the nat urals 17 up 1 0 11 1 X1 T1 w p prime N ZpZ e STRUCZN Multlnverses E 2 0 ElMu X o 2 1 N 2 MultInverses Z pZ 2 Multlnverses l9 Beginning to De ne Truth In propositional logic we inductively de ned what it meant for a truth assignment to satisfy a formula or make it true In the same way we can inductively de ne what it means for a structure of the appropriate vocabulary V to satisfy a formula The rst step is to assign an element of the domain to ev ery term of V To do this we inductively extend the function u terms gt M already de ned on variables and constants Hltfjltt17 vt7 fj f ultllwwultrgj Now every term has a meaning 20 Tarski s Inductive De nition of Truth MW i t1 t2 lt9 W1 W2 GAL Rjt1739 39 atrRj ltHltt1v 39 39 39 7HtrRjgt E 1941110 W19 lt9 194W 95 lt19 1A11MH lt19 V 2 lt lt1A111ltltH lt19 0r 194W i 21 011 Vxltp lt for alla E 1A11u1ax i lt19 Where 11 axy 9 ify 7g x a ifyzx 21 Play Tarski s Truth Game world W sentence 9 players A B A asserts that W cp B denies that W cp The game rules depend inductively on the formula cp 99 is atomic A Wins iffW cp p E av AassertsWozorAassertsW8 p E oz8 BdeniesWiozorBdeniesW8 p E og A and B switch roles and B asserts W i 04 99 E 323w A chooses an element from 1W assign ing it a name 71 A asserts that W Mr lt p E wa B chooses an element from 1W as signing it a name 71 B denies that W Mr lt 22 Example Does Z3Z 2 2 0 3vu X 11 2 1 Z3Zu0 2 2 0 3vu X 1 21 lt2 forall a 6 012 Z3Zu0au 2 u 2 0 3vu X 1 2 Z3Zu00u 2 u 2 0 lt2 0 0100 M0 0 MO 020 ltz3zuo1ugt 1 MW gtlt v 1 lt2 exists I e 012Z3Zu01ubv 2 u X 11 2 1 ZSZu01u 11 2 u X 1 21 Similarly ltz3zuo2ugt 1 MW gtlt v 1 23 BE has a clause in the inductive de nition for each boolean operator but it suf ces to have only and I as above Proposition 132 Wan i WW lt2 Wan i wandOAW i w Proof Wan i WW ltgt Wan i n p V W lt DOW1131M w V W lt IMHO1W i w0rlu417u i W lt Wan be w andlt1u413u W ltgt Wan i lt19 and WM i w 24 Similarly de ning satisfaction for one quanti er allows you to de ne it for the other Proposition 133 WM 61099 lt23 exists a 6 MUG117 ax l lt19 Proof Wan l SEW 6 Watt l anhw 6 Watt be WOW lt2 not for all a e MUG1 ax l W lt23 for some a 6 MUG113M ax t6 w lt23 for some a 6 MUG113M ax l 99 25 Fitch Proofs for FOL The Fitch proof system of BE can prove FOL formulas as well as propositional ones We have to add SlX new proof rules to deal with the new concepts of identity and quanti ers 0 Intr0 Derive n 2 11 cf Atlas Shrugged 0 Elim From Pn and n 2 m derive Pm 0 V Intro Ordinary form If for a new variable 0 you derive 130 derive Vx Px 0 V Intro General conditional form If from 130 for a new variable 0 you derive Qc conclude Vx PCT gt QW 0 V Elim From Vx 3x derive 30 0 EJIntro From 30 derive 3x S 0 EJelim If from S c for a new variable 0 you derive Q then you may derive Q from 3x S 26 Coming Attractions We will prove Fitch to be sound for FOL following BE Section 183 with some details on HW4 The basic idea is very similar to soundness for propositional Fitch We show by induction on steps of any proof that each state ment is true in any structure in which all of its premises are true instead of for any truth assignment Then we will prove the completeness of Fitch for FOL following BE Chapter 19 with some details on HW5 The goal is to prove that any FOLvalid sentence can be proved in Fitch We will do this as follows 0 De ne an in nite set of sentences called the Henkin theory 0 Show that any propositional extension of the Henkin theory has a model 0 Use propositional completeness to get a propositional Fitch proof of any FOLvalid sentence from the Henkin theory and nally 0 Show that in Fitch we can eliminate every use of the Henkin theory in this proof to get a Fitch proof of the FOLvalid sentence 27
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'