Верещагин Н.К., Шень А. - Языки и исчисления (1076783), страница 33

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 33)

(Впоследствии мы увидим, что любое полное множествоможет быть получено таким способом — это легко следует из теоремы 46.)В определении полноты существенно, что мы ограничиваемся замкнутыми формулами той же сигнатуры. Например, если мы возьмём одноместный предикатный символ S, не входящий в Γ, то формулы из Γ про него ничего не утверждают, и потому, скажем, ниформула ∀x S(x), ни её отрицание не выводимы из Γ. Замкнутостьформулы ϕ тоже важна. Например, множество всех истинных в натуральном ряду формул сигнатуры (=, <) полно, но ни формулаx = y, ни формула x 6= y из него не выводятся, иначе по правилу обобщения мы получили бы ложную в N формулу ∀x∀y (x = y)или ∀x∀y (x 6= y).Полное множество подобно мировоззрению человека, достигшегопредела умственного развития: на всё, что входит в круг его понятий(выражается формулой сигнатуры σ), он имеет точку зрения.

Ноэто не относится ни к формулам большей сигнатуры (содержащимновые для него понятия), ни к формулам с параметрами (посколькузначения параметров не фиксированы).Теперь мы готовы к доказательству основного результата этогораздела.Теорема 46 (полнота исчисления предикатов, сильная форма). Всякая непротиворечивая теория совместна. Напомним, как мы доказывали аналогичное утверждение для148Исчисление предикатов[гл. 4]высказываний. Мы расширяли наше непротиворечивое множество Γдо полного множества Γ0 , а потом полагали пропозициональную переменную p истинной, если Γ0 ` p.

Здесь этого будет недостаточно,как мы увидим (например, непонятно, откуда брать носитель искомой модели). Но начало рассуждения будет таким же.Лемма 1. Для всякого непротиворечивого множества Γ замкнутых формул сигнатуры σ существует полное непротиворечивое множество Γ0 замкнутых формул той же сигнатуры, содержащее Γ.Доказательство повторяет рассуждение раздела 2.2: рассматривая по очереди замкнутые формулы, мы добавляем либо их, либо ихотрицания в множество Γ.Это можно сделать без труда для конечной или счётной сигнатуры (тогда множество всех замкнутых формул этой сигнатуры счётно); для общего случая надо воспользоваться трансфинитной индукцией или леммой Цорна, как объяснялось в разделе 2.2.

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

Попробуем взять в качественосителя как раз множество T всех замкнутых термов нашей сигнатуры. При этом понятно, как надо определять сигнатурные функциина этом множестве: функция, соответствующая символу f валентности k, отображает замкнутые термы t1 , . . . , tk в терм f (t1 , . . . , tk ).(Это определение никак не зависит от Γ.)Предикаты на этом множестве определяем так: если A — предикатный символ, а t1 , . . .

, tn — замкнутые термы, то предикат, соответствующий символу A, истинен на термах t1 , . . . , tn , если формулаA(t1 , . . . , tn ) выводима из Γ.Тем самым интерпретация полностью описана, и мы хотели быдоказать, что все формулы из Γ в ней истинны. Мы будем доказывать по индукции такой факт: если Γ ` ϕ, то формула ϕ истинна впостроенной интерпретации, а если Γ ` ¬ϕ, то формула ϕ ложна.Однако без дополнительных предположений о множестве Γ этотплан обречён на неудачу, поскольку замкнутых термов может бытьсовсем мало (или даже вовсе не быть), в то время как соответствующая теория не имеет конечных моделей. Если начать индуктивное[п.

5]Полнота исчисления предикатов149рассуждение, то выяснится, что трудность возникает в случае, когда формула ϕ начинается с квантора. Например, может оказаться,что формула ∃x A(x) выводима из множества Γ, в то время как нидля какого замкнутого терма t формула A(t) не выводима из Γ.

Тогда формула ∃x A(x) будет ложной в описанной нами модели (хотявыводимой). Чтобы преодолеть эту трудность, мы наложим дополнительные требования на множество Γ.Назовём теорию (множество замкнутых формул сигнатуры σ) экзистенциально полной в сигнатуре σ, если для всякой замкнутойформулы ∃ξ ϕ сигнатуры σ, выводимой из Γ, найдётся замкнутыйтерм t этой сигнатуры, для которого Γ ` ϕ(t/ξ).Если множество Γ полно и экзистенциально полно, то описаннаявыше конструкция с замкнутыми термами даёт его модель. Преждечем проверять это, покажем, как расширить Γ до полного и экзистенциально полного множества.

Ключевую роль здесь играет такаялемма:Лемма 2. Пусть Γ — непротиворечивое множество замкнутыхформул, из которого выводится замкнутая формула ∃ξ ϕ. Пусть c —константа, не встречающаяся ни в Γ, ни в ϕ. Тогда множество Γостанется непротиворечивым после добавления формулы ϕ(c/ξ).(Замечание. Здесь и далее, говоря о непротиворечивости и выводимости, мы не уточняем, в какой сигнатуре строятся выводы: всенаши сигнатуры будут отличаться лишь набором констант, и леммао добавлении констант на с. 145 даёт нам такое право.)Доказательство леммы 2. Пусть Γ становится противоречивымпосле добавления формулы ϕ(c/ξ).

