First Order Logic

Motivation

Background — Propositional logic is simple, but it lacks expressive power.¹1. First Order Logic is the standard formal language of mathematics and is expressive enough to define almost any rule-based system. In propositional logic, to say “All men are mortal”, we would need to write a separate proposition for every single human.

First Order Logic (FOL): A logic that assumes the world contains Objects (people, houses, numbers), Relations (red, round, brother of), and Functions (father of, best friend).

Syntax and Semantics

Basic Elements

• Constants: Specific objects (e.g., KingJohn, 2, CS4200).
• Predicates: Relations that return true or false (e.g., Brother(Richard, John), > (3, 2)).
• Functions: Relations that return exactly one object (e.g., LeftLegOf(John)).
• Variables: Placeholders for objects (e.g., x, y).
• Connectives: Same as propositional (\land, \lor, \neg, \implies, \iff).

Quantifiers

Allow us to express properties of entire collections of objects.

• Universal Quantifier (\forall): “For all”. True if the sentence is true for every possible object.
  • Typically paired with \implies.
  • e.g., \forall x \text{ King}(x) \implies \text{Person}(x)
• Existential Quantifier (\exists): “There exists”. True if the sentence is true for at least one object.
  • Typically paired with \land.
  • e.g., \exists x \text{ Crown}(x) \land \text{OnHead}(x, KingJohn)

Inference in FOL

Inference in FOL is harder than propositional logic because of variables. We need ways to instantiate variables with objects.

Unification

Finding a substitution that makes two different logical expressions look identical.²2. Standard Unification algorithms must also include an “occurs check” to prevent recursive variable assignments like x / F(x).

UNIFY(Knows(John, x), Knows(John, Jane)) = {x / Jane}
UNIFY(Knows(John, x), Knows(y, Bill)) = {x / Bill, y / John}

Generalized Modus Ponens (GMP)

An upgraded version of Modus Ponens that handles variables.³3. GMP is efficient because it takes one big step rather than requiring us to instantiate a rule with every single known object just to use regular Modus Ponens once.

If we have a rule P(x) \implies Q(x) and a fact P(John), GMP unifies x with John and immediately concludes Q(John).

Chaining

Forward Chaining

Start with the facts in the KB, apply rules that trigger, and add the new conclusions to the KB. Repeat until the goal is found.

• Data-driven (used in production systems).

Backward Chaining

Start with the goal, find rules that could prove it, and recursively try to prove the premises of those rules.

• Goal-driven (used in logic programming languages like Prolog).

Resolution for FOL

Just like in propositional logic, we can use Resolution for a complete inference procedure, but we must first convert FOL sentences into Conjunctive Normal Form (CNF).

Steps to CNF:

1. Eliminate \iff and \implies.
2. Move \neg inwards.
3. Standardize variables (ensure each quantifier uses a unique variable name).
4. Skolemize: Replace existential quantifiers with Skolem constants or Skolem functions.
5. Drop universal quantifiers (assume all remaining variables are universally quantified).
6. Distribute \lor over \land.