Logic (ch9)

35 flashcards · Mathematics · by J M COOPER

When is ∀X S(X) true?
• is true iff S(X) is true for all possible values of X • i.e. iff S(X) is true when we replace X in it by every object that exists
When is ∃X S(X) true?
• is true iff S(X) is true for at least one possible values of X • i.e. iff S(X) is true when we replace X in it by some object that exists
What do these mean? • ∀X in_room(X,jc_133_a) → taking_module(X,cs3105) • ∃X in_room(X,jc_133_a) ∧ teaching_module(X,cs3105) What happens if we swap → and ∧ ?
• ∀X in_room(X,jc_133_a) → taking_module(X,cs3105) everything that is in jc_133_a is taking cs3105 • ∃X in_room(X,jc_133_a) ∧ teaching_module(X,cs3105) there exists something in jc_133_a that is teaching cs3105 when swapped: • ∀X in_room(X,jc_133_a) ∧ taking_module(X,cs3105) • “everything is in this room and everything is taking module cs3105” • ∃X in_room(X,jc_133_a) → teaching_module(X,cs3105) • “there is something which is either not in this room or is teaching module cs3105” so take care
Does ∃X ∀Y S(X,Y) mean the same as ∀Y ∃X S(X,Y)?
∃X ∀Y S(X,Y) often doesn’t mean the same as ∀Y ∃X S(X,Y) e.g. ∃X∀Y Parent(X,Y) vs ∀Y ∃X Parent(X,Y) "there exists an X who is a parent to all Y" vs "For each and every Y, there exists a parent X"
In which combinations do the quantifiers mean the same? E.g write equivalent sentences for: ∀X ∀Y S(X,Y) ∃X∃Y S(X,Y) ∀X S(X) ¬∀X ¬S(X)
∀X ∀Y S(X,Y) always means the same as ∀Y ∀X S(X,Y) ∃X∃Y S(X,Y) always means the same as ∃Y ∃X S(X,Y) • ∀X S(X) always means the same as ¬∃X ¬S(X) if S(X) is true for all X, then there does not exist an X for which S(X) is not true. • ∃X S(X) always means the same as ¬∀X ¬S(X) if there exists an X for which S(X) is true, then it is not true that for all X S(X) is not true.
What is a model?
• “Models” represent contexts in which we can analyse truth of sentences - possible worlds? Contains ≥ 1 objects (domain elements) and relations among them Sentences are true (or false) with respect to a model and an interpretation
What is an interpretation?
An interpretation is an assignment of meaning to the symbols of a formal language. Statements in FOPL are defined in syntactic terms, and as such do not have any meaning until they are given some interpretation. links a set of sentences in FOPL and a model. • constant symbols → objects • function symbols → functions mapping tuples of objects to objects • predicate symbols → relations on those objects Sentences are true (or false) with respect to a model and an interpretation
When is an atomic sentence containing no variables true?
• An atomic sentence P(term1, . . . , termn) containing no variables is true iff the objects referred to by term1, . . . , termn satisfy relation referred to by P (Basically it is true, if P(X) is true, and X is not variable.)
Why are sentences of FOPL sometimes true and sometimes false, and what does this mean for automated reasoning?
• Sentences of FOPL are sometimes true and sometimes false depending on the model and the interpretation • So for Automated Reasoning, we don’t usually reason about sentences being true or false • We reason about things being always true • Either absolutely always true in any interpretation of any model or true in every interpretation which makes some other things true
Define entailment in FOL.
• If we have some “Knowledge Base” KB of a set of FOPL sentences • And another sentence S of FOPL then we say that KB “entails” S iff in any interpretation of any model that makes KB true, S must be true • written “KB ⊨ S”
What is Resolution?
A particular proof system that: • Works on FOPL sentences in clausal form - so we must convert to CNF • Is sound and complete
What are the characteristics of CNF?
Conjunctive Normal Form • sentences are conjunctions of clauses • each clause is a disjunction of literals • Can be done for any 1st order sentence
Why is inferential equivalence good enough when converting from FOL to CNF? Why don't we need full equivalence?
Because we are doing proofs by refutation. • We want to prove that whenever P is true, Q is true • Proof by refutation means we prove that we can’t have P true and Q false • I.e. we want to prove that P ⋀ ¬Q is unsatisfiable • Remember “CNF sentence unsatisfiable iff the original is unsatisfiable” • Convert P ⋀ ¬Q to CNF(P ⋀ ¬Q) • CNF(P ⋀ ¬Q) is unsatisfiable • iff P ⋀ ¬Q is unsatisfiable • iff Q follows from P
What is inferential equivalence?
a converted sentence is unsatisfiable iff the original is unsatisfiable
What is the CNF recipe for first order logic?
• Eliminate implications and other connectives except ⋀⋁¬ • Move negations inwards • Standardise quantified variable names apart • Skolemise • Drop universal quantifiers • Distribute ⋀ over ⋁ • Clean up 1, 0 etc for example 1. Eliminate biconditionals and implications: • Eliminate ⇔, replacing α ⇔ β with (α ⇒ β) ∧ (β ⇒ α). • Eliminate ⇒, replacing α ⇒ β with ¬α ∨ β. 2. Move ¬ inwards: • ¬(∀ x p) ≡ ∃ x ¬p, • ¬(∃ x p) ≡ ∀ x ¬p, • ¬(α ∨ β) ≡ ¬α ∧ ¬β, • ¬(α ∧ β) ≡ ¬α ∨ ¬β, • ¬¬α ≡ α. 3. Standardize…
How are existentially quantified variables replaced in the Skolemisation process?
replace existentially quantified variables • E.g. we replace an existential variable X in “∃X norwegian(X) ⋀ mathematician(X)” “there is an X which is norwegian and a mathematician • by a “skolem constant”, e.g. “skolem” “norwegian(skolem) ⋀ mathematician(skolem)” “object skolem is norwegian and a mathematician" the second statement implies the first (If the second is true, then we can set X = skolem in the first) If we KNOW the first statement is true in a model it does not
“∃X norwegian(X) ⋀ mathematician(X)” 2. “norwegian(skolem) ⋀ mathematician(skolem)” What does it mean if we know that the first statement is true in a model? And what should we do?
• It does not mean that the second must be true • skolem might not be an atom in this model • or skolem might be a Welsh psychologist • but maybe in this model object abel is a Norwegian mathematician • So make a new model in which the norwegian mathematician is called skolem • We are allowed to do this • So the two formulas are inferentially equivalent • there is a model for the first iff there is a model for the second
What is a skolem function?
• If an ∃ is inside one or more ∀ we have to make a new function, called a skolem function • arguments are the ∀ variables outside the ∃ • E.g. “every person has a mother” “∀X person(X) →∃Y mother(X,Y)” “∀X person(X) →mother(X,skolemf(X))” • We can’t use a skolem constant, because no one person is everybody’s mother! • We can think of skolemf as the function that takes an X and returns the object which is the mother of X
• Convert the following to CNF: ∀X[∀Y Pet(Y) ⇒ Loves(X,Y)] ⇒ [∃Y Loves(Y,X)]
∀X [∀Y Pet(Y) ⇒ Loves(X,Y)] ⇒ [∃Y Loves(Y,X)] ∀X ¬ [∀Y (¬Pet(Y) ∨ Loves(X,Y))] ∨ [∃Y Loves(Y,X)] ∀X [∃ Y Pet(Y) ∧ ¬Loves(X,Y)] ∨ [∃Y Loves(Y,X)] ∀X [∃ Y Pet(Y) ∧ ¬Loves(X,Y)] ∨ [∃Z Loves(Z,X)] ∀X [Pet(skolf1(X)) ∧ ¬Loves(X,skolf1(X))] ∨ Loves(skolf2(X),X) [Pet(skolf1(X)) ∧ ¬Loves(X,skolf1(X))] ∨ Loves(skolf2(X),X) [Pet(skolf1(X)) ∨ Loves(skolf2(X),X)] ∧ [¬Loves(X,skolf1(X)) ∨ Loves(skolf2(X),X)]
What is the CNF recipe for propositional logic?
• Eliminate implications and other connectives except ⋀⋁¬ • Move negations inwards • Distribute ⋀ over ⋁ • Clean up 1, 0 etc
Convert to FOL everyone who loves all pets is loved by someone
∀X[∀Y Pet(Y) ⇒ Loves(X,Y)] ⇒ [∃Y Loves(Y,X)]
Does this produce the empty clause?
• YES. a,b,c are constants so must refer to the same thing
Does this produce the empty clause?
NO! c does does not match with b so we can do nothing
Does this produce the empty clause?
YES! We can set X to any term so we can choose X = b • If we assign X = b and substitute we get P(a,b,c)
Does this produce the empty clause?
YES! We can set X to any term so we can choose X=skolf(b) • So we get P(a,scolf(b),c)
Does this produce the empty clause?
NO! We have to set X the same wherever it appears • If we set X = b we get P(a,b,b), if X=c we get P(a,c,c)
Does this produce the empty clause?
YES! We can set Y=a, X=f(a) • Gives ¬P(a,f(a),f(f(a)) and P(a,f(a),f(f(a))
Does this produce the empty clause?
NO! It fails the occurs check • A variable cannot be assigned a value in which it occurs itself • We would have to set X=f(X) but we are not allowed to do this
FOPL is semidecidable - what does this mean?
• If there is a proof then resolution is guaranteed to find it • If there is not a proof then resolution might never terminate • This is fundamental to FOPL and not resolution’s fault • It is known that there is no decision procedure for FOPL