Definition
Predicate logic — also called first-order logic — is the formal system that extends propositional logic with variables, predicates, and quantifiers. Where propositional logic can only manipulate whole statements ("it is raining"), predicate logic can talk about the internal structure of statements ("for every cloud x, x contains water"). The quantifier symbols are the universal quantifier ∀ ("for all") and the existential quantifier ∃ ("there exists"). Predicates are statements with placeholders — Human(x), LovesParent(x, y) — that become true or false once their variables are bound to specific objects in a domain of discourse.
First-order logic is the workhorse of modern mathematics, computer science, and analytic philosophy. Most formal proofs, programming-language type systems, database queries (SQL is essentially restricted predicate logic over relations), and automated theorem provers operate at this level.
Why it matters
How it works
A predicate-logic statement is built from three layers. Atomic predicates name properties or relations: Cat(felix), Owns(alice, felix). Logical connectives — ∧ (and), ∨ (or), ¬ (not), → (implies), ↔ (iff) — combine atomic statements into compound ones, exactly as in propositional logic. Quantifiers then bind variables to range over the domain: ∀x. Cat(x) → Mammal(x) reads "every cat is a mammal"; ∃x. Cat(x) ∧ Black(x) reads "there exists a black cat."
Inference proceeds by rules that respect quantifier scope. Universal instantiation lets us substitute any specific object for a universally-quantified variable: from ∀x. Mortal(x) we may conclude Mortal(socrates). Existential generalisation goes the other way: from Mortal(socrates) we may conclude ∃x. Mortal(x). The structural discipline that makes these moves valid — keeping bound and free variables separate, renaming on capture — is the technical bookkeeping that distinguishes first-order proof from natural-language reasoning, where these moves are usually invisible.