Доказательства и семантические таблицы

1. Что такое доказательство

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

Это требование строже, чем кажется. «Идёт дождь, значит, земля мокрая» — разумное высказывание, но оно опирается на то, что вы знаете о дожде и земле. Формальная логика убирает это и задаёт более узкий вопрос: возможно ли вообще, исходя лишь из формы предложений, чтобы посылки были истинны, а заключение ложно? Если такой возможности нет, аргумент верен, а доказательство — это запись того, почему её нет.

Это руководство — об одном способе получить такую запись: о методе семантических таблиц, которые называют также деревьями истинности. Именно этот метод сайт применяет всякий раз, когда вы вводите аргумент в калькулятор, и, пройдя его один раз, вы сможете проверить аргумент на бумаге, имея только ручку.

2. Верен — и откуда это известно

Запишите аргумент со знаком следования: посылки слева, заключение справа. Утверждение p → q, ¬q ⊨ ¬p говорит, что из импликации и отрицания её следствия вытекает отрицание её основания. Знак следования — не ещё одна связка. Это утверждение о формулах по обе стороны от него, и оно либо верно, либо нет.

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

Таблица в смысле tableau подступает к тому же вопросу с другого конца. Вместо того чтобы перечислять все возможности и искать среди них плохую, она предполагает, что плохая существует, и пытается её построить. Если попытка на каждом возможном пути обрушивается в противоречие, такого распределения нет и аргумент верен. Если попытка удаётся, построенное и есть контрпример, который можно прочесть напрямую.

3. Метод семантических таблиц

Семантическая таблица — это дерево помеченных формул. Каждая строка — формула с T или F перед ней, и знак говорит, что ветвь предполагает об этой формуле: не какова её истинностная оценка, а какой она должна была бы быть, чтобы аргумент не прошёл. Весь метод — четыре шага:

1. Запишите каждую посылку с T. Вы допускаете, что все посылки аргумента выполняются.
2. Запишите заключение с F. Вы допускаете, что оно тем не менее не выполняется, — это и есть допущение, которое вы стремитесь опровергнуть.
3. Возьмите любую строку, которая ещё не атом, и примените правило для её главной связки и знака, добавив то, что даёт правило, в конец каждой ветви, проходящей через неё.
4. Закройте ветвь, как только она содержит и T A, и F A для одной и той же формулы A. Остановитесь, когда все ветви закрыты или не осталось строк для разложения.

Ничто в этом цикле не требует смекалки или выбора стратегии. У каждой строки ровно одно правило, и применение правил в любом порядке даёт один и тот же итог — поэтому это может делать машина, и поэтому её результату можно доверять.

4. Правила

Есть по одному правилу на связку при каждом знаке — всего десять. Они распадаются на два вида, и различие между видами и есть вся причина, по которой семантическая таблица — дерево, а не список. Правило α говорит, что несколько вещей должны выполняться вместе, и потому складывает свои результаты вниз по ветви. Правило β говорит, что должно выполняться одно из двух, и потому расщепляет ветвь надвое, пуская каждый случай своим путём.

Каждое правило — это всего лишь условие истинности его связки, прочитанное задом наперёд. Конъюнкция истинна, только когда истинны обе стороны, поэтому T (A ∧ B) складывает T A и T B. Конъюнкция ложна, когда ложна хотя бы одна сторона, но формула не говорит какая, поэтому F (A ∧ B) вынуждено пробовать обе: оно ветвится. Та же асимметрия действует наоборот для дизъюнкции, а ложная импликация означает, что основание выполнилось, а следствие — нет: единственный случай, когда импликация рвётся.

Обратите внимание, чего правила никогда не делают: они никогда не изобретают формулу. Всё, что даёт правило, — это часть той строки, из которой оно получено. Это свойство — свойство подформулы — и делает метод конечным, и ниже мы к нему вернёмся.

5. Как закрывается ветвь

