Предикаты, кванторы и методы доказательства

Расширяем логику кванторами «для всех» и «существует» и осваиваем главные способы доказывать утверждения.

Предикат — это высказывание с переменной, которое становится истинным или ложным после подстановки конкретного значения.

Зачем нужны кванторы и доказательства

Логики высказываний мало: она не умеет сказать «для всех элементов массива выполнено условие» или «существует пользователь с правами админа». Для таких утверждений нужны предикаты и кванторы. А методы доказательства — это инструменты, которыми математик (и грамотный программист) убеждается, что алгоритм корректен, инвариант сохраняется, утверждение верно для всех входов, а не только для тех, что он проверил руками. Это переход от «кажется, работает» к «доказано, что работает».

Предикаты

«x — чётное число» — это не высказывание (нельзя сказать, истинно оно или ложно, пока x не задан), а предикат P(x). Подставим x = 4 — получим истинное высказывание; подставим x = 5 — ложное. Предикат может зависеть от нескольких переменных: P(x, y) = «x меньше y». Предикат — это «высказывание с дыркой», в которую подставляют значения.

Кванторы: «для всех» и «существует»

Связь с программированием прямая: ∀x P(x) — это all(P(x) for x in S), а ∃x P(x) — это any(P(x) for x in S). Именно так кванторы и реализуются в Python.

Отрицание кванторов — важнейшее правило

Как отрицать «для всех»? Чтобы опровергнуть «все лебеди белые», достаточно одного чёрного лебедя. Это и есть правило:

• ¬∀x P(x) ≡ ∃x ¬P(x) — «неверно, что для всех» = «существует, для которого нет».
• ¬∃x P(x) ≡ ∀x ¬P(x) — «не существует» = «для всех неверно».

При отрицании квантор меняется на двойственный, а предикат уходит под отрицание. Это логическое продолжение де Моргана (∀ — это «большое И», ∃ — «большое ИЛИ»). Порядок кванторов тоже важен: ∀x ∃y и ∃y ∀x — разные утверждения. «У каждого человека есть мать» (∀x∃y) истинно, а «есть некто, кто мать всех» (∃y∀x) — нет.

Три метода доказательства

Допустим, нужно доказать утверждение вида «если p, то q». Есть три основных способа.

1. Прямое доказательство

Предполагаем, что p истинно, и логической цепочкой выводим q. Пример: «если n чётное, то n² чётное». Пусть n = 2k. Тогда n² = 4k² = 2·(2k²) — делится на 2, значит чётное. Готово. Прямой путь — самый естественный, когда из посылки легко «дойти» до вывода.

2. Доказательство от противного (приведение к абсурду)

Предполагаем, что доказываемое утверждение ложно, и приходим к противоречию — значит, предположение неверно, и утверждение истинно. Классика — иррациональность √2: предположим, что √2 = a/b (несократимая дробь), возведём в квадрат, получим, что и a, и b чётные, — а это противоречит несократимости. Значит, √2 нельзя записать дробью.

3. Доказательство контрапозицией

Вместо p → q доказываем равносильное ¬q → ¬p. Пример: «если n² чётное, то n чётное». Доказать напрямую неудобно. По контрапозиции докажем «если n нечётное, то n² нечётное»: пусть n = 2k+1, тогда n² = 4k²+4k+1 = 2·(2k²+2k)+1 — нечётное. Готово. Контрапозиция спасает, когда «с конца» рассуждать легче.

Проверяем доказанное на Python

Доказательство — это про «для всех», а машина может быстро проверить утверждение на множестве значений (это не заменяет доказательство, но ловит ошибки и укрепляет уверенность).

# Проверяем: для всех n из диапазона  n чётно  <=>  n² чётно
# и что контрапозиция держится: n нечётно => n² нечётно
def even(x):
    return x % 2 == 0

all_ok = all(even(n) == even(n * n) for n in range(-1000, 1001))
print("∀n: (n чётно) <=> (n² чётно) на [-1000..1000]:", all_ok)

# Отрицание квантора: ¬∀(все простые нечётные) <=> ∃ чётное простое
def is_prime(x):
    if x < 2: return False
    return all(x % d for d in range(2, int(x ** 0.5) + 1))

counterexample = [p for p in range(2, 30) if is_prime(p) and even(p)]
print("Контрпример к «все простые нечётны»:", counterexample)

Вывод:

∀n: (n чётно) <=> (n² чётно) на [-1000..1000]: True
Контрпример к «все простые нечётны»: [2]

Первый all(...) — это прямая проверка квантора всеобщности на диапазоне: эквивалентность «n чётно ⟺ n² чётно» держится для всех проверенных n (что согласуется с нашим доказательством). Второй пример показывает отрицание квантора в действии: чтобы опровергнуть «все простые нечётны», машина нашла единственный контрпример — число 2, единственное чётное простое. Один контрпример рушит «для всех» — ровно как чёрный лебедь.

Нормальные формы и SAT: где логика становится индустрией

Логические эквивалентности нужны не только для упрощения — с их помощью любую формулу приводят к стандартному виду. Особенно важна КНФ (конъюнктивная нормальная форма) — «И из ИЛИ-скобок», например (p ∨ ¬q) ∧ (¬p ∨ r). Любая формула сводится к КНФ цепочкой знакомых преобразований: импликации убираем через ¬p ∨ q, отрицания загоняем внутрь по де Моргану, раскрываем скобки дистрибутивностью.

Зачем это нужно? На КНФ работает целая индустрия SAT-решателей — программ, проверяющих, можно ли сделать формулу истинной. Задача выполнимости (SAT) была первой доказанно NP-полной, и тем не менее современные решатели справляются с миллионами переменных. Их применяют для верификации микросхем (доказать, что в процессоре нет ошибки), поиска багов в программах, планирования, анализа криптосистем. Так ручные преобразования логики, которыми мы упрощаем формулы, оказываются входными воротами в один из самых мощных практических инструментов информатики.

Типичные ошибки

• Менять порядок кванторов. ∀x ∃y и ∃y ∀x — разные утверждения. Перестановка может превратить истину в ложь.
• «Доказывать» на примерах. Проверка для n=1,2,3 — не доказательство «для всех n». Это лишь проверка гипотезы; контрпример может прятаться дальше.
• Путать контрапозицию и обратное. Доказав q → p (обратное), вы не доказали исходное p → q. Равносильна исходному именно контрапозиция ¬q → ¬p.

Итог

• Предикат — высказывание с переменной; кванторы ∀ («для всех», all) и ∃ («существует», any) превращают его в высказывание.
• Отрицание меняет квантор на двойственный: ¬∀x P ≡ ∃x ¬P.
• Три метода: прямое, от противного, контрапозицией.
• Проверка на примерах укрепляет уверенность, но не заменяет доказательство «для всех».