Predicate Logic

Why we need more than propositional logic

Propositional logic treats whole statements as indivisible atoms: P, Q, R. That’s great for reasoning about fixed, named facts, but it doesn’t let you open up a statement and talk about its internal structure.

Consider the English statement:

• •“Every student in this class submitted an assignment.”

In propositional logic, you’d need one proposition per student (“Alice submitted”, “Bob submitted”, …) and then conjoin them all. That’s not scalable and it misses the structure that these are all instances of the same pattern.

Predicate logic (often called first-order logic, FOL) solves this by introducing:

1. 1)A domain of discourse: a nonempty set of objects we’re talking about.
2. 2)Variables that range over that domain.
3. 3)Predicates (relations) that say something about objects.
4. 4)Quantifiers to express “for all” (∀) and “there exists” (∃).

This is the language used by mathematics (“∀ε > 0 ∃N …”), by program specification (“∀i: 0 ≤ i < n → a[i] ≥ 0”), and by many formal methods tools.

The basic ingredients

Predicate logic is built from a small set of syntactic building blocks.

Domain of discourse

The domain (also called the universe) is the set over which variables range. It must be nonempty.

Examples:

• •Domain = all integers ℤ
• •Domain = all people in a database
• •Domain = all nodes in a graph

The same formula can mean different things under different domains.

Terms (naming objects)

A term denotes an element of the domain.

Terms come from:

• •Variables: x, y, z (range over the domain)
• •Constants: a, b, c (fixed named elements of the domain)
• •Function symbols: f(·), g(·,·) applied to terms

Examples of terms:

• •x
• •alice
• •parentOf(x)
• •add(x, 1)

Intuition: a term is like an expression that evaluates to “an object”.

Predicates / atomic formulas (stating facts)

A predicate is an n-ary relation symbol, like:

• •Human(·) (unary predicate)
• •Likes(·,·) (binary predicate)
• •LessThan(·,·)

When you apply a predicate to terms, you get an atomic formula:

• •Human(x)
• •Likes(alice, bob)
• •LessThan(x, add(y, 1))

An atomic formula evaluates to True/False once you know what the symbols mean in your domain.

Building complex formulas

From atomic formulas, you build larger formulas using the same connectives as propositional logic:

• •¬ (not)
• •∧ (and)
• •∨ (or)
• •→ (implies)
• •↔ (iff)

And you add quantifiers:

• •∀x φ (for all x, φ)
• •∃x φ (there exists an x such that φ)

Crucially, quantifiers bind variables (like how parentheses bind subexpressions). The part of the formula a quantifier controls is its scope.

Free vs bound variables

A variable occurrence is:

• •Bound if it is under a quantifier for that variable.
• •Free if it is not.

Example:

• •∀x (Human(x) → Mortal(x))
• •all occurrences of x are bound.
• •Human(x) → Mortal(x)
• •x is free.

A formula with no free variables is called a sentence. Sentences are what we typically evaluate as True/False in a model.

A quick semantics snapshot (what makes formulas “true”)

To interpret a predicate-logic language, you need:

• •A domain D (nonempty)
• •An interpretation of each constant as an element of D
• •An interpretation of each function symbol as a function on D
• •An interpretation of each predicate as a relation on D

Then:

• •∀x φ is True iff φ is True for every assignment of x ∈ D
• •∃x φ is True iff φ is True for some assignment of x ∈ D

This “assignment of variables” idea is why quantifiers are powerful: they quantify over all objects in the domain, not just those you named.

Table: how predicate logic extends propositional logic

Predicate logic keeps propositional logic’s connectives, but gives you a language to express structure and patterns over a domain.

Why quantifiers matter

Most statements we care about in math and software are inherently quantified:

• •“Every array index is in bounds.”
• •“There exists an input that triggers an error.”
• •“For every request, there exists a response.”

Quantifiers let you express these patterns directly. But they also introduce subtlety: the order and scope of quantifiers can change meaning dramatically.

Universal quantifier ∀ (for all)

The formula:

• •∀x φ(x)

means: “for every x in the domain, φ(x) is true.”

Example:

• •∀x (Student(x) → HasID(x))

This does not claim that every object is a student. It says: if an object is a student, then it has an ID.

A common pattern:

• •∀x (A(x) → B(x))

reads as: “All A’s are B’s.”

Existential quantifier ∃ (there exists)

The formula:

• •∃x φ(x)

means: “there exists some x in the domain such that φ(x) is true.”

Example:

• •∃x (Student(x) ∧ Late(x))

This asserts at least one student is late.

Scope: where a quantifier applies

Scope is usually controlled by parentheses.

Compare:

1) ∀x (P(x) → Q(x))

2) (∀x P(x)) → Q(x)

These are not the same.

• •In (1), x is local to the implication.
• •In (2), the antecedent says “P(x) holds for all x”, but Q(x) has x free (so (2) isn’t even a sentence unless Q doesn’t mention x). Many mistakes come from losing track of scope.

