Математическая логика и доказательства: как рассуждать строго

Программист рассуждает логически каждый день, просто не называет это логикой. «Если кэш протух или ключа нет — идём в базу». «Функция вернёт не-null всегда, когда вход валиден». «Этот цикл завершится, потому что счётчик убывает». Всё это — утверждения, которые могут быть истинными или ложными, и почти каждый баг в проде — место, где такое утверждение оказалось ложным, а мы считали его истинным.

Математическая логика даёт две вещи, которых нет у «здравого смысла». Во-первых, язык, в котором утверждение записывается однозначно: ¬(A ∧ B) и ¬A ∧ ¬B на слух звучат похоже («не оба» и «ни то, ни другое»), а на деле это разные вещи, и путаница между ними — источник реальных инцидентов. Во-вторых, механическую процедуру проверки: доказательство — это не «меня убедили», а конечная последовательность шагов, каждый из которых проверяется без понимания смысла. Именно поэтому логику умеют проверять компьютеры — отсюда типы, SMT-солверы, верификаторы и property-based тесты.

Статья опирается на язык множеств из Теории множеств и служит фундаментом для вычислимости, теории сложности и автоматов.

1. Высказывания и связки: минимальный язык

Определение. Высказывание (propositional variable) — переменная, принимающая одно из двух значений: истина (1) или ложь (0). Формулы строятся связками, семантика задаётся таблицей истинности:

¬A     отрицание        A ∧ B  конъюнкция «и»       A ∨ B  дизъюнкция «или», допускает оба
A → B  импликация       A ↔ B  эквиваленция          A ⊕ B  исключающее «ровно одно»

 A  B | ¬A | A∧B | A∨B | A→B | A↔B | A⊕B
 0  0 |  1 |  0  |  0  |  1  |  1  |  0
 0  1 |  1 |  0  |  1  |  1  |  0  |  1
 1  0 |  0 |  0  |  1  |  0  |  0  |  1
 1  1 |  0 |  1  |  1  |  1  |  1  |  0

Ключевой момент: формула из n переменных полностью описывается таблицей из 2^n строк, то есть логическая формула — компактный способ записать булеву функцию.

Терминология, которую путают. Тавтология истинна при всех наборах (A ∨ ¬A); противоречие — ни при одном (A ∧ ¬A); выполнимая — хотя бы при одном. Запись ⊨ F означает «F истинна в любой интерпретации» (семантика), Γ ⊢ F — «существует формальный вывод F из посылок Γ» (синтаксис). Различие ⊨ и ⊢ — не педантизм: вся теория доказательств живёт в зазоре между ними, а теоремы корректности и полноты (§6) — ровно про то, что зазора нет.

Импликация — главный источник ошибок

A → B истинна, когда A ложно. «Если 2×2=5, то я папа римский» — истинное высказывание. Это не философия, а инженерное решение: импликация означает «нет случая, где A истинно, а B ложно», то есть A → B ≡ ¬A ∨ B. Контракт на непройденной ветке тривиально не нарушен. Отсюда же пустая квантификация в тестах: «все элементы пустого списка положительны» — истина, и потому тест на пустом входе часто зелёный и ничего не проверяет.

Из четырёх форм равносильны только диагонали:

A → B   ≡   ¬B → ¬A     контрапозиция — законна, ей и доказывают
B → A   ≡   ¬A → ¬B     обратное и противоположное равносильны друг другу
A → B   ≢   B → A       подмена прямого обратным — «ошибка обращения»

Классический баг из-за подмены: «если запрос невалиден, вернём 400» превращается в голове разработчика в «если вернули 400, значит запрос невалиден» — и метрика по 400-м интерпретируется неверно, потому что 400 отдаётся ещё и при рассинхроне схемы.

from itertools import product

def implies(p: bool, q: bool) -> bool:
    """Импликация ложна ровно в одном случае: истинная посылка, ложное следствие."""
    return (not p) or q

def truth_table(names, f):
    """Перебираем 2^n наборов значений; f принимает переменные по именам."""
    for values in product([False, True], repeat=len(names)):
        yield dict(zip(names, values))

def equivalent(names, f, g) -> bool:
    """Формулы эквивалентны, если совпадают на ВСЕХ наборах."""
    return all(f(**env) == g(**env) for env in truth_table(names, f))

print(equivalent(["p","q"], lambda p,q: implies(p,q), lambda p,q: implies(not q, not p)))  # True  контрапозиция
print(equivalent(["p","q"], lambda p,q: implies(p,q), lambda p,q: implies(q,p)))           # False обращение
print(equivalent(["p","q"], lambda p,q: not (p and q), lambda p,q: (not p) or (not q)))    # True  де Морган

Сложность проверки — O(2^n · n) по времени, O(n) по памяти. Для 20 переменных это миллион строк (доли секунды), для 60 — больше, чем секунд в возрасте Вселенной. Отсюда потребность в умных алгоритмах (§4).

2. Эквивалентности, которые стоит знать наизусть

Это «алгебраические тождества» логики; ими переписывают условия в коде, не меняя смысла.

Двойное отрицание   ¬¬A ≡ A
Де Морган           ¬(A ∧ B) ≡ ¬A ∨ ¬B          ¬(A ∨ B) ≡ ¬A ∧ ¬B
Дистрибутивность    A ∧ (B ∨ C) ≡ (A∧B) ∨ (A∧C)  A ∨ (B ∧ C) ≡ (A∨B) ∧ (A∨C)
Импликация          A → B ≡ ¬A ∨ B               A → B ≡ ¬B → ¬A
Эквиваленция        A ↔ B ≡ (A → B) ∧ (B → A)
Поглощение          A ∨ (A ∧ B) ≡ A              A ∧ (A ∨ B) ≡ A
Экспорт             (A ∧ B) → C ≡ A → (B → C)    ← это буквально карринг

Последнее тождество — не совпадение: «экспорт» в логике и каррирование функций в программировании суть одно утверждение в разных нотациях. Первый намёк на соответствие Карри–Ховарда (§8.4).

Функциональная полнота. Набора {¬, ∧, ∨} достаточно, чтобы выразить любую булеву функцию (доказывается построением ДНФ прямо по таблице истинности). Более того, достаточно одной связки — NAND или NOR. Отсюда факт из железа: любую комбинационную схему можно собрать из одних NAND-вентилей, что и делают в реальных техпроцессах.

Вывод для ревью кода. Условие if not (a and b) почти всегда стоит переписать как if not a or not b — не ради скорости, а чтобы читатель не применял де Моргана в уме. Отрицания следует проталкивать к листьям; это же первая фаза приведения к нормальной форме.

3. Нормальные формы: КНФ, ДНФ и преобразование Цейтина

Определение. Литерал — переменная или её отрицание. Дизъюнкт (clause) — дизъюнкция литералов. Формула в КНФ — конъюнкция дизъюнктов: (x1 ∨ ¬x2 ∨ x3) ∧ (¬x1 ∨ x3) ∧ (x2). ДНФ — зеркальная форма, дизъюнкция конъюнктов.

Почему КНФ важнее на практике: она читается как «список ограничений, каждое из которых обязано выполняться» — ровно то, во что превращаются планирование, разрешение зависимостей и верификация. Менеджеры пакетов (apt, dnf, Dart pub, Swift Package Manager) сводят разрешение версий именно к SAT в КНФ; см. классическую OPIUM: Optimal Package Install/Uninstall Manager.

Ловушка размера. Наивное приведение через дистрибутивность даёт экспоненциальный взрыв: у (a1∧b1) ∨ … ∨ (an∧bn) в КНФ получается 2^n дизъюнктов. На практике применяют преобразование Цейтина: на каждое подвыражение вводится свежая переменная-ярлык t, и записывается t ↔ подвыражение:

t ↔ (a ∧ b)  →  (¬t ∨ a) ∧ (¬t ∨ b) ∧ (t ∨ ¬a ∨ ¬b)
t ↔ (a ∨ b)  →  (¬t ∨ a ∨ b) ∧ (t ∨ ¬a) ∧ (t ∨ ¬b)
t ↔ ¬a       →  (¬t ∨ ¬a) ∧ (t ∨ a)

Затем требуется истинность верхнего ярлыка. На узел приходится не больше трёх коротких дизъюнктов, значит размер результата O(|F|) по времени и памяти. Результат не эквивалентен исходной формуле — у него больше переменных, — но равновыполним, а для SAT этого достаточно. Это стандартный фронтенд любого солвера: как бы уродливо ни выглядела формула, в солвер она приезжает линейной КНФ.

4. SAT: выполнимость и алгоритм DPLL

Задача SAT. Дана формула в КНФ — существует ли набор значений, делающий её истинной? Это первая задача, для которой доказана NP-полнота (теорема Кука–Левина, 1971), подробности в Теории сложности.

Наивный перебор — O(2^n · m). DPLL (Davis–Putnam–Logemann–Loveland, 1962) — тот же перебор с двумя приёмами, режущими дерево на порядки. Unit propagation: если в дизъюнкте остался ровно один литерал, его значение вынуждено. Pure literal: если переменная встречается только в одной полярности, её можно смело зафиксировать.

def simplify(clauses, lit):
    """Присваиваем литералу lit значение «истина» и упрощаем набор дизъюнктов.
    Возвращает None, если возник пустой дизъюнкт (конфликт)."""
    out = []
    for c in clauses:
        if lit in c:
            continue                 # дизъюнкт уже удовлетворён — выкидываем
        if -lit in c:
            c = c - {-lit}           # ложный литерал вычёркиваем
            if not c:
                return None          # пустой дизъюнкт = противоречие
        out.append(c)
    return out

def dpll(clauses, model=None):
    """clauses — список frozenset целых литералов (n / -n). Вернёт модель или None."""
    model = dict(model or {})

    while True:                                   # unit propagation до неподвижной точки
        unit = next((next(iter(c)) for c in clauses if len(c) == 1), None)
        if unit is None:
            break
        model[abs(unit)] = unit > 0
        clauses = simplify(clauses, unit)
        if clauses is None:
            return None

    if not clauses:                               # все ограничения удовлетворены
        return model

    lit = next(iter(clauses[0]))                  # эвристика выбора — здесь самая примитивная
    for guess in (lit, -lit):
        rest = simplify(clauses, guess)
        if rest is None:
            continue
        res = dpll(rest, {**model, abs(guess): guess > 0})
        if res is not None:
            return res
    return None

# (x1 ∨ x2) ∧ (¬x1 ∨ x3) ∧ (¬x2 ∨ ¬x3) ∧ (x1 ∨ ¬x3)
f = [frozenset({1, 2}), frozenset({-1, 3}), frozenset({-2, -3}), frozenset({1, -3})]
print(dpll(f))                                     # {1: True, 3: True, 2: False}
print(dpll([frozenset({1}), frozenset({-1})]))     # None — UNSAT

Худший случай остаётся O(2^n), память — O(n·m) из-за копирования дизъюнктов. Промышленные солверы вместо копирования держат trail с откатами и «watched literals», дающие амортизированную O(1) на распространение. Поверх DPLL современный CDCL добавляет обучение конфликтным дизъюнктам, нехронологические откаты, эвристику VSIDS и рестарты — благодаря этому MiniSat, CaDiCaL и Kissat решают промышленные экземпляры на миллионы переменных. Читать: Handbook of Satisfiability и исходники MiniSat — там около 2000 строк, разбираемых за вечер.

Где это встречается в работе: разрешение зависимостей, расписания и раскладка задач по машинам, символьное исполнение и фаззинг, верификация RTL, проверка конфигураций и облачных политик доступа, а иногда и тайпчекинг сложных систем типов.

5. Логика предикатов: кванторы

Пропозициональной логики не хватает, чтобы сказать «каждый пользователь имеет ровно один активный токен». Нужны предикаты — функции из объектов в {истина, ложь} — и кванторы: ∀x P(x) («для всех»), ∃x P(x) («существует»), ∃!x P(x) («существует ровно один»).

Отрицание кванторов — обобщённый де Морган, которым пользуются постоянно:

¬∀x P(x)  ≡  ∃x ¬P(x)      «не все» = «хотя бы один не»
¬∃x P(x)  ≡  ∀x ¬P(x)      «ни одного» = «все не»

Отсюда практическое правило: чтобы опровергнуть «все запросы укладываются в 200 мс», нужен ровно один контрпример; чтобы опровергнуть «существует дедлок», нужно доказать отсутствие для всех сценариев. Из-за этой асимметрии тестирование ловит баги, но не доказывает их отсутствие — знаменитое замечание Дейкстры.

Порядок кванторов решает всё

∀x ∃y и ∃y ∀x — разные утверждения, и это главная ловушка раздела.

D = range(-20, 21)
def forall(dom, p): return all(p(x) for x in dom)
def exists(dom, p): return any(p(x) for x in dom)

# ∀x ∃y: x + y = 0 — для каждого x найдётся СВОЙ y. Истина.
print(forall(D, lambda x: exists(D, lambda y: x + y == 0)))   # True
# ∃y ∀x: x + y = 0 — ОДИН y, гасящий любой x. Ложь.
print(exists(D, lambda y: forall(D, lambda x: x + y == 0)))   # False

Инженерная версия той же путаницы: «для каждого запроса существует реплика, которая его обслужит» (нормальная деградация) против «существует реплика, обслуживающая все запросы» (single point of failure). Одинаковые слова — противоположные архитектуры. Формулировки SLA, определения консистентности и ε-δ в матанализе ломаются ровно здесь.

Связанность. В ∀x (P(x) → Q(x)) переменная x связана; в P(x) ∧ ∀x Q(x) первое вхождение свободно. Формула без свободных переменных называется замкнутой, и только про такую осмысленно спрашивать «истинна ли она». Та же дисциплина связывания — в лямбда-исчислении и в областях видимости языков программирования.

Осторожно: ∀x ∈ ∅: P(x) истинно всегда (vacuous truth) — это то же самое, что all([]) == True в Python и «контрпримера не нашлось» в проверке.

6. Правила вывода и формальные системы

До сих пор речь шла о семантике — истинности в интерпретации. Доказательство же — понятие синтаксическое: конечная последовательность формул, где каждая либо аксиома или посылка, либо получена по правилу вывода.

Modus ponens         A,  A → B  ⊢  B
Modus tollens        A → B,  ¬B  ⊢  ¬A
Введение / удаление ∧   A, B ⊢ A ∧ B          A ∧ B ⊢ A
Введение ∨           A  ⊢  A ∨ B
Разбор случаев       A ∨ B,  A → C,  B → C  ⊢  C
Введение →           из «допустив A, вывели B»   ⊢  A → B
Reductio ad absurdum из «допустив A, вывели ⊥»   ⊢  ¬A
Обобщение            P(c) для произвольного c    ⊢  ∀x P(x)
Конкретизация        ∀x P(x)  ⊢  P(t)

Две теоремы о связи ⊢ и ⊨. Корректность (soundness): если Γ ⊢ F, то Γ ⊨ F — система не доказывает лжи; без этого доказательства бесполезны. Полнота (Гёдель, 1929): если Γ ⊨ F, то Γ ⊢ F — всё семантически истинное выводимо; для логики первого порядка это верно.

Разработчику полезна аналогия: корректность — «типизированная программа не падает с ошибкой типа в рантайме», полнота — «всякая корректная программа принимается тайпчекером». Реальные системы типов почти всегда корректны и неполны: они отвергают часть хороших программ. Это осознанный trade-off; о его алгебраической стороне — в Теории категорий в программировании.

Резолюция: одно правило вместо десяти

Для КНФ достаточно единственного правила: из (A ∨ x) и (B ∨ ¬x) следует (A ∨ B). Чтобы доказать Γ ⊢ F, добавляют ¬F к посылкам и выводят пустой дизъюнкт. Резолюция опровергающе полна: если множество дизъюнктов невыполнимо, пустой дизъюнкт выводим. На этом стоят Prolog (SLD-резолюция) и целый класс автоматических пруверов.

from itertools import combinations

def resolve(c1, c2):
    """Все резольвенты: склеиваем пару дизъюнктов по противоположным литералам."""
    return [(c1 - {l}) | (c2 - {-l}) for l in c1 if -l in c2]

def refute(clauses):
    """Насыщение резолюцией. True = множество невыполнимо."""
    known = set(clauses)
    while True:
        new = {r for a, b in combinations(known, 2) for r in resolve(a, b)} - known
        if frozenset() in new:
            return True                 # выведен пустой дизъюнкт = противоречие
        if not new:
            return False                # ничего нового не выводится
        known |= new

# «Сократ смертен»: (человек → смертен), человек, ¬смертен  →  противоречие
ЧЕЛОВЕК, СМЕРТЕН = 1, 2
print(refute([frozenset({-ЧЕЛОВЕК, СМЕРТЕН}), frozenset({ЧЕЛОВЕК}), frozenset({-СМЕРТЕН})]))  # True

Наивное насыщение экспоненциально по времени и памяти, поэтому в реальных пруверах применяют упорядочения литералов, стратегию множества поддержки и индексирование термов.

7. Методы доказательств: рабочий набор

Общая проверка для любой ветки: каждый шаг обоснован, доказываемое утверждение нигде не использовано внутри собственного доказательства.

Прямое доказательство — разворачиваем определения и идём по цепочке импликаций. Сумма двух чётных чисел чётна: пусть a = 2k, b = 2m, тогда a + b = 2(k+m), где k+m целое. ∎ Кажется тривиальным, но так выглядит 90% доказательств корректности алгоритмов: развернуть инвариант, применить шаг, свернуть обратно.

Контрапозиция. Если n² чётно, то n чётно. Прямо неудобно — из чётности n² надо извлечь структуру n. Докажем ¬B → ¬A: если n нечётно, n = 2k+1, то n² = 4k² + 4k + 1 = 2(2k²+2k) + 1 нечётно. ∎

От противного. √2 иррационально. Пусть √2 = p/q — несократимая дробь. Тогда p² = 2q², значит p² чётно, значит p чётно (по предыдущему пункту), p = 2r. Подставляем: 4r² = 2q², то есть q² = 2r², значит и q чётно. Но тогда p/q сократима — противоречие с выбором. ∎

Важный нюанс: доказательство от противного использует закон исключённого третьего A ∨ ¬A. В конструктивной (интуиционистской) логике он не принимается: там доказательство существования обязано предъявить объект. Это не экзотика — Coq, Agda, Lean и Idris построены на конструктивной логике именно потому, что из конструктивного доказательства можно извлечь работающую программу.

Индукция

Принцип. Если (1) P(0) и (2) для любого k из P(k) следует P(k+1), то P(n) для всех n ∈ ℕ. В сильной форме в шаге разрешено предполагать P(0), …, P(k) сразу — удобно для «разделяй и властвуй», где рекурсия идёт на n/2, а не на n−1.

Утверждение. 1 + 2 + … + n = n(n+1)/2. База. n = 0: пустая сумма равна 0 = 0·1/2. ✓ Шаг. Пусть верно для k. Тогда 1+…+k+(k+1) = k(k+1)/2 + (k+1) = (k+1)(k+2)/2. ✓ ∎

Структурная индукция — та же идея для рекурсивных типов: база на конструкторах-листьях, шаг на составных конструкторах. Это буквально «доказательство по форме типа», и оно ложится один-в-один на рекурсивные функции.

from dataclasses import dataclass
from typing import Union
import random

@dataclass(frozen=True)
class Leaf:  value: int

@dataclass(frozen=True)
class Node:  left: "Tree"; right: "Tree"

Tree = Union[Leaf, Node]

def leaves(t: Tree) -> int:
    match t:
        case Leaf():     return 1                             # база
        case Node(l, r): return leaves(l) + leaves(r)         # шаг

def internals(t: Tree) -> int:
    match t:
        case Leaf():     return 0
        case Node(l, r): return 1 + internals(l) + internals(r)

# ТЕОРЕМА: в полном бинарном дереве листьев ровно на 1 больше, чем внутренних узлов.
# База: Leaf — 1 лист, 0 внутренних, и 1 = 0 + 1. ✓
# Шаг:  для Node(l, r) по предположению leaves(l) = i_l + 1, leaves(r) = i_r + 1, тогда
#       leaves = (i_l + 1) + (i_r + 1) = (i_l + i_r + 1) + 1 = internals + 1. ✓ ∎
def random_tree(depth=0):
    if depth > 4 or random.random() < 0.4:
        return Leaf(random.randint(0, 9))
    return Node(random_tree(depth + 1), random_tree(depth + 1))

random.seed(42)
print(all(leaves(t) == internals(t) + 1 for t in (random_tree() for _ in range(2000))))  # True

Прогон на 2000 случайных деревьях — не доказательство, а проверка гипотезы. Доказательство — три строки индукции в комментарии. Разница принципиальна: перебор ловит контрпримеры, но никогда не даёт ∀.

Перебор случаев и принцип Дирихле

Разбор случаев: делим область на конечное число вариантов и доказываем каждый. Так доказана теорема о четырёх красках — компьютерной проверкой 1834 конфигураций, что вызвало спор «доказательство ли это»; сейчас есть машинно проверенная версия в Coq (Gonthier, Formal Proof of the Four-Color Theorem).

Принцип Дирихле (pigeonhole): если n+1 объект разложить по n ящикам, в каком-то окажется минимум два. Так доказывается неизбежность коллизий хеш-функции: у SHA-256 вход неограничен, выход — 2²⁵⁶ значений, значит коллизии существуют; вопрос лишь в вычислительной трудности их поиска. Подробнее — в Дискретной математике.

8. Логика в коде

8.1 Инвариант цикла — доказательство корректности на месте

Инвариант — утверждение, истинное перед каждой итерацией. Схема из CLRS: инициализация (верно до цикла), сохранение (итерация сохраняет), завершение (из инварианта плюс отрицания условия следует нужный результат). Это индукция по номеру итерации.

def lower_bound(a: list[int], target: int) -> int:
    """Индекс первого элемента >= target в отсортированном a. O(log n) времени, O(1) памяти."""
    lo, hi = 0, len(a)
    while lo < hi:
        # ИНВАРИАНТ (в отладке — ассерты, в доказательстве — три строки на бумаге):
        assert 0 <= lo <= hi <= len(a)
        assert all(v < target for v in a[:lo])      # слева от lo — строго меньше
        assert all(v >= target for v in a[hi:])     # справа от hi — не меньше
        mid = (lo + hi) // 2
        if a[mid] < target:
            lo = mid + 1
        else:
            hi = mid
    # ЗАВЕРШЕНИЕ: lo == hi, значит всё слева < target, всё справа >= target.
    return lo

Отдельно доказывается завершение: величина hi - lo — натуральное число, строго убывающее на каждой итерации (проверять надо оба ветвления!). Такая убывающая величина называется вариантом цикла, а строго убывающая последовательность натуральных чисел конечна — это принцип вполне упорядоченности, двойственный индукции.

Заметьте: mid = (lo + hi) // 2 в Python безопасно, а в Java или C++ на int32 это знаменитый баг переполнения, проживший в JDK девять лет — Nearly All Binary Searches Are Broken. Инвариант был верен, а модель арифметики — нет: доказательство корректно лишь относительно той модели, в которой ведётся.

8.2 Property-based тестирование: ∀ в тестах

Обычный тест проверяет одну точку; property-based тест — квантор ∀ на случайной выборке плюс автоматическое сжатие контрпримера.

# pip install hypothesis
from hypothesis import given, strategies as st

@given(st.lists(st.integers()), st.integers())
def test_lower_bound_spec(xs, t):
    # ∀ xs, t: результат делит отсортированный массив ровно по границе target
    a = sorted(xs)
    i = lower_bound(a, t)
    assert all(v < t for v in a[:i])
    assert all(v >= t for v in a[i:])

Это не доказательство ∀, а мощная охота за контрпримером. Правильный ментальный сдвиг — писать спецификации (что верно всегда), а не примеры. Документация: Hypothesis, для Erlang и Elixir — PropEr и StreamData.

8.3 SMT-солверы: логика как библиотека

SAT работает с булевыми переменными; SMT (Satisfiability Modulo Theories) добавляет теории — целые и вещественные числа, битовые векторы, массивы, строки. Практически это значит: можно спросить «существует ли вход, при котором код падает», и получить конкретный вход.

# pip install z3-solver
from z3 import Int, Solver

x, y = Int("x"), Int("y")
s = Solver()
s.add(x > 0, y > 0, x + y == 10, x * y == 21)
print(s.check())                # sat
print(s.model())                # [x = 3, y = 7]  (или наоборот)

# Проверка теоремы: ищем контрпример, то есть добавляем ОТРИЦАНИЕ и ждём unsat.
n = Int("n")
t = Solver()
t.add(n >= 0, (n * (n + 1)) % 2 != 0)   # «существует n, для которого n(n+1) нечётно»
print(t.check())                        # unsat → контрпримера нет → теорема доказана

Приём «добавь отрицание и жди unsat» — та же резолюция из §6, только промышленная. Так работают верификаторы Dafny, Viper и Kani, символьные исполнители KLEE и angr, проверка гипотез в компиляторах и анализ политик доступа AWS (Zelkova). Документация: Z3 Guide.

8.4 Карри–Ховард: типы — это утверждения, программы — доказательства

Одно из красивейших соответствий в информатике:

Логика              Типы                          В коде
------------------------------------------------------------------------
A → B               функция A -> B                (a: A) => B
A ∧ B               произведение (A, B)           кортеж, структура
A ∨ B               сумма Either<A, B>            union, enum
истина ⊤            unit-тип                      void, ()
ложь ⊥              необитаемый тип               never, Void
∀x. P(x)            параметрический полиморфизм   <T>(x: T) => ...
∃x. P(x)            экзистенциальный тип          интерфейс, скрывающий реализацию
доказательство      программа                     значение нужного типа
нормализация        вычисление                    редукция

Практическое следствие: если тотальная функция типа (A) -> B существует, вы доказали A → B. Тип never необитаем, поэтому функция (A) -> never доказывает ¬A.

// A ∧ B → A — удаление конъюнкции
const fst = <A, B>(p: [A, B]): A => p[0];

// A → (B → A) — аксиома K
const k = <A, B>(a: A) => (_b: B): A => a;

// (A → B → C) → ((A → B) → (A → C)) — аксиома S, она же комбинатор S
const s = <A, B, C>(f: (a: A) => (b: B) => C) =>
          (g: (a: A) => B) => (a: A): C => f(a)(g(a));

k и s — в точности аксиомы импликационного фрагмента интуиционистской логики, а вместе они образуют комбинаторный базис SKI. Логика и вычисления — один объект с двух сторон; подробнее в Теории вычислимости и на треке TypeScript.

Оговорка: соответствие работает для тотальных языков. В Python, TS или Go бесконечный цикл «доказывает» что угодно — function f<A>(): A { while(true){} } имеет тип ∀A. A, то есть доказывает ложь. Поэтому Coq и Lean требуют доказательства завершения.

8.5 Трёхзначная логика SQL

В SQL связки живут не в булевой алгебре: значений три — TRUE, FALSE, UNKNOWN (NULL).

-- Кажется, что вместе эти запросы покрывают все строки. Это не так.
SELECT count(*) FROM users WHERE status =  'active';
SELECT count(*) FROM users WHERE status <> 'active';
-- Строки со status IS NULL не попадут НИ В ОДИН: NULL <> 'active' даёт UNKNOWN,
-- а WHERE пропускает только TRUE. Закон исключённого третьего здесь не работает.

SELECT NULL = NULL;      -- NULL, а не TRUE
SELECT NULL IS NULL;     -- true
SELECT true  OR NULL;    -- true   — дизъюнкция поглощает неизвестность
SELECT false AND NULL;   -- false  — конъюнкция тоже
SELECT true  AND NULL;   -- NULL

Это логика Клини K3, и она нужна, чтобы NULL означал «значение неизвестно». Цена — потеря привычных тождеств: A ∨ ¬A больше не тавтология. Отсюда правило продакшна: условия по nullable-колонке пишите с явным IS NULL или COALESCE, а NOT IN (подзапрос) с NULL внутри вернёт пустоту, потому что x <> NULL — UNKNOWN. См. PostgreSQL: Comparison Functions and Operators.

9. Пределы формализации: Гёдель и неразрешимость

Первая теорема о неполноте. Любая непротиворечивая рекурсивно перечислимая формальная система, достаточно богатая для арифметики натуральных чисел, содержит истинное утверждение, которое в ней недоказуемо. Вторая. Такая система не может доказать собственную непротиворечивость.

Идея инженерно узнаваема: Гёдель кодирует формулы числами (гёделева нумерация — буквально сериализация синтаксиса в данные) и строит утверждение «я недоказуемо». Будь оно доказуемо, система доказала бы ложь; значит, оно истинно и недоказуемо. Тот же трюк самоприменения — в проблеме остановки и в парадоксе Рассела.

Чего теорема не утверждает:

• Не «существуют вечно непознаваемые истины». Недоказуемое в S может доказываться в более сильной S′ — просто у S′ появится своё недоказуемое.
• Не «математика противоречива или бесполезна».
• Не «люди умнее компьютеров»: аргумент Лукаса–Пенроуза большинством логиков не принят, поскольку тайком предполагает непротиворечивость человеческого рассуждения.
• Не применима к слабым системам: арифметика Пресбургера (сложение без умножения) полна и разрешима — на этом стоят некоторые солверы и анализаторы указателей.

Вывод для инженера: универсального анализатора, дающего для любой программы точный ответ о её поведении, не существует (теорема Райса — см. Теорию вычислимости). Поэтому реальные инструменты выбирают одно из трёх: работать на ограниченном фрагменте языка, давать консервативные ложноположительные срабатывания или требовать подсказок от человека — аннотаций и инвариантов. Когда линтер ругается на заведомо корректный код, это не «глупый линтер», это цена корректности.

10. Типичные заблуждения

1. «Из A следует B» = «B следует из A». Ошибка обращения. Проверяйте: контрапозиция — да, обращение — нет.
2. ¬(A ∧ B) = ¬A ∧ ¬B. Нет: ¬A ∨ ¬B. Классика в правилах доступа — «не (админ и активен)» ≠ «не админ и не активен».
3. Перестановка кванторов. ∀x∃y ≠ ∃y∀x. Асимптотика ломается на этом постоянно: «для каждого n есть константа» и «есть константа для всех n» — разные утверждения.
4. Много примеров = доказательство. Гипотеза Пойа держалась до n ≈ 9·10⁸ и оказалась ложной; полином n² + n + 41 даёт простые для n = 0…39 и составное при n = 40.
5. Индукция без базы. «Все лошади одной масти»: шаг верен для k ≥ 2, но ломается при переходе от 1 к 2, где множества не пересекаются.
6. Круговое доказательство. Использование доказываемого внутри шага легко проглядеть в длинных выкладках; ассистенты доказательств ловят это автоматически.
7. unsat ≠ «ложно», а WHERE x = NULL не сработает никогда. Солвер, вернувший unsat на отрицание, доказал теорему; unsat на само утверждение означает невыполнимость — путаница в направлении типична для самописных верификаторов. Для NULL нужен IS NULL.
8. Доказательство «в модели» ≠ корректность в проде. Инвариант бинарного поиска верен над ℤ и ломается на int32. Всегда фиксируйте модель, в которой рассуждаете (то же самое с вещественными — в Численных методах).

11. Мини-итог

• Пропозициональная логика = булевы функции; всё сводится к таблице 2^n, поэтому SAT NP-полна.
• Импликация ложна ровно в одном случае; равносильна ей только контрапозиция.
• КНФ — язык ограничений; Цейтин переводит в неё линейно, DPLL и CDCL решают на практике.
• Кванторы добавляют выразительность, а их порядок меняет смысл радикально.
• ⊨ — про истинность, ⊢ — про выводимость; корректность и полнота связывают их.
• Методы: прямое, контрапозиция, от противного, индукция (в том числе структурная), перебор случаев, конструкция.
• Инвариант цикла — индукция по итерациям; вариант цикла доказывает завершение.
• Карри–Ховард: типы — утверждения, тотальные программы — доказательства.
• Гёдель ставит границу: полного и корректного автоанализа всего не будет, инструменты всегда выбирают компромисс.

Источники

• Velleman D. How to Prove It: A Structured Approach — лучший вход в доказательства для самоучки.
• Huth M., Ryan M. Logic in Computer Science: Modelling and Reasoning about Systems — логика именно для CS: натуральный вывод, model checking, LTL/CTL.
• Enderton H. A Mathematical Introduction to Logic — строгий курс с теоремами о полноте; Nagel E., Newman J. Gödel’s Proof — честное популярное изложение неполноты.
• Cormen T. и др. Introduction to Algorithms (CLRS), гл. 2 — инварианты цикла как метод.
• Pierce B. Software Foundations — softwarefoundations.cis.upenn.edu — Карри–Ховард на практике в Coq.
• Handbook of Satisfiability, MiniSat, Z3 Guide — практика SAT и SMT.
• SEP: Gödel’s Incompleteness Theorems — аккуратные формулировки без мистики.
• Lean 4 и Mathlib — живой проект машинно проверенной математики.

Что дальше

Логика дала язык утверждений и способ их доказывать. Следующий шаг — научиться считать объекты, о которых мы рассуждаем: сколько существует паролей, перестановок, путей в сетке, состояний автомата. Комбинаторные доказательства — прямое продолжение индукции и принципа Дирихле из этой статьи.

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