Class Note for CMPSCI 601 at UMass(5)
Class Note for CMPSCI 601 at UMass(5)
Popular in Course
Popular in Department
This 15 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 26 views.
Reviews for Class Note for CMPSCI 601 at UMass(5)
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 Formal De nition of a Vocabulary A vocabulary E 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 IT 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 xyzx1y1z1 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 A quanti ed formula Elm P or Va P where a is a variable and P is a formula CMPSCI 601 FirstOrder Structures Lecture 14 A structure also called a model of a vocabulary E 2 CD 117 is a pair A U M such that U W 5 7 M V gtU a Hatl M1 D gt total functions on U0 3 f HfAUTf gtU u H gt relations on U0 u R HRAQUNR In propositional logic a model was an assignment of a truth value to every atomic formula In FOL the model must tell us 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 tables for each function and relation 3 Example of a Binary String Structure Let 11 be the string 01101 Aw 0 1 4 lt 124gt e STRUCES 2s 7vltv5vltv2gtvlt72gt7ltSalgt lt251 1 350Vyy S 56 580 2 lt yA Sa 5y gt lt z lt Tarski s Inductive De nition of Truth Mind i t1 t2 42gt Mil 2 MW Rjt17 atrRj ltgt Mal 39 39 39 l l tTRjgt E MW i W9 ltgt MW F 90 MW i 90 V1 ltgt MW i 90 WWW i w AM Vacltp 42gt for alla E lAlaMaaSC i 90 where Mad93Xy W mquot 7g 36 a ifyza Play Tarski s Truth Game world W sentence 0 players A B A asserts that W 90 B denies that W p The game rules depend inductively on the formula 0 p is atomic A Wins iffW p p E av AassertsWaorAassertsW aA BdeniesW aorBdeniesW iz 6 ll a A and B switch roles and B asserts W i 9 I p E 33mm A chooses an element from 1W assign ing it a name n A asserts that W 2M3 lt p E VxW B chooses an element from 1W as signing it a name n B denies that W 2M3 lt 6 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 Intro Derive n 2 n 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 P0 derive Va Pa 0 V Intro General conditional form If from P0 for a new variable 0 you derive 620 conclude Va PM gt 6280 0 V Elim From Va 5 as derive 50 0 EJIntro From 50 derive Ela 5 0 EJelim If from 50 for a new variable 0 you derive Q then you may derive Q from 39 5 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 Example of an FOL Proof DeMorgan s Law For Quanti ers Given Va Pa prove Ea Pa Though this is a wellknown fact no Fitch rule gives it to you directly Here s a proof 1 Assume Va 2 Assume EJa Pa 3 Let c be arbitrary 4 Assume Pc 5 Ha Pa by 3intro 6 i by iintro from 2 5 7 Pc by ielim 8 Va Pa by Vintro 9 i by iintro from 1 8 10 EJa Pa by ielim 11 Ba Pa by elim Soundness 0f Fitch for FOL Once again we prove by induction on all steps in any proof that every statement is a FOL consequence of the premises in force when it occurs This means that if M is any structure such that M P for every premise in force when Q occurs then M l Q Since the last step of the proof can use any of our eighteen proof rules we need eighteen cases in our inductive step We ll do two of these cases with a few others to follow on HW4 First the gtelim case to demonstrate how the previ ous proofs for the propositional Fitch rules carry over Suppose that the last step uses gtelim to derive Q from P gt Q and P Let M be any structure such that M P gt Q and M l P By the de nition of truth for gt it must be that M Q which is what we need to prove 10 The ElElim Case Suppose that with the premise Ela Pa in force we said Let c be such that 130 and from this we derived the statement R in which 0 does not occur The last step was to conclude R outside of this derivation Now let M be a structure such that M l Ela Pa and also any other premises used in our derivation By the de nition of truth for El there must be some object I in the universe of M such that M l Pb Let M be the structure obtained from M by changing the binding of variable 0 so that its value is b We know that M Pc by the meaning of c The proof steps we used to get R from Pc and the other premises are all sound so we know that M B To conclude that M R we need the irrelevant variable rule the easily proved fact that changing the binding of a variable that does not occur in R cannot affect the truth of R The cases of the other new Fitch rules are either similar to this case or are even easier ll Making an Existentially Complete Structure We now begin the proof of completeness for Fitch Given a set of sentences T from which we cannot prove l we want to show that T has a model a structure in which all of its sentences are true This is an equivalent form of completeness if T U S has no model it must be that we can derive i from T U 15 and thus prove S from T using lelim Our rst step is to convert T into an existentially com plete set of sentences over an expanded vocabulary We do this by adding an in nite set of witnessing constants to the vocabulary For every formula Pa in the vocab ulary with exactly one free variable we add a new con stant named Cp Eventually we will insist that if there is any element such that Pa is true then PCp will be true Note that there is nothing wrong with a vocabulary being in nite In almost any imaginable computer science ap plication we will want the vocabulary we use to be nite but everything we have proved about FOL systems and Fitch has applied equally well to in nite vocabularies 12 An Interesting Technicality We want to have a constant claw for every formula Pa over the vocabulary But of course we mean every for mula over the new improved vocabulary with the Wit nessing constants already in it This leads us to an appar ent circularity in the de nition But we can get around this problem Let solo be the orig inal set of formulas over the original vocabulary Let 3811 be the set of valid formulas over the vocabulary that in cludes the original one and Witnessing constants for all onefreevariable formulas in solo Let 881241 be the set of valid formulas over the vocabulary that has Witnessing constants for all onefreevariable formulas in seli for each number 239 Our nal set of formulas L3 is the union of seli for all 239 Every Witnessing contant has a date of birth the num ber of the phase of this construction on which it is cre ated It s easy to see that if a formula of seli contains a Witnes sing constant for a formula containing another Wit nessing constant I then the date of birth of bis less than 2 l3 The Henkin Axioms We want to apply our completeness result for proposi tional Fitch in order to get the completeness result we want for full Fitch To do this we will create a set of ax ioms for the augmented vocabulary with the Witnessing constants Every statement that is an FOL consequence of some premises will be a rstorder consequence of those premises plus the Henkin axioms The ve classes of Henkin axioms will correspond to the nonpropositional proof rules of Fitch Let Pa be any formula with exactly one free variable and let 0 and d be any constants The Henkin axioms H consist of H1 Every statement ofthe form Ela Pa gt PCp H2 Every statement of the form Pc gt 33 Pa H3 Every statement of the form Va lt gt Elm 4306 H4 Every statement of the form c 2 c and H5 Every statement of the form Pc c 2 d gt Pd 14 Proposition 141 Given any model M of the vocabulary for 0 we can interpret the witnessing constants to get a model M of the vocabulary for L such that M l H Proof The statements in H2 H3 H4 and H5 are true in every FOL structure because they are provable in Fitch and Fitch is sound We proved half of the generic H3 statement earlier and the other half is similar Statements in H2 H4 and H5 have oneline proofs using Elintro intro and elim respectively So all we need to do is pick the witnessing constants to satisfy all the H1 statements For every formula Pa with one free variable we assign 0pm to be an element 1 such that M Pb if any such element exists If no such element exists any element of the domain will do why More precisely we pick a I such that M Pb where M refers to M with the partial assignment of values for witnessing constants with dates of birth less than that of 01333 A 15
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'