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