A topic in the Open Knowledge Graph — a free, open map of 15,290 topics and the order to learn them in.
First-order logic (FOL) extends propositional logic with terms (variables, constants, function symbols applied to terms) and atomic formulas (predicate symbols applied to terms). Quantifiers ∀ (for all) and ∃ (there exists) bind variables, giving rise to the distinction between free and bound occurrences. A sentence is a formula with no free variables. The language of a first-order theory is specified by its signature: a collection of constant, function, and predicate symbols with their arities. Different signatures yield different logical languages (e.g., the language of arithmetic vs. the language of set theory).
Practice translating English statements into FOL and back. Carefully track variable scope to distinguish bound and free occurrences. Build formulas of increasing complexity from simple atomic predicates.
In propositional logic, the basic units were atomic propositions like P and Q — whole claims that were either true or false. First-order logic is more expressive: it lets you talk about *objects*, their *properties*, and *relations* between them, and it lets you make claims about *all* or *some* objects in a domain. To do this, it introduces a new kind of syntax built from three layers: terms, atomic formulas, and compound formulas with quantifiers.
Terms are the expressions that refer to objects. A constant like `alice` or `0` refers to a specific object. A variable like `x` is a placeholder that can range over objects in the domain. A function symbol applied to terms — like `father(alice)` or `s(0)` — builds a new term by applying an operation to existing ones. Terms are *not* true or false; they just denote things. Predicates, by contrast, take terms as arguments and produce truth values: `Loves(alice, bob)` or `Prime(3)` are atomic formulas — the smallest units that can be true or false.
Quantifiers are what make first-order logic genuinely more powerful than propositional logic. ∀x φ(x) asserts that φ holds for every object in the domain; ∃x φ(x) asserts that at least one object satisfies φ. The critical concept is *scope*: the quantifier ∀x binds occurrences of x within the subformula it governs. If you write ∀x P(x) ∧ Q(x), the scope of ∀x is only P(x) — the x in Q(x) is *free* (unbound). This is identical to the scoping rules for variables in programming languages, and that analogy is a reliable guide.
The signature of a first-order theory specifies what vocabulary is available: which constant, function, and predicate symbols exist and how many arguments each takes (its arity). The same syntax rules apply to every first-order language, but different signatures yield different languages — the language of arithmetic uses 0, s (successor), +, × and =; the language of set theory uses only ∈. Understanding the signature tells you which atomic formulas are even well-formed before you worry about what they mean.
A formula is a *sentence* if it has no free variables. Sentences have definite truth values in a model; open formulas only acquire truth values once the free variables are assigned values. When you read or write FOL, always track which variables are bound and which are free — this is the most common source of syntax errors and the foundation for everything in semantics and proof theory that follows.