Математическая логика
Предикатная логика первого порядка
Rust не даёт программам падать с use-after-free. Не через тесты, не через runtime - через систему типов, основанную на линейной логике. Компилятор отвергает программу, если не может доказать безопасность: borrow checker - это theorem prover. В 2024-м DeepMind's AlphaProof решил задачи МатОлимпиады через формальный вывод в Lean. SQL WHERE - это ∀ и ∃ в промышленном масштабе. Предикатная логика первого порядка - не абстракция. Это язык, на котором работают современные системы верификации, автоматические доказатели и языки запросов.
- **Z3 (Microsoft Research)**: SMT-солвер на основе FOL верифицирует Windows kernel, AWS IAM-политики, Apple M-серию чипов - формулы с миллионами ограничений
- **Lean / Coq**: proof assistants на FOL и зависимых типах - AlphaProof (DeepMind, 2024) решил 4 из 6 задач IMO через формальный вывод в Lean
- **Rust borrow checker**: линейная логика как система типов - компилятор как theorem prover, формально исключающий целые классы ошибок
- **SQL WHERE / JOIN**: ∀ и ∃ на миллиардах строк - каждый EXISTS (SELECT 1 ...) это квантор существования в действии
Кванторы
В 2024 году DeepMind's AlphaProof решил 4 из 6 задач Международной математической олимпиады. Не нейросеть, угадывающая ответ методом перебора. Формальный доказатель теорем, работающий в системе Lean - языке, основанном на предикатной логике. Пропозициональная логика позволяет рассуждать о фиксированных фактах: «p или q». Предикатная логика первого порядка (FOL) добавляет **кванторы** - и позволяет рассуждать об **общих утверждениях** над бесконечными множествами объектов.
Кванторы вкладываются - и порядок критичен. `∀x ∃y (y > x)` говорит: для каждого x находится свой y (верно для целых чисел). `∃y ∀x (y > x)` говорит: существует одно y, большее всех x (ложно - максимума нет). Одни и те же символы, переставленные местами - и смысл меняется кардинально. Этот факт Гёдель превратил в теорему о неполноте.
**Предикаты** - функции, возвращающие True/False: Human(x), Greater(x, y), Connected(a, b). **Функции** - термы: father(x), plus(x, y). **Константы** - конкретные объекты: 0, Socrates, Moscow. Формула первого порядка комбинирует предикаты, функции, константы, связки и кванторы.
| Утверждение | Формула FOL | Чтение |
|---|---|---|
| Все студенты учатся | ∀x (Student(x) -> Studies(x)) | Если студент, то учится |
| Кто-то любит всех | ∃x ∀y Loves(x, y) | Есть тот, кто любит каждого |
| Каждого кто-то любит | ∀y ∃x Loves(x, y) | У каждого есть тот, кто его любит |
| Нет наибольшего числа | ∀x ∃y (y > x) | Для каждого числа есть большее |
| Транзитивность | ∀x∀y∀z ((R(x,y) ∧ R(y,z)) -> R(x,z)) | Если xRy и yRz, то xRz |
SQL - это предикатная логика в производственном масштабе. `SELECT * FROM users WHERE EXISTS (SELECT 1 FROM orders WHERE orders.user_id = users.id)` - буквально `∀u (User(u) ∧ ∃o (Order(o) ∧ related(o,u)))`. Каждый JOIN - квантор. Каждый WHERE - предикат. Миллиарды запросов в секунду - это FOL в железе.
∀x ∃y (y > x) и ∃y ∀x (y > x) - в чём разница?
Свободные и связанные переменные
В формуле `∀x (P(x) -> Q(x, y))` переменная x **связана** квантором ∀, а y - **свободная**: она не попадает в область действия ни одного квантора. Свободные переменные - параметры формулы. Формула не имеет определённого истинностного значения, пока не зафиксировано значение y.
**Замкнутая формула** (sentence) - формула без свободных переменных. Только замкнутые формулы имеют определённое истинностное значение в данной интерпретации. Формула со свободными переменными - шаблон, предикат, который становится утверждением после подстановки.
**Capture avoidance**: при подстановке нужно избегать «захвата» переменной квантором. Подстановка x := y в `∀y (P(x,y))` даёт `∀y (P(y,y))` - свободная y стала связанной. Правильно: сначала переименовать `∀z (P(x,z))`, потом подставить: `∀z (P(y,z))`. Та же проблема - shadowing переменных - существует в каждом языке программирования.
Это аналог **scope** в программировании. В Python `for x in range(10): print(x, y)` - x связана циклом, y свободная (должна быть в outer scope). Rust пошёл дальше: его borrow checker - это система типов на основе линейной логики, которая формально отслеживает scope каждой переменной. Компилятор - это theorem prover.
| Формула | Свободные | Связанные | Sentence? |
|---|---|---|---|
| ∀x P(x) | - | x | Да |
| P(x) ∧ Q(y) | x, y | - | Нет |
| ∀x (P(x) -> Q(x, y)) | y | x | Нет |
| ∀x ∃y R(x, y, z) | z | x, y | Нет |
| ∀x ∀y ∃z (x + y = z) | - | x, y, z | Да |
В формуле ∀x (P(x, y) -> ∃y Q(x, y)) - какие переменные свободные?
Интерпретация и модель
Формула `∀x ∃y (y > x)` - истинна или ложна? Зависит от того, что означают x, y и «>». На натуральных числах - истинна. На множестве {1} - ложна. На рациональных числах промежутка [0,1] - тоже истинна (берём (x+1)/2). **Интерпретация** задаёт смысл: домен, значения предикатов, функций и констант.
**Модель** - интерпретация, в которой формула истинна. Формула **выполнима** (satisfiable), если у неё есть хотя бы одна модель. **Невыполнима**, если ни одна интерпретация не делает её истинной. В пропозициональной логике интерпретация - это просто набор T/F значений для переменных. В FOL интерпретация требует домена, предикатов, функций - что делает язык несравнимо выразительнее.
**Логическое следствие** (entailment): φ |= ψ означает, что в каждой модели φ, формула ψ тоже истинна. Пример: {∀x (Human(x) -> Mortal(x)), Human(Socrates)} |= Mortal(Socrates). Это формализация силлогизма Аристотеля - в строгих математических терминах.
| Термин | Определение | Пропозициональный аналог |
|---|---|---|
| Интерпретация | Домен + значения символов | Valuation (T/F) |
| Модель | Интерпретация, где φ = True | Satisfying assignment |
| Выполнимость | Есть хотя бы одна модель | SAT |
| Общезначимость | Истинна во ВСЕХ интерпретациях | Тавтология |
| Логическое следствие | φ |= ψ: в каждой модели φ, ψ тоже True | Entailment |
Формула ∀x P(x) в интерпретации I = {D={1,2,3}, P={1,2}}. Истинна?
Общезначимость и неразрешимость
1936 год. Алонзо Чёрч и Алан Тьюринг независимо друг от друга доказывают один и тот же факт: не существует алгоритма, который бы для произвольной FOL-формулы определял, общезначима она или нет. Это **теорема Чёрча** - и она фундаментально отличает FOL от пропозициональной логики. В SAT задача NP-полная, но разрешимая. В FOL - неразрешимая вообще.
**Полуразрешимость** - интересный промежуточный случай. Если формула общезначима, существует алгоритм (Resolution, Tableaux), который это подтвердит за конечное время. Если формула не является общезначимой - алгоритм может работать вечно. Нельзя сказать «закончи через час и скажи ответ»: гарантии завершения нет. Именно поэтому автоматические доказатели теорем - не полностью автоматические.
**Связь с проблемой остановки**: Тьюринг показал, что задача остановки машины Тьюринга неразрешима. Чёрч показал, что общезначимость FOL неразрешима. Это не совпадение - эти два результата изоморфны. Любую программу можно закодировать как FOL-формулу: остановка программы = выполнимость формулы. Предел вычислений и предел логики - одно и то же.
| Проблема | Пропозициональная логика | FOL |
|---|---|---|
| SAT (выполнимость) | NP-полная (разрешима) | Неразрешима (в общем) |
| VALID (общезначимость) | co-NP (разрешима) | Полуразрешима |
| Модели | Конечные (valuations) | Могут быть бесконечными |
| Автоматизация | SAT-солверы (Z3, CaDiCaL) | SMT-солверы, Lean, Coq |
∀x ∃y R(x,y) - это то же самое, что ∃y ∀x R(x,y)
Порядок кванторов критичен: ∀x∃y означает «для каждого x свой y», а ∃y∀x - «один y для всех x»
∀x ∃y (y > x): для каждого числа x найдётся большее y - TRUE для целых (берём y = x+1). ∃y ∀x (y > x): существует число больше ВСЕХ чисел - FALSE, максимального целого нет. Перестановка кванторов меняет зависимость: y от x vs фиксированный y. Эта разница - основа всей теории баз данных и логики.
Формула ∀x (P(x) ∨ ¬P(x)). К какому классу она относится?
Ключевые идеи
- **Кванторы** ∀ (для всех) и ∃ (существует) расширяют пропозициональную логику до общих утверждений над произвольными доменами
- **Порядок кванторов критичен**: ∀x∃y и ∃y∀x - разные утверждения, что видно на ∀x∃y(y>x) vs ∃y∀x(y>x) для целых чисел
- **Свободные/связанные** переменные: связанная управляется квантором, свободная - параметр формулы; аналог scope в программировании
- **Интерпретация** = домен + значения предикатов/функций/констант; одна формула - разные интерпретации - разные значения
- **Общезначимость FOL неразрешима** (теорема Чёрча, 1936), но SMT-солверы (Z3, CVC5) решают практические задачи через эффективные эвристики
Связанные темы
Предикатная логика - мост между математикой и computer science:
- Пропозициональная логика — FOL расширяет пропозициональную логику кванторами и предикатами
- Естественный вывод — Формальная система доказательств: introduction/elimination правила для кванторов
- Резолюция — Алгоритмический метод автоматического доказательства в FOL
Вопросы для размышления
- Формализуй на FOL: «Каждый студент сдал хотя бы один экзамен, или получил справку». Где ∀, где ∃, где ∨?
- Почему проблема общезначимости в FOL неразрешима, а в пропозициональной логике разрешима? Что именно добавляет кванторы к сложности?
- Как SQL-запрос SELECT * FROM users WHERE EXISTS (SELECT 1 FROM orders WHERE orders.user_id = users.id) соответствует FOL-формуле? Запиши явно.
Связанные уроки
- ml-01 — Пропозициональная логика - фундамент, который FOL расширяет
- ml-03 — Естественный вывод строится поверх FOL-формул
- ml-04 — Резолюция - алгоритмический движок FOL-доказательств
- ml-15 — Модальная логика - FOL с операторами возможности/необходимости
- fl-03-grammars