Языки и исчисления

       

Примеры выводимых формул


Прежде чем доказывать теорему Геделя о полноте исчисления предикатов, мы должны приобрести некоторый опыт построения выводов в этом исчислении.

  • Прежде всего отметим, что возможность сослаться на теорему о полноте исчисления высказываний и считать выводимым любой частный случай пропозициональной тавтологии сильно облегчает жизнь. Например, пусть мы вывели две формулы и и хотим теперь вывести формулу . Это просто: заметим, что формула

    является частным случаем пропозициональной тавтологии (а на самом деле и аксиомой) и дважды применяем правило MP.

  • Другой пример такого же рода: если формула

    выводима, то выводима и формула , поскольку импликация

    является частным случаем пропозициональной тавтологии.

  • Еще один пример: если выводимы формулы и , то выводима и формула , поскольку формула

    является частным случаем пропозициональной тавтологии.

  • Для произвольной формулы выведем формулу

    В самом деле, подстановка переменной вместо себя всегда допустима, поэтому формулы и являются аксиомами. Остается воспользоваться предыдущим замечанием.

  • Для произвольной формулы выведем формулу

    Формулы и являются аксиомами. С их помощью выводим формулу . Теперь заметим, что левая часть импликации не имеет параметра , а правая часть не имеет параметра , так что можно применить два правила Бернайса (в любом порядке) и добавить справа квантор , а слева — квантор .

  • Предположим, что формула выводима, а — произвольная переменная. Покажем, что в этом случае выводима формула . В самом деле, формула является аксиомой. Далее выводим (с помощью пропозициональных тавтологий и правила MP) формулу ; остается воспользоваться правилом Бернайса (левая часть не имеет параметра ).
  • Аналогичным образом из выводимости формулы

    следует выводимость формулы , только надо начать с аксиомы , затем получить , а потом применить правило Бернайса.

  • Таким образом, если формулы и доказуемо эквивалентны (это значит, что импликации и выводимы), то формулы

    и также доказуемо эквивалентны. (Аналогичное утверждение верно и для формул и .)


    Теперь несложно доказать и более общий факт: замена подформулы на доказуемо эквивалентную дает доказуемо эквивалентную формулу.
  • Выведем формулу (здесь — одноместный предикатный символ). Это несложно: начнем с аксиомы , в ней левая часть не имеет параметра и потому по правилу Бернайса из нее получается искомая формула. Этот пример показывает, что связанные переменные можно переименовывать, не меняя смысла формулы

  • Выведем формулы, связывающие кванторы всеобщности и существования: Напомним, что мы считаем сокращением для , так что нам надо вывести четыре формулы.
    Начнем с формулы . Имея в виду правило Бернайса, достаточно вывести формулу . Тавтология позволяет вместо этого выводить формулу , которая является аксиомой.
    В только что выведенной формуле можно в качестве взять любую формулу, в том числе начинающуюся с отрицания. Подставив вместо , получим где доказуемо эквивалентна
    и потому может быть заменена на . После этого правило контрапозиции (если из следует , то из следует ) дает

    Выведем третью формулу: . По правилу Бернайса достаточно вывести , что после контрапозиции превращается в аксиому .
    Четвертая формула получится, если заменить в третьей
    на и применить контрапозицию.


Содержание раздела