1Metalevel LogicTim HinrichsCS 157May 19, 20052Metalevel Logic• Propositional Logic– No quantifiers, e.g. p ∧ q ⇒ r• First-order (Relational) Logic– Quantify over single elements ∀xyz.(p(x,y) ∧ p(y,z) ⇒ p(x,z))• Metalevel Logic– Quantify over first-order sentences∀x. sentence(x) ⇒ p(x, “r(e,b)”)3Metalevel Logic• Metalevel logic allows one to writesentences about first-order sentences.p(“q(a,b)”)relation(x) ⇒ p(x, “r(e,b)”)• Those descriptions can be asserted truetrue(“q(a,b)”)4Joe vs. “Joe”• Joe is a tall man, say 6’4”tall(Joe)• The symbol Joe is short, only 3 letters longshort(“Joe”)5Objective• Given a baselevel, first-order language LB,construct a disjoint first-order language LMsuch that1. Sentences in LB can be described in LM2. Such sentences can be asserted true3. Including such descriptions in a knowledge basehas the same effect as adding the describedsentences themselves.6Overview• Expression Descriptions• Finite Describability• true Sentences• Example• Formal Properties• Proof Procedures7Expression Descriptions• How might we state q is true of thissentence?p(a) ∧ p(b)• One idea: use stringsq(“p(a) ∧ p(b)”)– What if we wanted to existentially quantify p?8Expression Descriptions• Constructor functionsq(and(relnSent(“p”, “a”), relnSent(“p”, “b”)))• Quantification is then easy.∃x.q(and(relnSent(x, “a”), relnSent(x, “b”)))• “p” is just an object constant that happens tobe spelled using quotes9Types• It is useful to distinguish between variablesand relation, function, and object constants. relation(“p”) function(“f”) object(“a”) variable(“x”) relation(“q”) function(“g”) object(“b”) variable(“y”) function(“h”) variable(“z”) …10The Language LM• relations of LB: {r1,….,rk}functions of LB: {f1,…,fm}objects of LB: {c1,…,cn}variables of LB: {x1,…,xh,…}• relations of LM: {true, relation, function, object, variable, =}functions of LM: {and, or, not, impl, forall, exists, relnSent, funcTerm}objects of LM: {“r1”,…, “rk”, “f1”,…, “fm”,“c1”, …, “cn”, “x1”,…, “xh”,…}11Syntactic Sugar• Constructor functions are hard to read. Thestrings are prettier, but less functional.• Use the strings as syntactic sugar, i.e. macros“p(a)” means relnSent(“p”, “a”)• Escape the quotes for quantification, etc.“<p>(a)” means relnSent(p, “a”)12Example 1• State that p is reflexive, symmetric, transitivep(x,x)p(x,y) ⇒ p(y,x)p(x,y) ∧ p(y,z) ⇒ p(x,z)• rst is true of reflexive, symmetric, transitivesentencesrelation(r) ⇒ rst(“<r>(x,x)”)relation(r) ⇒ rst(“<r>(x,y) ⇒ <r>(y,x)”)relation(r) ⇒ rst(“<r>(x,y) ∧<r>(y,z) ⇒ <r>(x,z)”)13Example 2: Sentencesterm(x) ⇐ object(x) ∨ variable(x) ∨ funcExpr(x)funcExpr( funcTerm(y, z1, z2) ) ⇐function(y) ∧ term(z1) ∧ term(z2)atom( relnSent(y, z1, z2) ) ⇐relation(y) ∧ term(z1) ∧ term(z2)14Example 2: Sentences (2)sentence(x) ⇐atom(x) ∨(x=and(y,z) ∧ sentence(y) ∧ sentence(z)) ∨(x=or(y,z) ∧ sentence(y) ∧ sentence(z)) ∨(x=not(y) ∧ sentence(y)) ∨(x=impl(y,z) ∧ sentence(y) ∧ sentence(z)) ∨(x=forall(y,z) ∧ variable(y) ∧ sentence(z)) ∨(x=exists(y,z) ∧ variable(y) ∧ sentence(z))15Axioms ΓM (1-4)• Naturally we want to ensure that LB-sentencedescriptions that look different are unequal.• Constructor functions: and, not, or, impl, forall,exists, relnSent, funcTerm1. “σ1” ≠ “σ2”, σ1 and σ2 are distinct pairs of constantsand variables in LB.2. ∀x.c(x) ≠ “σ”, c is a constructor function3. ∀xy.c(x) = c(y) ⇒ x = y4. ∀xy.c1(x) ≠ c2(y)16Axioms ΓM (5-6)• Definitions for the types relation, function,object, variable.5. relation(“σ”), σ is a relation constant in LB¬relation(“σ”), σ is a function, object, variable• Likewise for function, object, variable6. ¬relation(c(x)), c is a constructor function.• Likewise for function, object, variable17Designators• A designator names a set of LB-sentences using adistinguished, unary relation.relation(r) ⇒ d(“<r>(x,x)”)relation(r) ⇒ d(“<r>(x,y) ⇒ <r>(y,x)”)relation(r) ⇒ d(“<r>(x,y) ∧<r>(y,z) ⇒ <r>(x,z)”)• Want negations entailed as well, e.g. ¬d(“Ax.p(x)”)d(z) ⇔ ∃r. (relation(r) ∧z= “<r>(x,x)” ∨z= “<r>(x,y) ⇒ <r>(y,x)” ∨z=“<r>(x,y) ∧<r>(y,z) ⇒ <r>(x,z)”)18Designators, Formally• Designator: a designator for a set of LB-sentences Δ is a set of LM-sentences D witha distinguished, unary relation d such that– for every LB-sentence ϕ in Δ, ΓM ∪ D |= d(ϕ)– for every LB-sentence ϕ not in Δ, ΓM ∪ D |=¬d(ϕ)19true Sentences• Describing a set of sentences with a designator isonly useful if we can assert those sentences true.• Description: Let D be a designator for Δ withdistinguished relation d. A description for Δ isD ∪ {d(x) ⇒ true(x)}20Axiomatizing true• For every sentence ϕ, includetrue(“ϕ”) ⇔ ϕ• Examplestrue(“p(a,b)”)relation(r) ⇒ true(“<r>(x,x)”)true(“true(p(a,b))”)true(“¬true(p(a,b))”)21Paradoxes• “This sentence is false.”• Are either of the following consistent?true(“This sentence is false.”)¬true(“This sentence is false.”)• Relies on self-reference and the embedding of true22Axiomatizing true (Ver. 2)• For every LB-sentence ϕ, includetrue(“ϕ”) ⇔ ϕ• Examplestrue(“p(a)”) ⇔ p(a)true(“∀x.p(x)”) ⇔ ∀x.p(x)true(“p(x) ∨ q(x)”) ⇔ p(x) ∨ q(x)23Open Sentences and true• Open sentences are trouble.true(“p(x) ∨ q(x)”) ⇔ p(x) ∨ q(x)true(“p(x)”) ⇔ p(x)true(“q(x)”) ⇔ q(x)• Quickly get contradictions:true(“p(x) ∨ q(x)”)iff p(x) ∨ q(x)iff true(“p(x)”) ∨ true(“q(x)”)24Axiomatizing true (Ver. 3)• Include for each closed LB-sentence ϕ thefollowing axiom.true(“ϕ”) ⇔ ϕ• These axioms and ΓM comprise the set Γ.25Example• Unique-names axioms (for just f and a) :a ≠ f(a) f(a) ≠ f(f(a)) …a ≠ f(f(a)) f(a) ≠ f(f(f(a))) …a ≠ f(f(a)) f(a) ≠ f(f(f(f(a)))) …… … …26Example• Non-solution if we additionally include a ≠ ba ≠ ba ≠ f(x)f(x) ≠ f(y) ⇐ x ≠ y• Includes f(a) ≠ f(b)27SolutionfaTerm(“a”)faTerm(“f(<x>)”) ⇐ faTerm(x)d(“<x>≠<y>”) ⇐faTerm(x) ∧
View Full Document
Unlocking...