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

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

Однако это не означает, что такой ответ нельзя найти для конкретных формул. Мы уже убедились, что в ряде частных случаев, построив таблицу истинности для соответствующей формулы, можно определить, является ли она общезначимой или законом логики в исчислении предикатов. То же самое следует сказать о процессе вывода одних формул из других по соответствующим правилам исчисления. Отсюда становится ясным, что процесс вывода следствий в логике предикатов носит творческий характер, поскольку он требует догадки и интуиции. Другими словами, отсутствие алгоритма вовсе не исключает возможности поиска решения отдельных задач, для которых не существует общего метода решения. Творческий характер мышления проявляется именно при решении нестандартных проблем. Там, где есть алгоритмы, задачу можно программировать и использовать для ее решения компьютер, т.е., проще говоря, заменить рассуждение вычислением. Напротив, там, где нет разрешающей процедуры, или алгоритма, приходится строить догадки и гипотезы, проверять их и отбрасывать негодные, вновь и вновь пробовать и проверять, чтобы найти требуемое решение. В целях облегчения такого поиска существуют определенные эвристические методы, которые хотя и не гарантируют безошибочно верного результата, но могут в значительной мере приблизить к его достижению.

Одним из таких методов в исчислении предикатов является способ построения аналитических, или, точнее, аналитико-семантических таблиц. Этот метод основывается, во-первых, на рассуждении от противного, т.е. сначала допускается, что рассматриваемая формула является необщезначимой, или данная формула логически не следует из других. Затем доказывают, что такое допущение приводит к противоречию, и поэтому оно опровергается. Во-вторых, для такого рассуждения строится аналитическая таблица, каждая строка которой содержит определенный список формул. В первой строке таблицы записывается антитезис, означающий, либо отрицание общезначимой формулы А, либо некоторого следствия, т.е. допускается истинность его посылок 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, оставляя при этом остальные списки неизменными: