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

Полнота исчисления предикатов В этом разделе мы докажем, что всякая общезначимая формула выводима в исчислении  предикатов. Мы будем следовать схеме, использованной в разделе  "Второе доказательство теоремы о полноте", и введем понятия непротиворечивой и  полной теории. Фиксируем некоторую сигнатуру  есть произвольное множество замкнутых формул этой сигнатуры. Говорят, что теория  противоречива, если в ней выводится некоторая формула  этом случае из   выводится любая формула, так как   — теория в сигнатуре   и ее отрицание  . Пусть  , то  . В    имеется аксиома  она называется непротиворечивой. . Если теория   не является противоречивой, то  99. Докажите, что теория противоречива тогда и только тогда, когда в ней выводится  формула   — произвольная формула сигнатуры).  (здесь  Непосредственно из определения следует, что  всякое подмножество непротиворечивого множества непротиворечиво. Кроме того,  еслибесконечное множество противоречиво, то некоторое его  конечное подмножество тоже противоречиво (поскольку в выводе участвует лишь  конечное число формул). Синтаксическое понятие непротиворечивости мы будем сравнивать с семантическим  понятием совместности. Пусть имеется некотораяинтерпретация  .   истинны в  Напомним, что она называется моделью теории  . Множество   называется совместным, если оно имеет модель, то есть если все его  формулы истинны в некоторой интерпретации. , если все формулы из   сигнатуры  Теорема 45 (о корректности; переформулировка). Любое совместное множество  замкнутых формул непротиворечиво.  истинны в некоторой интерпретации  Пусть все формулы из  что  самом деле, в этом случае теорема 44 показывает, что формулы  одновременно истинны в   для некоторой замкнутой формулы  , что, очевидно, невозможно.  и  . Может ли оказаться,  ? Легко понять, что нет. В   и  должны быть  Для доказательства обратного утверждения (о совместности непротиворечивой теории)  нам понадобится понятие полной теории.Непротиворечивое множество  называется полным в этой сигнатуре, если для любой замкнутой формулы  сигнатуры либо формула  , состоящее из замкнутых формул сигнатуры  , либо ее отрицание   выводятся из  . ,   этой  Другими словами, теория полна, если из любых двух формул  (соответствующей сигнатуры) ровно одна является теоремой этой теории.  и    Полное множество можно получить, взяв какую­либо интерпретацию и рассмотрев все  замкутые формулы, истинные в этой интерпретации. (Впоследствии мы увидим, что  любое полное множество может быть получено таким способом — это легко следует из  теоремы 46.) В определении полноты существенно, что мы ограничиваемся замкнутыми формулами  той же сигнатуры. Например, если мы возьмем одноместный предикатный символ  входящий в   про него ничего не утверждают, и потому, скажем, ни  , то формулы из  , не формула  важна. Например, множество всех истинных в натуральном ряду формул  , ни ее отрицание не выводимы из  . Замкнутость формулы   тоже  сигнатуры  выводятся, иначе по правилу обобщения мы получили бы ложную в   полно, но ни формула  , ни формула   из него не    формулу   или  . Полное множество подобно мировоззрению человека, достигшего предела умственного  развития: на все, что входит в круг его понятий (выражается формулой сигнатуры   ),  он имеет точку зрения. Но это не относится ни к формулам большей сигнатуры  (содержащим новые для него понятия), ни к формулам с параметрами (поскольку  значения параметров не фиксированы). Теперь мы готовы к доказательству основного результата этого раздела. Теорема 46 (полнота исчисления предикатов, сильная форма). Любая  непротиворечивая теория совместна. Напомним, как мы доказывали аналогичное утверждение для высказываний. Мы  расширяли наше непротиворечивое множество  полагали пропозициональную переменную  недостаточно, как мы увидим (например, непонятно, откуда брать носитель искомой  модели). Но начало рассуждения будет таким же.  до полного множества   истинной, если  . Здесь этого будет  , а потомЛемма 1. Для всякого непротиворечивого множества  сигнатуры  той же сигнатуры, содержащее   существует полное непротиворечивое множество  .  замкнутых формул   замкнутых формул  Доказательство повторяет рассуждение раздела "Второе доказательство теоремы о  полноте": рассматривая по очереди замкнутые формулы, мы добавляем либо их, либо их  отрицания в множество  . Это можно сделать без труда для конечной или счетной сигнатуры (тогда множество  всех замкнутых формул этой сигнатуры счетно); для общего случая надо  воспользоваться трансфинитной индукцией или леммой Цорна, как объяснялось в  разделе "Второедоказательство теоремы о полноте". Лемма 1 доказана. Как же нам теперь построить модель полного множества  ? Прежде всего надо  решить, что будет носителем этой модели. Заметим, что в сигнатуре могут быть  некоторые константы (функциональные символы валентности   ). Им должны  соответствовать некоторые элементы носителя. Кроме того, замкнутым термам (которые не содержат никаких переменных, только константы) также должны соответствовать  элементы носителя. Попробуем взять в качестве носителя как раз множество   всех  замкнутых термов нашей сигнатуры. При этом понятно, как надо определять  сигнатурные функции на этом множестве: функция, соответствующая символу  валентности  (Это определение никак не зависит от  , отображает замкнутые термы  .)  в терм  .   — предикатный символ,  Предикаты на этом множестве определяем так: если  а   — замкнутые термы, то предикат, соответствующий символу  , истинен  на термах  , если формула   выводима из  . Тем самым интерпретация полностью описана, и мы хотели бы доказать, что все  формулы из  если  формула   в ней истинны. Мы будем доказыватьпо индукции такой факт:   истинна в построенной интерпретации, а если  , то формула  ложна. , то  Однако без дополнительных предположений о множестве   этот план обречен на  неудачу, поскольку замкнутых термов может быть совсем мало (или даже вовсе не  быть), в то время как соответствующая теория не имеет конечных моделей. Если начать  индуктивное рассуждение, то выяснится, что трудность возникает в случае, когда  формула   начинается с квантора. Например, может оказаться, что формулавыводима из множества  , в то время как ни для какого замкнутого терма     не выводима из  формула  нами модели (хотя выводимой). Чтобы преодолеть эту трудность, мы наложим  дополнительные требования на множество  . Тогда формула  .  будет ложной в описанной  Назовем теорию (множество замкнутых формул сигнатуры  в сигнатуре  , если для всякой замкнутой формулы   ) экзистенциально полной   сигнатуры  , выводимой  из  , найдется замкнутый терм   этой сигнатуры, для которого  .  полно и экзистенциально полно, то описанная выше конструкция с  Если множество  замкнутыми термами дает его модель. Прежде чем проверять это, покажем, как  расширить  играет такая лемма:  до полного и экзистенциально полного множества. Ключевую роль здесь