Quantifier order (∃∀ vs ∀∃)

This is one of the biggest conceptual leaps from propositional logic.

Consider:

• •∀x ∃y Loves(x, y)
• •∃y ∀x Loves(x, y)

Assume the domain is people.

1) ∀x ∃y Loves(x, y)

• •“Everyone loves someone.”
• •Each person can have their own y.

2) ∃y ∀x Loves(x, y)

• •“There exists someone whom everyone loves.”
• •One special y loved by all.

These are very different. The second is much stronger.

A careful translation pipeline (English → logic)

When translating, go slowly:

1. 1)Choose the domain explicitly.
2. 2)Define predicates with clear meaning.
3. 3)Identify quantifier words: “every”, “all”, “any” → ∀; “some”, “there exists” → ∃.
4. 4)Attach conditions using → or ∧.

Example: “Every user who reset their password can log in.”

• •Domain: users
• •Predicates:
• •Reset(x): “x reset their password”
• •CanLogin(x): “x can log in”

Translation:

• •∀x (Reset(x) → CanLogin(x))

Notice why it’s → and not ∧: we’re not claiming everyone reset their password.

Negating quantified statements (De Morgan’s for quantifiers)

Negation interacts with quantifiers in a structured way:

• •¬∀x φ ≡ ∃x ¬φ
• •¬∃x φ ≡ ∀x ¬φ

Intuition:

• •“Not everyone passed” means “someone did not pass.”
• •“No one passed” means “everyone did not pass.”

Do the algebra carefully. For example:

¬(∀x (P(x) → Q(x)))

Step-by-step:

1. 1)¬∀x ψ(x) ≡ ∃x ¬ψ(x)

where ψ(x) = (P(x) → Q(x))

So:

2. 2)¬(∀x (P(x) → Q(x)))

≡ ∃x ¬(P(x) → Q(x))

Now expand implication:

3. 3)(P → Q) ≡ (¬P ∨ Q)

so ¬(P → Q) ≡ ¬(¬P ∨ Q)

Apply De Morgan:

4. 4)¬(¬P ∨ Q) ≡ (P ∧ ¬Q)

Final:

5. 5)¬(∀x (P(x) → Q(x)))

≡ ∃x (P(x) ∧ ¬Q(x))

Reading: “It is not true that all P’s are Q’s” means “There exists a P that is not Q.”

Table: common English patterns

Quantifiers are simple symbols with big consequences. Most real errors are scope/order errors, not symbol errors.

Why terms and predicates are separate ideas

Predicate logic splits the world into two roles:

• •Terms denote objects (elements of the domain).
• •Formulas denote truth values (True/False).

Predicates are what turn objects into truth claims.

This separation is why you can’t, for example, treat a predicate like an object unless your logic explicitly supports that (standard first-order logic does not—this is a doorway to higher-order logic).

Arity: how many inputs a symbol takes

Predicates and functions have an arity:

• •Unary predicate: P(x)
• •Binary predicate: R(x, y)
• •Ternary predicate: T(x, y, z)

Similarly for functions:

• •Unary function: f(x)
• •Binary function: g(x, y)

Arity matters because it encodes what kind of relationship you’re expressing.

Relations as sets (a useful mental model)

If your domain is D, then:

• •A unary predicate P(·) corresponds to a subset P ⊂ D.
• •A binary predicate R(·,·) corresponds to a set of pairs R ⊂ D × D.
• •An n-ary predicate corresponds to a set R ⊂ Dⁿ.

So the atomic formula R(a, b) is true exactly when (a, b) ∈ R.

This viewpoint connects predicate logic to:

• •database tables (relations)
• •graph edges (binary relations)
• •constraints in CSP/SAT modulo theories

Equality

Most first-order settings include equality “=”.

Equality lets you state things like:

• •∃x (x = alice)
• •∀x (f(x) = x)

Be careful: equality is a logical symbol with its own meaning (identity), not just another predicate you can interpret arbitrarily (in standard FOL with equality).

Function symbols (building more complex terms)

Function symbols let you talk about structured objects without introducing extra quantifiers.

Example domain: integers.

• •succ(x) means x + 1

Then you can write:

• •∀x (LessThan(x, succ(x)))

Without functions, you’d need a relation Plus(x, 1, y) to express y = x + 1, and then quantify y.

Functions vs relations: two equivalent styles (often)

You can encode a function f(x) using a relation F(x, y) meaning “y = f(x)” plus axioms:

• •∀x ∃y F(x, y) (totality)
• •∀x ∀y₁ ∀y₂ ((F(x, y₁) ∧ F(x, y₂)) → y₁ = y₂) (uniqueness)

But using function symbols is typically cleaner.

Binding and substitution (the safe way)

A fundamental operation is substituting a term into a formula.

If φ(x) is a formula with x free, and t is a term, then φ(t) is the result of substituting t for x.

Example:

• •φ(x) := Human(x) → Mortal(x)
• •t := socrates
• •φ(t) = Human(socrates) → Mortal(socrates)

