Predicate (First-Order) Logic

Why propositional logic is not enough, the syntax of first-order logic (constants, variables, predicates, functions, quantifiers), semantics over a domain, translating English sentences (and the classic ∀/→ and ∃/∧ pattern), quantifier negation and ordering, valid equivalences, prenex form and Skolemisation, unification and the most general unifier, and first-order resolution and chaining.

Why first-order logic?

Propositional logic needs a separate symbol for every fact: "Socrates is mortal", "Plato is mortal", … and cannot say "all men are mortal" in one sentence. First-order logic (FOL), also called predicate logic, talks about objects, their properties and relations, with quantifiers over all objects.

Syntax

Element	Examples	Denotes
Constants	`Ravi`, `2`, `Delhi`	specific objects
Variables	$x, y, z$	arbitrary objects
Functions	$\text{Father}(x)$ , $x + 1$	maps objects to objects (a term)
Predicates	$\text{Student}(x)$ , $\text{Loves}(x, y)$ , $x > y$	properties/relations (true or false)
Connectives	$\neg, \wedge, \vee, \to, \leftrightarrow$	as in propositional logic
Quantifiers	$\forall x$ (for all), $\exists x$ (there exists)
Equality	$t_1 = t_2$

Terms (constants, variables, function applications) denote objects; atomic sentences apply a predicate to terms. A variable is bound if it is in the scope of a quantifier, otherwise free; a sentence has no free variables.

Semantics

An interpretation fixes a non-empty domain of objects and maps constants to objects, functions to functions, predicates to relations. Then:

$\forall x\,\varphi$ is true iff $\varphi$ is true for every object assigned to $x$ ;
$\exists x\,\varphi$ is true iff $\varphi$ is true for at least one object.

Translating English

English	FOL
Everyone loves someone	$\forall x\,\exists y\,\text{Loves}(x, y)$
Someone is loved by everyone	$\exists y\,\forall x\,\text{Loves}(x, y)$
Every student takes at least one course	$\forall x\,(\text{Student}(x) \to \exists c\,(\text{Course}(c) \wedge \text{Takes}(x, c)))$
There is exactly one president	$\exists x\,(\text{Pres}(x) \wedge \forall y\,(\text{Pres}(y) \to y = x))$
Not every bird flies	$\neg\forall x\,(\text{Bird}(x) \to \text{Flies}(x)) \equiv \exists x\,(\text{Bird}(x) \wedge \neg\text{Flies}(x))$

Equivalences

Rule	Equivalence
Quantifier negation	$\neg\forall x\,\varphi \equiv \exists x\,\neg\varphi$ ; $\neg\exists x\,\varphi \equiv \forall x\,\neg\varphi$
Distribution	$\forall x\,(\varphi \wedge \psi) \equiv \forall x\,\varphi \wedge \forall x\,\psi$ ; $\exists x\,(\varphi \vee \psi) \equiv \exists x\,\varphi \vee \exists x\,\psi$
Not distributive	$\forall x\,(\varphi \vee \psi) \not\equiv \forall x\,\varphi \vee \forall x\,\psi$ ; $\exists x\,(\varphi \wedge \psi) \not\equiv \exists x\,\varphi \wedge \exists x\,\psi$
Same quantifiers commute	$\forall x\,\forall y \equiv \forall y\,\forall x$ ; $\exists x\,\exists y \equiv \exists y\,\exists x$
Scope ( $x$ not free in $\psi$ )	$\forall x\,(\varphi \to \psi) \equiv (\exists x\,\varphi) \to \psi$

Normal forms for inference

To use resolution, convert sentences to clausal form:

Eliminate $\leftrightarrow$ and $\to$ .
Move $\neg$ inwards (including quantifier negation).
Standardise variables apart (distinct names for distinct quantifiers).
Skolemise: replace each existential variable by a new constant (if not inside any $\forall$ ) or a new function of the enclosing universal variables.
Drop the universal quantifiers (all remaining variables are implicitly universal).
Distribute $\vee$ over $\wedge$ to get CNF clauses.

Unification

To apply inference rules, find a substitution $\theta$ making two expressions identical. The most general unifier (MGU) commits as little as possible.

Expressions	MGU
$\text{Knows}(\text{John}, x)$ , $\text{Knows}(\text{John}, \text{Jane})$	$\{x/\text{Jane}\}$
$\text{Knows}(\text{John}, x)$ , $\text{Knows}(y, \text{Bill})$	$\{x/\text{Bill}, y/\text{John}\}$
$\text{Knows}(\text{John}, x)$ , $\text{Knows}(y, \text{Mother}(y))$	$\{y/\text{John}, x/\text{Mother}(\text{John})\}$
$\text{Knows}(\text{John}, x)$ , $\text{Knows}(x, \text{Elizabeth})$	fail (standardise apart first: then $\{x_1/\text{Elizabeth}, x_2/\text{John}\}$ )
$P(x)$ , $P(f(x))$	fail — occurs check ( $x$ cannot contain itself)

Inference in FOL

Generalised modus ponens: from $p_1', \dots, p_n'$ and $(p_1 \wedge \dots \wedge p_n \to q)$ , with $\theta$ unifying each $p_i'$ with $p_i$ , infer $q\theta$ . Basis of forward and backward chaining over definite clauses (Prolog, production systems).
Resolution with unification: from $(\ell \vee A)$ and $(\neg m \vee B)$ where $\theta = \text{MGU}(\ell, m)$ , infer $(A \vee B)\theta$ . Refutation-complete: if KB $\models \alpha$ , resolution on KB $\wedge \neg\alpha$ derives the empty clause.

Decidability: entailment in FOL is only semi-decidable — if KB $\models \alpha$ , a complete procedure eventually proves it, but if not, it may run forever.

Predicate (First-Order) Logic

Why first-order logic?

Syntax

Semantics

Translating English

Equivalences

Normal forms for inference

Unification

Inference in FOL

Quick revision

Practice questions