Переменные и константы
Отметим еще несколько простых свойств выводимости, которые нам потребуются:
Лемма о свежих константах.
Пусть выводима формула , где — произвольная формула, — переменная, — константа, не входящая в формулу . Тогда выводима и формула .
Интуитивный смысл леммы: если мы доказали что-то про "свежую" константу (не запятнавшую себя участием в формуле ), то фактически мы доказали формулу
для произвольных значений переменной.
Доказательство леммы. По условию существует вывод формулы . Возьмем "свежую" переменную , не встречающуюся в этом выводе, и всюду заменим в нем константу
на эту переменную. При этом вывод останется выводом, так как правила обращения с переменными и константами ничем не отличаются (кванторов по новой переменной в нем нет, так что корректные подстановки останутся корректными и применения правил Бернайса останутся допустимыми). Таким образом, выводима формула .
По правилу обобщения выводима формула . Осталось применить аксиому ; подстановка в правой части корректна и дает формулу , так как сначала мы заменили свободные вхождения на , а затем обратно (так что в зону действия кванторов по они попасть не могли). Лемма доказана.
97. Сформулируйте и докажите аналогичную лемму для нескольких констант.
Аналогичное рассуждение позволяет доказать и другое утверждение, которое нам потребуется:
Лемма о добавлении констант.
Пусть формула некоторой сигнатуры выводима в исчислении предикатов расширенной сигнатуры , полученной из
добавлением новых констант. Тогда выводима и в исчислении предикатов сигнатуры .
Доказательство. Пусть формула , не содержащая новых констант, имеет вывод, в котором новые константы встречаются. Как их оттуда удалить? Легко понять, что их можно заменить на свежие переменные, не входящие в вывод, и он останется выводом, но уже без новых констант. Лемма доказана.
На самом деле эта лемма верна для произвольного расширения сигнатуры (можно добавлять не только константы, но и функциональные символы любой валентности, а также предикатные символы).
Чтобы удалить новые символы из вывода, поступаем так. Все термы вида , где — добавленный функциональный символ, мы заменяем на новую переменную (можно взять одну и ту же переменную для всех новых символов и всех их вхождений). Все атомарные формулы с новыми предикатными символами заменяем на какую-либо замкнутую формулу (одну и ту же; какая именно формула, роли не играет).
98. Проведите это рассуждение подробно.
Таким образом, мы можем говорить о выводимости формулы, не уточняя, в какой именно сигнатуре (содержащей все использованные в формуле предикатные и функциональные символы) мы ищем ее вывод.
Если принять теорему о полноте, по которой выводимость равносильна общезначимости, независимость выводимости от сигнатуры становится очевидной: истинность формулы не зависит от интерпретации символов, которые в нее не входят. (Если интерпретировать отсутствующие в формуле символы как постоянные функции и предикаты, мы приходим к синтаксическому рассуждению, упомянутому выше.)
