Прямое доказательство и контрапозиция: цепочки импликаций и когда их переворачивать
Прямое доказательство — цепочка импликаций от посылки к цели, каждое звено обосновано: предположи, преобразуй, заключи. Когда прямой путь крут, переверните импликацию: ¬Q→¬P доказывает P→Q. Код-ревью устроено так же: функцию одобряют, сцепляя её гарантии звено за звеном.
На код-ревью джуниор задал тимлиду вопрос, который звучит наивно, но таковым не является: «А откуда вы вообще знаете, что здесь никогда не вернётся null?» Тимлид не стала запускать код. Она прочитала его вслух, медленно. Маршрут срабатывает только после auth-мидлвары, значит req.user существует. Обработчик передаёт req.user.id, который схема уже провалидировала как UUID. getProfile либо возвращает строку таблицы, либо бросает — по контракту он никогда не возвращает null для корректного UUID. Значит, вызывающий код null не увидит. Четыре предложения, каждое опирается на предыдущее, заканчиваются ровно там, где был вопрос. Никто так это не назвал, но тимлид только что построила прямое доказательство — древнейший приём математики: цепочка утверждений, где каждое звено обосновано, от того, что известно, к тому, что утверждается.
После этого урока ты можешь строить прямое доказательство по структуре «предположи, преобразуй, заключи», использовать определения как рукоятки, за которые держится доказательство, распознавать необоснованное звено на код-ревью, объяснять, почему контрапозиция доказывает ту же импликацию, и отличать контрапозицию от конверсии.
Доказательство утверждения — цепочка высказываний, каждое из которых обосновано. Каждое высказывание — либо определение, либо установленный факт, либо явное предположение, либо корректный шаг из предыдущих звеньев. Ничего мистического: доказательство настолько явно, что у враждебного читателя в каждом звене найдётся обоснование. Большинство утверждений, которые стоит доказывать, имеют форму P→Q. Прямое доказательство P→Q делает очевидный ход: идёт вперёд.
Три хода: предположи, преобразуй, заключи. Предположи, что P выполняется, и распакуй, что P означает, через определения. Преобразуй то, что есть, — алгебра, известные факты — по одному обоснованному шагу. Заключи, узнав определение Q в том, что получилось. Определения — рукоятки; не можете сформулировать определение — не сможете начать цепочку.
Утверждение. Если n чётно, то n² чётно.
Доказательство. Предположим, n чётно. По определению n = 2k для некоторого целого k. Тогда n² = (2k)² = 4k² = 2·(2k²). Поскольку целые замкнуты относительно умножения, 2k² — целое, а значит, n² равно 2, умноженному на целое, — а это определение чётности. Следовательно, n² чётно. ∎
Оборот «для некоторого целого k» называет свидетеля, не выбирая его, — вот как четыре предложения покрывают бесконечно много чисел.
Контрапозиция ¬Q→¬P — то же самое утверждение, что P→Q. Их таблицы истинности совпадают в каждой строке. Доказать любую — доказать обе. Когда прямой путь крут — посылка вручает более сложный объект — переворачивайте.
«Если n² нечётно, то n нечётно» сопротивляется лобовой атаке: в руках факт про n², а до n пришлось бы добираться через корни. Контрапозиция: «если n чётно, то n² чётно» — мы только что доказали это на шаге 2. Одна ссылка закрывает дело: по контрапозиции, раз чётность n влечёт чётность n², нечётность n² влечёт нечётность n. ∎
Конверсия Q→P — другое утверждение и не доказывает ничего о P→Q. Конверсия — стрелка, развёрнутая без отрицания. Её таблица истинности отличается от P→Q в двух строках: это действительно другое утверждение. Классический продакшен-баг: спецификация говорит «если вход некорректен, вернуть null». В логах null. Ревьюер пишет «значит, вход был некорректен» — это конверсия, которую спецификация никогда не обещала. Null может прийти из таймаута или пустой выборки. Единственный разрешённый разворот — контрапозиция: если не null, вход был корректен.
Код-ревью как прямое доказательство.
// Утверждение: если вход прошёл валидацию, sendReceipt никогда не получит пустой email.
app.post("/orders", validate(orderSchema), (req, res) => {
const order = req.body; // звено 1: validate() отработал → body соответствует схеме
const email = order.customer.email; // звено 2: схема требует customer.email
sendReceipt(email); // звено 3: email непустой → никогда не null
res.sendStatus(201);
});Ответственно одобрить этот PR — значит проверить прямое доказательство: каждая строка должна быть обоснована гарантией, установленной ранее. В момент, когда схема помечает email необязательным, звено 2 рвётся — и ровно на эту строку укажет будущий баг-репорт. Комментарий «а что гарантирует, что order.customer здесь существует?» — запрос недостающего обоснования, слово в слово то, что математик спрашивает на семинаре.
▸Почему это работает
«Вы предположили, что n чётно — это не жульничество?» Нет. P→Q не утверждает Q; она утверждает, что Q выполняется всякий раз, когда выполняется P. Чтобы проверить «всякий раз, когда P, — Q», вы входите в мир, где P выполняется, и показываете, что Q следует. Вы не заявляете, что n чётно где-то в реальном мире, — вы исследуете мир, где это так. Доказательство было бы порочным кругом, только если бы вы предположили Q — то, что выводится. Предположить P — не баг метода; это и есть метод.
Назовите три хода прямого доказательства (через запятую).
В доказательстве «если n чётно, то n² чётно» — что вы распаковываете на шаге «предположи»? Запишите алгебраическую форму.
Контрапозиция ¬Q→¬P — то же утверждение, что P→Q? Ответьте «да» или «нет».
Спецификация: «если вход некорректен, вернуть null». Вы видите null. Можно ли заключить, что вход был некорректен? Ответьте «да» или «нет».
Спецификация: «если вход некорректен, вернуть null». Вы видите НЕ-null. Можно ли заключить, что вход был корректен? Ответьте «да» или «нет».
Спецификация гарантирует: если вход некорректен, функция возвращает null. В продакшен-логах вы видите вызов, вернувший null. Что можно заключить о его входе?
Доказательство — конечная цепочка высказываний, каждое из которых — определение, известный факт, явное предположение или корректный шаг из предыдущих звеньев, и всё настолько явно, что у любого звена враждебный читатель найдёт обоснование. Прямое доказательство P→Q предполагает P, распаковывает его определением, продвигает обоснованную алгебру и запаковывает результат в определение цели. «Для некоторого целого k» называет свидетеля, не выбирая его, — так четыре предложения покрывают бесконечно много случаев. Код-ревью — то же ремесло с гарантиями вместо алгебры, а необоснованное звено — ровно то место, куда укажет будущий баг-репорт. Циклы подключаются через инварианты: «каждая итерация сохраняет свойство» — звенья одной цепи. Когда прямая дорога крута, переворачивайте к контрапозиции: P→Q и ¬Q→¬P — одно утверждение. Но никогда не разворачивайте без отрицания: конверсия Q→P — другое утверждение, и «вернулся null, значит вход был некорректен» — её классическая продакшен-маскировка. Отрицай и разворачивай — или не разворачивай вовсе.
Практика
Начни сверху. Задачи идут от простого к сложному: вспомнить факт, применить к случаю, затем senior-уровень. Открой, попробуй, потом открой ответ.
Что-то непонятно?
Задай вопрос по этому уроку. Вопросы анонимны и попадают напрямую автору — урок станет лучше.
Примени это
Примени этот урок в реальном проекте.