--- name: predicate-logic description: 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. type: skill category: logic status: stable origin: tibsfox modified: false first_seen: 2026-04-12 first_path: examples/skills/logic/predicate-logic/SKILL.md superseded_by: null --- # Predicate Logic (First-Order Logic) 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 ## Syntax: The Alphabet Expanded First-order logic adds to the propositional alphabet: - **Variables**: x, y, z, ..., ranging over objects in a domain - **Constants**: a, b, c, ..., naming specific objects - **Predicate symbols**: P, Q, R, ..., of arity 1, 2, 3, ... (one-place, two-place, etc.) - **Function symbols**: f, g, h, ..., of positive arity - **Quantifiers**: ∀ (universal, "for all"), ∃ (existential, "there exists") - **Equality**: = (in FOL with identity) **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: - If φ is a formula and x is a variable, then ∀x φ is a formula - If φ is a formula and x is a variable, then ∃x φ is a formula **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. ## Semantics: Interpretation Over a Domain An interpretation of a first-order language consists of: 1. A nonempty **domain** (also called universe) D of objects 2. For each constant c, an object c^I in D 3. For each n-place function symbol f, a function f^I : D^n → D 4. For each n-place predicate symbol P, a relation P^I ⊆ D^n Given an interpretation and an assignment of domain elements to the free variables, every formula has a truth value, determined recursively: - **∀x φ** is true if φ is true for every assignment of x to an element of D - **∃x φ** is true if φ is true for at least one assignment of x to an element of D This is Tarski's inductive definition of truth, which is why Tarski is the semantics specialist in this department. ## The Two Quantifiers ### Universal quantifier ∀ "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. ### Existential quantifier ∃ "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. ## Quantifier Scope and Alternation ### Scope 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. ### Alternation order matters `∀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. ### Quantifier duality (De Morgan for quantifiers) | | | |---|---| | ¬∀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" | ## Worked Example: Aristotle's Syllogism **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:** 1. ∀x (Human(x) → Mortal(x)) (Premise 1) 2. Human(s) (Premise 2) 3. Human(s) → Mortal(s) (Universal elimination from 1, substituting s for x) 4. Mortal(s) (Modus ponens from 3 and 2) This is the paradigm derivation of predicate logic. It looks trivial only because we have seen it a thousand times. ## Natural Deduction for Quantifiers ### Universal introduction (∀I) 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. ### Universal elimination (∀E) 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. ### Existential introduction (∃I) From φ(t) for a specific term t, conclude ∃x φ(x). ### Existential elimination (∃E) 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. ## Translation Discipline Translating English to FOL requires careful attention: ### "All" + "is" usually needs → "All dogs bark" → `∀x (Dog(x) → Bark(x))` ### "Some" + "is" usually needs ∧ "Some dogs bark" → `∃x (Dog(x) ∧ Bark(x))` ### "No" requires negation "No dogs meow" → `∀x (Dog(x) → ¬Meow(x))` ≡ `¬∃x (Dog(x) ∧ Meow(x))` ### Restricted quantification "Every student passed" uses the restricted quantifier over students. Formalize: `∀x (Student(x) → Passed(x))`. ### Two-place predicates "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). ### Uniqueness and numerical quantifiers "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 and Completeness **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. ## Undecidability at First Order 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. ## When NOT to Use This Skill - **Arguments with no quantifier structure.** Use `propositional-logic`. - **Arguments essentially involving necessity or possibility.** Use `modal-logic`. - **Rhetorical error classification.** Use `informal-fallacies`. - **Mathematical proofs that use FOL as a tool but are really about math.** Use `mathematical-proof-logic`. ## Decision Guidance When formalizing an argument into FOL: 1. **Identify the domain.** What are the objects? Humans? Numbers? Sets? 2. **Identify the predicates.** What properties and relations are being asserted? 3. **Identify the quantifier structure.** Where is "every," "some," "none"? What is the scope of each quantifier? 4. **Translate carefully.** All-is-→, some-is-∧, no requires negation. Alternation order matters. 5. **Derive or countermodel.** For valid arguments, give a natural-deduction proof. For invalid arguments, exhibit an interpretation where premises are true and conclusion false. ## Cross-References - **frege agent:** Invention of quantifiers, Begriffsschrift, foundational framing - **russell agent:** Type discipline, Russell's paradox, Principia - **tarski agent:** Semantic definition of truth, model theory - **propositional-logic skill:** The base system FOL extends - **mathematical-proof-logic skill:** FOL as the working language of proof ## References - Enderton, H. B. (2001). *A Mathematical Introduction to Logic*. 2nd edition. Academic Press. - Mendelson, E. (2015). *Introduction to Mathematical Logic*. 6th edition. CRC Press. - Frege, G. (1879). *Begriffsschrift*. Halle. - Tarski, A. (1933/1956). "The Concept of Truth in Formalized Languages," in *Logic, Semantics, Metamathematics*. Oxford University Press. - Church, A. (1936). "An unsolvable problem of elementary number theory." *American Journal of Mathematics* 58, 345-363. - Godel, K. (1930). "Die Vollstandigkeit der Axiome des logischen Funktionenkalkuls." *Monatshefte fur Mathematik und Physik* 37, 349-360.