Ветвь — это одна цепочка рассуждения: прочтите её от корня до листа, и вы получите один полный набор допущений. Ветвь закрывается, когда эти допущения прямо противоречат друг другу, то есть когда она несёт и T A, и F A для одной и той же формулы. Неважно, насколько сложна A и как далеко друг от друга стоят обе строки: если ветви нужно, чтобы формула была одновременно истинной и ложной, ничто её не удовлетворит.

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

Когда закрывается каждая ветвь, таблица закрыта, и это и есть доказательство. Оно показывает, что исходное предположение — все посылки истинны, заключение ложно — ведёт к противоречию на каждом пути, какой оно могло избрать. Раз путей не осталось, такого распределения нет, и аргумент верен. Это доказательство от противного, разложенное так, чтобы ни один случай нельзя было упустить.

6. Доказательство, строка за строкой

Возьмём modus tollens: p → q, ¬q ⊨ ¬p. Строки 1 и 2 — посылки, принятые за истинные. Строка 3 — заключение, принятое за ложное; а поскольку заключение есть ¬p, принять его ложным значит принять p истинным, что и записывает строка 5. Строка 4 получена по правилу отрицания, применённому к строке 2: если ¬q истинно, то q ложно. Импликация в строке 1 — единственная оставшаяся строка со связкой, и это правило β, поэтому дерево разветвляется:

Левая ветвь предполагает, что импликация выполнилась из-за того, что не выполнилось её основание, — но в строке 5 p уже истинно, поэтому ветвь противоречит себе и закрывается. Правая ветвь предполагает, что она выполнилась из-за истинности следствия, — но в строке 4 q уже ложно, поэтому закрывается и она.

Обе ветви закрылись, значит, нельзя сделать p → q и ¬q истинными при ложном ¬p. Аргумент верен, и дерево — тому причина. Заметьте, что доказательство ни разу не упоминает ни дождь, ни землю, ни того, что означают p и q. Ему это не понадобилось.

7. Когда ветвь остаётся открытой

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

Открытая ветвь — это больше, чем вердикт «неверно». Считайте знаки её атомов, и вы получите распределение: каждый атом с T истинен, каждый атом с F ложен. Это распределение делает все посылки истинными, а заключение ложным, то есть представляет собой ровно то, чем и является контрпример. Логики называют его контрмоделью, и это конкретный ответ на вопрос «почему нет?», а не отказ отвечать.

Утверждение следствия, p → q, q ⊨ p, — образцовый случай. Его таблица оставляет открытой ветвь с ложным p и истинным q: положение, при котором импликация выполняется и её следствие выполняется, а основание — нет. Одного этого распределения довольно, чтобы опровергнуть аргумент.

8. Почему метод всегда завершается

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

Это настоящая гарантия, а не надежда. Она означает, что метод — разрешающая процедура для логики высказываний: примените его к любому аргументу, и он остановится, дав либо закрытое дерево, либо открытую ветвь, и никогда не разведёт руками. Прувер этого сайта вдобавок соблюдает лимит на число узлов, но лишь как защиту от того, чтобы патологическая формула не исчерпала вкладку браузера, — самой математике никакой такой границы не нужно.

9. Другие системы доказательства

Семантические таблицы — одна из нескольких систем доказательства, и она устроена как опровержение: работает, исключая неудачу. Натуральный вывод действует наоборот и строит заключение вперёд из посылок, правилами вроде modus ponens и доказательства импликации, и куда больше похож на то, как математик рассуждает прозой. Доказательство в натуральном выводе обычно короче; найти его обычно труднее и требует изобретательности.

Секвенциальное исчисление формализует сам знак следования и обращается с утверждениями о следовании как с объектами, что делает его излюбленным средством, когда нужно доказывать утверждения о доказательствах. Резолюция сводит всё к дизъюнктам и единственному правилу — читать это неинтересно, а исполняется оно чрезвычайно быстро, и именно на ней построено большинство автоматических пруверов и SAT-решателей.

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

10. Практика

Быстрее всего метод усваивается, когда вы его выполняете. Введите аргумент в калькулятор со знаком ⊨, ⊢ или |=, и таблица будет нарисована рядом с таблицей истинности, так что дерево можно сверить со строками. Затем разберите несколько доказательств на бумаге, прежде чем смотреть ответ.