Cheatsheet

Math Logic & Algorithms

All topics on one page

5modules

15articles

0definitions

14formulas

Propositional Logic

Syntax, semantics, normal forms, and the DPLL algorithm

Syntax and Semantics of Propositional Logic

Motivation: Why Formalize Reasoning? → Syntax → Semantics: Truth Tables → Logical Consequence and Equivalence → Numerical Example → Real-world Application → Additional Aspects → Connection with Other Branches of Mathematics → Historical Background and Development of the Idea

Formulas

Logical equivalence: φ ≡ ψ if I(φ) = I(ψ) for all I. Examples:Step 5. (p → q) = 1 with p = 1 → q = 1. But from step 4: q = 0. Contradiction!Truth table (abbreviated): For p=1, q=0, r=0:

·Propositional variables: p, q, r, p₁, p₂, ...
·Logical connectives: ¬ (negation), ∧ (conjunction—“and”), ∨ (disjunction—“or”), → (implication—“if... then”), ↔ (equivalence—“if and only if”).
·Parentheses: (, ).
·I(¬φ) = 1 − I(φ)
·I(φ ∧ ψ) = min(I(φ), I(ψ)) — true if both are true
·I(φ ∨ ψ) = max(I(φ), I(ψ)) — true if at least one is true
·I(φ → ψ) = max(1−I(φ), I(ψ)) — false only when φ=1, ψ=0
·I(φ ↔ ψ) = 1 if and only if I(φ) = I(ψ)
·Tautology: I(φ) = 1 for all interpretations. Denotation: ⊨ φ.
·Contradiction (antitautology): I(φ) = 0 for all interpretations.
·Satisfiability: I(φ) = 1 for some I.
·¬¬p ≡ p (double negation)
·(p → q) ≡ (¬p ∨ q) (implication via disjunction)
·¬(p ∧ q) ≡ (¬p ∨ ¬q) (De Morgan’s law)
·¬(p ∨ q) ≡ (¬p ∧ ¬q) (De Morgan’s law)
·p ∧ (q ∨ r) ≡ (p ∧ q) ∨ (p ∧ r)
·p ∨ (q ∧ r) ≡ (p ∨ q) ∧ (p ∨ r)

Mathematical proofs consist of steps in which some statements are derived from others. But what is a “correct” step? Propositional logic provides a precise language: syntax (how to write formulas) and semantics (what they mean). This is the foundation underlying automated provers, compilers, and ...

Inductive definition of formulas: 1. Every variable p is a formula. 2. If φ is a formula, then ¬φ is a formula. 3. If φ and ψ are formulas, then (φ ∧ ψ), (φ ∨ ψ), (φ → ψ), (φ ↔ ψ) are formulas. 4. Nothing else is a formula.

Interpretation (valuation): function I: {variables} → {0, 1}. Extends to all formulas:

Problem: Prove the tautology called the “law of syllogism”: (p → q) → ((q → r) → (p → r)).

Normal Forms and the DPLL Algorithm

Motivation: Automated Satisfiability Checking → Normal Forms → The SAT Problem and the DPLL Algorithm → Numerical Example → Real-World Application → Additional Aspects → Connection with Other Branches of Mathematics → Historical Note and Development of the Idea

Formulas

Second option (if DPLL hit a dead end): if $r = 0 \to (\neg q \vee 0) = (\neg q) \to q = 0 \to (0 \vee 0) = 0$—contradiction! Backtrack.

·$(p \vee q)$: remove (contains $p = 1$) ✓
·$(\neg p \vee r)$: remove $\neg p$ from this disjunct $\to$ $(r)$
·$(\neg q \vee \neg r)$: remains
·$(p \vee \neg r)$: remove ✓
·$(\neg q \vee \neg r)$: remove $\neg r$ $\to$ $(\neg q)$

The SAT (SATisfiability) problem—whether a propositional formula is satisfiable—is NP-complete, but in practice is solved in seconds for millions of variables by modern SAT solvers. They operate on formulas in conjunctive normal form (CNF) and use the DPLL algorithm and its extensions. SAT is the...

Disjunct: A disjunction of literals: $(l_1 \lor l_2 \lor \ldots \lor l_k)$. A unit disjunct: a disjunct consisting of a single literal.

