Корректность исчисления предикатов
Теорема 43. Всякая выводимая в исчислении предикатов формула является общезначимой.
Для исчисления высказываний проверка корректности была тривиальной — надо было по таблице проверить, что все аксиомы (1)-(11) являются тавтологиями. С этими аксиомами и сейчас нет проблем. Но в двух следующих аксиомах есть ограничение на корректность подстановки, без которого они могут не быть общезначимыми. Естественно, это ограничение должно быть использовано и в доказательстве корректности, и это потребует довольно скучных рассуждений — тем более скучных, что сам факт кажется ясным и так. Тем не менее такие рассуждения надо уметь проводить, так что мы ничего пропускать не будем.
Итак, пусть фиксирована сигнатура , а также некоторая интерпретация этой сигнатуры. Всюду далее, говоря о термах и формулах, мы имеем в виду термы и формулы этой сигнатуры, а говоря об их значениях, имеем в виду значения в этой интерпретации.
Лемма 1. Пусть и — термы, а — переменная. Тогда
для произвольной оценки .
Напомним обозначения: в левой части мы подставляем вместо в терм , и берем значение получившегося терма на оценке . В правой части стоит значение терма на оценке, которая получится из , если значение переменной изменить и считать равным значению терма на оценке .
В сущности, это утверждение совершенно тривиально: оно говорит, например, что значение при равно значению при . Но раз уж мы взялись все доказывать формально, докажем его индукцией по построению терма . Если терм есть переменная, отличная от , то ни подстановка, ни изменение оценки не сказываются на значении терма . Для случая получаем слева и справа. Если терм получается из других термов применением функционального символа, то подстановка выполняется отдельно в каждом из этих термов, так что искомое равенство также сохраняется. Лемма 1 доказана.
Аналогичное утверждение для формул таково:
Лемма 2. Пусть — формула, — терм, а — переменная, причем подстановка вместо в формулу корректна. Тогда
для произвольной оценки .
Поясним смысл этой леммы на примере. Пусть является единственным параметром формулы , а — константа. Тогда формула замкнута; лемма утверждает, что ее истинность равносильна истинности на оценке, при которой значение переменной есть элемент интерпретации, соответствующий константе .
Доказательство леммы проведем индукцией по построению формулы . Для атомарных формул это утверждение является прямым следствием леммы 1. Кроме того, из определения истинностного значения формулы и из определения подстановки ясно, что если утверждение леммы 2 верно для двух формул и , то оно верно для их любой их логической комбинации (конъюнкции, дизъюнкции и импликации); аналогично для отрицания.
Единственный нетривиальный случай — формула, начинающаяся с квантора. Здесь наши определения вступают в игру. Пусть имеет вид . Есть два принципиально разных случая: либо является параметром формулы (т. е. формулы ), либо нет. Во втором случае совпадает с , а изменение значения переменной в оценке не влияет на значение формулы , так что все сходится. Осталось разобрать случай, когда является параметром формулы
(отсюда следует, что не совпадает с ). По определению корректной подстановки, в этом случае переменная не входит в терм и подстановка корректна. Тогда
Мы воспользовались определением подстановки, определением истинности ( означает конъюнкцию по всем элементам из носителя интерпретации) и предположением индукции для формулы . Теперь надо заметить, что переменная не входит в по предположению корректности, и потому значение терма не изменится, если заменить на . Далее, и
различны, поэтому два изменения в можно переставить местами. Используя эти соображения, можно продолжить цепочку равенств:
что и требовалось. Случай формулы вида
разбирается аналогично, надо только заменить на . Лемма 2 доказана.
Теперь уже ясно, почему формула
будет истинна на любой оценке (если подстановка корректна). В самом деле, если левая часть импликации истинна на , то будет истинна на любой оценке , которая отличается от лишь значением переменной . В частности, будет истинна и на оценке , что по только что доказанной лемме 2 означает, что правая часть импликации истинна на .
Общезначимость формулы
доказывается аналогично.
Нам осталось проверить, что правила вывода сохраняют общезначимость. Для правила MP это очевидно (как и в случае исчисления высказываний). Проверим это для правил Бернайса. Это совсем несложно, так как здесь нет речи ни о каких корректных подстановках.
Пусть, например, формула общезначима и переменная не является параметром формулы . Проверим, что формула общезначима, то есть истинна на любой оценке (в любой интерпретации). В самом деле, пусть истинна на оценке . Тогда она истинна и на любой оценке , отличающейся от
только значением переменной (значение переменной не влияет на истинность , так как не является параметром). Значит, и формула истинна на любой такой оценке . А это в точности означает, что истинна на оценке , что и требовалось.
Для второго правила Бернайса рассуждение симметрично. Пусть формула общезначима и переменная не является параметром формулы . Покажем, что формула общезначима. В самом деле, пусть ее левая часть истинна на некоторой оценке . По определению истинности формулы, начинающейся с квантора существования, это означает, что найдется оценка , которая отличается от только на переменной , для которой истинно. Тогда и
истинно. Но переменная не является параметром формулы , так что . Следовательно, формула
истинна на оценке , что и требовалось доказать.
