First-Order Logic Summary

Mathematical Logic · Axiom Academy

Comprehensive overview of FOL syntax, semantics, and automated reasoning techniques that power modern program verification and theorem proving. First-Order Language: Defined by a signature specifying function symbols, relation symbols, and their arities Constant Symbols: 0-ary function symbols representing specific objects (e.g., 0, 1, true) Function Symbols: Operations that combine objects (e.g., +, ×, successor) Relation Symbols: Express properties and relationships between objects (e.g., <, =, Prime) Variables: Placeholders (x, y, z) that range over objects in the domain Terms: Built from variables, constants, and functions. Examples: x, 0, f(x), g(x, y) Atomic Formulas: Relations applied to terms: R(t₁, ..., tₙ) or t₁ = t₂ Complex Formulas: Built using connectives ¬, ∧, ∨, →, ↔ and quantifiers ∀, ∃ Well-Formed Formulas: Recursively defined: atomics are formulas, and formulas are closed under connectives and quantifiers Sentence: A formula with no free variables - a complete statement Structure/Model: A non-empty domain D plus interpretations of all symbols in the language Domain: The universe of objects we're reasoning about (e.g., natural numbers, graphs, programs) Function Interpretation: Each function symbol f mapped to an actual function f M : Dⁿ → D Relation Interpretation: Each relation R mapped to a subset R M ⊆ Dⁿ Example: Standard model of arithmetic: domain = ℕ, 0 M = 0, + M = addition, M = less-than

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