FoundationsofLogic (2).pdf

《FoundationsofLogic (2).pdf》由会员分享，可在线阅读，更多相关《FoundationsofLogic (2).pdf（37页珍藏版）》请在得力文库 - 分享文档赚钱的网站上搜索。

1、FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequenceOnline Course:Foundations of LogicDag Westerst ahlTsinghua LogicFOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequenceThis is Chapter 2.2Atomic formulas in FOL contain more information that thesen

2、tence letters of PL.They say that some things are related to each other,or thatsome thing has a property.For this we need symbols for things and for relations.A vocabulary L in FOL is a set of non-logical symbols:Iindividual constants:c,d,c1,.)In-ary predicate symbols(n 1):P,Q,R,P1,.In-ary function

3、symbols(n 1):f,g,h,f1,.(We can also treat 0-ary predicate symbols as sentence letters,and 0-ary function symbols as individual constants.)1 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequenceTermsTerms are expressions that stand for individuals.Let L be a vocabulary.

4、The set of L-terms is defined as follows.Definition(L-terms)IA variable(one of v0,v1,v2,.)is an L-term.IA individual constant in L is an L-term.IIf f is an n-ary function symbol in L and t1,.,tnareL-terms,then ft1.tnis an L-term.If L contains function symbols,this is an inductive definition.When L i

5、s understood from the context,or arbitrary,we just sayterm.2 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequenceAtomic formulasDefinition(atomic L-formulas)If P is an n-ary predicate symbol in L and t1,.,tnare L-terms,then Pt1.tnis an atomic L-formula.This is an expl

6、icit definition,not an inductive one.There is a fixed 2-ary predicate symbol for identity:=Instead of writing=t1t2(which is officially correct),we writet1=t2And t16=t2means t1=t2.Also,we sometimes writeP(t1,.,tn)orf(t1,.,tn)when this is easier to read.3 of 36FOL:terms and formulasFOL:informal semant

7、icsFOL:formal semanticsFOL:consequenceLogical symbols/constantsThe logical symbols(or logical constants)of FOL areI,(connectives)I=(identity)I,(quantifier symbols)Sometimes a subset of these are chosen,e.g.,=,(this does not decrease expressive power).Or drop identity(significantly decreases expressi

8、ve power).4 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequenceFormulasDefinition(L-formulas)IAtomic L-formulas are L-formulas.IIf and are L-formulas,then,(),(),and()are also L-formulas.IIf is an L-formula and x is a variable,then x andx are also L-formulas.In a quan

9、tified formula x or x,is the scope of(thatoccurrence of)the quantifier expression x or x.5 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequenceTerms and formulas 2Again,we can write the inductive definitions of terms andformulas more compactly as follows:L-terms:It:=c

10、|x|ft1.tnL-formulas:I:=Pt1.tn|()|()|()|()|x|x6 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequenceSentencesAn occurrence of x in a formula is free,if it is not withinthe scope of any quantifier expressions x or x in.Otherwise,it is bound.If x is bound in,we say it is

11、 bound by the occurrence of xor x with the smallest scope within which this x occurs.Definition(sentences)An L-formula is a sentence if no variables occur free in.7 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequenceExamples8 of 36FOL:terms and formulasFOL:informal s

12、emanticsFOL:formal semanticsFOL:consequenceSubstitutionIf is a formula,we write as(x1,.,xn)to indicate that the free variables in are among x1,.,xn.Then,if t1,.,tnare terms,we write(t1/x1,.,tn/xn)or simply(t1,.,tn)for the result of simultaneously replacing all free occurrence ofx1,.,xnin by t1,.,tn.

13、9 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequenceSubstitution:examplesDont accidentally bind variables!You can skip the formal account of substitution(last part of Ch.2.2.1)for now.10 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:conseq

14、uenceTranslation into FOL 1It is absolutely necessary to have an intuitive grasp of themeaning of predicate logic(FOL)sentences.To test this:translate,or formalize,natural languagesentences involving quantification into FOL sentences.The first step is to identify words(such as names)translatableas i

