 |
 |
 |
 |
|
 |
 |
63
4.5. Выводимость и доказуемость
Приведенные выше понятия общезначимой формулы логического следования в конечном итоге
опираются на построение таблицы истинности. Но проверка с помощью таблиц оказывается, как мы
видели, и крайне громоздким, и весьма неэффективным средством. Такой способ проверки
целесообразно использовать для выявления общезначимых формул и логического следования в
исчислении высказываний, где с помощью таблицы истинности мы можем всегда ответить на вопрос,
является ли данная формула общезначимой или законом логики в этом исчислении, а также следует ли
формула В из формул А¹, А²,..., Аm. Когда существует определенная процедура, посредством которой
можно за конечное число шагов разрешить определенный вопрос, тогда в логике и математике говорят,
что для ответа на него существует алгоритм или эффективная процедура. Мы можем, например,
сказать, что для сложения, умножения, деления и других хорошо известных математических действий
существуют определенные алгоритмы. То же самое относится и к исчислению высказываний, где с
помощью таблицы истинности всегда можно в конечном итоге ответить на вопрос, является ли данная
формула законом исчисления или нет, либо следует ли рассматриваемая формула из другой или других
формул.
В исчислении предикатов мы встречаемся с принципиальными трудностями, поскольку не можем
проверить неограниченное количество интерпретаций, которые соответствуют заданной формуле из ее
универсума рассуждений. Вот почему становится необходимым обратиться к другому способу
проверки, основанному на выводе формул по точно установленным правилам. Такая необходимость
связана с тем, что для исчисления предикатов не существует алгоритмической процедуры, с помощью
которой можно было бы установить, является ли произвольная формула исчисления общезначимой, а
также следует ли в ней одна формула из другой. Таким образом, здесь мы не можем так просто
разрешить эти вопросы, как в исчислении высказываний. В связи с этим логика предикатов не имеет
разрешающей процедуры или алгоритма, которые можно было бы применить к любой формуле
исчисления, и решить поставленный вопрос чисто механически.
Однако это не означает, что такой ответ нельзя найти для конкретных формул. Мы уже убедились,
что в ряде частных случаев, построив таблицу истинности для соответствующей формулы, можно
определить, является ли она общезначимой или законом логики в исчислении предикатов. То же самое
следует сказать о процессе вывода одних формул из других по соответствующим правилам исчисления.
Отсюда становится ясным, что процесс вывода следствий в логике предикатов носит творческий
характер, поскольку он требует догадки и интуиции. Другими словами, отсутствие алгоритма вовсе не
исключает возможности поиска решения отдельных задач, для которых не существует общего метода
решения. Творческий характер мышления проявляется именно при решении нестандартных проблем.
Там, где есть алгоритмы, задачу можно программировать и использовать для ее решения компьютер,
т.е., проще говоря, заменить рассуждение вычислением. Напротив, там, где нет разрешающей
процедуры, или алгоритма, приходится строить догадки и гипотезы, проверять их и отбрасывать
негодные, вновь и вновь пробовать и проверять, чтобы найти требуемое решение. В целях облегчения
такого поиска существуют определенные эвристические методы, которые хотя и не гарантируют
безошибочно верного результата, но могут в значительной мере приблизить к его достижению.
Одним из таких методов в исчислении предикатов является способ построения аналитических, или,
точнее, аналитико-семантических таблиц. Этот метод основывается, во-первых, на рассуждении от
противного, т.е. сначала допускается, что рассматриваемая формула является необщезначимой, или
данная формула логически не следует из других. Затем доказывают, что такое допущение приводит к
противоречию, и поэтому оно опровергается. Во-вторых, для такого рассуждения строится
аналитическая таблица, каждая строка которой содержит определенный список формул. В первой
строке таблицы записывается антитезис, означающий, либо отрицание общезначимой формулы А, либо
некоторого следствия, т.е. допускается истинность его посылок А¹, А²,..., Аn и ложность заключения (¬
В). Переход от одной строки таблицы к другой связан с преобразованием формул с помощью
определенных правил редукции, опирающихся на семантический анализ смысла таких логических
связок, как отрицание, конъюнкция, дизъюнкция, импликация, а также кванторов общности и
существования. В-третьих, таблица считается замкнутой, если в некоторой ее строке в каждом списке
формул встречается определенная формула С вместе с ее отрицанием ¬C. Полученное противоречие
свидетельствует о том, что принятое допущение необоснованно и, следовательно, доказывает либо
общезначимость исходной формулы A, либо правильность следствия В из посылок А¹, A²,..., Аm, т.е. А¹,
А²,..., Аm
| = В. Если же аналитическая таблица остается незамкнутой, то нельзя однозначно решить