But you must avoid variable capture: substituting a term containing a variable that becomes accidentally bound.

Example of what can go wrong:

• •φ(x) := ∀y Loves(x, y)
• •substitute t := y

Naively you get ∀y Loves(y, y), where the y inside t became bound by ∀y.

The safe approach is:

• •rename bound variables first (α-renaming)
• •then substitute

So you’d rename:

• •∀y Loves(x, y) ≡ ∀z Loves(x, z)

Then substitute x := y:

• •∀z Loves(y, z)

Quantifiers as “big AND / big OR” (finite intuition)

If the domain is finite D = {d₁, …, dₙ}, then:

• •∀x φ(x) ≡ φ(d₁) ∧ φ(d₂) ∧ … ∧ φ(dₙ)
• •∃x φ(x) ≡ φ(d₁) ∨ φ(d₂) ∨ … ∨ φ(dₙ)

This is not how we compute it in general (domains can be infinite), but it’s an excellent intuition-builder.

Summary of the “typing” discipline

Keep these categories separate:

• •Terms: x, alice, f(x), g(a, b)
• •Atomic formulas: P(x), R(f(x), a)
• •Formulas: build from atomic formulas using ¬, ∧, ∨, →, ↔, plus ∀, ∃

If you can reliably tell “object expressions” from “truth expressions”, you’ll write correct formulas much faster.

Why this matters in formal methods

Formal methods is about specifying and proving properties of systems. Predicate logic is the backbone for:

• •Specifications: describing what a program should do.
• •Verification conditions: logical formulas whose validity implies correctness.
• •Model checking and theorem proving interfaces: even when tools go beyond FOL, FOL is the starting point.

Predicate logic is the first language where you can naturally express invariants like:

• •“All elements are nonnegative.”
• •∀i (0 ≤ i ∧ i < n → a[i] ≥ 0)

or existence claims like:

• •“There exists a counterexample input.”
• •∃x BadInput(x)

Typical CS domains and predicate meanings

Predicate logic is flexible because you choose the domain and interpretation.

Examples:

1) Data structures

• •Domain: nodes in a linked list
• •Predicates:
• •Next(x, y): “y is the next node after x”
• •Reachable(x, y): “y is reachable from x”

2) Security policies

• •Domain: principals/users
• •Predicates:
• •CanRead(u, f)
• •Owns(u, f)
• •Admin(u)

Then a policy might be:

• •∀u ∀f (CanRead(u, f) → (Owns(u, f) ∨ Admin(u)))

3) Databases (relational model)

A table like Enrolled(student, course) is literally a binary predicate Enrolled(·,·).

Queries often correspond to existential formulas.

Example: “Find students enrolled in CS101” corresponds to:

• •∃c (c = CS101 ∧ Enrolled(s, c))

Proof patterns you’ll reuse

Even if you don’t do full theorem-prover work yet, you should recognize the standard moves.

Universal instantiation (UI)

From ∀x φ(x), you may conclude φ(t) for any term t.

Example:

1. 1)∀x (Human(x) → Mortal(x))
2. 2)Human(socrates)

UI on (1) with t = socrates gives:

3. 3)Human(socrates) → Mortal(socrates)

Then by modus ponens with (2):

4. 4)Mortal(socrates)

Existential instantiation (EI) (with care)

From ∃x φ(x), you can introduce a fresh symbol k such that φ(k) holds, but k must be new (it can’t carry hidden assumptions).

This is subtle: you don’t get to pick a specific known constant unless you can prove it works.

Existential generalization (EG)

From φ(t), infer ∃x φ(x) (replace t by a variable).

Example:

• •Human(socrates) implies ∃x Human(x)

Universal generalization (UG) (with care)

From φ(x) for an arbitrary x (with no special assumptions about x), infer ∀x φ(x).

This “arbitrary” requirement is exactly where many informal proofs go wrong.

Satisfiability, validity, and models (a quick bridge from propositional logic)

You already know satisfiability in propositional logic. In FOL:

• •A model is a domain plus interpretations making formulas true.
• •A sentence is satisfiable if it’s true in at least one model.
• •A sentence is valid if it’s true in all models.

Example (valid):

• •∀x P(x) → ∃x P(x)

This is valid because if P holds for all x in a nonempty domain, then certainly there exists an x where P holds.

Non-valid (not always true):

• •∃x P(x) → ∀x P(x)

True in some models, false in others.

Why tooling often restricts or extends FOL

Pure FOL is expressive, but automated reasoning is harder than for propositional logic.

• •SAT is decidable and heavily optimized.
• •FOL validity is (in general) undecidable.

So real tools often:

• •restrict to decidable fragments (e.g., certain theories), or
• •use semi-decision procedures (can find proofs/countermodels sometimes), or
• •combine SAT with theories (SMT: satisfiability modulo theories), where formulas often look like FOL with arithmetic, arrays, etc.

The key takeaway: learning predicate logic is the gateway to reading specifications, understanding solver input languages, and following proofs about programs.