Model Theory Basics

Loewenheim-Skolem theorem: a theory with an infinite model has a countable model, including the theory of real numbers. This seems paradoxical (R is uncountable), but reveals a fundamental limitation of first-order logic - uncountability cannot be captured in first-order axioms.

• Robinson's nonstandard analysis: Leibniz infinitesimals are rigorously justified via the compactness theorem - they exist in nonstandard models of R
• Databases: the theory of finite structures and SQL queries uses model-theoretic methods to analyze the expressive power of queries
• SAT solvers: satisfiability-checking algorithms (DPLL, CDCL) implement the compactness theorem for propositional formulas in conjunctive normal form
• SMT solvers (Z3, CVC5): decide theories such as linear arithmetic and arrays using satisfiability procedures for first-order fragments

Structures, Models, and the Compactness Theorem

Model theory studies the relationship between formal theories and their interpretations. Abraham Robinson in 1961 used the compactness theorem to justify nonstandard analysis - fields with genuine infinitesimals. The Loewenheim-Skolem theorem reveals a paradoxical consequence: the theory of the real numbers has a countable model.

Elementary Equivalence and Complete Theories

Two structures are elementarily equivalent if they satisfy the same first-order sentences. A theory is complete if every sentence is either provable or refutable. The theory Th(N, +, x) (true arithmetic) is complete but not recursively axiomatizable - it is too rich for machine verification.

The theory of dense linear orders without endpoints (DLO) is complete and recursively axiomatized. The theory of real closed fields (RCF) is also complete - a consequence of Tarski's quantifier elimination theorem. This explains why computers can decide certain geometric problems.

Итоги

• Structure = (domain, interpretations of predicates, functions, constants) - a concrete mathematical interpretation of a theory
• Compactness theorem: T is satisfiable if and only if every finite subset of T is satisfiable
• Downward Loewenheim-Skolem: a consistent countable first-order theory has a countable model
• Nonstandard analysis: PA plus {c > n | n in N} is satisfiable by compactness, yielding nonstandard models with infinitely large elements
• Elementary equivalence: M equiv N means they satisfy the same first-order sentences (isomorphism implies it, converse fails)
• RCF is complete (Tarski quantifier elimination): real algebraic geometry is algorithmically decidable