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

Полнота исчисления предикатов


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

Фиксируем некоторую сигнатуру . Пусть — теория в сигнатуре , то есть произвольное множество замкнутых формул этой сигнатуры. Говорят, что теория противоречива, если в ней выводится некоторая формула и ее отрицание . В этом случае из выводится любая формула, так как имеется аксиома . Если теория не является противоречивой, то она называется непротиворечивой.

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

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

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

Теорема 45 (о корректности; переформулировка).

Любое совместное множество замкнутых формул непротиворечиво.

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

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

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


выводятся из .

Другими словами, теория полна, если из любых двух формул и (соответствующей сигнатуры) ровно одна является теоремой этой теории.

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

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

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

Теперь мы готовы к доказательству основного результата этого раздела.

Теорема 46 (полнота исчисления предикатов, сильная форма).

Любая непротиворечивая теория совместна.

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

Лемма 1. Для всякого непротиворечивого множества замкнутых формул сигнатуры

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

Доказательство повторяет рассуждение раздела "Второе доказательство теоремы о полноте": рассматривая по очереди замкнутые формулы, мы добавляем либо их, либо их отрицания в множество .



Это можно сделать без труда для конечной или счетной сигнатуры (тогда множество всех замкнутых формул этой сигнатуры счетно); для общего случая надо воспользоваться трансфинитной индукцией или леммой Цорна, как объяснялось в разделе "Второе доказательство теоремы о полноте". Лемма 1 доказана.

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

Предикаты на этом множестве определяем так: если — предикатный символ, а — замкнутые термы, то предикат, соответствующий символу , истинен на термах , если формула

выводима из .

Тем самым интерпретация полностью описана, и мы хотели бы доказать, что все формулы из в ней истинны. Мы будем доказывать по индукции такой факт: если , то формула

истинна в построенной интерпретации, а если , то формула ложна.

Однако без дополнительных предположений о множестве

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



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

Если множество полно и экзистенциально полно, то описанная выше конструкция с замкнутыми термами дает его модель. Прежде чем проверять это, покажем, как расширить до полного и экзистенциально полного множества. Ключевую роль здесь играет такая лемма:

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

(Замечание. Здесь и далее, говоря о непротиворечивости и выводимости, мы не уточняем, в какой сигнатуре строятся выводы: все наши сигнатуры будут отличаться лишь набором констант, и лемма о добавлении констант.)

Доказательство леммы 2. Пусть становится противоречивым после добавления формулы . Отсюда следует (используем подходящую пропозициональную тавтологию), что отрицание этой формулы выводится из , то есть выводима формула , где — конъюнкция конечного числа формул из . По лемме о свежих константах выводима формула (напомним, что не входит ни в , ни в ). Контрапозиция дает формулу , а правило Бернайса — формулу . По предположению формула выводима из , и множество оказывается противоречивым. Лемма 2 доказана.

100. Докажите такое усиление леммы 2: при добавлении в



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

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

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


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

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

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

Что меняется, если сигнатура несчетна? Тогда мы уже не можем рассматривать все экзистенциальные формулы по очереди, и надо обрабатывать их все сразу. При этом противоречие не появится: в самом деле, оно использовало бы лишь конечное число добавленных формул, а для конечного числа все уже доказано.

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

Лемма 3 доказана.

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

Лемма 4. Пусть — полное и экзистенциально полное множество замкнутых формул некоторой сигнатуры . Тогда существует интерпретация сигнатуры , в которой истинны все формулы из .



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

Как интерпретировать функциональные символы, понятно (это не зависит от множества ): если символ имеет валентность , то ему соответствует функция, которая отображает замкнутых термов в замкнутый терм . Константы (функциональные символы валентности ) интерпретируются сами собой.

Интерпретация предикатных символов такова. Пусть — предикатный символ валентности . Чтобы узнать, истинен ли соответствующий ему предикат на замкнутых термах , надо составить атомарную формулу и выяснить, что выводится из — сама эта формула или ее отрицание. (Здесь мы используем полноту.) В первом случае предикат будет истинным, во втором — ложным.

Индукцией по числу логических связок и кванторов в замкнутой формуле сигнатуры докажем такое утверждение: Для атомарных формул это верно по построению интерпретации .

Для пропозициональных связок рассуждение ничем не отличается от приведенного в разделе "Второе доказательства теоремы о полноте". Нам нужно проверить, что выводимость из подчиняется тем же правилам, что и истинность: Все эти свойства несложно доказать. Первое из них выражает полноту (и непротиворечивость — напомним, что по определению полная теория всегда непротиворечива) множества . Остальные свойства легко проверить, если иметь в виду, что все частные случаи пропозициональных тавтологий выводимы.

Пусть теперь формула имеет вид , где — формула с единственным параметром

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



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

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

Если формула не выводима из , то из выводится ее отрицание. Оно, как мы видели, доказуемо эквивалентно формуле . Поэтому в силу экзистенциальной полноты выводима формула для некоторой константы . Эта формула истинна, поэтому ложна при некотором значении переменной , так что формула ложна в .

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

Анализ доказательства позволяет сделать такое наблюдение:

Теорема 47. Непротиворечивое множество замкнутых формул конечной или счетной сигнатуры имеет счетную модель.

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

Аналогичное рассуждение с использованием свойств операций с мощностями (о которых можно прочесть в [6]) устанавливает такой факт:

Теорема 48. Всякое непротиворечивое множество формул сигнатуры

имеет модель мощности (где

обозначает счетную мощность, а — мощность сигнатуры).

Кстати, при доказательстве теорем 47 и 48 можно было бы сослаться на теорему Левенгейма-Сколема об элементарной подмодели (построить модель произвольной мощности, а потом уменьшить, если надо).



Возвратимся теперь к исходной формулировке теоремы о полноте.

Теорема 49 (полнота исчисления предикатов, слабая форма)

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

Пусть формула замкнута. Если она невыводима, то множество непротиворечиво и потому совместно. В его модели формула будет ложной, что противоречит предположению.

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

Как и в разделе "Второе доказательство теоремы о полноте", из теоремы о полноте можно вывести такое следствие:

Теорема 50. (компактность для исчисления предикатов).

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

В самом деле, по теореме о полноте (и корректности, если быть точным) наличие модели (совместность) равносильно непротиворечивости. А по определению противоречивость затрагивает лишь конечное число формул из .

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

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

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

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

Теорема 51.


Если , то .

Напротив, пусть не выводима из . Тогда теория непротиворечива и (в силу теоремы о полноте) имеет модель. Значит

не следует из .

102.Какими нужно взять и в этой теореме, чтобы получить приведенные ранее формулировки теоремы о полноте? (Ответ: при (тождественно ложная формула) получаем сильную форму теоремы о полноте, при — слабую.)


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