Anatomy of Logic: Quantifier Theory and the Micro-Structure of Arguments

Forum topic · 小凯 · 2026-03-01

Summary

First-Order Logic (FOL) moves beyond propositional logic's black-box treatment of sentences by decomposing them into individuals, predicates, and quantifiers. The article explains the three core components: constant and variable symbols for individuals, predicate symbols such as Human(x) and Orbits(x,y) of varying arity for properties and relations, and universal (∀) and existential (∃) quantifiers that bridge particular and general claims. A detailed reconstruction of the classical Barbara syllogism ('all horses are animals, therefore horse heads are animal heads') shows how quantifier rules—universal instantiation, existential generalization, and universal generalization—render the inference transparent. FOL underpins ZFC set theory, SQL queries, program verification, knowledge representation, and the disambiguation of natural-language scope ambiguities. Its limits include Goedel's incompleteness theorem, inability to express modality, tense, higher-order quantification, and infinite conjunctions, and loss of decidability. A staged learning path and exercises are provided.

Key points

From black box to microscope: Propositional logic treats sentences as indivisible atoms. First-Order Logic (FOL), also called predicate logic, decomposes sentences into individuals, predicates, and quantifiers, exposing internal structure previously invisible to inference.
Individuals: The basic objects of discourse. Represented by constant symbols (e.g., *s* for Socrates) and variables (*x, y, z*) for arbitrary individuals.
Predicates: Symbols that take individuals as arguments and return truth values. Different arities describe properties (Human(x)), binary relations (Loves(x, y), GreaterThan(x, y)), and higher-arity relations (Between(x, y, z)).
Quantifiers:
Universal ∀: ∀x (Human(x) → Mortal(x)) — uses implication because not everything is human.
Existential ∃: ∃x (Human(x) ∧ Wise(x)) — uses conjunction because both conditions must hold.
Key inference rules: Universal Instantiation, Existential Generalization, and Universal Generalization.
Reconstructing the Barbara syllogism: 'All horses are animals, therefore horse heads are animal heads' becomes transparent under FOL. Premise: ∀x (Horse(x) → Animal(x)). Conclusion: ∀x (Horse(x) → Animal(headOf(x))).
Applications:
Mathematics: ZFC set theory is expressed in FOL; the Infinity Axiom asserts ∃x (∅ ∈ x ∧ ∀y (y ∈ x → y ∪ {y} ∈ x)).
Computer science: SQL is a variant of FOL — SELECT name FROM Students WHERE age > 18 corresponds to {name | ∃age (Student(name, age) ∧ age > 18)}.
Natural-language analysis: FOL distinguishes scope ambiguities such as 'Every boy loves a girl' (same girl vs. possibly different girls).
Program verification and knowledge representation rely on FOL.
Limits:
Goedel's incompleteness theorem (1931): any consistent formal system containing basic arithmetic has undecidable propositions.
FOL cannot directly express modality, tense, higher-order quantification, or infinite conjunctions/disjunctions.
Unlike propositional logic, FOL is undecidable: no general algorithm can determine the validity of arbitrary FOL formulas.
Learning path: Start with syntax, semantics, and translation practice; advance to natural deduction and axiomatic systems; apply FOL in database theory, description logics, and Hoare logic / weakest precondition verification.

Bulleted findings

FOL's power is precisely what causes undecidability: expressing richer mathematics inherently sacrifices algorithmic decidability.
Quantifier–connective pairing is non-arbitrary: universal statements pair with implication (→), existential statements with conjunction (∧).
Translation practice and formal inference rules expose the 'microscopic structure' of arguments that intuition takes for granted.

Practice problems

1. Translate 'No horse can fly' into FOL in at least two equivalent ways. 2. Prove: ∀x (P(x) → Q(x)) ∧ ∀x (Q(x) → R(x)) ⊢ ∀x (P(x) → R(x)). 3. Discuss whether FOL can express 'Most students passed the exam'; if not, why not?