3. The language of first-order logic LESSON PLAN ******************************[Sept 14]****************************** Syntax of FOL Logical Symbols: meaning does not depend upon the application Punctuation: ( ) . Connectives: NOT OR AND ALL EXISTS = Variables: x, y, z, ... Nonlogical Symbols: Functions symbols (with fixed arity) Predicate symbols (with fixed arity) How are these combined? What is a "term"? variable function(variable,...) 0-ary function ALSO called a "constant", short for "constant function" What is a "formula"? Predicate(term,...) 0-ary predicate ALSO called a "proposition", short for "propositional symbol" term = term --- these called ATOMS or ATOMIC FORMULAS How do the other CONNECTIVES work? NOT, AND, OR, EXISTS, ALL Abbreviations: (A1 & A2 & ... & A) for (...((A1 & A1) & A3) & ... An) A=>B for (~A v B) About variables: SCOPE of a quantifier SENTENCE = formula with no "free variables" RENAMING - making every quantifier in a formula bind a different variable The MEANING of a sentence (or set of sentence) is relative to an INTERPRETATION J = (for J write German I) D = domain = some non-empty set - may be finite or infinite - may be countable (integers) or uncountable (reals) I[f_n] = a function from D^n to D Note: for constant, n = 0 I[P_n] = set of tuples from D^n = function from D^n -> {0,1} Note: for proposition, n = 0 Example: predicate: Cat constants: puff, fluff Start with interpretation with 2 cats. Is there an interpretation where |D| = 0? No. Is there an interpretation where |I[Cat]| = 0? Yes. Is there an interpretation where |D| = 1? Is there an interpretation where |D| > 2? add: function: mother Is there an interpretation of size 1? Of size 2? Of size 3? Infinite size? The non-logical symbols can have many different meanings, since they depend upon the interpretation. So how do we get them to mean what we want them to mean? We do this by writing a set of sentences (a THEORY), which will restrict us to INTERPRETATIONS where the THEORY is TRUE. There will still be many interpretations, but if the THEORY is DETAILED enough, then the differences between the interpretations WON'T MATTER to us. So we need to determine what it means for a SENTENCE is to be true according to an interpretation. Definition: A VARIABLE ASSIGNMENT u is a MAPPING FROM Variables -> D u[x] in D We will see how our rules for interpreting a sentence relative to an interpretation will CREATE specific variable assignments along the way. Definition: the denotation of a term t, written ||t||_J,u is if x is a variable ||x||_J,u = u[x] if t1...tn are terms an f is a function symbol, ||f(t1,...,tn)|| = I[f] ( ||t1||_J,u, .... ||tn||_J,u ) If A is formula with no free variables, then we write J |= A to mean that A is TRUE in the interpretation J, also stated as "J satisfies A". We will now DEFINE |= for an interpretation J and variable mapping u: ******************************[Sept 14]****************************** J,u |= P(t1...tn) iff J,u |= t1=t2 J,u |= ~A iff J,u |= (A & B) J,u |= (A V B) J,u |= Exists x . A iff J,u' |= A for some u' that differs from u by at most the assignment to x J,u |= All x . A PROPOSITION 1: If A has no free variables, then for any two variable assignments u, u' J,u |= A iff J,u' |= A PROOF: Evaluate A in both pairs in parallel. At any point in the evaluation where a quantifier appears for a variable x, let u* be the mapping that is a descendent of u, and u'* be the mapping that is a descendent of u'. When interpreting a quantifier for a variable x, choose u'* such that u'*[x] = u*[x]. Therefore, the denotation of any term in the first evaluation will be the same as the denotation of the term in the second evaluation. Since the interpretations are the same, the truth value of every subformula in the first evaluation will be the same as the truth value of the subformula in the second evaluation. In particular, A will receive the same truth value in both evaluations. PROPOSITION 2: If A has no free variables, J,u|=A for some u iff J,u|=A for all u PROOF: Suppose J,u|=A for some u. By Proposition 1, then for any other u', J,u'|=A. Therefore J,u|=A for all u. The reverse is immediate: since J,u|=A for all u, and there always are variable assignments, then certainly J,u|=A for some u. Definition: for A w/o free variables, J|=A iff for some u, J,u|=A. Definition: For a SET of sentences {S1,...,Sn} J|={S1,...,Sn} iff J|=S1 ... J|=Sn In this case, we say J is a LOGICAL MODEL of the set of sentences. LEMMA: J|={S1,...,Sn} iff J|=(S1 & ... & Sn) LOGICAL CONSEQUENCE A is a logical consequence of a sentence or set of sentences S iff every model of S is a model of A. Written: S |= A Some examples and NON-examples of logical consequence. P |= P v Q EXPLAIN WHY USING MODELS: Let I be any model of P. So, for any u, I,u|=P By definition of |= I,u |= P v Q iff I,u|=P or I,u|=Q Therefore I,u |= P v Q. Since PvQ has no free variables, I|=P Therefore P |= P v Q MORE INTERESTING EXAMPLE: {P, ~P v Q} |= Q (For simplicity, we'll not bother about the variable mapping u.) Choose any I such that I |= P I |= ~P v Q We know I |= ~P v Q iff I|=~P or I|=Q We know that I|=~P cannot hold, because I|=P holds. Therefore I|=Q holds. Since this is true for all models of {P, ~PvQ}, then {P, ~P v Q} |= Q QUANTIFIERS: A x . P(x) |= E x . P(x) DOMAIN MUST HAVE SOME INDIVIDUAL. A x . Man(x)=>Mortal(x) |=/= E x . Man(x) & Mortal(x) THERE IS AN INTERPRETATION WHERE THERE ARE NO MEN. EXPLAIN WHY USING MODELS {Color(auto1,blue), SameColor(auto1,auto2)} |=/= Color(auto2,blue) HOWEVER: {Blue(auto1), SameColor(auto1,auto2), A x,y,z . (Color(x,y) & SameColor(x,z)) => Color(z,y)} |=/= Color(auto2,blue) MORE DEFINITIONS: A sentence is satisfiable if it is true in some interpretation, and unsatisfiable if it is true in all interpretations. OBSERVATION: S |= A iff S U {~A} is unsatisfiable WHY IS THIS OBSERVATION IMPORTANT? It allows us to determine logical consequence by satisfiability testing. VALIDITY: A sentence is VALID if it is true in all interpretations. |= A OBSERVATION: |= A iff ~A is unsatisfiable RELATIONSHIP OF => and |=: For any FINITE set of formulas S = {A1,...,An}, S |= B iff |= (A1 & ... & An) => B Note: one of the homework problems is to write out the proof of this! ****** Inference: making implicit knowledge explicit. Deductive inference: process of computing the entailments (logical consequences) of a knowledge base KB. We write KB |- A If talking about different deductive processes, we may add a subscript to |-. While there are many possible |-, there is only one |= for FOL! A deductive systems is SOUND: if KB |- A then KB |= A A deductive systems is COMPLETE: if KB |= A then KB |- A What is an example a simple (but dumb) SOUND BUT INCOMPLETE INFERENCE PROCEDURE? - always say "no" - just look up A in KB - look to see if a sentence of the form A & ... is in the KB What is an example a simple (but dumb) UNSOUND BUT COMPLETE INFERENCE PROCEDURE? - always say "yes" - say "yes" unless ~A is in the KB ... HOW HARD IS IT TO DETERMINE LOGICAL CONSEQUENCE FOR FOL? Propositional case: There are proof systems that are SOUND and COMPLETE. Furthermore, these systems are DECIDABLE: if KB |=/= A, then the system can determine "Not a theorem". Note: this is much stronger than simply KB|-/- A Equivalently: if KB U {~A} is satisfiable, then algorithm can FIND A MODEL OF A. Determining satisfiability is ... NP-complete. Determining unsatisfiability in ... co-NP-complete. THEREFORE, determining LOGICAL CONSEQUENCE is ... co-NP Complete. THEREFORE, determining VALIDITY is ... co-NP Complete. For FOL: There are proof systems that are both SOUND and COMPLETE. HOWEVER, any SOUND and COMPLETE system is SEMI-DECIDABLE: if KB |= A, system will always find a proof. if KB |=/= A, the system may RUN FOREVER. Even if KB U {~A} is satisfiable, then algorithm might not be able to find a model. HOWEVER: if we are will to put on FIXED BOUND on the SIZE of the domain, then complete MODEL FINDING is possible. This "finite model" case was long considered UNINTERESTING to logicians, who were primarily concerned with using logic to FORMALIZE THE MATHEMATICS OF THE REAL NUMBERS. However, in AI and applications of CS, we OFTEN care about FINITE DOMAINS -- possibly large, but not INFINITE. This has led to an EXPLOSION in recent years of ALGORITHMS and APPLICATIONS based on MODEL FINDING, as we will see! But first -- an example of a theory that does deal with INFINITE sets, namely the natural numbers: There is a natural number 0. Every natural number a has a natural number successor, denoted by S(a). Intuitively, S(a) is a+1. There is no natural number whose successor is 0. Distinct natural numbers have distinct successors: if a =/= b, then S(a) =/= S(b). CLAIM: There is no finite model of these axioms! CLAIM: The integers are a model of these axioms! CLAIM: There are OTHER models of these axioms!