Выбрать главу

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

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

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

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

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

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

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