Георгий Рузавин - Логика и аргументация: Учебн. пособие для вузов.

Одним из таких методов в исчислении предикатов является способ построения аналитических, или, точнее, аналитико-семантических таблиц. Этот метод основывается, во-первых, на рассуждении от противного, т.е. сначала допускается, что рассматриваемая формула является необщезначимой, или данная формула логически не следует из других. Затем доказывают, что такое допущение приводит к противоречию, и поэтому оно опровергается. Во-вторых, для такого рассуждения строится аналитическая таблица, каждая строка которой содержит определенный список формул. В первой строке таблицы записывается антитезис, означающий, либо отрицание общезначимой формулы А, либо некоторого следствия, т.е. допускается истинность его посылок A 1, А 2,..., A nи ложность заключения (— В). Переход от одной строки таблицы к другой связан с преобразованием формул с помощью определенных правил редукции, опирающихся на семантический анализ смысла таких логических связок, как отрицание, конъюнкция, дизъюнкция, импликация, а также кванторов общности и существования. В-третьих, таблица считается замкнутой, если в некоторой ее строке в каждом списке формул встречается определенная формула С вместе с ее отрицанием —C. Полученное противоречие свидетельствует о том, что принятое допущение необоснованно и, следовательно, доказывает либо общезначимость исходной формулы A, либо правильность следствия В из посылок A 1, A 2,..., А m, т.е. A 1, А 2,..., А m| = В. Если же аналитическая таблица остается незамкнутой, то нельзя однозначно решить вопрос об общезначимости формулы А или логического следствия A 1, А 2,..., А m| = В. Ведь подобный результат мог бы свидетельствовать не только о необщезначимости формулы и неправильности логического следствия, но и о том, что нам не удалось найти комбинацию формул, которая привела бы к замыканию таблицы.

Решающая роль при построении аналитической таблицы принадлежит правилам редукции, с помощью которых происходит переход от формул на строке n таблицы к следующей строке n + 1.

Правило конъюнкции(∧). Допустим, что на одной строке таблицы мы имеем список формул: Г, А ∧ В, Δ, где Г - последовательность формул, предшествующих конъюнкции, а д - последовательность формул, следующая за ней. Поскольку из истинности конъюнкции можно сделать вывод об истинности каждого ее члена, то всюду, где она встречается, вместо истинной конъюнкции можно переходить к ее членам. В результате можно перейти от некоторой строки n к строке n + 1, оставляя при этом остальные списки неизменными:

Правило дизъюнкции(∨) разрешает перейти от строки, в которой встречается она, к другой, где вместо дизъюнкции встречаются два списка, в одном из которых находится один дизъюнктивный член, во втором - другой:

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

Правило импликации(→) разрешает переходить от строки, где она встречается, к другой, в которой встречаются два списка формул, в одной из них содержится отрицание антецедента, в другой - консеквент импликации:

Действительно, импликация будет истинна, если ложен ее антецедент или истинен консеквент, что и представлено в заключении вывода.

Правило отрицания конъюнкцииразрешает в заключении переходить к отрицанию конъюнктивных членов, поскольку отрицание конъюнкции означает отрицание этих членов.

Г, ¬ (А ∧В)

Г, ¬ А, Δ ¬ Г, ¬ В, Δ

Правило отрицания дизъюнкцииразрешает в заключении переходить от отрицания дизъюнкции к отрицательным членам дизъюнкции, ибо дизъюнкция является ложной только тогда, когда ложны все члены дизъюнкции:

Г, ¬ ( А ∨ В ), Δ

Г, ¬ А, ¬ В, Δ

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

Г, ¬ (А → В), Δ

Г, А, ¬ В, Δ

Двойное отрицание в одной строке может быть заменено утверждением в другой:

Г, ¬ ¬ А, Δ

Г, А, Δ

Квантор существования, который стоит перед формулой А, указывает на наличие объекта, удовлетворяющего

А. Назовем этот объект константой к. Очевидно, что А(к) будет истинно, ибо к удовлетворяет условию А:

Г, (Е х ) А , Δ

Г, А, (к), Δ

Квантор общности, встречающийся перед формулой, свидетельствует о том, что формула (х) А истинна тогда и только тогда, когда каждый индивид из универсума рассуждения удовлетворяет условию А, Тогда истинной оказывается любая формула вида А (т), получающаяся путем замены всех свободных вхождений переменной на любой замкнутый терм:

Г, (х) А, Δ

Г, (х) А, А(т), Δ

Формула с квантором общности (х) А сохраняется для того, чтобы в дальнейшем можно было применить его к другим термам.

Более строгий подход к доказательству формул достигается с помощью аксиоматического построения исчисления предикатов. Для доказательства формул логики, как и для доказательства теорем геометрии, необходимо указать некоторые исходные формулы, которые принимаются в качестве аксиом. В принципе в качестве аксиом могут быть взяты любые тождественно истинные или общезначимые формулы, которые играют роль законов логики. Но обычно при выборе аксиом руководствуются разного рода дополнительными требованиями: простоты получаемой формальной системы, минимального числа аксиом, их интуитивной очевидности и т.п. Чтобы вывести из исходных формул новые формулы, т.е. доказать последние как теоремы логики, необходимо ясно и точно перечислить также правила вывода или доказательства. К их числу относится правило заключения по схеме modus ponens: из двух формул А и А → В следует новая формула В. Кроме того, для получения новых формул используются различные правила подстановки. Например, свободная предметная переменная может быть заменена другой предметной переменной, если эта замена проводится одновременно на всех местах, где встречается свободная переменная. То же самое относится к переменной, обозначающей высказывание.

В качестве аксиом исчисления предикатов берутся, во-первых, аксиомы исчисления высказываний, во-вторых, к ним присоединяют две аксиомы, относящиеся к использованию кванторов общности и существования: