First-order logic
Professor Devin Balkcom
devin@cs.dartmouth.edu
office: Sudikoff 206
From Self-Reliance, Ralph Waldo Emerson:
$\forall x ((\operatorname{mind}(x) \wedge \operatorname{little}(x)) \Rightarrow \operatorname{hobgoblin}(x, consistency)$
What I think he meant to say was:
$\exists x (\operatorname{mind}(x) \wedge \operatorname{great}(x) \wedge \neg \operatorname{consistent}(x))$
Or even stronger:
$\operatorname{great}(x) \Rightarrow \neg \operatorname{consistent}(x)$
If great minds were precise, I guess he would have said "consistency is the hobgoblin only of little minds."
Proliferation of symbols:
$B_{11} \iff (P_{1,2} \vee P_{2, 1})$, ...
Can be imprecise and depend on context. "Spring":
Using natural language as communication assumes large knowldge base, and seems to require some probability based reasoning.
Most formal languages are procedural rather than declarative. You can have objects, but don't expect Java to reason about them automatically.
There are exceptions. Prolog can reason about statements like "All cars are red." (Constraint satisfaction and some formal logic tools are built-in to Prolog!)
We want something that:
First-order logic makes a stronger ontological commitment (what exists in the world) than propositional logic.
Propositional logic: facts that are true or false
First-order logic: objects, and relationships between them that hold (true) or do not hold (false).
You can think of first-order objects as graph vertices, and relationships as (hyper-)edges. Sentences constrain possible (hyper-)graph structures.
Propositional logic and first-order logic make a similar epistmiological commitment (degree of knowledge): true/false values.
Probabilistic reasoning allows values of $[0, 1]$: fact or relationship holds with probability $x$.
First-order logic includes:
Relation (binary): $\operatorname{siblings}(Leia, Luke)$
Property (a unary relation): $\operatorname{evil}(emperor)$
Function: $\operatorname{father}(Luke)$ is $DarthVader$
or equivalently,
$\operatorname{father}(Obiwon, Luke) = false$
$\operatorname{father}(Leia, Luke) = false$
$\operatorname{father}(DarthVader, Luke) = true$
Symbols: Richard, John, leftleg(Richard), leftleg(John), leftleg(leftleg(John)), ...
Three types of symbols:
Connectives: $\wedge | \vee | \Rightarrow | \Leftrightarrow | \neg$
Constant symbols: $A | X | John$
Equality: $=$ Two symbols
variables: x, y, z
Quantifiers: $\forall, \exists$; ways to refer to groups of objects.
sentences + (model, interpretation) $\mapsto$ true/false
interpretation is new, and makes use of the $=$ sign. Will come back to it.
Models, objects, relations
model: a set of true/false values for every relation among objects. (Think of a set of directed edges, with different colors for each relation, of graph.)
$r_1(O_1, O_2) = t$, $r_1(O_1, O_3) = f$, $r_1(O_2, O_1) = f$, ...
How many models?
For each binary relation (possible edge), there are $n^2$ possible object pairs (2-tuples), $n^3$ possible ternary relations, $n^k$ possible k-array relations.
That's just the number of tuples. Each can be true or false. So for each relation, we get a factor of $2^{n^k}$ models.
By the way, $n$ might be infinite. (Maybe the objects are natural numbers, which can be described in FOL.)
Computational complexity gets even worse. The syntax doesn't bind symbols to particular objects.
Symbols: Luke, DarthVader, Emperor, Palpatine, Anikin. Five symbols, but how many objects?
Intended interpretation
Multiple interpretations may be consistent with a set of first-order logic sentences. Need DarthV = Anikin.
Universal ($\forall$)
$\forall x \operatorname{king}(x) \Rightarrow \operatorname{person}(x)$
What it really means (universal instantiation):
$\operatorname{king}(John) \Rightarrow \operatorname{person}(John)$
($\wedge$) $\operatorname{king}(Richard) \Rightarrow \operatorname{person}(Richard)$
($\wedge$) $\operatorname{king}(crown) \Rightarrow \operatorname{person}(crown)$
Existential ($\exists$)
$\neg \exists x \operatorname{wise}(x) \wedge \operatorname{person}(x)$
What it really means (existential instantiation):
$\neg$ ( $(\operatorname{wise}(John) \wedge \operatorname{person}(John))$
$ \vee (\operatorname{wise}(Richard) \wedge \operatorname{person}(Richard))$
$\vee (\operatorname{wise}(crown) \wedge \operatorname{person}(crown))$ )
Instantiation gives simple proof that Demorgan's rules apply to quantifiers.
$\neg(A \wedge B \wedge C) \equiv \neg A \vee \neg B \vee \neg C$. So,
$\neg \forall x \operatorname{person}(x) \Rightarrow \operatorname{king}(x) \equiv$
$\exists x (\neg (\operatorname{person(x)} \Rightarrow \operatorname{king}(x))) \equiv$
$\exists x (\neg (\neg \operatorname{person}(x) \vee \operatorname{king}(x))) \equiv$
$\exists x (\operatorname{person}(x) \wedge \neg \operatorname{king}(x))$
Universal: usually with $\Rightarrow$, since $\vee$ or $\wedge$ too strong. Example:
$\forall x \operatorname{person}(X) \wedge \operatorname{king}(x)$
But as George Orwell said,
$\forall x \operatorname{animal}(x) \Rightarrow \operatorname{equal}(x)$
Existential: usually with $\wedge$. (Implication is usually too weak, since any false premise will satisfy the quantifier.)
The equality operator is used to indicate that two symbols refer to the same object.
"Every person has at least two brothers."
Wrong: $\forall x \exists y, z \operatorname{person}(x) \Rightarrow \operatorname{brother}(x, y) \wedge \operatorname{brother}(x, z)$
Correct: need to include $y \ne z$.
"Everybody loves somebody":
$\forall x \exists y \operatorname{loves(x, y)}$
"Everybody is loved by somebody":
$\forall x \exists y \operatorname{loves(y, x)}$
"There is somebody everybody loves":
$\exists y \forall x \operatorname{loves(x, y)}$
Numbers are good for counting, ordering, and measuring. Let's describe them with FOL.
So, $0$, $S(0)$, $S(S(0))$, $S(S(S(0)))$ all natural numbers.
Could call them 0, 1, 2, 3, 4, but not yet.
(3) and (4) describe the intended interpretation.
"$0$ is not the successor of any natural number, and no two natural numbers have the same successor.""
We want:
We need to rule out things like this:
One more function symbol, $+$, and two rules:
Additive identity: add 0 $\mapsto$ same number
Example: Compute $+( S(S(0)), S(S(S(0))) )$
Rule (6): move an $S$ from first term outwards:
$S(+( S(0), S(S(S(0))) ))$
Play it again, Sam:
$S(S(+( 0, S(S(S(0))) )))$
$S(S(+( 0, S(S(S(0))) )))$
Rule (5) says adding zero to a number gives that number, so we can remove the addition symbol from the inner part:
$S(S(S(S(S(0)))))$
Repeated applications of rule 5, followed by one application of rule 6, give us a machine to add any two natural numbers.
Awesome!
Modus ponens: $\frac{A \Rightarrow B \quad A}{B}$
Say we have the knowledge base:
$\forall x \, king(x) \wedge greedy(x) \Rightarrow evil(x)$
$king(John)$
$greedy(John)$
Want to show $evil(John)$. How?
Find a substitution $s$ (here $\{x / John \}$ so that:
$king(John) \wedge greedy(John) \Rightarrow evil(John)$
Idea #1: convert FOL to propositional logic by getting rid of quantifiers.
Universal instantiation: $\frac{\forall v \quad \alpha}{\operatorname{subst}(\{v/g\}, \alpha)}$,
for any variable $v$, sentence $\alpha$, any ground term $g$.
Existential instantiation: $\frac{\exists v \quad \alpha}{\operatorname{subst}(\{v/k\}, \alpha)}$,
for any variable $v$ and constant symbol $k$ that does not appear elsewhere.
Existential instantiation: $\frac{\exists v \quad \alpha}{\operatorname{subst}(\{v/k\}, \alpha)}$.
Example:
From $\exists crown(x) \wedge onhead(x, John)$
infer $crown(c_1) \wedge onhead(c_1, John)$
The new name $c_1$ is called the Skolem constant.
$\forall x \, king(x) \wedge greedy(x) \Rightarrow evil(x)$
$king(John)$
$greedy(John)$
Apply universal instantiation first, using all possible ground terms:
$king(John) \wedge greedy(John) \Rightarrow evil(John)$
$king(Richard) \wedge greedy(Richard) \Rightarrow evil(Richard)$
Now view $king(john)$, $greedy(john)$, etc, as propositional symbols.
Do we have a complete algorithm for entailment?
Function symbols can lead to infinite ground terms:
$0$, $S(S(0))$, $S(S(S(0)))$
Herbrands theorem (1930): if a sentence is entailed by the original FOL KB, then there exists a proof involving only a finite subset of the propositionalized KB.
Since any subset has a maximum depth of ground terms, generate all terms of depth 0, then depth 1 (BFS): $John, Richard, father(John)$, $father(Richard), father(father(John)), ...$
Propositionalization is complete: any entailed sentence can be proven.
But what if a sentence is not entailed?
It seems silly to generate $king(Richard)$ and $greedy(Richard)$ to prove $evil(John)$.
Unification and lifting: Find some $x$ such that $x$ is a king, and $x$ is greedy; infer that this $x$ is evil.
More generally, if there exists a substitution $\theta$ that makes the premise identical to sentences already in the KB, then we can infer the conclusion.
$\forall x \, king(x) \wedge greedy(x) \Rightarrow evil(x)$
$king(John)$
$\forall y \, greedy(y)$
We'd like to concluded Johhn is evil, since John is king, and everyone is greedy. We need a substitution for:
Apply $\{x / John\}$, $\{y/John\}$ to the implication premises $king(x)$, $greedy(x)$, and to the KB sentences $king(John)$ and $greedy(y)$.
For atomic sentences $p_i$, $p_i'$, and $q$, where there is a substitution $\theta$ s.t. $\operatorname{subst}(\theta, p_i') = \operatorname{subst}(\theta, p_i)$ for all $i$,
$$ \frac{p_1', p_2', ... p_n' \quad (p_1 \wedge p_2...\wedge p_n \Rightarrow q)}{\operatorname{subst}(\theta, q)}$$
GMP is an example of lifting: a first-order version of a propositional logic rule.
$\operatorname{unify}(knows(John, x), knows(John, Jane))$
$= \{x/Jane\}$
$\operatorname{unify}(knows(John, x), knows(y, Bill))$
$= \{x/Bill\}, \{y/John\}$
$\operatorname{unify}(knows(John, x), knows(y, mother(y)))$
$= \{y/John\}, \{x/mother(John)\}$
$\operatorname{unify}(knows(John, x), knows(x, Elizabeth)$
fails
John knows everybody. Everybody knows Elizabeth. Surely John knows Elizabeth? Why doesn't it work?
Need a new variable: standardize apart
Implement unification by standardizing apart, then exploring inputs side-by-side.
Resolution is expensive (even in prop logic), and sometimes you don't need it. Use GMP instead.
Datalog KB: no function symbols, first-order definite clauses:
$\forall x \, king(x) \wedge greedy(x) \Rightarrow evil(x)$
$\forall x \, \neg king(x) \vee \neg greedy(x) \vee evil(x)$
(From AIMA.) "The law says that it is a crime for an American to sell weapons to hostile nations. The country Nono, an enemy of America, and all of its missiles were sold to it by Colonel West, an American." Prove that West is a criminal.
$\exists \,x \, owns(Nono,x) \wedge missile(x)$. Not a definite clause. Skolemize and and-eliminate:
(From AIMA.) "The law says that it is a crime for an American to sell weapons to hostile nations. The country Nono, an enemy of America, and all of its missiles were sold to it by Colonel West, an American." Prove that West is a criminal.