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

       

Аксиомы и правила вывода


Возвратимся к нашей задаче: какие аксиомы и правила вывода нам нужны, чтобы получить все общезначимые формулы некоторой сигнатуры ? Естественно использовать все схемы аксиом - исчисления высказываний, но только вместо букв , и теперь можно подставлять произвольные формулы сигнатуры . Теорема о полноте исчисления высказываний гарантирует, что после этого мы сможем вывести любой частный случай любой пропозициональной тавтологии (то есть любую формулу, которая получается из пропозициональной тавтологии заменой пропозициональных переменных на формулы сигнатуры ). В самом деле, возьмем вывод этой тавтологии в исчислении высказываний (которое, как мы знаем, полно) и выполним соответствующую замену во всех формулах этого вывода.

Почти столь же просто понять, что ничего другого такие аксиомы не дадут: если пользоваться лишь схемами аксиом - , разрешая брать в них в качестве , ,

произвольные формулы сигнатуры , а в качестве правила вывода использовать modus ponens, то все выводимые формулы будут частными случаями пропозициональных тавтологий. В самом деле, если какая-то подформула начинается с квантора, то в выводе она может встречаться только как единое целое, то есть такая подформула ведет себя как пропозициональная переменная.

92. Проведите это рассуждение аккуратно.

Это наблюдение скорее тривиально, чем удивительно — если среди наших аксиом и правил вывода нет ничего о смысле кванторов, то формулы, начинающиеся с кванторов, будут вести себя как неделимые блоки. Таким образом, нам нужны аксиомы и правила вывода, отражающие интуитивный смысл кванторов.

Вспомним, как выглядели аксиомы исчисления высказываний. У нас было два типа аксиом для конъюнкции и дизъюнкции: одни говорили, что из них следует (например, из следовало ), а другие — как их можно доказать (например, аксиома говорила, что для доказательства надо доказать и ). Кванторы всеобщности и существования в некотором смысле аналогичны конъюнкции и дизъюнкции, и аксиомы для них тоже будут похожими. Например, среди аксиом будет формула
где — одноместный предикатный символ нашей сигнатуры, а — константа, переменная или вообще любой терм. (Если верно для всех , то оно должно быть верно и для нашего конкретного . Можно сказать и так: из "бесконечной конъюнкции" всех вытекает один из ее членов.)

Конечно, такую аксиому надо иметь не только для одноместного предикатного символа , но для любой формулы , любой переменной и любого терма . Естественно сказать, что если — любая формула, а — любой терм, то формула где обозначает результат подстановки вместо всех вхождений переменной в формулу , является аксиомой. (Запись можно читать как "фи от тэ вместо кси".)

К сожалению, все не так просто. Например, если формула

имеет вид то подстановка терма вместо даст абсурдное выражение

вообще не являющееся формулой. А если подставить только внутри и , то получится выражение

которое хотя и будет формулой, но имеет совсем не тот смысл, который нам нужен.

Конечно, в данном случае по смыслу ясно, что подставлять

надо лишь вместо самого первого вхождения переменной . Но если мы хотим определить формальную систему аксиом и правил вывода, то надо дать формальные определения.

Для каждого квантора в формуле рассмотрим его область действия — начинающуюся с него подформулу. Свободным вхождением индивидной переменной в формулу называется вхождение, не попадающее в область действия одноименного квантора. Легко понять, что это определение можно переформулировать индуктивно:

  • любое вхождение переменной в терм или атомарную формулу свободно;
  • свободные вхождения переменной в формулу



    являются ее свободными вхождениями в формулу ;
  • свободные вхождения любой переменной в одну из формул

    и являются свободными вхождениями в , и ;
  • переменная не имеет свободных вхождений в формулы и ; свободные вхождения остальных переменных в являются свободными вхождениями в эти две формулы.


Сравнивая это определение с индуктивным определением параметров формулы, мы видим, что параметры — это переменные, имеющие свободные вхождения в формулу.



Вхождения переменной, не являющиеся свободными (в том числе стоящие рядом с квантором) называют связанными. Например, переменная имеет одно свободное и три связанных вхождения в формулу .

Теперь можно внести поправку в сказанное выше и считать, что аксиомами являются формулы где есть результат подстановки

вместо всех свободных вхождений переменной . Однако такой оговорки недостаточно, как показывает следующий пример.

Подставляя вместо в формулу , мы получаем (в полном согласии с нашей интуицией) формулу . Теперь рассмотрим формулу , которая отличается от лишь именем связанной переменной и должна иметь тот же смысл. Переменная в ней по- прежнему свободна, но подстановка вместо

дает формулу , в которой

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

93. Приведите пример формулы вида

в которой происходит коллизия переменных и которая не является общезначимой. (Ответ: .)

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

вместо переменной корректна, если в процессе текстуальной замены всех свободных вхождений переменной на терм никакая переменная из не попадает в область действия одноименного квантора.

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

Сначала определим индуктивно результат подстановки терма

вместо переменной в терм ; этот результат будем обозначать :

  • есть ; для любой переменной , отличной от , мы полагаем равным .
  • если есть - местный функциональный символ, а — термы, то



Теперь индуктивное определение продолжается для формул:

  • для атомарных формул: если есть -местный предикатный символ, а — термы, то

    и подстановка является корректной;
  • подстановка терма вместо переменной в формулу корректна, если она корректна для формулы , при этом



    ( квадратные скобки указывают порядок действий, не являясь частью формулы);
  • подстановка терма вместо переменной в формулу корректна, если она корректна для обеих формул и , при этом

    аналогично для формул и ;


  • наконец, подстановка вместо в формулу корректна в двух случаях:

    (1) если не является параметром формулы (это возможно, когда не является параметром или когда совпадает с ); при этом подстановка ничего не меняет в формуле;

    (2) переменная является параметром формулы , но переменная не входит в терм и подстановка корректна; при этом

    Аналогично определяется корректная подстановка в формулу .



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

После всех этих приготовлений мы можем сформулировать две оставшиеся схемы аксиом исчисления предикатов: формула

(12)

и двойственная ей формула

(13)

будут аксиомами исчисления предикатов, если указанные в них подстановки корректны.

Два частных случая, когда подстановка заведомо корректна: во-первых, можно безопасно подставлять константу (или любой терм без параметров), во-вторых, подстановка переменной вместо себя всегда корректна (и ничего не меняет в формуле).

Отсюда следует, что формулы

и будут аксиомами исчисления предикатов (для любой формулы и переменной ).

Нужны ли нам еще какие-нибудь аксиомы и правила вывода? Конечно, нужны, поскольку уже сформулированные аксиомы не полностью отражают смысл кванторов. (Например, они вполне согласуются с таким пониманием этого смысла: формула всегда ложна, а формула

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

Если переменная не является параметром формулы , то правила Бернайса разрешают такие переходы:


Мы говорим, что стоящая снизу от черты (в каждом из правил) формула получается по соответствующему правилу из верхней. Соответственно дополняется и определение вывода как последовательности формул, в которой каждая формула либо является аксиомой, либо получается из предыдущих по одному из правил вывода (раньше было только правило MP, теперь добавились два новых правила).

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

Используя первое правило Бернайса, легко установить допустимость правила обобщения (если в исчислении предикатов выводима формула сверху от черты, то выводима и формула снизу). В самом деле, возьмем какую-нибудь выводимую формулу без параметров (например, аксиому, в которой вместо , и

подставлены замкнутые формулы). Раз выводима формула , то выводима и формула (поскольку

является тавтологией и даже аксиомой). Теперь по правилу Бернайса выводим и применяем правило MP к этой формуле и к формуле .

Правило (Gen) (от Generalization — обобщение) кодифицирует стандартную практику рассуждений: мы доказываем какое-то утверждение со свободной переменной , после чего заключаем, что мы доказали , так как было произвольным.

Второе правило Бернайса также вполне естественно: желая доказать в предположении , мы говорим: пусть такое существует, возьмем его и докажем (то есть докажем

со свободной переменной ).

94. Покажите, что класс выводимых в исчислении предикатов формул не изменится, если мы вместо правил Бернайса добавим туда правило обобщения и две аксиомы и

(в которых требуется, чтобы переменная не была параметром формулы ).

Как и в случае исчисления высказываний, перед нами стоят две задачи: надо доказать корректность исчисления предикатов (всякая выводимая формула общезначима) и его полноту (всякая общезначимая формула выводима). Этим мы и займемся в следующих разделах.


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