Model Theory Basics

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:

1. Domain (Universe): Set of objects the language talks about
2. 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