CNF (Conjunctive Normal Form): A conjunction of disjuncts: $D_1 \wedge D_2 \wedge \ldots \wedge D_m$. Any propositional formula can be converted to CNF (equisatisfiable, if using Tseitin transformation).

Algorithm to convert to CNF: 1. Eliminate $\to$ and $\leftrightarrow$: $p \to q \equiv \neg p \vee q$; $p \leftrightarrow q \equiv (\neg p \vee q) \wedge (p \vee \neg q)$ 2. Push $\neg$ inward (de Morgan's laws, double negation) 3. Apply distributivity of $\vee$ over $\wedge$

Axiom Systems and Theorems of Completeness

Motivation: Do “True” and “Provable” Coincide? → Propositional Calculus (Hilbert-Style) → Theorems of Soundness and Completeness → Functional Completeness → Numeric Example → Real-World Application → Additional Aspects → Relation to Other Areas of Mathematics → Historical Note and Development of the Idea

·(A1) φ → (ψ → φ) — "weakening"
·(A2) (φ → (ψ → χ)) → ((φ → ψ) → (φ → χ)) — "distribution"
·(A3) (¬ψ → ¬φ) → (φ → ψ) — "contraposition"
·{¬, ∧} is a basis: p∨q ≡ ¬(¬p∧¬q).
·{NAND} is one-element: p NAND q ≡ ¬(p∧q); ¬p ≡ p NAND p.
·{NOR} is one-element: p NOR q ≡ ¬(p∨q).

In propositional logic, we have two independent concepts: semantics (what is true under every assignment) and syntax (what is derived from axioms by rules). The completeness theorem states their equivalence: everything semantically true is provable. The soundness theorem asserts the converse: eve...

Derivation from Γ: a sequence φ₁, ..., φₙ, where each φᵢ is either an axiom, belongs to Γ, or is obtained from previous formulas using MP. Γ ⊢ φ — φ is derivable from Γ.

Soundness Theorem: Γ ⊢ φ ⟹ Γ ⊨ φ. Proof: induction on the length of the derivation. Axioms are tautologies; MP preserves truth.

Completeness Theorem (Post 1921): Γ ⊨ φ ⟹ Γ ⊢ φ. Every semantic consequence is syntactically provable. This means: the axiom system is "sufficient" for the whole of classical logic.

First-Order Predicate Logic

Predicates, quantifiers, structures, and Gödel’s completeness theorem

Syntax and Semantics of First-Order Logic

Motivation: Speaking About Structures, Not Just Propositions → Syntax of FOL → Semantics: First-Order Structures → Key Concepts → Numerical Example → Real-World Application → Additional Aspects → Connection with Other Areas of Mathematics → Historical Background and Concept Development

Formulas

Structure M = (D, P^M, f^M, c^M):Problem: Let M = (ℤ, <, S), where < is the standard order, S(x) = x+1. Check the truth of:Step 1. (a) ∀x ∃y (x < y): for any integer x we need y > x. Take y = x+1 ∈ ℤ. True ✓.

·Variables x, y, z, ... are terms.
·Constants c are terms.
·If f is a function symbol of arity n and t₁,...,tₙ are terms, then f(t₁,...,tₙ) is a term.
·P(t₁,...,tₙ) is an atomic formula (predicate P applied to terms).
·t₁ = t₂ is an atomic equality formula.
·¬φ, φ∧ψ, φ∨ψ, φ→ψ come from propositional connectives.
·∀x φ is the universal quantifier: “for all x, φ holds.”
·∃x φ is the existential quantifier: “there exists x such that φ holds.”
·D ≠ ∅ is the domain (universe), e.g., ℕ, ℤ, ℝ, a graph, etc.
·For each predicate P of arity n: P^M ⊆ Dⁿ is a relation.
·For each function f of arity n: f^M: Dⁿ → D is a function.
·For each constant c: c^M ∈ D.
·M ⊨ P(t₁,...,tₙ)[μ] ⟺ (t₁^M[μ],...,tₙ^M[μ]) ∈ P^M
·M ⊨ ∀x φ[μ] ⟺ M ⊨ φ[μ[x↦d]] for all d ∈ D
·M ⊨ ∃x φ[μ] ⟺ M ⊨ φ[μ[x↦d]] for some d ∈ D

Propositional logic cannot express “all natural numbers are even” or “there exists a prime number.” First-order logic (FOL) adds quantifiers ∀ and ∃, predicate symbols, and function symbols—this is the language of modern mathematics. FOL is used to formulate group theory, arithmetic, set theory.

Signature σ: a set of predicate symbols P (of arity n), function symbols f (of arity n), and constants c (nullary functions).

Free and bound variables: x is free in φ if it is not within the scope of quantifiers over x. In ∀x P(x, y): x is bound, y is free.

Sentence (closed formula): no free variables. Truth does not depend on assignment.

The Resolution Method and Unification

Motivation: Automated Theorem Proving → Conversion to Clausal Form → Unification → The Resolution Rule → Numerical Example → Real-World Application → Additional Aspects → Connection with Other Areas of Mathematics → Historical Background and Development of the Idea

Formulas

Most General Unifier (MGU): σ such that any other unifier τ = τ' ∘ σ. The MGU is unique up to variable renaming.

·If s = x (a variable): check the occur check (x does not occur in t) → σ = {x↦t}.
·If s = f(s₁,...,sₙ) and t = f(t₁,...,tₙ): unify pairwise.
·If s and t are different constants or functors of different arity → failure.
·∀x (Human(x) → Mortal(x)) → clause: {¬Human(x) ∨ Mortal(x)}
·Human(Socrates) → clause: {Human(Socrates)}
·Negation of the conclusion: ¬Mortal(Socrates) → clause: {¬Mortal(Socrates)}

How can a computer prove mathematical theorems? The resolution method (Robinson, 1965) is an algorithm that reduces checking logical consequence to searching for a contradiction: we negate the conclusion, add it to the premises, and try to derive the empty disjunct ☐. This is the foundation of th...

Steps: 1. Eliminate → and ↔. 2. Push ¬ inward (De Morgan's laws, elimination of double negation). 3. Rename variables (each quantifier gets its own variable). 4. Move quantifiers to the front (convert to prenex form). 5. Skolemization: eliminate ∃. ∃x P(x) → P(c) (new Skolem constant); ∀y ∃x P(x,...

A substitution σ is a mapping of variables → terms. σ(t) is the result of applying σ to term t.

A unifier for a set of pairs {(s₁,t₁),...,(sₙ,tₙ)}: σ such that σ(sᵢ) = σ(tᵢ) for all i.

Gödel's Theorems and First-Order Boundaries

Motivation: Are There Limits to Mathematics? → Gödel's Completeness Theorem for FOL (1930) → The Compactness Theorem for FOL → Gödel's First Incompleteness Theorem (1931) → Numerical Example → Real-World Application → Additional Aspects → Connection With Other Areas of Mathematics → Historical Reference and Development of the Idea

·Γ ⊨ φ ⟺ Γ ⊢ φ (equivalence of semantics and syntax).
·Every consistent theory has a model.
·T ⊬ G_T and T ⊬ ¬G_T.

At the beginning of the 20th century, Hilbert dreamed of formalizing all mathematics within a single complete and consistent system. Gödel in 1930–31 showed that this is impossible. His theorems are the most important philosophical and mathematical result of the 20th century, limiting the power o...

Theorem: φ is logically valid in FOL (holds in all structures) ⟺ φ is derivable from the axioms of FOL (standard predicate calculus).

The key idea of the proof is the Henkin lemma: if Γ is consistent, we construct a “canonical model” from the terms of the language, extended by “witness constants” for each ∃-statement.

Consequence — nonstandard models: Consider Th(ℕ) ∪ {c > 0, c > 1, c > 2, ...}. Every finite subset is satisfiable in ℕ (take c sufficiently large). By compactness, the whole set has a model *ℕ with “infinitely large” c. This is a nonstandard model of arithmetic — ℕ “cannot be uniquely axiomatized...

Computability Theory

Turing machines, decidability, and the Church–Turing thesis

Turing Machines and Computable Functions

Motivation: What is an "algorithm"? → Formal Definition of Turing Machine → Church–Turing Thesis → Languages and Hierarchy → Numerical Example → Real Application → Additional Aspects → Connection with Other Areas of Mathematics → Historical Note and Development of the Idea

Formulas

Deterministic TM M = (Q, Σ, Γ, δ, q₀, q_acc, q_rej):Configuration: (q, u, a, v) — state q, tape = u·a·v, head over a. Compact notation: u_q_v (underlines the position of the head).

·Q — a finite set of states.
·Σ ⊆ Γ — input alphabet (□ ∉ Σ, □ is the blank symbol).
·Γ — tape alphabet.
·δ: Q × Γ → Q × Γ × {L, R} — transition function (read, write, move the head).
·q₀ — initial state; q_acc, q_rej — accepting and rejecting.
·Decidable ⊊ RE (enumerable) ⊊ All languages.
·co-RE = {L : L̄ ∈ RE}. L is decidable ⟺ L ∈ RE ∩ co-RE.
·Start: _q₀_aba. Read 'a', remember it (transition to qₐ), erase the first symbol (→ □): □_qₐ_ba. Move right to the end: □b_qₐ_a. Read last 'a': matches qₐ → erase: □b_q_ret_□.
·Return left: _q_ret_□b□. Find next symbol 'b', transition to q_b, go right: □_q_seek_b_b□. Last 'b' matches: □_q_ret_□□□. Tape is empty → accept ✓.
·Read 'a' → qₐ: □_qₐ_b. Last symbol 'b' ≠ 'a' → reject ✓.

Until the 1930s, the notion of "algorithm" was intuitive. In 1936, Turing proposed a mathematical model of computation—a Turing machine (TM)—and substantiated the thesis: anything that a person can compute "mechanically" is computed by a TM. This made it possible to rigorously prove the existence...

Configuration: (q, u, a, v) — state q, tape = u·a·v, head over a. Compact notation: u_q_v (underlines the position of the head).

Acceptance: M accepts w if computation from the initial configuration reaches q_acc. Rejects if it reaches q_rej. Loops if it reaches neither.

Decider: TM which halts on any input (accept or reject). If L is accepted by a decider, L is decidable. If L is recognized only by a TM, L is enumerable (RE, recursively enumerable).

The Halting Problem and Undecidable Problems

Motivation: The First Limit of Computation → The Halting Problem → Enumerability Without Decidability → Rice’s Theorem → Numerical Example → Real Application → Additional Aspects → Connection with Other Areas of Mathematics → Historical Reference and Development of the Idea

·D(⟨M⟩): if H(⟨M,⟨M⟩⟩) = “yes” → loop forever; if “no” → halt.
·If H(⟨D,⟨D⟩⟩) = “yes” (D halts on ⟨D⟩) → D loops forever → H gave the wrong answer. Contradiction.
·If H(⟨D,⟨D⟩⟩) = “no” (D does not halt) → D halts → Contradiction.
·Some Turing machine possesses P, some do not.
·P is semantic (depends on the computed function, not the code of the Turing machine).
·Will M halt on a specific input w₀?
·Does M accept at least one word (L(M) ≠ ∅)?
·Is L(M) regular?
·Are M₁ and M₂ equivalent (L(M₁) = L(M₂))?
·M_w(x): run M on w; if M(w) halts — accept (for any x).
·(M_w ignores the input x, only simulates M on w.)

Turing in 1936 proved: there exists no program that, for an arbitrary program P and input w, would determine whether P halts on w. This is the Halting Problem. The proof uses an elegant diagonal argument—the same one that Cantor applied for the uncountability of ℝ.

HALT: Given a pair ⟨M, w⟩ (the code of a Turing machine M and a word w). Does M halt on w?

Suppose there exists a decider H for HALT: H(⟨M,w⟩) = “yes” if M(w) halts; “no” otherwise.

Enumerability: Turing machine U (universal Turing machine) simulates M on w and accepts if M halts. If M(w) = ∞ — U loops forever (does not halt with “no”).

Complexity Theory: P vs NP

Motivation: Not Only Computable, but Also Fast → Complexity Classes → NP-Completeness → The P ≠ NP Problem → Numerical Example → Real-World Application → Additional Aspects → Connection with Other Areas of Mathematics → Historical Reference and Development of the Idea

·RSA and elliptic cryptography are broken (the factoring problem ∈ NP).
·Automatic theorem proving: finding a proof = no harder than checking it.
·Optimization: thousands of NP problems are solvable in polynomial time.

The halting problem is undecidable altogether. But most practical problems are computable—the question is, how fast? Complexity theory studies the resources (time, memory) required by algorithms. The question P = NP? is the most important open question in computer science: do the problems whose s...

P (Polynomial Time): L ∈ P if there exists a deterministic Turing machine M and a polynomial p such that: M decides L in time O(p(|w|)) for any input w.

Examples in P: array sorting (O(n log n)), shortest path search (Dijkstra's algorithm O(n²)), primality testing (AKS algorithm, 2002, O((log n)^{12})).

NP (Nondeterministic Polynomial Time): L ∈ NP if there exists a "verifier" V (deterministic Turing machine) with polynomial-time such that: w ∈ L ⟺ there exists a "certificate" c (|c| ≤ poly(|w|)): V(w,c) = "accept".

Proof Theory

Natural deduction, sequent calculus, and the cut-elimination theorem

Natural Deduction and Gentzen Systems

Motivation: How to Formalize Real Mathematical Reasoning? → Rules of Natural Deduction → Curry–Howard Correspondence → Numerical Example → Additional Aspects → Real-World Application → Connection with Other Areas of Mathematics → Historical Note and Development of the Idea

Logic	Type Theory (λ-calculus)
Formula $\varphi$	Type $A$
Proof of $\varphi$	Term $t: A$
$\varphi \to \psi$	Function type $A \to B$
$\varphi \wedge \psi$	Product $A \times B$ (pair)
$\varphi \vee \psi$	Sum $A + B$ (union)
$\bot$	Empty type

·∧-introduction (∧I): from $\varphi$ and $\psi$ infer $\varphi \wedge \psi$.
·∧-elimination (∧E₁): from $\varphi \wedge \psi$ infer $\varphi$. (∧E₂): infer $\psi$.
·→-introduction (→I): if $\psi$ is derived from $[\varphi]$ (the hypothesis $\varphi$ is discharged) then infer $\varphi \to \psi$.
·→-elimination (modus ponens): from $\varphi \to \psi$ and $\varphi$ infer $\psi$.
·∨-introduction: from $\varphi$ infer $\varphi \vee \psi$ (and from $\psi$ infer $\varphi \vee \psi$).
·∨-elimination: from $\varphi \vee \psi$, $[\varphi] \vdash \chi$, $[\psi] \vdash \chi$ infer $\chi$ (case analysis).
·$\forall$-introduction: from $\varphi(y)$ (where $y$ is not free in the hypotheses) infer $\forall x\,\varphi(x)$.
·$\forall$-elimination: from $\forall x\,\varphi(x)$ infer $\varphi(t)$ for any term $t$.
·$\exists$-introduction: from $\varphi(t)$ infer $\exists x\,\varphi(x)$.
·$\exists$-elimination: from $\exists x \varphi(x)$ and $[\varphi(y)\vdash\chi]$ (where $y$ is not free in $\chi$) infer $\chi$.

Hilbert's axiom system (A1, A2, A3 + MP) is technically adequate, but inconvenient in practice: real mathematicians do not reason in terms of "prove $p \to p$ in five steps." Natural deduction (Gentzen, 1935) is a system that imitates standard mathematical practice: we introduce hypotheses, perfo...

A proof is a tree with the proven formula at the root and hypotheses at the leaves (which may be "discharged").

Negation: $\neg \varphi := \varphi \to \bot$. From $\varphi$ and $\neg \varphi$ infer $\bot$. From $[\neg \varphi] \vdash \bot$ infer $\varphi$ (reductio ad absurdum — in classical logic).

Consequence: a constructive proof of $\varphi \to \psi$ is a program transforming a proof of $\varphi$ into a proof of $\psi$. In Coq and Agda: writing programs = constructing mathematical proofs.

Sequent Calculus and Gentzen's Theorem

Motivation: Symmetry and Proof Normalization → Sequents and the LK Calculus → Cut Elimination Theorem (Cut Elimination / Hauptsatz) → Applications → Numerical Example → Additional Aspects → Real-World Application → Connection to Other Areas of Mathematics → Historical Background and Development of the Idea

·Weakening: from Γ ⊢ Δ → Γ, φ ⊢ Δ (and analogously on the right).
·Contraction: from Γ, φ, φ ⊢ Δ → Γ, φ ⊢ Δ.
·Exchange: permutation of formulas in Γ or Δ.

Natural deduction is asymmetric: hypotheses are on the left, conclusion on the right, and the introduction/elimination of connectives is asymmetric. The sequent calculus (Gentzen, 1935) is a symmetric system in which proofs have an explicit structure convenient for metatheorems. The main result—t...

Sequent: Γ ⊢ Δ (read as "from the hypotheses Γ, at least one of Δ follows"). Γ and Δ are multisets of formulas.

Logical rules (example for ∧ on the right): from Γ ⊢ Δ, φ and Γ ⊢ Δ, ψ → Γ ⊢ Δ, φ∧ψ.

Cut rule: from Γ ⊢ Δ, φ and φ, Π ⊢ Λ → Γ, Π ⊢ Δ, Λ. This is "using the lemma φ".

Intuitionism and Constructive Mathematics

Motivation: What Does It Mean to “Prove”? → Intuitionistic Logic (IL) → Diaconescu’s Theorem → Constructive Mathematics and Computer Science → Numerical Example → Real-World Application → Additional Aspects → Connections with Other Fields of Mathematics → Historical Background and Development of the Idea

Formulas

Step 3. Check ¬p in w₀: ¬p = p → ⊥. Is it forced that w₀ ⊩ ¬p? No, because w₁ ≥ w₀ and w₁ ⊩ p, so w₀ ⊬ ¬p (we have a higher world where p is true).Step 4. Check ¬¬p = ¬p → ⊥ in w₀: ¬p → ⊥. Since w₀ ⊬ ¬p (from step 3), the condition “if w₀ ⊩ ¬p” is false → w₀ ⊩ ¬¬p vacuously ✓.

·Law of Excluded Middle (LEM): φ ∨ ¬φ — not accepted in IL (not a tautology).
·Double negation elimination: ¬¬φ → φ — not accepted.
·De Morgan's law: ¬(φ ∧ ψ) → ¬φ ∨ ¬ψ — not accepted.
·Coq (tactical language Gallina + Ltac).
·Agda (dependent types, without tactics).
·Lean 4 (combines mathematics and programming).
·Isabelle/HOL (classical higher-order logic).

Classical mathematics accepts the law of excluded middle: φ ∨ ¬φ — a tautology. Brouwer (1908) and the intuitionists insist: “to prove φ ∨ ψ” means to prove either φ or prove ψ — you cannot simply prove it “by contradiction.” This leads to a weaker logic, but in return every proof is constructive...

What is accepted: modus ponens, ∧-rules, →-rules, ∃xφ(x) only with an explicit witness.

Kripke semantics (1965): “Worlds” w (moments of knowledge) with relation ≤ (growth of knowledge). w ⊩ φ ∨ ψ ⟺ w ⊩ φ or w ⊩ ψ. Countermodel for LEM: world w with w ⊬ p and w ⊬ ¬p.

Theorem: Full Axiom of Choice + Intuitionistic Logic → Law of Excluded Middle.

Model Theory

Models, elementary equivalence, types, and the Löwenheim–Skolem theorem

Löwenheim–Skolem Theorem and Its Paradoxes

Motivation: FOL Cannot “Fix” Cardinality → The Löwenheim–Skolem Theorems → The Skolem Paradox → Isomorphism and Elementary Equivalence → Numerical Example → Real-World Application → Additional Aspects → Connection with Other Areas of Mathematics → Historical Note and Development of the Idea

·Linearity: $\forall x \forall y\ (x < y \vee x = y \vee y < x)$
·Transitivity: $\forall x \forall y \forall z\ (x < y \wedge y < z \rightarrow x < z)$
·Density: $\forall x \forall y\ (x < y \rightarrow \exists z\ (x < z \wedge z < y))$
·No endpoints: $\forall x\ \exists y\ (y < x) \wedge \exists y\ (x < y)$

The Löwenheim–Skolem theorem is the first profound result in model theory. It demonstrates that a first-order theory does not control the cardinality of its models: a theory with a countable model also has an uncountable one, and vice versa. This is the “Skolem paradox” — a countable model of ZFC...

Downward (Löwenheim 1915, Skolem 1920): If T has an infinite model, then T has a countable model.

Upward (Tarski–Vaught): If T has an infinite model of cardinality $\kappa$, then T has a model of cardinality $\lambda$ for any $\lambda \geq \max(\kappa, |\sigma|, \aleph_0)$.

Combined version: If T has a model of cardinality $\kappa \geq |T|$, then T has a model of cardinality $\lambda$ for any $\lambda \geq |T|$.

Types and Saturated Models

Motivation: The "Portrait" of an Element in a Model → Types → Saturated Models → ω-Categoricity → Numerical Example → Real Application → Additional Aspects → Connection with Other Branches of Mathematics → Historical Note and Development of the Idea

Formulas

Fully saturated: $M$ is $\kappa$-saturated with $\kappa = |M|$.

The type of an element is the aggregate of all properties possessed by that element in a given theory. Two models may have different types of elements. A "saturated" model "contains" all possible types—it is maximally rich. The theory of types is the key to understanding when models are isomorphi...

Partial n-type (over the empty set of parameters): A set of formulas $p(x_1,\ldots,x_n)$ such that $p \cup T$ is satisfiable (i.e., there exist elements in some model of $T$ which satisfy all $\varphi \in p$).

Complete n-type: For every formula $\varphi(x_1,\ldots,x_n)$: either $\varphi \in p$, or $\neg\varphi \in p$. The maximally informative type.

Realization of a type: Elements $(a_1,\ldots,a_n) \in M^n$ realize type $p$ if $M \models \varphi(a_1,\ldots,a_n)$ for all $\varphi \in p$.

The Compactness Theorem and Applications

Motivation: Working with Infinite Theories via Finite Ones → The Compactness Theorem → Nonstandard Analysis (Robinson, 1960) → Ultraproducts → Numerical Example → Real-Life Application → Additional Aspects → Connection with Other Areas of Mathematics → Historical Background and Development of the Idea

Formulas

Łoś’s theorem: $\prod_U M_i \equiv M_i$ (for $I = \{$all $i\}$ and fixed ultrafilter $U$) — ultrapower $\prod_U M \equiv M$.

·$\forall i$: $R^{c_1}(v_i) \vee R^{c_2}(v_i) \vee R^{c_3}(v_i)$ — “each vertex has a color.”
·$\forall i$: $\neg(R^{c_1}(v_i) \wedge R^{c_2}(v_i)) \wedge \ldots$ — “no more than one color.”
·For each edge $(v_i,v_j)$ and color $c$: $\neg(R^c(v_i) \wedge R^c(v_j))$ — “adjacent vertices have different colors.”

The compactness theorem is one of the most powerful tools in model theory. It allows us to “construct” models with desired properties by verifying an infinite set of requirements: we only need to ensure that every finite requirement is satisfiable. This is how nonstandard analysis, nonstandard mo...

Theorem (follows from Gödel’s completeness theorem): A set of LFP statements $\Gamma$ is satisfiable ⟺ every finite subset $\Gamma_0 \subset \Gamma$ is satisfiable.

Two ways to prove it: 1. Via the completeness theorem: $\Gamma$ is unsatisfiable ⟺ $\Gamma \vdash \bot$ ⟺ $\vdash$ uses only finitely many axioms from $\Gamma$. 2. Via ultraproducts (more constructive).

The *ℝ construction: Consider $\operatorname{Th}(\mathbb{R}) \cup \{0 < \varepsilon, \varepsilon < 1, \varepsilon < 1/2, \varepsilon < 1/3, \ldots\}$. Every finite subset is satisfiable (take $\varepsilon < 1/n$). By compactness → there exists *ℝ with an “infinitesimal” $\varepsilon > 0$, less th...