```November 12

Logic

* Truth tables

A B | -A  A->B  -A->(A->B)
----+---------------------
T T | F    T       T
T F | F    F       T
F T | T    T       T
F F | T    T       T

*  Rules of Inference for Propositional Logic

- Idempotency	 fvf = f
f^f = f

- Commutativity    fvg = gvf
f^g = g^f
f<->g = g<->f

- Associativity    (fvg)vh = fv(gvh)
(f^g)^h = f^(g^h)

- Absorption       fv(f^g) = f
f^(fvg) = f

- Distributivity   f^(gvh) = (f^g)v(f^h)
fv(g^h) = (fvg)^(fvh)

- Tautology        fvg = f  if f is a tautology
f^g = g  if f is a tautology

- Unsatisfiability fvg = g  if f is unsatisfiable
f^g = f  if f is unsatisfiable

- Modus ponens:   A, A=>B   (antecedent, consequent)
-------
B
All men are mortal (Man => Mortal)
Socrates is a man  (Man)
----------------------------------
Socrates is mortal (Mortal)

- And introduction:  A, B
----
A^B

- Or introduction:   A
-
A, B, C, D, ...

- And elimination:   A^B^C^...^Z
-----------
A

- Double-Negation Elimination:   ~~A
---
A

- Unit Resolution:  A v B, ~B
---------
A

Today is either Tuesday or Thursday, Today is not Thursday
----------------------------------------------------------
Today is Tuesday

- Resolution:  A v B, ~B v C       ~A => B, B => C
-------------       ---------------
A v C                ~A => C

Today is Tuesday or Thursday
Today is not Thursday or tomorrow is Friday
-------------------------------------------
Today is Tuesday or tomorrow is Friday

* Propositional Logic vs. First-Order Predicate Calculus

PL - only propositions (symbols representing facts)
Only values True and False

First-Order Logic includes:

Objects:  peoples, numbers, places, ideas (atoms)
Relations: relationships between objects (predicates, T/F)
father(fred, mary)
Properties: properties of atoms (predicates, T/F)
red(ball)
Functions: father-of next, (any value in range)

*  FOPC

* Syntax

Constant symbols (Capitalized, Constants with no arguments)
Interpretation must map to exactly one object in the world
Predicates (can take arguments, True/False)
Interpretation maps to relationship or property T/F value
Function (can take arguments)
Maps to exactly one object in the world

* Definitions

Term
Anything that identifies an object
Function(args)
Constant (function with 0 args)

Atomic sentence
Predicate with term arguments
Bunny(Bugs)
Married(Father_Of(Alex), Mother_Of(Alex))

Literals
atomic sentences and negated atomic sentences

Connectives
^, v, ->, <=>, ~
if connected by "^", conjunction (components are conjuncts)
if connected by "v", disjunction (components are disjuncts)

Quantifiers
Universal Quantifier
How do we express "All unicorns speak English" in PL?
We have to specify proposition for each unicorn

FORALL is used to express facts and relationships that we know
to be true for all members of a group (objects in the world)

A variable is used in the place of an object
FORALL x, Unicorn(x) => SpeakEnglish(x)
The domain of x is the world
The scope of x is the statement following FORALL (sometimes in [])

Same as specifying
Unicorn(Uni1) => SpeakEnglish(Uni1) ^
Unicorn(Uni2) => SpeakEnglish(Uni2) ^
Unicorn(Uni3) => SpeakEnglish(Uni3) ^
...
Unicorn(Table1) => Table(Table1)    ^
...

One statement for each object in the world

We will leave variables lower case (sometimes ?x)
Notice that x ranges over all objects, not just unicorns.

A term with no variables is a "ground term"

Existential Quantifier
This makes a statement about some object (not named)

THERE EXISTS x, Bunny(x) ^ EatsCarrots(x)

means there exists some object in the world (at least one)
for which the statement is true.  Same as disjunction over
all objects in the world.

(Bunny(Bun1) ^ EatsCarrots(Bun1))   v
(Bunny(Bun2) ^ EatsCarrots(Bun2))   v
(Bunny(Bun3) ^ EatsCarrots(Bun3))   v
(Bunny(Bun4) ^ EatsCarrots(Bun4))   v
(Bunny(Bun5) ^ EatsCarrots(Bun5))   v
...
(Bunny(Table1) ^ EatsCarrots(Table1))   v
...

THERE EXISTS x, Unicorn(x) => SpeakEnglish(x)
?

Means implication applies to at least one object in the universe.

* Properties

FORALL x ~P   <=>   ~EXISTS x P
FORALL x P    <=>   ~EXISTS x ~P
~FORALL ~P    <=>   EXISTS x P
~FORALL x P   <=>   EXISTS x ~P

FORALL x LovesWatermelon(x)   <=>   ~EXISTS x ~LovesWatermelon(x)

(X => Y)   <=>   ~X v Y
Prove with truth table.

NOT TRUE:
(X => Y)   <=>   (Y => X)
This is a type of inference/learning that is not sound (abduction).

Examples

* All men are mortal

FORALL x [Man(x) => Mortal(x)]

* Socrates is a man.

Man(Socrates)

* Socrates is mortal

Mortal(Socrates)

Notice - if we could match Socrates with x, we could prove this
statement using Modus Ponens.  We would look at such a matching
(unification) later.

* All purple mushrooms are poisonous

FORALL x [(Purple(x) ^ Mushroom(x)) => Poisonous(x)]

* A mushroom is poisonous only if it is purple

FORALL x [(Mushroom(x) ^ Poisonous(x)) => Purple(x)]

* No purple mushroom is poisonous

~(EXISTS x [Purple(x) ^ Mushroom(x) ^ Poisonous(x)]

* There is exactly one mushroom

EXISTS x [Mushroom(x) ^ (FORALL y (NEQ(x, y) => ~Mushroom(y)))]

Because exactly one is difficult, we can use EXISTS! x
to denote exactly one object.

* Every city has a dog catcher who has been bitten by every dog in town.
Use City(1), DogCatcher(1), Bit(2), Lives(2)

FORALL a, b [City(a) => EXISTS c {DogCatcher(c) ^
(Dog(b) ^ Lives(b,a) => Bit(b,c))}]

* No human enjoys golf

FORALL x [Human(x) => ~Enjoys(x, Golf)]

* Some professor that is not a historian writes programs

EXISTS x [Professor(x) ^ ~Historian(x) ^ Writes(x, Programs)]

* Every boy owns a dog

FORALL x EXISTS y [Boy(x) => Owns(x, y)]
EXISTS dog FORALL x [Boy(x) => Owns(x, y)]

Do these mean the same thing?

* Higher-order Logic

FOPC quantifies over objects in the universe.
Higher-order logic quantifies over relations and functions as well
as objects.

* All functions with a single argument return a value of 1.

FORALL x, y [Equal(x(y), 1)]

* Two objects are equal iff all properties applied to them are equivalent.

FORALL x, y [(x=y) <=> (FORALL p[p(x) <=> p(y)])]

Notice that we use "=" as a shorthand for equal.
equal means they are in fact the same object.

* Example Proof

The law says that it is a crime for an American to sell weapons to hostile
nations.  The country Nono, an enemy of America, has some missiles,
and all of its missiles were sold to it by Colonel West, who is American.

Prove:  West is a criminal.

Known:

1) FORALL x, y, z [(American(x) ^ Weapon(y) ^ Nation(z) ^ Hostile(z) ^
Sells(x,z,y)) => Criminal(x)]
It is a crime for an American to sell weapons to hostile nations

2) EXISTS x Owns(Nono, x) ^ Missile(x)
Nono has some missiles

3) FORALL x Owns(Nono,x) ^ Missile(x) => Sells(West,Nono,x)
All of its missiles were sold to it by Colonel West

4) FORALL x Missile(x) => Weapon(x)

5) FORALL x Enemy(x,America) => Histile(x)

6) American(West)

7) Nation(Nono)

8) Enemy(Nono,America)

9) Nation(America)

Proof:

10) Owns(Nono,M1) ^ Missile(M1)
2 ^ Existential Elimination

Existential Elimination
EXISTS v []
Substitute k for v anywhere in sentence, if k does not appear in []
k is a constant (term with no arguments)

(Skolemization)

11) Owns(Nono,M1)
10 ^ And-Elimination

12) Missile(M1)
10 ^ And-Elimination

13) Missile(M1) => Weapon(M1)
4 ^ Universal Elimination

Universal Elimination
FORALL v []
If true for universal variable v, true for a ground term
(term with no variables g)

14) Weapon(M1)
12, 13, Modus Ponens

15) Owns(Nono,M1) ^ Missile(M1) => Sells(West,Nono,M1)
3 ^ Universal Elimination

16) Sells(West,Nono,M1)
10, 15, Modus Ponens

17) American(West) ^ Weapon(M1) ^ Nation(Nono) ^ Hostile(Nono) ^
Wells(West,Nono,M1) => Criminal(West)
1 ^ Universal Elimination (x West) (y M1) (z Nono)

18) Enemy(Nono,America) => Hostile(Nono)
5 ^ Universal Elimination

19) Hostile(Nono)
8, 18, Modus Ponens

20) American(West) ^ Weapon(M1) ^ Nation(Nono) ^ Hostile(Nono) ^
Sells(West,Nono,M1)
6, 7, 14, 16, 19, And-Introduction

21) Criminal(West)
17, 20, Modus Ponens

Another rule:  Existential Introduction
If [..g..] true (where g is ground term)
then EXISTS v [..v..] true (v is substituted for g)

* Generalized Modus Ponens

If we have a rule

p1 ^ p2 ^ p3 ^ p4 ^ p5 ^ ... ^ pn => q
Each p involves universal / existential quantifiers

And we have each antecedent clause
p1(x)
p2(y)
...
pn(z)

And we can find a way to UNIFY the variables

Then we can infer q

Missile(x) ^ Owns(Nono,x) => Sells(West,Nono,x)

Missile(M1)
Owns(Nono,M1)

Must make sure that instantiations of x are the same

This process is "unification".
```