Отсюда следует (используем подходящую пропозициональную тавтологию), что отрицание этой формулы выводится из Γ, то есть выводима формула γ → ¬ϕ(c/ξ), гдеγ — конъюнкция конечного числа формул из Γ. По лемме о свежихконстантах (с. 144) выводима формула γ → ¬ϕ (напомним, что c невходит ни в ϕ, ни в γ). Контрапозиция даёт формулу ϕ → ¬γ, а правило Бернайса — формулу ∃ξ ϕ → ¬γ. По предположению формула∃ξ ϕ выводима из Γ, и множество Γ оказывается противоречивым.Лемма 2 доказана.100. Докажите такое усиление леммы 2: при добавлении в ` формулыϕ(c/ξ) (в предположениях леммы) множество выводимых из ` формулисходной сигнатуры (без константы c) не меняется.Лемма 3.

Пусть Γ — непротиворечивое множество замкнутыхформул сигнатуры σ. Тогда существует расширение сигнатуры σновыми константами и непротиворечивое, полное и экзистенциально150Исчисление предикатов[гл. 4]полное (в расширенной сигнатуре) множество Γ0 замкнутых формул,содержащее Γ.Доказательство. Пусть сигнатура конечна или счётна. Тогда замкнутых формул вида ∃ξ ϕ, выводимых из Γ, не более чем счётноечисло. К каждой из них по очереди будем применять лемму 2, вводяновую константу.

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

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

При этом противоречие не появится: всамом деле, оно использовало бы лишь конечное число добавленныхформул, а для конечного числа всё уже доказано.После этого доказательство проходит как раньше (мы по-прежнему делаем счётное число чередующихся пополнений множества ирасширений сигнатуры).Лемма 3 доказана.Последним шагом в доказательстве теоремы о полноте (всякоенепротиворечивое множество замкнутых формул совместно) является такая лемма:Лемма 4. Пусть Γ — полное и экзистенциально полное множествозамкнутых формул некоторой сигнатуры σ. Тогда существует интер-[п.

5]Полнота исчисления предикатов151претация M сигнатуры σ, в которой истинны все формулы из Γ.Мы уже говорили, как надо строить такую интерпретацию. Повторим это более подробно. Рассмотрим все замкнутые термы сигнатуры σ, то есть термы, не содержащие переменных, а только функциональные символы и константы. (Такие термы существуют, поскольку теория Γ экзистенциально полна.) Это множество будет носителем интерпретации.Как интерпретировать функциональные символы, понятно (этоне зависит от множества Γ): если символ f имеет валентность n, тоему соответствует функция, которая отображает n замкнутых термов t1 , . . .

, tn в замкнутый терм f (t1 , . . . , tn ). Константы (функциональные символы валентности 0) интерпретируются сами собой.Интерпретация предикатных символов такова. Пусть A — предикатный символ валентности n. Чтобы узнать, истинен ли соответствующий ему предикат на замкнутых термах t1 , . . .

, tn , надо составить атомарную формулу A(t1 , . . . , tn ) и выяснить, что выводитсяиз Γ — сама эта формула или её отрицание. (Здесь мы используемполноту.) В первом случае предикат будет истинным, во втором —ложным.Индукцией по числу логических связок и кванторов в замкнутойформуле ϕ сигнатуры σ докажем такое утверждение:Γ ` ϕ ⇔ ϕ истинна в M .Для атомарных формул это верно по построению интерпретации M .Для пропозициональных связок рассуждение ничем не отличается от приведённого в разделе 2.2. Нам нужно проверить, что выводимость из Γ подчиняется тем же правилам, что и истинность:Γ ` ¬A ⇔ Γ 6` A,Γ ` A ∧ B ⇔ Γ ` A и Γ ` B,Γ ` A ∨ B ⇔ Γ ` A или Γ ` B,Γ ` A → B ⇔ Γ 6` A или Γ ` B.Все эти свойства несложно доказать. Первое из них выражает полноту (и непротиворечивость — напомним, что по определению полнаятеория всегда непротиворечива) множества Γ. Остальные свойствалегко проверить, если иметь в виду, что все частные случаи пропозициональных тавтологий выводимы.Пусть теперь формула ϕ имеет вид ∃ξ ψ, где ψ — формула с единственным параметром ξ (или без параметров).

Предположим, что152Исчисление предикатов[гл. 4]она выводима из Γ. Тогда в силу экзистенциальной полноты найдётся константа c, для которой Γ ` ψ(c/ξ). Формула ψ(c/ξ) имеетменьшее число логических связок, поэтому к ней можно применитьпредположение индукции и заключить, что она истинна в M . Тогда формула ψ истинна на оценке ξ 7→ c (см. лемму 2 на с.

Характеристики

Список файлов книги