Interpretations and models: a review

We went through an activity to reinforce interpretations and models from last class.

Tautologies, contradictions and SAT in first order logic

We saw the importance of tautologies in our investigations into propositional logic. Recall: For propositional logic, formula F has only a finite number of possible interpretations, so we had the option of proof by exhaution - explicitly checking F for every possible interpretation. In the same way, we could check for F being a contradiction (false for every interpretation) or SAT solve (find an interpretation satisfying F) by testing all possible interpretations, one by one. For first order logic this is not, in general, possible. Why? Because there are infinitely many possible interpretations. This leaves us with two options, both of which are big topics:

• We can rely on deduction to discover new truths.
• We can restrict the constants, functions, predicates and the formulas that define their behavior (called axioms) to some set where more direct ways of SAT solving or tautology checking are possible. Such a restriction is called a theory.

Deduction in first order logic: Part 2

Now that we know about functions, we can give a more extensive list of what deductions are allowed in first order logic. Here are a few more standard deductions that can be made in first order logic.

1. expressions involving only functions, constants and variables that are syntactically identical can be assumed to describe the same object (with the technical detail that the variables have to be the same in terms of scope, i.e. if variable x appears in the two expressions, we need to be in the same scope with respect to x). Here some examples:

   P(x,f(c,x)) => ¬Q(g(f(c,x))) ∧ ∀x[P(f(c,x),x)]
       \____/          \____/          \____/
            \_ same!___/               different because 'x' is a new variable here!	  

2. predicate expressions that are syntacticaly identical can be assumed to have the same true/false value (with the same caveat as in the previous item)

   P(foo,bar) => (Q(foo) ∨ P(foo,bar))
   \________/              \________/
            \____same!_____/	  

3. propositional simplifications/rewritings are allowed in any context, treating each distinct predicate expression or quantified subformula as a propositional variable. Here is an example:

   1: ∀x[ ¬R(x,c) ∨ Q(c) ] 
   2: ∀x[ R(x,c) => Q(c) ]     [Impliction rewriting of 1]
   	  

4. propositional deductions are allowed when the "facts" are either not inside any quantifiers, or inside only a "forall" block, treating each distinct predicate expression or quantified subformula as a propositional variable. Here is an example:

   1: R(a,f(b)) => Q(b,a)
   2: R(a,f(b))
   3: Q(b,a)              [Modus Ponens on 1 and 2]
   	  

5. specialization: "if F is true for all possible values of x, then it must be true for x taking on the value e specifically".
   If ∀x [F] is known to be true, where no quantifiers in F introduce a new scope for the name x, and e is a function/constant expression such that no constant contained in e has the same name as a variable introduced by a quantifier in F, then the formula we get by replacing all occurences of x with e inside of F is true.

   1: ∀x[inClass(x,HH215) => isSleepy(x)]
   2: inClass(Joe,HH215) => isSleepy(Joe)     [specializing x to Joe in 1]	  

6. existential introduction: "If F is true and contains expression e, then ∃x[G] is true where G is F with e's replaced with x's".
   If formula F is known to be true, exp is a function/constant expression in F, and x is a new variable (i.e. does not occur inside F), then letting F* be the result of replacing some or all occurences of exp with the variable x, the formula ∃x[F*] is true. For example, if F := P(f(a),b) => Q(c,f(a)) ∧ R(f(a)) is known to be true, and we let exp := f(a) and our new variable is z, then we could deduce ∃z[P(z,b) => Q(c,z) ∧ R(z)].

   1: friends(alice,mother(bob)) ∧ enemies(mother(bob),cathy)  [Given]
   2: ∃z[friends(alice,z) ∧ enemies(z,cathy)]                  [Existential intro. on 1 using z for mother(bob)]
   	  

Examples of proofs with first-order logic deductions

Now we can prove something a bit more complicated ... like the fact that the mother of Socrates is mortal. Note that this requires us to specialize a universally quantified variable not to a constant, but to the function expression mother(socrates).

Given: ∀x [IsHuman(x) => IsMortal(x)], ∀y [IsHuman(y) => IsHuman(mother(y))], and IsHuman(socrates)
Prove: IsMortal(mother(socrates))
1: ∀y [IsHuman(y) => IsHuman(mother(y))]                   [given]
2: IsHuman(socrates)                                       [given]
3: IsHuman(socrates) => IsHuman(mother(socrates))          [specializing y to socrates in 1]
4: IsHuman(mother(socrates))                               [modus ponens with 3 and 2]
5: ∀x [IsHuman(x) => IsMortal(x)]                          [given]
6: IsHuman(mother(socrates)) => IsMortal(mother(socrates)) [specializing x to mother(socrates) in 5]
7: IsMortal(mother(socrates))                              [modus ponens with 6 and 4]
	

Finally, we will look at a proof that has us using existential introduction:

Given:  ∀x [∃y [ChildOf(y,x)] => IsWorried(x)], and ChildOf(steve,socrates)
Prove: IsWorried(socrates)
1: ∀x [∃y [ChildOf(y,x)] => IsWorried(x)]            [given]
2: ∃y [ChildOf(y,socrates)] => IsWorried(socrates)   [specializing x to socrates in 1]
3: ChildOf(steve,socrates)                           [given]
4: ∃y [ChildOf(y,socrates)]                          [existential introduction on 3 using y for steve]
5: IsWorried(socrates)                               [modus ponens on 2 and 4]