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

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

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

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

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

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

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

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

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

Лекция "Метакомпьютеры" также может быть Вам полезна.

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

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

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

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

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

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

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