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



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


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

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

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

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

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

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

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

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

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


Содержание  Назад  Вперед