Introduction
Model theory studies the relationship between formal languages (syntax) and their interpretations (semantics). It answers questions like:
- What does a formula mean?
- When is a formula true?
- What structures satisfy a formula?
- How are different models related?
Model theory is fundamental to:
- Logic and proof theory
- Database theory
- Formal verification
- Artificial intelligence
- Philosophy of mathematics
In this article, we’ll explore the basics of model theory.
Models and Interpretations
Definition of Model
A model is a mathematical structure that assigns meaning to the symbols of a formal language.
Components:
- Domain (Universe): Set of objects the language talks about
- Interpretation: Assignment of meaning to symbols
Formal Definition:
M = (D, I)
D = domain (non-empty set)
I = interpretation function
Interpretation Function
The interpretation function assigns meaning to:
- Constants: Elements of the domain
- Functions: Operations on the domain
- Relations: Subsets of the domain
Examples:
Constant a: I(a) = 5 (element of domain)
Function f: I(f) = addition (operation on domain)
Relation R: I(R) = {(1,2), (2,3)} (subset of domain²)
Example: Model for Arithmetic
Language: {0, 1, +, ×, <}
Model M₁ (Natural Numbers):
Domain: ℕ = {0, 1, 2, 3, ...}
I(0) = 0
I(1) = 1
I(+) = addition
I(×) = multiplication
I(<) = less than
Model M₂ (Integers mod 5):
Domain: ℤ₅ = {0, 1, 2, 3, 4}
I(0) = 0
I(1) = 1
I(+) = addition mod 5
I(×) = multiplication mod 5
I(<) = less than mod 5
Satisfiability
Definition
A formula φ is satisfied by a model M (written M ⊨ φ) if φ is true in M.
Formal Definition:
M ⊨ φ means: φ is true under interpretation I in domain D
Satisfaction Rules
Atomic Formulas:
M ⊨ R(t₁, ..., tₙ) iff (I(t₁), ..., I(tₙ)) ∈ I(R)
Negation:
M ⊨ ¬φ iff M ⊭ φ
Conjunction:
M ⊨ φ ∧ ψ iff M ⊨ φ and M ⊨ ψ
Disjunction:
M ⊨ φ ∨ ψ iff M ⊨ φ or M ⊨ ψ
Implication:
M ⊨ φ → ψ iff M ⊭ φ or M ⊨ ψ
Universal Quantification:
M ⊨ ∀x φ(x) iff for all d ∈ D: M ⊨ φ(d)
Existential Quantification:
M ⊨ ∃x φ(x) iff there exists d ∈ D: M ⊨ φ(d)
Example: Checking Satisfaction
Formula: ∀x (x + 0 = x)
Model M (Natural Numbers):
Domain: ℕ
I(+) = addition
I(0) = 0
Check: For all n ∈ ℕ, n + 0 = n?
Yes, this is true.
Therefore, M ⊨ ∀x (x + 0 = x)
Validity and Satisfiability
Definition of Valid Formula
A formula is valid (or a tautology) if it is satisfied by all models.
Notation:
⊨ φ (φ is valid)
Formal Definition:
⊨ φ iff for all models M: M ⊨ φ
Definition of Satisfiable Formula
A formula is satisfiable if it is satisfied by at least one model.
Formal Definition:
φ is satisfiable iff there exists a model M: M ⊨ φ
Definition of Unsatisfiable Formula
A formula is unsatisfiable if it is not satisfied by any model.
Formal Definition:
φ is unsatisfiable iff for all models M: M ⊭ φ
Examples
Valid Formula:
φ = P(x) ∨ ¬P(x)
True in all models (law of excluded middle)
Satisfiable but Not Valid:
φ = P(x)
True in some models, false in others
Unsatisfiable Formula:
φ = P(x) ∧ ¬P(x)
False in all models (contradiction)
Logical Consequence
Definition
A formula ψ is a logical consequence of φ (written φ ⊨ ψ) if every model that satisfies φ also satisfies ψ.
Formal Definition:
φ ⊨ ψ iff for all models M: if M ⊨ φ then M ⊨ ψ
Examples
Example 1:
φ = ∀x P(x)
ψ = P(a)
φ ⊨ ψ (if all x satisfy P, then a satisfies P)
Example 2:
φ = P(a) ∧ Q(a)
ψ = P(a)
φ ⊨ ψ (if both P and Q hold, then P holds)
Example 3:
φ = P(a) → Q(a)
ψ = ¬P(a) ∨ Q(a)
φ ⊨ ψ (implication is equivalent to disjunction)
Completeness and Soundness
Soundness
A proof system is sound if every provable formula is valid.
Formal Definition:
If ⊢ φ then ⊨ φ
(provable implies valid)
Completeness
A proof system is complete if every valid formula is provable.
Formal Definition:
If ⊨ φ then ⊢ φ
(valid implies provable)
Gödel’s Completeness Theorem
Theorem: First-order logic is complete.
Significance:
- Proof theory and model theory are equivalent
- Every valid formula has a proof
- Syntax and semantics align
Elementary Equivalence
Definition
Two models are elementarily equivalent if they satisfy the same formulas.
Notation:
M ≡ N (M and N are elementarily equivalent)
Formal Definition:
M ≡ N iff for all formulas φ: M ⊨ φ iff N ⊨ φ
Example
Models:
M₁ = (ℕ, +, ×, <)
M₂ = (ℚ, +, ×, <)
Are they elementarily equivalent?
No. The formula ∃x (x × x = 2) is true in M₂ but false in M₁.
Glossary
- Model: Mathematical structure interpreting a language
- Domain: Set of objects in a model
- Interpretation: Assignment of meaning to symbols
- Satisfiability: Formula is true in a model
- Validity: Formula is true in all models
- Logical consequence: Formula follows from another
- Soundness: Provable implies valid
- Completeness: Valid implies provable
- Elementary equivalence: Models satisfy same formulas
- Tautology: Valid formula
Practice Problems
Problem 1: Satisfaction
Given model M with domain {1, 2, 3} and I(P) = {1, 2}:
Is M ⊨ ∃x P(x)?
Solution:
Yes. There exists x (e.g., x = 1) such that P(x) is true.
Problem 2: Validity
Is the formula ∀x P(x) → ∃x P(x) valid?
Solution:
Yes. If all x satisfy P, then at least one x satisfies P.
This is true in all models.
Problem 3: Logical Consequence
Does ∀x (P(x) → Q(x)) and P(a) logically imply Q(a)?
Solution:
Yes. If all x satisfy P → Q, and P(a) is true,
then Q(a) must be true.
Problem 4: Elementary Equivalence
Are the models (ℕ, +) and (ℤ, +) elementarily equivalent?
Solution:
No. The formula ∃x (x + x = 1) is false in (ℕ, +)
but true in (ℤ, +).
Related Resources
Online Platforms
- Stanford Encyclopedia of Philosophy - Model theory articles
- Khan Academy Logic
- Coursera Logic Courses
- MIT OpenCourseWare
- Brilliant.org Logic
Interactive Tools
- Logic Visualizer - Visualize models
- Model Checker - Check satisfaction
- Formula Evaluator - Evaluate formulas
- Interpretation Builder - Build interpretations
- Satisfiability Checker - Check satisfiability
Recommended Books
- “Model Theory” by Chang & Keisler - Comprehensive reference
- “Introduction to Model Theory” by Marker - Accessible introduction
- “A Shorter Model Theory” by Hodges - Concise overview
- “Model Theory: An Introduction” by Rothmaler - Modern approach
- “Logic for Mathematicians” by Hamilton - Mathematical logic
Academic Journals
- Journal of Symbolic Logic
- Studia Logica
- Archive for Mathematical Logic
- Annals of Pure and Applied Logic
- Mathematical Logic Quarterly
Software Tools
- Prolog - Logic programming
- Coq - Theorem prover
- Isabelle - Proof assistant
- Z3 - SMT solver
- Datalog - Logic database
Conclusion
Model theory bridges syntax and semantics:
- Models give meaning to formal languages
- Satisfiability determines truth in models
- Validity holds in all models
- Logical consequence relates formulas
- Completeness connects proof and semantics
Understanding model theory is essential for logic, formal verification, and artificial intelligence.
In the next article, we’ll explore satisfiability and validity in more depth.
Next Article: Satisfiability and Validity
Comments