15、ndividual constants,and words(such as nouns,adjectives,verbs)translatabel as predicate symbols.Then quantified expressions,indicated by words like“every”,“some”,“a(n)”,“no”.11 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequenceTranslation into FOL 2For quantified exp

16、ression there are two rules of thumb thatalmost always work:(*)A universally quantified(sub)sentence,“All As are B”,“EveryA is B”,etc.becomesx(Ax Bx)(*)An existentially quantified(sub)sentence,“some As are B”,“An A is B”,etc.becomesx(Ax Bx)12 of 36FOL:terms and formulasFOL:informal semanticsFOL:form

17、al semanticsFOL:consequenceTranslation into FOL:examples(1)A student greeted Mary.(2)John knows every student.(3)No teacher knows every student.(4)Every professor who knows Bill met some student.13 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequenceTranslation into F

18、OL:more examples(5)Every graduate student knows someone who knows Diana.(6)Some professor knows every student except Henry.(7)Samantha owns at least two bikes.(8)If a farmer owns a donkey he loves it.14 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequenceTruth in pred

19、icate logicWe also need a formal semantics,a truth definition like theone for PL.That is,we must define the relation true in an interpretation,M|=(is true in M)where is a FOL-sentence and M is an interpretation(of thenon-logical symbols in).15 of 36FOL:terms and formulasFOL:informal semanticsFOL:for

20、mal semanticsFOL:consequenceInterpretations(models)An interpretation(a model)for the vocabulary L is a pairM=(M,I)where M is a non-empty set(the domain or universe)and Iassigns suitable values(extensions)to the symbols in L:Iif c L,then I(c)is an element of the domain(I(c)M);Iif P is an n-ary predic

21、ate symbol in L,then I(P)is an n-aryrelation over M(I(P)Mn);Iif f is an n-ary function symbol in L,then I(f)is an n-aryfunction on M(I(f):Mn M).We often writecM,PM,fMinstead of I(c),I(P),I(f).16 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequenceInterpretations(model

22、s):examples17 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequenceTruth and satisfactionAgain,it is often intuitively clear that a sentence is true,orfalse,in a given model.But a formal truth definition faces a problem.The inductive clause for M|=xPx should somehow re

23、ly onthe clause for M|=Px.But Px is not a sentence,so it has no truth value in M!Tarskis solution(1933)is to define satisfaction instead oftruth.We say that an object a in M satisfies Px in M if a belongsto PM,writtenM|=Px a18 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:

24、consequenceAssignmentsThenM|=xPx iffBut in general there may be lots of free variables,each ofwhich has to be assigned an object in the domain.Definition(assignments)An assignment in M is a function from the set Var of variablesto M.So for every variable vi,(vi)M.Thus,we need to define the relationM

25、|=(satisfies in M)for every formula.19 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequenceThe values of termsFirst,we must specify the value of each term t in M,relativeto an assignment,writtentM,Thats clear if t is a constant or a variable:(i)if t is a constant c,th

26、en tM,=cM(ii)if t is a variable x,then tM,=(x)If t is a complex term,we need an inductive clause:(iii)if t is ft1.tk,thentM,=fM(tM,1,.,tM,k)20 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequenceFinally,the truth definition:IM|=Pt1.tn iffPM(tM,1,.,tM,n)IM|=t1=t2 ifftM

27、,1=tM,2(two uses of=!)IM|=iffM 6|=IM|=iffM|=and M|=Isimilarly for ,etc.IM|=x iffthere is a M s.t.M|=(a/x)IM|=x ifffor all a M we have M|=(a/x)(a/x)is like,except that a is assigned to the variable x.21 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequenceLocality and t

28、ruthHave we forgotten about truth?No,it can be seen as a special case of satisfaction,because ofthe following:Lemma(Locality,Lemma 2.2.15)If and 0agree on the free variables in,then M|=iffM|=0.It follows that if is a sentence,then either all assignments inM satisfy it,which we writeM|=(is true in M)

29、or none do.22 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequenceMore localityThere is another sense in which satisfaction are truth are local:onlythe interpretation of the non-logical symbols actually occurring in aformula matter for whether M|=holds or not.This is

30、the content of Lemma 2.2.18,which you can checkyourselves.It should be intuitively obvious(given our truth definition),butagain a strict proof by induction is possible(indicated in Exercise2.3.20).It has the consequence that when we writeM|=orM|=we only need to assume that M is an L-interpretation f

31、or somevocabulary L that includes the non-logical symbols in.23 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequenceA simplified notationLocality(with respect to free variables)also allows us tosimplify the notation for satisfaction.We writeM|=(x1,.,xn)a1,.,anwhen the

32、 free variables in are among x1,.,xn,and aiisassigned to xifor i=1,.,n.For example:M|=y(y,x1,.,xn)a1,.,an iffthere is b M s.t.M|=(y,x1,.,xn)b,a1,.,anOr even:M|=y y,a1,.,an iffthere is b M s.t.M|=b,a1,.,an24 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequenceChecking

33、truth in interpretationsUsing the truth definition,one can check step by step if aFOL sentence is true in an interpretation M or not.But in practice,using our informal understanding of whatquantified sentences mean is crucial for determining truth inmodels.Once you understand that,step by step check

34、ing with thetruth definition is more cumbersome,takes more time,andusually doesnt give a better understanding.But we need the formal definition when we want to prove byinduction general facts involving truth and satisfaction,as wewill see later.Back to some earlier examples:25 of 36FOL:terms and for

35、mulasFOL:informal semanticsFOL:formal semanticsFOL:consequence26 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequenceLogical consequence in FOLThis is eactly like consequence in PL!The only difference is that we are talking about FOL-sentences(notformulas!),and FOL-in

36、terpretations rather than PL-interpretations(i.e.valuations).Thus:Definition(FOL-consequence)is a logical consequence of,in symbols|=if no interpretation that makes all sentences in true also makes false.Or,more briefly as before:|=ifffor all M,M|=implies M|=27 of 36FOL:terms and formulasFOL:informa

37、l semanticsFOL:formal semanticsFOL:consequenceRelated logical notions exactly as beforeLet,be FOL-sentences and a set of FOL-sentences.I is logically true(|=)if is true in all interpretations;I and are logically equivalent()if they are truein the same interpretations;I is satisfiable if there is an

38、interpretation making allsentences in true.The notions can be defined in terms of each other.E.g.I|=iff is not satisfiable.I is satisfiable iff 6|=.Here is any contradictory FOL-sentence,e.g.x x 6=x.28 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequenceUseful equival

39、encesBesides those from PL,there are many FOL equivalences one shouldknow about(37)in Ch.2):defining in terms of and vice versa:distributing a quantifier in a conjunction or disjunction:same when one of the formulas doesnt contain the variable:and for implication:29 of 36FOL:terms and formulasFOL:in

40、formal semanticsFOL:formal semanticsFOL:consequenceLets check the implication case:30 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequenceMore equivalences quantifier switch:bound variable change:The following facts are also useful:Suppose c is an individual constant

41、not occurring in or in(x)or.Then we have:IIf,(c)?,then,x(x)?.IIf?(c),then?x(x).31 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequenceCheck:if?(c)then?x(x)Suppose the vocabulary of and(x)is L.Assume?(c).Let M bean L-interpretation such that M|=.We must show M|=x(x).32

42、 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequencePrenex normal form(Exercise 2.3.13)Using the equivalences that we listed,one can transform everyFOL-sentence into an equivalent one in prenex normal form:All the quantifiers come first,and then a quantifier-freeform

43、ula.Here is an example:xPx x(Qx yRxy)xPx z(Qz yRzy)x(Px z(Qz yRzy)xz(Px (Qz yRzy)xz(Px y(Qz Rzy)xzy(Px (Qz Rzy)33 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequenceNext week:Monday:Chapter 3.1 3.2Thursday:Chapter 3.334 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequence35 of 36FOL:terms and formulasFOL:informal semanticsFOL:formal semanticsFOL:consequence36 of 36