Metalevel LogicExamplesNaming WordsNaming ExpressionsBasic MetavocabularyWordsTermsSentencesTruth RelationParadoxesSubstitutionMetalevel Logic ExampleKripke-Gilmore-Perlis SolutionLogic of BeliefAxiomsLogics of BeliefMetalevel LogicComputational Logic Lecture 18Michael Genesereth Spring 200201/14/19 2ExamplesSentences about SyntaxThe expression “John likes Mary” is a sentence.Truth of SentencesThe sentence “John likes Mary” is true.Reasoning HintsTo prove completeness, first prove the lifting lemma.01/14/19 3Naming WordsName-referent confusionlarge(john)small (john)Separate NamesQuotationlarge(john)small(‘john’)medium(“john”)01/14/19 4Naming ExpressionsBy crossing out rows, it is possible to find interpretationsimplicit in a set of sentences.01/14/19 5Basic Metavocabularyoperator() - the object denoted by is an operator.variable() - the object denoted by is a variable.objconst() - the object denoted by is an object constant.funconst() - the object denoted by is a function constant.relconst() - the object denoted by is a relation constant.arity() - denotes the arity of object denoted by .operator(‘’) variable(“x”)operator(“”) objconst(“john”)operator(“”) funconst(“father”)operator(“”) relconst(“parent”)operator(“”) arity(“father”)=1operator(“”) arity(“parent”)=201/14/19 6Wordsword(x) variable(x)\vee constant(x)\vee operator(x)01/14/19 7Termsterm(x) variable(x)\vee objconst(x)\vee funterm(x)funterm(f.l)\Leftarrow funconst(f)\wedge termlist(l)termlist(nil)termlist(x.l)\Leftarrow term(x)\wedge termlist(l)&Term(``Father(John)")?&Funterm(``Father(John)")?&Funterm(``Father".(``John".Nil))?&Funconst(‘Father’)\wedge Termlist(``John".Nil)?&Termlist(``John".Nil)?&Term(``John")\wedge Termlist(Nil)?&Termlist(Nil)?&Success01/14/19 8Sentencesrelsent(r.l)\Leftarrow relconst(r)\wedge termlist(l)$Negation(``\neg\overline{p}")\Leftarrow Sentence(p)$\cr$Conjunction(``\overline{p}\wedge\overline{q}")\Leftarrow Sentence(p)\wedge Sentence(q)$\cr$Disjunction(``\overline{p}\vee\overline{q}")\Leftarrow Sentence(p)\wedge Sentence(q)$\cr\cr$Unisent(``\forall\overline{v}.\overline{p}")\LeftarrowVariable(v)\wedge Sentence(p)$\cr$Exisent(``\exists\overline{v}.\overline{p}")\LeftarrowVariable(v)\wedge Sentence(p)$\cr}sentence(x) relsent(x)\vee negation(x)\vee\ldots Exisent(x)$\cr01/14/19 9Truth RelationBasic Vocabularytrue(‘’) means that the sentence is true.Semantics via axiom schematrue(‘’) Sadly, this leads to paradoxes.01/14/19 10ParadoxesDefinition:A paradox is a sentence that is neither true nor false.Examples:I am a liar.This sentence is false.01/14/19 11Substitutionsub(x,y,y)=xsub(x,y,z)=z word(z) yzsub(x,y,z.l)=sub(x,y,z).sub(x,y,l)sub(“a”, “b”, “p(a,b)”)sub (“a”, “b”,“p”.“a”.“b”. nil)sub (“a”, “b”,“p”). sub(“a”,“b”,“a”.“b”. nil)“p”. sub(“a”,“b”,“a”.“b”. nil)“p”. sub(“a”, “b”, “a"). sub(“a”,“b”,“b”. nil)“p”. “a”. sub(“a”, “b”,“b”. nil)“p”. “a”. sub(“a”, “b”,“b”).sub(“a”,“b”,nil)“p”. “a”. “a”. sub(“a”,“b”,nil)“p”. “a”. “a”. nil“p(a,a)”01/14/19 12Metalevel Logic Exampletrue(sub(&Q(`sub(q(x),`x’,`\neg Tr(\overline{x})")"),\cr &``x",\cr &``\neg Tr(Sub(Q(x),``x",``\neg Tr(\overline{x})"))"))\cr}$Tr(``\neg Tr(Sub(&Q(``Sub(Q(x),``x",``\neg Tr(\overline{x})")"), &``x",\cr &``\neg Tr(\overline{``Sub(Q(x),``x",``\negTr(\overline{x})")"})"))")\cr}Tr(``\neg Tr(Sub(&Q(``Sub(Q(x),``x",``\neg Tr(\overline{x})")"),\cr &``x",\cr &``\neg Tr(Sub(Q(x),``x",``\neg Tr(\overline{x})"))"))")\cr}$\neg Tr(Sub(&Q(``Sub(Q(x),``x",``\neg Tr(\overline{x})")"),\cr &``x",\cr &``\neg Tr(Sub(Q(x),``x",``\neg Tr(\overline{x})"))"))01/14/19 13Kripke-Gilmore-Perlis SolutionAxiom Schema KGP:\par$Tr(\phi)\Leftrightarrow*[\phi]$\par\bigskip\bigskipwhere $*[\phi]$ is $\phi$ with negations pushed all the way in:\par\halign{\strut#\hfil\cr$*[\neg\neg\phi]=\phi$\cr$*[\neg(\phi\wedge\psi)]=\neg\phi\vee\neg\psi$\cr$*[\neg(\phi\vee\psi)]=\neg\phi\wedge\neg\psi$\cr$*[\neg\forall\nu.\phi]=\exists\nu.\phi$\cr$*[\neg\exists\nu.\phi]=\forall\nu.\phi$\cr$*[-Tr(``\phi")]=Tr(``\neg\phi")$\cr$*[Tr(``-phi")]=Tr(``-phi")$\cr}\bigskip\bigskip\bigskipExample:\par\halign{\strut#\hfil\quad&#\hfil\cr &$Tr(``-P => -Tr(``P")")$\cr\crXXX&$-P => -Tr(``P")$\cr\cr &$-P => Tr(``-P")$\cr}\bigskip\bigskip\bigskip\theorem{Theorem}{If $\Delta$ is a consistent set of sentences with no occurrences of the $Tr$relation constant, then there is a model of $\Delta\cup\{KGP\}$.}\vfill\eject01/14/19 14Logic of BeliefVocabulary:b(,) means that the agent denoted by the term believes the sentence denoted by the term .Examples:01/14/19 15Axioms1. Tautologies &$\forall p.(Provable(p,Setof())\Rightarrow B(a,p))$\cr2.&Distribution\cr &$\forall p.\forall q.(B(a,p)\wedgeB(a,``\overline{p}\Rightarrow\overline{q}")\Rightarrow B(a,q))$\cr3.&Knowledge\cr &$B(a,\phi)\Rightarrow\phi$\cr4.&Positive Introspection\cr &$\forall p.(B(a,p)\Rightarrow B(a,``B(a,\overline{p})"))$\cr5.&Negative Introspection\cr &$\forall p.(\neg B(a,p)\Rightarrow B(a,``\neg B(a,\overline{p})"))01/14/19 16Logics of
View Full Document
Unlocking...