Cheatsheet
Математическая логика и теория алгоритмов — all topics on one page
Пропозициональная логика
Синтаксис, семантика, нормальные формы и алгоритм DPLL
Мотивация: зачем формализовывать рассуждения? → Синтаксис → Семантика: таблицы истинности → Логическое следование и эквивалентность → Численный пример → Реальное приложение → Дополнительные аспекты → Связь с другими разделами математики → Историческая справка и развитие идеи
- •Пропозициональные переменные: p, q, r, p₁, p₂, ...
- •Логические связки: ¬ (отрицание), ∧ (конъюнкция — «и»), ∨ (дизъюнкция — «или»), → (импликация — «если... то»), ↔ (эквиваленция — «тогда и только тогда»).
- •Скобки: (, ).
- •I(¬φ) = 1 − I(φ)
- •I(φ ∧ ψ) = min(I(φ), I(ψ)) — истинно, если оба истинны
- •I(φ ∨ ψ) = max(I(φ), I(ψ)) — истинно, если хотя бы одно
- •I(φ → ψ) = max(1−I(φ), I(ψ)) — ложно только при φ=1, ψ=0
- •I(φ ↔ ψ) = 1 тогда и только тогда, когда I(φ) = I(ψ)
- •Тавтология: I(φ) = 1 при всех интерпретациях. Обозначение: ⊨ φ.
- •Противоречие (антитавтология): I(φ) = 0 при всех интерпретациях.
- •Выполнимость: I(φ) = 1 для некоторой I.
- •¬¬p ≡ p (двойное отрицание)
- •(p → q) ≡ (¬p ∨ q) (импликация через дизъюнкцию)
- •¬(p ∧ q) ≡ (¬p ∨ ¬q) (закон де Моргана)
- •¬(p ∨ q) ≡ (¬p ∧ ¬q) (закон де Моргана)
- •p ∧ (q ∨ r) ≡ (p ∧ q) ∨ (p ∧ r)
- •p ∨ (q ∧ r) ≡ (p ∨ q) ∧ (p ∨ r)
Математические доказательства состоят из шагов, в которых одни утверждения выводятся из других. Но что такое «правильный» шаг? Пропозициональная логика даёт точный язык: синтаксис (как записывать формулы) и семантику (что они означают). Это фундамент, на котором стоят автоматические доказатели, к...
Индуктивное определение формул: 1. Каждая переменная p — формула. 2. Если φ — формула, то ¬φ — формула. 3. Если φ и ψ — формулы, то (φ ∧ ψ), (φ ∨ ψ), (φ → ψ), (φ ↔ ψ) — формулы. 4. Ничто другое не является формулой.
Интерпретация (оценка): функция I: {переменные} → {0, 1}. Расширяется на все формулы:
Следование: Γ ⊨ φ, если любая I, делающая все ψ ∈ Γ истинными, делает истинным φ.
Мотивация: автоматическая проверка выполнимости → Нормальные формы → Задача SAT и алгоритм DPLL → Численный пример → Реальное приложение → Дополнительные аспекты → Связь с другими разделами математики → Историческая справка и развитие идеи
- •(p ∨ q): удалить (содержит p = 1) ✓
- •(¬p ∨ r): удалить ¬p из дизъюнкта → (r)
- •(¬q ∨ ¬r): остаётся
- •(p ∨ ¬r): удалить ✓
- •(¬q ∨ ¬r): удалить ¬r → (¬q)
Задача SAT (SATisfiability) — проверить, выполнима ли пропозициональная формула — NP-полна, но на практике решается за секунды для миллионов переменных с помощью современных SAT-солверов. Они работают с формулами в конъюнктивной нормальной форме (КНФ) и используют алгоритм DPLL и его расширения. ...
Дизъюнкт: дизъюнкция литералов: (l₁ ∨ l₂ ∨ ... ∨ lₖ). Единичный дизъюнкт: дизъюнкт из одного литерала.
КНФ (конъюнктивная нормальная форма): конъюнкция дизъюнктов: D₁ ∧ D₂ ∧ ... ∧ Dₘ. Любая пропозициональная формула приводима к КНФ (равновыполнимой, если использовать трансформацию Цейтина).
Алгоритм приведения к КНФ: 1. Устранить → и ↔: p→q ≡ ¬p∨q; p↔q ≡ (¬p∨q)∧(p∨¬q) 2. Загнать ¬ внутрь (законы де Моргана, двойное отрицание) 3. Применить дистрибутивность ∨ над ∧
Мотивация: совпадают ли «истинно» и «доказуемо»? → Исчисление высказываний (стиль Гильберта) → Теоремы корректности и полноты → Функциональная полнота → Численный пример → Реальное приложение → Дополнительные аспекты → Связь с другими разделами математики → Историческая справка и развитие идеи
- •(A1) φ → (ψ → φ) — «слабление»
- •(A2) (φ → (ψ → χ)) → ((φ → ψ) → (φ → χ)) — «распределение»
- •(A3) (¬ψ → ¬φ) → (φ → ψ) — «контрапозиция»
- •{¬, ∧} — базис: p∨q ≡ ¬(¬p∧¬q).
- •{NAND} — однэлементный: p NAND q ≡ ¬(p∧q); ¬p ≡ p NAND p.
- •{NOR} — однэлементный: p NOR q ≡ ¬(p∨q).
В пропозициональной логике мы имеем два независимых понятия: семантика (что истинно при каждой оценке) и синтаксис (что выводится из аксиом по правилам). Теорема полноты утверждает их совпадение: всё семантически истинное доказуемо. Теорема корректности — обратное: всё доказуемое истинно. Вместе ...
Вывод из Γ: последовательность φ₁, ..., φₙ, где каждая φᵢ — аксиома, либо принадлежит Γ, либо получена из предыдущих по MP. Γ ⊢ φ — φ выводима из Γ.
Теорема корректности (Soundness): Γ ⊢ φ ⟹ Γ ⊨ φ. Доказательство: индукция по длине вывода. Аксиомы — тавтологии; MP сохраняет истинность.
Теорема полноты (Completeness, Пост 1921): Γ ⊨ φ ⟹ Γ ⊢ φ. Любое семантическое следствие — синтаксически доказуемо. Это означает: система аксиом «достаточна» для всей классической логики.
Логика предикатов первого порядка
Предикаты, кванторы, структуры и теорема Гёделя о полноте
Мотивация: говорить о структурах, а не просто о высказываниях → Синтаксис ЛПП → Семантика: структуры первого порядка → Ключевые понятия → Численный пример → Реальное приложение → Дополнительные аспекты → Связь с другими разделами математики → Историческая справка и развитие идеи
- •Переменные x, y, z, ... — термы.
- •Константы c — термы.
- •Если f — функциональный символ арности n и t₁,...,tₙ — термы, то f(t₁,...,tₙ) — терм.
- •P(t₁,...,tₙ) — атомарная формула (предикат P применён к термам).
- •t₁ = t₂ — атомарная формула равенства.
- •¬φ, φ∧ψ, φ∨ψ, φ→ψ — из пропозициональных связок.
- •∀x φ — квантор всеобщности: «для всех x выполнено φ».
- •∃x φ — квантор существования: «существует x, для которого φ».
- •D ≠ ∅ — домен (носитель), например ℕ, ℤ, ℝ, граф и т.д.
- •Для каждого P арности n: P^M ⊆ Dⁿ — отношение.
- •Для каждого f арности n: f^M: Dⁿ → D — функция.
- •Для каждой константы c: c^M ∈ D.
- •M ⊨ P(t₁,...,tₙ)[μ] ⟺ (t₁^M[μ],...,tₙ^M[μ]) ∈ P^M
- •M ⊨ ∀x φ[μ] ⟺ M ⊨ φ[μ[x↦d]] для всех d ∈ D
- •M ⊨ ∃x φ[μ] ⟺ M ⊨ φ[μ[x↦d]] для некоторого d ∈ D
Пропозициональная логика не может выразить «все натуральные числа чётны» или «существует простое число». Логика первого порядка (ЛПП, FOL) добавляет кванторы ∀ и ∃, предикатные символы и функциональные символы — это язык современной математики. В ЛПП формулируются теория групп, арифметика, теория...
Сигнатура σ: множество предикатных символов P (с арностью n), функциональных символов f (с арностью n) и констант c (нульарные функции).
Свободные и связанные переменные: x свободна в φ, если она не в области действия кванторов по x. В ∀x P(x,y): x — связана, y — свободна.
Предложение (замкнутая формула): нет свободных переменных. Истинность не зависит от оценки.
Мотивация: автоматическое доказательство теорем → Приведение к клаузальной форме → Унификация → Правило резолюции → Численный пример → Реальное приложение → Дополнительные аспекты → Связь с другими разделами математики → Историческая справка и развитие идеи
Definitions
- •Если s = x (переменная): проверить occur check (x не входит в t) → σ = {x↦t}.
- •Если s = f(s₁,...,sₙ) и t = f(t₁,...,tₙ): унифицировать попарно.
- •Если s и t — различные константы или функторы разной арности → неудача.
- •∀x (Human(x) → Mortal(x)) → клауза: {¬Human(x) ∨ Mortal(x)}
- •Human(Socrates) → клауза: {Human(Socrates)}
- •Отрицание заключения: ¬Mortal(Socrates) → клауза: {¬Mortal(Socrates)}
Как компьютер может доказывать математические теоремы? Метод резолюций (Робинсон, 1965) — алгоритм, который сводит проверку логического следования к поиску противоречия: мы отрицаем заключение, добавляем к посылкам, и пытаемся вывести пустой дизъюнкт ☐. Это основа языка Prolog и современных ATP-с...
Шаги: 1. Устранить → и ↔. 2. Загнать ¬ внутрь (де Морган, снятие двойного отрицания). 3. Переименовать переменные (каждый квантор — своя переменная). 4. Вынести кванторы (привести к предварённой форме). 5. Сколемизация: устранить ∃. ∃x P(x) → P(c) (новая константа Сколема); ∀y ∃x P(x,y) → ∀y P(f(...
Подстановка σ — отображение переменных → термы. σ(t) — результат применения σ к терму t.
Унификатор для множества пар {(s₁,t₁),...,(sₙ,tₙ)}: σ такой, что σ(sᵢ) = σ(tᵢ) для всех i.
Мотивация: есть ли пределы у математики? → Теорема Гёделя о полноте ЛПП (1930) → Теорема о компактности ЛПП → Первая теорема Гёделя о неполноте (1931) → Численный пример → Реальное приложение → Дополнительные аспекты → Связь с другими разделами математики → Историческая справка и развитие идеи
- •Γ ⊨ φ ⟺ Γ ⊢ φ (эквивалентность семантики и синтаксиса).
- •Каждая непротиворечивая теория имеет модель.
- •T ⊬ G_T и T ⊬ ¬G_T.
В начале XX века Гильберт мечтал: формализовать всю математику в единой полной и непротиворечивой системе. Гёдель в 1930–31 годах показал, что это невозможно. Его теоремы — важнейший философский и математический результат XX века, ограничивающий силу любой формальной системы.
Теорема: φ логически истинна в ЛПП (выполнена во всех структурах) ⟺ φ выводима из аксиом ЛПП (стандартное исчисление предикатов).
Ключевая идея доказательства — лемма Хенкина: если Γ непротиворечива, строим «каноническую модель» из термов языка, расширенного «константами-свидетелями» для каждого ∃-предложения.
Следствие — нестандартные модели: Рассмотрим Th(ℕ) ∪ {c > 0, c > 1, c > 2, ...}. Каждое конечное подмножество выполнимо в ℕ (возьмём c достаточно большим). По компактности, всё множество имеет модель *ℕ с «бесконечно большим» c. Это нестандартная модель арифметики — ℕ «не аксиоматизируется» первы...
Теория вычислимости
Машины Тьюринга, разрешимость и теорема Черча-Тьюринга
Мотивация: что такое «алгоритм»? → Формальное определение МТ → Тезис Черча–Тьюринга → Языки и иерархия → Численный пример → Реальное приложение → Дополнительные аспекты → Связь с другими разделами математики → Историческая справка и развитие идеи
Formulas
- •Q — конечное множество состояний.
- •Σ ⊆ Γ — входной алфавит (□ ∉ Σ, □ — символ пробела).
- •Γ — ленточный алфавит.
- •δ: Q × Γ → Q × Γ × {L, R} — функция переходов (прочитать, записать, сдвинуть головку).
- •q₀ — начальное состояние; q_acc, q_rej — принимающее и отвергающее.
- •Разрешимые ⊊ RE (перечислимые) ⊊ Все языки.
- •co-RE = {L : L̄ ∈ RE}. L разрешим ⟺ L ∈ RE ∩ co-RE.
- •Начало: _q₀_aba. Читаем 'a', запоминаем (переходим в qₐ), стираем первый символ (→ □): □_qₐ_ba. Перемещаемся вправо до конца: □b_qₐ_a. Читаем последний 'a': совпадает с qₐ → стираем: □b_q_ret_□.
- •Возвращаемся влево: _q_ret_□b□. Находим следующий символ 'b', переходим в q_b, идём вправо: □_q_seek_b_b□. Последний 'b' совпадает: □_q_ret_□□□. Лента пуста → принять ✓.
- •Читаем 'a' → qₐ: □_qₐ_b. Последний символ 'b' ≠ 'a' → отвергнуть ✓.
До 1930-х годов понятие «алгоритм» было интуитивным. Тьюринг в 1936 году предложил математическую модель вычислений — машину Тьюринга (МТ) — и обосновал тезис: любое, что человек может вычислить «механически», вычисляет МТ. Это позволило строго доказать существование невычислимых функций.
Конфигурация: (q, u, a, v) — состояние q, лента = u·a·v, головка над a. Компактная запись: u_q_v (подчёркивает позицию головки).
Принятие: M принимает w, если вычисление из начальной конфигурации достигает q_acc. Отвергает — если достигает q_rej. Зацикливается — если не достигает ни того, ни другого.
Разрешитель: МТ, которая останавливается на любом входе (принять или отвергнуть). Если L принимается разрешителем — L разрешим (decidable). Если только распознаётся МТ — L перечислим (RE, recursively enumerable).
Мотивация: первый предел вычислений → Проблема остановки → Перечислимость без разрешимости → Теорема Райса → Численный пример → Реальное приложение → Дополнительные аспекты → Связь с другими разделами математики → Историческая справка и развитие идеи
- •D(⟨M⟩): если H(⟨M,⟨M⟩⟩) = «да» → зациклиться; если «нет» → остановиться.
- •Если H(⟨D,⟨D⟩⟩) = «да» (D останавливается на ⟨D⟩) → D зацикливается → H выдал неверный ответ. Противоречие.
- •Если H(⟨D,⟨D⟩⟩) = «нет» (D не останавливается) → D останавливается → Противоречие.
- •Некоторая МТ обладает P, некоторая — нет.
- •P — семантическое (зависит от вычисляемой функции, а не от кода МТ).
- •Остановится ли M на конкретном входе w₀?
- •Принимает ли M хотя бы одно слово (L(M) ≠ ∅)?
- •Является ли L(M) регулярным?
- •Эквивалентны ли M₁ и M₂ (L(M₁) = L(M₂))?
- •M_w(x): запустить M на w; если M(w) останавливается — принять (для любого x).
- •(M_w игнорирует вход x, только симулирует M на w.)
Тьюринг в 1936 году доказал: не существует программы, которая для произвольной программы P и входа w определила бы, завершится ли P на w. Это проблема остановки (Halting Problem). Доказательство использует элегантный диагональный аргумент — тот же, что Кантор применял для несчётности ℝ.
Предположим, существует разрешитель H для HALT: H(⟨M,w⟩) = «да», если M(w) останавливается; «нет» — иначе.
Перечислимость: МТ U (универсальная МТ) симулирует M на w и принимает, если M останавливается. При M(w) = ∞ — U зацикливается (не останавливается с «нет»).
Теорема (Райс, 1953): Любое нетривиальное семантическое свойство вычислимых функций неразрешимо.
Мотивация: не только вычислимо, но и быстро → Классы сложности → NP-полнота → Проблема P ≠ NP → Численный пример → Реальное приложение → Дополнительные аспекты → Связь с другими разделами математики → Историческая справка и развитие идеи
- •RSA и эллиптическая криптография сломаны (задача факторизации ∈ NP).
- •Автоматическое доказательство теорем: найти доказательство = не сложнее проверить.
- •Оптимизация: тысячи NP-задач решаются за полиномиальное время.
Проблема остановки неразрешима совсем. Но большинство практических задач вычислимы — вопрос в том, насколько быстро. Теория сложности изучает ресурсы (время, память), требуемые алгоритмами. Проблема P = NP? — важнейший открытый вопрос информатики: совпадают ли задачи, решения которых быстро наход...
P (Polynomial Time): L ∈ P, если ∃ детерминированная МТ M и полином p: M разрешает L за время O(p(|w|)) при любом входе w.
Примеры в P: сортировка массива (O(n log n)), поиск кратчайшего пути (алгоритм Дейкстры O(n²)), проверка простоты числа (алгоритм AKS, 2002, O((log n)^{12})).
NP (Nondeterministic Polynomial Time): L ∈ NP, если ∃ «верификатор» V (детерминированная МТ) с полиномиальным временем такой, что: w ∈ L ⟺ ∃ «сертификат» c (|c| ≤ poly(|w|)): V(w,c) = «принять».
Теория доказательств
Натуральный вывод, секвенциальное исчисление и теорема об устранении сечений
Мотивация: как формализовать реальные математические рассуждения? → Правила натурального вывода → Соответствие Карри–Говарда → Численный пример → Дополнительные аспекты → Реальное приложение → Связь с другими разделами математики → Историческая справка и развитие идеи
| Логика | Теория типов (λ-исчисление) |
|---|---|
| Формула φ | Тип A |
| Доказательство φ | Терм t: A |
| φ → ψ | Функциональный тип A → B |
| φ ∧ ψ | Произведение A × B (пара) |
| φ ∨ ψ | Сумма A + B (объединение) |
| ⊥ | Пустой тип |
- •∧-введение (∧I): из φ и ψ ⊢ φ ∧ ψ.
- •∧-устранение (∧E₁): из φ ∧ ψ ⊢ φ. (∧E₂): ⊢ ψ.
- •→-введение (→I): если из [φ] доказано ψ (гипотеза φ разряжается) → ⊢ φ → ψ.
- •→-устранение (modus ponens): из φ→ψ и φ ⊢ ψ.
- •∨-введение: из φ ⊢ φ ∨ ψ (и из ψ ⊢ φ ∨ ψ).
- •∨-устранение: из φ∨ψ, [φ]⊢χ, [ψ]⊢χ ⊢ χ (разбор случаев).
- •∀-введение: из φ(y) (y не свободна в гипотезах) ⊢ ∀x φ(x).
- •∀-устранение: из ∀x φ(x) ⊢ φ(t) для любого терма t.
- •∃-введение: из φ(t) ⊢ ∃x φ(x).
- •∃-устранение: из ∃xφ(x) и [φ(y)⊢χ] (y не свободна в χ) ⊢ χ.
Система аксиом Гильберта (A1, A2, A3 + MP) технически адекватна, но неудобна для работы: реальные математики не рассуждают «выведи p→p за пять шагов». Натуральный вывод (Gentzen, 1935) — система, имитирующая привычную математическую практику: вводим гипотезы, разбираем случаи, применяем правила в...
Вывод — дерево, в корне — доказываемая формула, в листьях — гипотезы (могут быть «разряжены»).
Отрицание: ¬φ := φ→⊥. Из φ и ¬φ ⊢ ⊥. Из [¬φ]⊢⊥ ⊢ φ (reductio ad absurdum — в классике).
Следствие: конструктивное доказательство φ → ψ — это программа, преобразующая доказательство φ в доказательство ψ. Coq и Agda: писать программы = строить математические доказательства.
Мотивация: симметрия и нормализация доказательств → Секвенции и исчисление LK → Теорема об устранении сечений (Cut Elimination / Hauptsatz) → Приложения → Численный пример → Дополнительные аспекты → Реальное приложение → Связь с другими разделами математики → Историческая справка и развитие идеи
- •Ослабление (Weakening): из Γ ⊢ Δ → Γ, φ ⊢ Δ (и аналогично справа).
- •Сжатие (Contraction): из Γ, φ, φ ⊢ Δ → Γ, φ ⊢ Δ.
- •Обмен (Exchange): перестановка формул в Γ или Δ.
Натуральный вывод несимметричен: гипотезы слева, заключение справа, и введение/устранение связок асимметрично. Секвенциальное исчисление (Gentzen, 1935) — симметричная система, где доказательства имеют явную структуру, удобную для мета-теоремы. Главный результат — теорема об устранении сечений — ...
Секвенция: Γ ⊢ Δ (читается «из гипотез Γ следует хотя бы одна из Δ»). Γ и Δ — мультимножества формул.
Логические правила (пример для ∧ справа): из Γ ⊢ Δ, φ и Γ ⊢ Δ, ψ → Γ ⊢ Δ, φ∧ψ.
Правило сечения (Cut): из Γ ⊢ Δ, φ и φ, Π ⊢ Λ → Γ, Π ⊢ Δ, Λ. Это «использование леммы φ».
Мотивация: что значит «доказать»? → Интуиционистская логика (ИИ) → Теорема Диаконеску → Конструктивная математика и компьютерные науки → Численный пример → Реальное приложение → Дополнительные аспекты → Связь с другими разделами математики → Историческая справка и развитие идеи
- •Закон исключённого третьего (ЛИТ): φ ∨ ¬φ — не принят в ИИ (не является тавтологией).
- •Снятие двойного отрицания: ¬¬φ → φ — не принято.
- •Закон де Моргана: ¬(φ ∧ ψ) → ¬φ ∨ ¬ψ — не принят.
- •Coq (тактический язык Gallina + Ltac).
- •Agda (зависимые типы, без тактик).
- •Lean 4 (объединяет математику и программирование).
- •Isabelle/HOL (классическая логика высшего порядка).
Классическая математика принимает закон исключённого третьего: φ ∨ ¬φ — тавтология. Брауэр (1908) и интуиционисты настаивают: «доказать φ ∨ ψ» означает либо доказать φ, либо доказать ψ — нельзя просто «от противного». Это ведёт к более слабой логике, но зато каждое доказательство конструктивно — ...
Что принято: modus ponens, ∧-правила, →-правила, ∃xφ(x) лишь при наличии конкретного свидетеля.
Семантика Крипке (1965): «Миры» w (моменты знания) с отношением ≤ (рост знаний). w ⊩ φ ∨ ψ ⟺ w ⊩ φ или w ⊩ ψ. Контрмодель для ЛИТ: мир w с w ⊬ p и w ⊬ ¬p.
Теорема: Аксиома Выбора (полная) + Интуиционистская логика → Закон Исключённого Третьего.
Теория моделей
Модели, элементарная эквивалентность, типы и теорема Лёвенхейма-Сколема
Мотивация: ЛПП не может «зафиксировать» мощность → Теоремы Лёвенхейма–Сколема → Парадокс Сколема → Изоморфизм и элементарная эквивалентность → Численный пример → Реальное приложение → Дополнительные аспекты → Связь с другими разделами математики → Историческая справка и развитие идеи
- •Линейность: ∀x∀y (x<y ∨ x=y ∨ y<x)
- •Транзитивность: ∀x∀y∀z (x<y ∧ y<z → x<z)
- •Плотность: ∀x∀y (x<y → ∃z (x<z ∧ z<y))
- •Без концов: ∀x ∃y (y<x) ∧ ∃y (x<y)
Теорема Лёвенхейма–Сколема — первый глубокий результат теории моделей. Она показывает, что первопорядковая теория не контролирует мощность своих моделей: теория, имеющая счётную модель, имеет несчётную, и наоборот. Это «парадокс Сколема» — счётная модель теории ZFC содержит «несчётные» множества.
Нисходящая (Löwenheim 1915, Skolem 1920): Если T имеет бесконечную модель, то T имеет счётную модель.
Восходящая (Тарский–Ваот): Если T имеет бесконечную модель мощности κ, то T имеет модель мощности λ для любой λ ≥ max(κ, |σ|, ℵ₀).
Объединённая версия: Если T имеет модель мощности κ ≥ |T|, то T имеет модель мощности λ для любой λ ≥ |T|.
Мотивация: «портрет» элемента в модели → Типы → Насыщенные модели → ω-категоричность → Численный пример → Реальное приложение → Дополнительные аспекты → Связь с другими разделами математики → Историческая справка и развитие идеи
Тип элемента — это совокупность всех свойств, которыми обладает данный элемент в данной теории. Две модели могут иметь разные типы элементов. «Насыщенная» модель «содержит» все возможные типы — она максимально богата. Теория типов — ключ к пониманию, когда модели изоморфны, и к построению «канони...
Частичный n-тип (над пустым множеством параметров): Множество формул p(x₁,...,xₙ) такое, что p ∪ T выполнимо (т.е. в некоторой модели T существуют элементы, удовлетворяющие всем φ ∈ p).
Полный n-тип: Для каждой формулы φ(x₁,...,xₙ): либо φ ∈ p, либо ¬φ ∈ p. Максимально информативный тип.
Реализация типа: Элементы (a₁,...,aₙ) ∈ Mⁿ реализуют тип p, если M ⊨ φ(a₁,...,aₙ) для всех φ ∈ p.
Мотивация: работа с бесконечными теориями через конечные → Теорема о компактности → Нестандартный анализ (Робинсон, 1960) → Ультрапроизведения → Численный пример → Реальное приложение → Дополнительные аспекты → Связь с другими разделами математики → Историческая справка и развитие идеи
- •∀i: Rᶜ¹(vᵢ) ∨ Rᶜ²(vᵢ) ∨ Rᶜ³(vᵢ) — «каждая вершина имеет цвет».
- •∀i: ¬(Rᶜ¹(vᵢ) ∧ Rᶜ²(vᵢ)) ∧ ... — «не более одного цвета».
- •Для каждого ребра (vᵢ,vⱼ) и цвета c: ¬(Rᶜ(vᵢ) ∧ Rᶜ(vⱼ)) — «смежные вершины разного цвета».
Теорема о компактности — один из самых мощных инструментов теории моделей. Она позволяет «строить» модели с нужными свойствами через проверку бесконечного набора требований: нужно лишь убедиться, что каждое конечное требование выполнимо. Так строятся нестандартный анализ, нестандартные модели ари...
Теорема (следует из теоремы полноты Гёделя): Множество предложений Γ ЛПП выполнимо ⟺ каждое конечное подмножество Γ₀ ⊂ Γ выполнимо.
Два способа доказательства: 1. Через теорему полноты: Γ невыполнимо ⟺ Γ ⊢ ⊥ ⟺ ⊢ используется лишь конечное число аксиом из Γ. 2. Через ультрапроизведения (более конструктивно).
Конструкция *ℝ: Рассмотрим Th(ℝ) ∪ {0 < ε, ε < 1, ε < 1/2, ε < 1/3, ...}. Каждое конечное подмножество выполнимо (взять ε < 1/n). По компактности → существует *ℝ с «бесконечно малым» ε > 0, меньшим 1/n для всех стандартных n.