Символически это определение можно представить в следующей форме:
A1 ,A2, ,Am | = B
где знак | = обозначает следование.
В приведенном выше определении логического следования свободные переменные рассматриваются как обозначающие некоторые элементы из универсума рассуждения. Поэтому в течение всего рассуждения они, так же, как и предикаты, должны оставаться фиксированными. При другом определении переменные могут быть различными в разных формулах. Чтобы яснее представлять различия между двумя подходами к определению логического следования, обратимся к языку алгебры, в котором, как известно, различают, с одной стороны, уравнения (или условные равенства), а с другой - тождества (или тождественные равенства). В то время как уравнению удовлетворяют только определенные значения переменной, называемые его корнями, тождество выполняется при любых значениях переменной. Именно поэтому уравнения считаются условными равенствами. Действительно, например, в уравнении х2 + 2х - 3 = 0 левая часть равняется правой только при значениях х = 1 и х = -3, а в тождестве (х + 1)2 = х2 + 2х + 1 вместо переменной можно подставлять любые числа.
Соответственно этому будем говорить, что для переменных в уравнениях дается условная интерпретация, а в тождествах - интерпретация всеобщности. При условной интерпретации переменной х в определенном допущении А(х) - куда х входит свободно - любое следствие, полученное из него, должно относиться к тому же самому элементу из универсума А(х). Иными словами, переменная х в этом случае фиксирована, так как представляет то же самое число в процессе рассуждения. При тождественной интерпретации значения переменных могут изменяться. Отсюда становится ясным, что приведенное выше определение для логического следования в исчислении предикатов соответствует условной интерпретации свободных переменных, входящих в допущения A1, А2,..., An. Чтобы сформулировать другое определение следования, необходимо опираться на интерпретацию всеобщности для всех переменных. Для этого необходимо, во- первых, связать все допущения А1, А2, ..., Am кванторами общности, а во-вторых, построить таблицы истинности, как и в первом определении.
4.5. Выводимость и доказуемость
Приведенные выше понятия общезначимой формулы логического следования в конечном итоге опираются на построение таблицы истинности. Но проверка с помощью таблиц оказывается, как мы видели, и крайне громоздким, и весьма неэффективным средством. Такой способ проверки целесообразно использовать для выявления общезначимых формул и логического следования в исчислении высказываний, где с помощью таблицы истинности мы можем всегда ответить на вопрос, является ли данная формула общезначимой или законом логики в этом исчислении, а также следует ли формула В из формул A1, А2,..., Аm. Когда существует определенная процедура, посредством которой можно за конечное число шагов разрешить определенный вопрос, тогда в логике и математике говорят, что для ответа на него существует алгоритм или эффективная процедура. Мы можем, например, сказать, что для сложения, умножения, деления и других хорошо известных математических действий существуют определенные алгоритмы. То же самое относится и к исчислению высказываний, где с помощью таблицы истинности всегда можно в конечном итоге ответить на вопрос, является ли данная формула законом исчисления или нет, либо следует ли рассматриваемая формула из другой или других формул.
В исчислении предикатов мы встречаемся с принципиальными трудностями, поскольку не можем проверить неограниченное количество интерпретаций, которые соответствуют заданной формуле из ее универсума рассуждений. Вот почему становится необходимым обратиться к другому способу проверки, основанному на выводе формул по точно установленным правилам. Такая необходимость связана с тем, что для исчисления предикатов не существует алгоритмической процедуры, с помощью которой можно было бы установить, является ли произвольная формула исчисления общезначимой, а также следует ли в ней одна формула из другой. Таким образом, здесь мы не можем так просто разрешить эти вопросы, как в исчислении высказываний. В связи с этим логика предикатов не имеет разрешающей процедуры или алгоритма, которые можно было бы применить к любой формуле исчисления, и решить поставленный вопрос чисто механически.
Однако это не означает, что такой ответ нельзя найти для конкретных формул. Мы уже убедились, что в ряде частных случаев, построив таблицу истинности для соответствующей формулы, можно определить, является ли она общезначимой или законом логики в исчислении предикатов. То же самое следует сказать о процессе вывода одних формул из других по соответствующим правилам исчисления. Отсюда становится ясным, что процесс вывода следствий в логике предикатов носит творческий характер, поскольку он требует догадки и интуиции. Другими словами, отсутствие алгоритма вовсе не исключает возможности поиска решения отдельных задач, для которых не существует общего метода решения. Творческий характер мышления проявляется именно при решении нестандартных проблем. Там, где есть алгоритмы, задачу можно программировать и использовать для ее решения компьютер, т.е., проще говоря, заменить рассуждение вычислением. Напротив, там, где нет разрешающей процедуры, или алгоритма, приходится строить догадки и гипотезы, проверять их и отбрасывать негодные, вновь и вновь пробовать и проверять, чтобы найти требуемое решение. В целях облегчения такого поиска существуют определенные эвристические методы, которые хотя и не гарантируют безошибочно верного результата, но могут в значительной мере приблизить к его достижению.