First-Order Syntax

Mathematical Logic · Axiom Academy

A rigorous treatment of first-order languages: building formulas from symbols, understanding the grammar of mathematical logic, and distinguishing free from bound variables A first-order language L consists of logical symbols (common to all languages) and non-logical symbols (specific to the structure we're studying). Variables: x, y, z, x₁, x₂, ... (infinitely many) Quantifiers: ∀ (for all), ∃ (there exists) Equality: = (in most formulations) Constants: c, d, 0, 1, ... (objects in the domain) Function symbols: f, g, +, ·, ... (each with arity n ≥ 1) Relation symbols: R, P, <, ≤, ... (each with arity n ≥ 1) Terms are expressions that denote objects in the domain. They are built recursively from variables, constants, and function symbols. If t₁, ..., tₙ are terms and f is an n-ary function symbol, then f(t₁, ..., tₙ) is a term 3. Atomic Formulas: Basic Assertions Atomic formulas are the simplest formulas—they make basic assertions about relationships between terms. Relation application: R(t₁, ..., tₙ) where R is an n-ary relation symbol and t₁, ..., tₙ are terms Equality: t₁ = t₂ where t₁ and t₂ are terms 4. Well-Formed Formulas (wffs) Well-formed formulas (wffs) are built recursively from atomic formulas using logical connectives and quantifiers. If φ is a wff, then ¬φ is a wff If φ and ψ are wffs, then (φ ∧ ψ), (φ ∨ ψ), (φ → ψ), (φ ↔ ψ) are wffs If φ is a wff and x is a variable, then ∀x φ and ∃x φ are wffs

This is the written version of the interactive lesson above. See the full Mathematical Logic course.