Дискретная математика

Предикатная логика

Z3 - SMT-solver от Microsoft Research - каждый день проверяет миллионы строк кода на корректность. Как? Берёт спецификацию «для всех входов x: если P(x), то Q(x)» - это ∀x (P(x) → Q(x)) - и автоматически доказывает или находит контрпример. Windows Kernel, LLVM, протоколы AWS - всё это верифицируется предикатной логикой. Это не академический язык: это язык, на котором записываются гарантии промышленного ПО.

  • **SMT-solvers (Z3, CVC5)**: program verification, compiler optimization в LLVM, formal verification нейронных сетей - гарантии безопасности DNN записываются через ∀x (P(x) → safe(x))
  • **SQL семантика**: WHERE = ∃ по строкам (найди строки где предикат истинен), HAVING = ∀ по группам, FK-constraint = ∀row ∃parent (refs(row, parent))
  • **Coq/Lean4**: формальные доказательства корректности backprop, сходимости SGD - пишутся на языке предикатной логики, каждый шаг - применение правил для кванторов
  • **Property-based testing**: Hypothesis (@given), QuickCheck - это проверка ∀x P(x) на случайных x. Нашёл контрпример - баг. Не нашёл - «вероятно верно»

Предварительные знания

  • Логика высказываний

Предикат P(x) и кванторы: ∀ vs ∃

Логика высказываний бьётся о потолок при первой же реальной задаче. «Все входные данные проходят валидацию» - невозможно выразить без переменных. SQL WHERE-clause - невозможно. Контракт API «для каждого запроса есть ответ» - тоже. Это не недостаток теории: просто логика высказываний не умеет говорить о множествах. Предикатная логика умеет.

**Предикат P(x)** - функция из домена (области значений) в {True, False}. Сам по себе - не высказывание. Становится высказыванием при подстановке значения или навешивании квантора. - P(x) = «x > 5» - предикат (зависит от x) - P(3) = «3 > 5» - высказывание (False) - **∀x P(x)** - «для всех x верно P(x)» (универсальный квантор) - **∃x P(x)** - «существует x, для которого P(x) верно» (экзистенциальный квантор)

Z3 от Microsoft Research ежедневно проверяет миллионы строк кода на корректность - именно так: берёт спецификацию «для всех входов x если P(x) то Q(x)», записывает как ∀x (P(x) → Q(x)), и автоматически доказывает или находит контрпример. SQL делает то же самое, только называет это иначе: SELECT WHERE - это ∃ по строкам таблицы.

**Доказать vs опровергнуть:** - ∀x P(x) - нужно доказать для всех x. Опровергнуть достаточно одним контрпримером. - ∃x P(x) - достаточно одного x. Опровергнуть - доказать для всех x, что P(x) ложно.

SQL-запрос `SELECT * FROM orders WHERE total > 1000` соответствует...

Отрицание кванторов: де Морган для бесконечных множеств

Z3 находит баги не доказательством, а опровержением. Пользователь пишет «все входные данные корректны» - ∀x P(x). Z3 ищет контрпример, то есть решает ¬∀x P(x). По закону де Моргана для кванторов это равно ∃x ¬P(x) - «существует x, для которого P(x) ложно». Одно правило - и поиск контрпримера сводится к SAT-задаче.

**Законы де Моргана для кванторов:** - **¬∀x P(x) ≡ ∃x ¬P(x)** - «не все» = «существует хоть один не такой» - **¬∃x P(x) ≡ ∀x ¬P(x)** - «не существует» = «все не такие» Аналогия с логикой высказываний: ¬(p ∧ q) ≡ ¬p ∨ ¬q - тот же де Морган, но для бесконечных AND/OR по домену.

Lean4 и Coq - системы формальных доказательств - используют именно эти законы при доказательстве корректности алгоритмов ML. Доказательство сходимости SGD, корректности backprop - всё это цепочки кванторов, где каждый шаг применяет де Моргана или другие эквивалентности. Предикатная логика - не академический артефакт: это язык, на котором написаны гарантии безопасности нейронных сетей.

**Частая ошибка:** «не все» - это не «никто». - ¬∀x P(x) = ∃x ¬P(x) - «существует нарушитель» (слабее) - ∀x ¬P(x) - «никто не удовлетворяет» (сильнее) Пример: «не все тесты проходят» ≠ «ни один тест не проходит». Второе - апокалипсис, первое - просто баг.

Спецификация: ∀x (input(x) → output_valid(x)). Z3 ищет баг. Что именно он ищет?

Вложенные кванторы: ∀x ∃y vs ∃y ∀x - порядок решает всё

«Каждый пользователь имеет пароль» и «существует один пароль для всех пользователей» - разница в две перестановки. Первое - норма, второе - катастрофа безопасности. В записи кванторами это ∀x ∃y против ∃y ∀x. Два символа - противоположные смыслы. Базы данных, матрицы, распределённые системы - везде этот порядок принципиален.

**Порядок кванторов критически важен:** - **∀x ∃y R(x, y)** - «для каждого x существует свой y» (y зависит от x) - **∃y ∀x R(x, y)** - «существует один y, общий для всех x» (y фиксирован) Если ∃y ∀x истинно, то ∀x ∃y тоже истинно - но не наоборот. «Один на всех» строже, чем «каждому своё».

ФормулаЧитаетсяПример
∀x ∃y R(x,y)у каждого x есть свой yкаждый пользователь имеет (свой) пароль
∃y ∀x R(x,y)один y работает для всех xсуществует пароль, общий для всех
∀x ∀y R(x,y)для любых x и y верно Rвсе пары дружат между собой
∃x ∃y R(x,y)хотя бы одна пара x,y с Rкто-то дружит с кем-то

В матричной алгебре ∃y ∀x R(x,y) - это утверждение о существовании вектора-собственного направления (eigenvalue). В реляционных базах ∀x ∃y - это FK-constraint: каждая запись в дочерней таблице ссылается на свою запись в родительской. SMT-солверы разворачивают вложенные кванторы в SAT-формулы именно через де Моргана и skolemization - каждый ∃ превращается в функцию от предшествующих ∀.

**Мнемоника порядка:** читай слева направо. ∀x ∃y - «для каждого x» (зафиксировали x), «найдём y» (y может зависеть от x). ∃y ∀x - «зафиксируем один y заранее», «он работает для любого x». Второе - гораздо сильнее.

∀x ∃y R(x,y) и ∃y ∀x R(x,y) - одно и то же, порядок кванторов не важен

Порядок меняет смысл кардинально. ∃y ∀x - строже и сильнее, из него следует ∀x ∃y, но не наоборот

∀x ∃y - «у каждого человека есть мама» (у каждого своя). ∃y ∀x - «одна женщина - мама всех людей». Первое - биологический факт. Второе - логический нонсенс. Из второго следует первое, но первое не влечёт второго.

FK-constraint в SQL: «каждый order ссылается на существующего customer». Какой квантор?

Ключевые идеи

  • **Предикат P(x)** - функция в {True, False}. Подстановка значения или навешивание квантора превращает предикат в высказывание
  • **∀x P(x)** - «для всех», **∃x P(x)** - «существует». В коде: all() и any(). В SQL: WHERE (∃) и FK-constraint (∀∃)
  • **Де Морган для кванторов:** ¬∀x P(x) ≡ ∃x ¬P(x) и ¬∃x P(x) ≡ ∀x ¬P(x). Z3 использует это чтобы искать контрпримеры
  • **Порядок кванторов критичен:** ∀x ∃y - «каждому своё» (слабее), ∃y ∀x - «один для всех» (строже). Из ∃y ∀x следует ∀x ∃y, но не наоборот
  • **Skolemization** - как SMT-солверы убирают ∃: каждый ∃y превращается в функцию f(x) от предшествующих ∀-переменных

Связанные темы

Предикатная логика - фундамент математических доказательств и формальной верификации:

  • Логика высказываний — Предикатная логика - надмножество: добавляет кванторы, переменные и домены
  • Методы доказательств — Доказательства используют кванторы: ∀-введение, ∃-введение, поиск контрпримера
  • Отношения и функции — R(x,y) - бинарный предикат; рефлексивность = ∀x R(x,x), транзитивность = ∀x∀y∀z (R(x,y)∧R(y,z)→R(x,z))

Вопросы для размышления

  • Z3 при верификации кода разворачивает ∀x ∃y в skolem-функцию f(x) - почему именно такой порядок? Что происходит если поменять ∀ и ∃?
  • Запись ∀user ∃session (authenticated(user, session)) - это FK-constraint или что-то сильнее? Чем отличается от ∃session ∀user?
  • Hypothesis в Python ищет контрпример к ∀x P(x). Если за тысячу попыток не нашёл - доказал ли он теорему? Что именно гарантирует property-based testing?

Связанные уроки

  • dm-02 — Логика высказываний - фундамент, кванторы надстраиваются поверх
  • dm-04 — Теория множеств через предикаты: принадлежность x∈A - это предикат P(x)
  • dm-07 — Методы доказательств: ∀-введение, ∃-введение, контрпример
  • dm-05 — R(x,y) - бинарный предикат, определяющий отношение на множестве
  • alg-01-big-o — ∀n≥n0: f(n)≤c·g(n) - определение Big O через квантор
  • ml-01
Предикатная логика

0

1

Войти