First-order logic with quantifiers, predicates, functions, and identity. Covers syntax, interpretation over a domain, the universal and existential quantifiers, quantifier scope and binding, translation from natural language with multi-variable predicates, natural deduction for quantifiers, undecidability at first order, and the soundness/completeness theorems. Use when propositional logic is insufficient -- whenever "for all" or "there exists" matters to the argument.
Predicate logic -- also called first-order logic (FOL) or quantificational logic -- extends propositional logic with the machinery of quantification. Where propositional logic can express "Socrates is mortal" as an atomic sentence, predicate logic can express "every man is mortal" as ∀x (Man(x) → Mortal(x)) and then actually derive "Socrates is mortal" from it. This expressive jump is what allows logic to capture mathematical reasoning, natural-language quantifier interactions, and the semantics of programming languages. This skill covers the syntax, semantics, proof theory, and translation discipline of first-order logic.
Agent affinity: frege (foundational framing), russell (type-theoretic discipline), tarski (semantic definition of truth)
Concept IDs: log-predicate-logic, log-argument-structure, log-deductive-reasoning, log-proof-techniques
First-order logic adds to the propositional alphabet:
Terms are built from variables, constants, and function applications. If f is a 2-place function symbol, then f(x, a) is a term.
Atomic formulas are predicate applications: P(t) or R(t, s), where t, s are terms.
Formulas are built from atomic formulas using the propositional connectives plus the two quantifier rules:
Free and bound variables. A variable x in a formula is bound if it lies inside the scope of a quantifier ∀x or ∃x. Otherwise it is free. A formula with no free variables is a sentence -- it has a definite truth value once the interpretation is fixed. A formula with free variables is open -- it is a property that some objects may satisfy.
An interpretation of a first-order language consists of:
Given an interpretation and an assignment of domain elements to the free variables, every formula has a truth value, determined recursively:
This is Tarski's inductive definition of truth, which is why Tarski is the semantics specialist in this department.
"For every x in the domain, property φ(x) holds."
In natural language: "all," "every," "any," "each," and sometimes "a" or "the" (depending on context -- "a whale is a mammal" usually means "every whale is a mammal").
Translation pattern: ∀x (P(x) → Q(x)). Not ∀x (P(x) ∧ Q(x)) -- that says "every object in the domain has both P and Q," which is almost never what English "every P is Q" means.
"There is at least one x in the domain such that property φ(x) holds."
In natural language: "some," "there is," "there exists," "at least one," and sometimes "a" or "the" (again context-dependent -- "a student failed" usually means "some student failed").
Translation pattern: ∃x (P(x) ∧ Q(x)). Not ∃x (P(x) → Q(x)) -- that is vacuously true as long as any object lacks P.
The translation asymmetry (universal uses →, existential uses ∧) is a persistent source of student confusion and is worth drilling until reflexive.
A quantifier's scope is the formula it governs, usually the smallest formula immediately following. Parentheses disambiguate. In ∀x (P(x) → Q(x)), the scope of ∀x is the full conditional. In ∀x P(x) → Q(x), the scope is only P(x), and Q(x) has a free variable.
∀x ∃y Loves(x, y) means: for every person, there is someone they love. Different person y for different x.
∃y ∀x Loves(x, y) means: there is one person y that everyone loves. Same y for every x.
These are not equivalent. In fact, ∃y ∀x φ(x, y) implies ∀x ∃y φ(x, y) but the reverse does not hold. This is the single deepest pitfall of quantifier logic.
| ¬∀x φ | ≡ ∃x ¬φ |
| ¬∃x φ | ≡ ∀x ¬φ |
| ¬∀x P(x) | "Not everything is P" ≡ "something is not P" |
| ¬∃x P(x) | "Nothing is P" ≡ "everything is not P" |
Argument: All humans are mortal. Socrates is human. Therefore, Socrates is mortal.
Formalization: Let Human(x), Mortal(x) be one-place predicates, and let s denote Socrates.
Premise 1: ∀x (Human(x) → Mortal(x))
Premise 2: Human(s)
Conclusion: Mortal(s)
Proof:
This is the paradigm derivation of predicate logic. It looks trivial only because we have seen it a thousand times.
If you can prove φ(x) for an arbitrary x (meaning x does not appear in any undischarged assumptions), you can conclude ∀x φ(x).
The "arbitrary" restriction is critical. You cannot introduce ∀ if you have been using specific properties of x.
From ∀x φ(x), conclude φ(t) for any term t.
Substitution must be capture-avoiding: if t contains a variable y, and y would become bound by a quantifier in φ, rename bound variables first.
From φ(t) for a specific term t, conclude ∃x φ(x).
From ∃x φ(x), introduce a fresh variable (or constant) c and assume φ(c). If you can derive ψ from this assumption without using c outside the sub-derivation, conclude ψ.
The "fresh" restriction is critical. You cannot use ∃E on a variable that appears elsewhere.
Translating English to FOL requires careful attention:
"All dogs bark" → ∀x (Dog(x) → Bark(x))
"Some dogs bark" → ∃x (Dog(x) ∧ Bark(x))
"No dogs meow" → ∀x (Dog(x) → ¬Meow(x)) ≡ ¬∃x (Dog(x) ∧ Meow(x))
"Every student passed" uses the restricted quantifier over students. Formalize: ∀x (Student(x) → Passed(x)).
"Alice loves Bob" → Loves(a, b) with constants a, b.
"Everyone loves Bob" → ∀x Loves(x, b).
"Alice loves everyone" → ∀x Loves(a, x).
"Everyone loves someone" → ∀x ∃y Loves(x, y) (different someone for different x).
"Someone loves everyone" → ∃y ∀x Loves(x, y) (same y for every x).
"There is exactly one x such that P(x)" → ∃x (P(x) ∧ ∀y (P(y) → y = x)).
"There are at least two P" → ∃x ∃y (P(x) ∧ P(y) ∧ x ≠ y).
"There are exactly two P" → combine both: at least two and at most two.
Soundness: If a formula is provable in the deduction system, it is true in every interpretation. This guarantees you cannot derive a false conclusion from true premises.
Completeness: If a formula is true in every interpretation, it is provable. This is Godel's completeness theorem for first-order logic (1929, dissertation; published 1930) -- not to be confused with the incompleteness theorems, which are about specific theories within first-order logic.
The soundness + completeness pair means that "true in every interpretation" and "derivable in the deduction system" are exactly the same set. This is philosophically significant: it means first-order logic captures its own semantic notion of validity.
Propositional logic is decidable. First-order logic is undecidable -- there is no algorithm that, given any first-order formula, always correctly determines whether it is valid in finite time. This is Church's theorem (1936) and independently Turing's proof via the halting problem.
First-order logic is semi-decidable: if a formula is valid, you can find a proof (given enough time), but if it is not valid, the search may run forever without terminating.
This is the first-order inflection point where logic meets computability theory. It is not a minor technical detail -- it sets the limits of what automated reasoning can do.
propositional-logic.modal-logic.informal-fallacies.mathematical-proof-logic.When formalizing an argument into FOL: