1. Что такое доказательство
АргументрассуждениеНабор посылок, выдвинутых в поддержку заключения.Читать статью целиком — это утверждение, что некоторое заключениезаключениеУтверждение, которое рассуждение стремится обосновать.Читать статью целиком следует излогическое следованиеЗаключение верно в каждой интерпретации, где верны посылки.Читать статью целиком некоторых посылок. Доказательство — это то, что решает вопрос об этом утверждении: конечный, проверяемый объект, который каждый может прочесть строка за строкой и признать, не полагаясь на ваше слово. Смысл доказательства не в том, что оно убеждает, — хорошая речь тоже убеждает, — а в том, что каждый его шаг не мог оказаться иным.
Это требование строже, чем кажется. «Идёт дождь, значит, земля мокрая» — разумное высказываниевысказываниеУтверждение, которое истинно либо ложно, но не то и другое сразу.Читать статью целиком, но оно опирается на то, что вы знаете о дожде и земле. Формальная логика убирает это и задаёт более узкий вопрос: возможно ли вообще, исходя лишь из формы предложений, чтобы посылкипосылкаУтверждение, которое рассуждение принимает, чтобы прийти к заключению.Читать статью целиком были истинны, а заключение ложно? Если такой возможности нет, аргумент верен, а доказательство — это запись того, почему её нет.
Это руководство — об одном способе получить такую запись: о методе семантических таблиц, которые называют также деревьями истинности. Именно этот метод сайт применяет всякий раз, когда вы вводите аргумент в калькулятор, и, пройдя его один раз, вы сможете проверить аргумент на бумаге, имея только ручку.
2. Верен — и откуда это известно
Запишите аргумент со знаком следования: посылки слева, заключение справа. Утверждение p → q, ¬q ⊨ ¬p говорит, что из импликацииимпликацияp → q, ложна только когда p истинно, а q ложно.Читать статью целиком и отрицанияотрицаниеМеняет значение истинности: ¬p истинно ровно тогда, когда p ложно.Читать статью целиком её следствия вытекает отрицание её основания. Знак следования — не ещё одна связкалогическая связкаСимвол, строящий сложное высказывание из более простых.Читать статью целиком. Это утверждение о формулах по обе стороны от него, и оно либо верно, либо нет.
Определение логического следования прямо указывает на способ проверки: перебрать все распределения истины и лжи по переменным и посмотреть, найдётся ли такое, при котором все посылки истинны, а заключение ложно. Именно это делает таблица истинноститаблица истинностиПо строке на каждый набор значений и значение формулы в каждой.Читать статью целиком, и для двух-трёх переменных она вполне годится. Беда в том, что таблица растёт как 2ⁿ. Десяти переменным нужна тысяча строк, двадцати — миллион, и таблица ничего не говорит о том, какие строки имели значение.
Таблица в смысле tableau подступает к тому же вопросу с другого конца. Вместо того чтобы перечислять все возможности и искать среди них плохую, она предполагает, что плохая существует, и пытается её построить. Если попытка на каждом возможном пути обрушивается в противоречиепротиворечиеФормула, ложная при любой интерпретации.Читать статью целиком, такого распределения нет и аргумент верен. Если попытка удаётся, построенное и есть контрпримерконтрмодельИнтерпретация, где посылки истинны, а заключение ложно.Читать статью целиком, который можно прочесть напрямую.
3. Метод семантических таблиц
Семантическая таблица — это дерево помеченных формул. Каждая строка — формула с T или F перед ней, и знак говорит, что ветвь предполагает об этой формуле: не какова её истинностная оценкаинтерпретацияОдно приписывание значений истинности всем переменным формулы.Читать статью целиком, а какой она должна была бы быть, чтобы аргумент не прошёл. Весь метод — четыре шага:
- Запишите каждую посылку с T. Вы допускаете, что все посылки аргумента выполняются.
- Запишите заключение с F. Вы допускаете, что оно тем не менее не выполняется, — это и есть допущение, которое вы стремитесь опровергнуть.
- Возьмите любую строку, которая ещё не атоматомарное высказываниеВысказывание, внутри которого нет ни одной связки.Читать статью целиком, и примените правило для её главной связки и знака, добавив то, что даёт правило, в конец каждой ветви, проходящей через неё.
- Закройте ветвь, как только она содержит и T A, и F A для одной и той же формулы A. Остановитесь, когда все ветви закрыты или не осталось строк для разложения.
Ничто в этом цикле не требует смекалки или выбора стратегии. У каждой строки ровно одно правило, и применение правил в любом порядке даёт один и тот же итог — поэтому это может делать машина, и поэтому её результату можно доверять.
4. Правила
Есть по одному правилу на связку при каждом знаке — всего десять. Они распадаются на два вида, и различие между видами и есть вся причина, по которой семантическая таблица — дерево, а не список. Правило α говорит, что несколько вещей должны выполняться вместе, и потому складывает свои результаты вниз по ветви. Правило β говорит, что должно выполняться одно из двух, и потому расщепляет ветвь надвое, пуская каждый случай своим путём.
| Строка | Даёт | Вид |
|---|---|---|
T ¬A | F A | складывает |
F ¬A | T A | складывает |
T (A∧B) | T A, T B | складывает |
F (A∧B) | F AF B | ветвится |
T (A∨B) | T AT B | ветвится |
F (A∨B) | F A, F B | складывает |
T (A→B) | F AT B | ветвится |
F (A→B) | T A, F B | складывает |
T (A↔B) | T A, T BF A, F B | ветвится |
F (A↔B) | T A, F BF A, T B | ветвится |
Каждое правило — это всего лишь условие истинности его связки, прочитанное задом наперёд. КонъюнкцияконъюнкцияИстинна только когда обе части истинны: p ∧ q.Читать статью целиком истинна, только когда истинны обе стороны, поэтому T (A ∧ B) складывает T A и T B. Конъюнкция ложна, когда ложна хотя бы одна сторона, но формула не говорит какая, поэтому F (A ∧ B) вынуждено пробовать обе: оно ветвится. Та же асимметрия действует наоборот для дизъюнкциидизъюнкцияИстинна, когда истинна хотя бы одна часть: p ∨ q.Читать статью целиком, а ложная импликация означает, что основание выполнилось, а следствие — нет: единственный случай, когда импликация рвётся.
Обратите внимание, чего правила никогда не делают: они никогда не изобретают формулу. Всё, что даёт правило, — это часть той строки, из которой оно получено. Это свойство — свойство подформулы — и делает метод конечным, и ниже мы к нему вернёмся.
5. Как закрывается ветвь
Ветвь — это одна цепочка рассуждения: прочтите её от корня до листа, и вы получите один полный набор допущений. Ветвь закрывается, когда эти допущения прямо противоречат друг другу, то есть когда она несёт и T A, и F A для одной и той же формулы. Неважно, насколько сложна A и как далеко друг от друга стоят обе строки: если ветви нужно, чтобы формула была одновременно истинной и ложной, ничто её не удовлетворит.
Отметьте закрытую ветвь знаком ×, назвав две строки, которые её закрыли, и больше с ней не работайте. Из допущения, которое и так было невозможным, узнать больше нечего.
Когда закрывается каждая ветвь, таблица закрыта, и это и есть доказательство. Оно показывает, что исходное предположение — все посылки истинны, заключение ложно — ведёт к противоречию на каждом пути, какой оно могло избрать. Раз путей не осталось, такого распределения нет, и аргумент верен. Это доказательство от противногодоказательство от противногоПредположить обратное, вывести противоречие, заключить исходное.Читать статью целиком, разложенное так, чтобы ни один случай нельзя было упустить.
6. Доказательство, строка за строкой
Возьмём modus tollensmodus tollensИз p → q и ¬q следует ¬p.Читать статью целиком: p → q, ¬q ⊨ ¬p. Строки 1 и 2 — посылки, принятые за истинные. Строка 3 — заключение, принятое за ложное; а поскольку заключение есть ¬p, принять его ложным значит принять p истинным, что и записывает строка 5. Строка 4 получена по правилу отрицания, применённому к строке 2: если ¬q истинно, то q ложно. Импликация в строке 1 — единственная оставшаяся строка со связкой, и это правило β, поэтому дерево разветвляется:
- 1Истинно: p→qпосылка
- 2Истинно: ¬qпосылка
- 3Ложно: ¬pотрицание заключения
- 4Ложно: qиз строки 2
- 5Истинно: pиз строки 3
- 6Ложно: pиз строки 1
Ветвь замкнута: строка 6 противоречит строке 5.
- 7Истинно: qиз строки 1
Ветвь замкнута: строка 7 противоречит строке 4.
замкнутая ветвь
Левая ветвь предполагает, что импликация выполнилась из-за того, что не выполнилось её основание, — но в строке 5 p уже истинно, поэтому ветвь противоречит себе и закрывается. Правая ветвь предполагает, что она выполнилась из-за истинности следствия, — но в строке 4 q уже ложно, поэтому закрывается и она.
Обе ветви закрылись, значит, нельзя сделать p → q и ¬q истинными при ложном ¬p. Аргумент верен, и дерево — тому причина. Заметьте, что доказательство ни разу не упоминает ни дождь, ни землю, ни того, что означают p и q. Ему это не понадобилось.
7. Когда ветвь остаётся открытой
Не всякий аргумент верен, и вот здесь метод и оправдывает себя. Если вы доводите ветвь до состояния, когда ничто на ней уже не раскладывается — остались лишь атомы и отрицания атомов, — а она так и не закрылась, эта ветвь насыщена и открыта. Она не осталась незакрытой оттого, что вы остановились слишком рано: пробовать больше нечего.
Открытая ветвь — это больше, чем вердикт «неверно». Считайте знаки её атомов, и вы получите распределение: каждый атом с T истинен, каждый атом с F ложен. Это распределение делает все посылки истинными, а заключение ложным, то есть представляет собой ровно то, чем и является контрпример. Логики называют его контрмоделью, и это конкретный ответ на вопрос «почему нет?», а не отказ отвечать.
Утверждение следствия, p → q, q ⊨ p, — образцовый случай. Его таблица оставляет открытой ветвь с ложным p и истинным q: положение, при котором импликация выполняется и её следствие выполняется, а основание — нет. Одного этого распределения довольно, чтобы опровергнуть аргумент.
8. Почему метод всегда завершается
Каждое правило заменяет формулу её же подформулами, а любая подформула строго короче формулы, из которой получена. Поэтому ни одна ветвь не может расти бесконечно: каждый шаг спускается по конечной лестнице из частей исходного аргумента, а у лестницы есть низ. Рано или поздно каждая строка ветви оказывается атомом или отрицанием атома, и делать больше нечего.
Это настоящая гарантия, а не надежда. Она означает, что метод — разрешающая процедура для логики высказываний: примените его к любому аргументу, и он остановится, дав либо закрытое дерево, либо открытую ветвь, и никогда не разведёт руками. Прувер этого сайта вдобавок соблюдает лимит на число узлов, но лишь как защиту от того, чтобы патологическая формула не исчерпала вкладку браузера, — самой математике никакой такой границы не нужно.
9. Другие системы доказательства
Семантические таблицы — одна из нескольких систем доказательства, и она устроена как опровержение: работает, исключая неудачу. Натуральный выводнатуральный выводДоказательство заключения последовательным применением правил.Читать статью целиком действует наоборот и строит заключение вперёд из посылок, правилами вроде modus ponensmodus ponensИз p → q и p следует q.Читать статью целиком и доказательства импликации, и куда больше похож на то, как математик рассуждает прозой. Доказательство в натуральном выводе обычно короче; найти его обычно труднее и требует изобретательности.
Секвенциальное исчисление формализует сам знак следования и обращается с утверждениями о следовании как с объектами, что делает его излюбленным средством, когда нужно доказывать утверждения о доказательствах. Резолюция сводит всё к дизъюнктам и единственному правилу — читать это неинтересно, а исполняется оно чрезвычайно быстро, и именно на ней построено большинство автоматических пруверов и SAT-решателей.
Все они согласны в том, какие пропозициональные аргументы верны; различаются они тем, как выглядит доказательство и что легко найти. Семантические таблицы дружелюбнее всех к учащемуся, потому что неудавшееся доказательство здесь не тупик — оно вручает вам контрпример.
10. Практика
Быстрее всего метод усваивается, когда вы его выполняете. Введите аргумент в калькулятор со знаком ⊨, ⊢ или |=, и таблица будет нарисована рядом с таблицей истинности, так что дерево можно сверить со строками. Затем разберите несколько доказательств на бумаге, прежде чем смотреть ответ.