Верещагин Н.К., Шень А. - Языки и исчисления (1076783), страница 34
Текст из файла (страница 34)
137 изамечание после неё), поэтому формула ∃ξ ψ истинна в M .Напротив, пусть формула ∃ξ ψ истинна в M . Тогда (по определению истинности) найдётся элемент (замкнутый терм) t, для которогоψ истинна на оценке ξ 7→ t и потому формула ψ(t/ξ) истинна в M . Попредположению индукции формула ψ(t/ξ) выводима из Γ. Осталосьвоспользоваться тем, что формула ψ(t/ξ) → ∃ξ ψ является аксиомой(напомним, подстановка замкнутого терма всегда корректна).Наконец, рассмотрим случай, когда формула ϕ имеет вид ∀ξ ψ.Пусть она выводима из Γ. Формула ∀ξ ψ → ψ(t/ξ) является аксиомойдля любого замкнутого терма t. Поэтому и формула ψ(t/ξ) выводимаиз Γ.
В ней меньше логических связок, чем в ϕ, поэтому по предположению индукции она истинна в M . Значит, формула ψ истинна налюбой оценке ξ 7→ t, и потому формула ∀ξ ψ истинна в M .Если формула ∀ξ ψ не выводима из Γ, то из Γ выводится её отрицание, которое (как мы видели) доказуемо эквивалентно формуле∃ξ ¬ψ. Поэтому в силу экзистенциальной полноты выводима формула ¬ψ(c/ξ) для некоторой константы c. Эта формула истинна, поэтому ψ ложна при некотором значении переменной ξ, так что формула∀ξ ψ ложна в M .Таким образом, мы доказали, что всякое непротиворечивое множество замкнутых формул имеет модель (расширив его до полногои экзистенциально полного множества, у которого есть модель иззамкнутых термов). Анализ доказательства позволяет сделать такое наблюдение:Теорема 47.
Непротиворечивое множество замкнутых формул конечной или счётной сигнатуры имеет счётную модель. В самом деле, элементами построенной нами модели являютсязамкнутые термы, образованные из добавленных констант и функциональных символов сигнатуры. На каждом шаге добавляется счётное множество констант, поэтому всех констант счётное число, значит, и термов счётное число. Аналогичное рассуждение с использованием свойств операций смощностями (о которых можно прочесть в [6]) устанавливает такойфакт:Теорема 48. Всякое непротиворечивое множество формул сигна-[п. 5]Полнота исчисления предикатов153туры σ имеет модель мощности max(ℵ0 , |σ|) (где ℵ0 обозначает счётную мощность, а |σ| — мощность сигнатуры).Кстати, при доказательстве теорем 47 и 48 можно было бы сослаться на теорему Левенгейма – Сколема об элементарной подмодели (построить модель произвольной мощности, а потом уменьшить,если надо).Вернёмся теперь к исходной формулировке теоремы о полноте.Теорема 49 (полнота исчисления предикатов, слабая форма).
Всякая общезначимая формула выводима в исчислении предикатов. Пусть формула ϕ замкнута. Если она невыводима, то множество {¬ϕ} непротиворечиво и потому совместно. В его модели формула ϕ будет ложной, что противоречит предположению.Для незамкнутых формул общезначимость и выводимость равносильны общезначимости и выводимости их замыкания.
Как и в разделе 2.2, из теоремы о полноте можно вывести такоеследствие:Теорема 50 (компактность для исчисления предикатов). Пусть Γ —множество замкнутых формул некоторой сигнатуры, и любое егоконечное подмножество имеет модель. Тогда и само множество Γимеет модель. В самом деле, по теореме о полноте (и корректности, если бытьточным) наличие модели (совместность) равносильно непротиворечивости. А по определению противоречивость затрагивает лишь конечное число формул из Γ.
101. Покажите, что теорема о полноте в сильной форме является следствием теоремы компактности и теоремы о полноте в слабой форме. (Указание: если множество ` не имеет модели, то его конечная часть не имеетмодели, поэтому формула h . . . i общезначима, поэтому . . . )Прямое доказательство теоремы компактности без использования понятия выводимости мы дадим в следующей главе (раздел 5.6).Ещё один важный результат, вытекающий из теоремы о полноте — совпадение синтаксического понятия выводимости и семантического понятия следования. Пусть дана некоторая сигнатура σ. Рассмотрим множество Γ замкнутых формул этой сигнатуры (такиемножества мы называем теориями в сигнатуре σ) и ещё одну замкнутую формулу ϕ.
Говорят, что ϕ семантически следует из Γ,если ϕ истинна во всякой модели теории Γ, то есть во всякой интерпретации сигнатуры σ, где истинны все формулы из Γ. (Обозначение:Γ ϕ.)154Исчисление предикатов[гл. 4]Теорема 51.Γ ` ϕ ⇔ Γ ϕ. Если Γ ` ϕ, то Γ ϕ (как мы видели в теореме 44 на с. 144).Напротив, пусть ϕ не выводима из Γ. Тогда теория Γ∪{¬ϕ} непротиворечива и (в силу теоремы о полноте) имеет модель. Значит ϕ неследует из Γ. 102. Какими нужно взять ϕ и ` в этой теореме, чтобы получить приведённые ранее формулировки теоремы о полноте? (Ответ: при ϕ =⊥ (тождественно ложная формула) получаем сильную форму теоремы о полноте,при ` = ∅ — слабую.)4.6.
Переименование переменныхВ этом разделе мы попытаемся аккуратно разобраться с простымвопросом о том, почему и как можно переименовывать связанные переменные, не меняя смысла формул. Мы уже видели, что формулы∀x A(x) и ∀y A(y) доказуемо эквивалентны (с. 140), то есть их эквивалентность доказуема в исчислении предикатов. Сейчас мы хотимдоказать общее утверждение об этом.Корректная формулировка утверждения о переименовании переменных требует осторожности. Например, нельзя сказать, что формула ∀ξ ϕ всегда эквивалентна ∀η ϕ(η/ξ).
Прежде всего, подстановкаможет быть некорректной, как в случае формул∀ξ∀η B(ξ, η) и∀η∀η B(η, η)(легко понять, что эти формулы не эквивалентны). Но даже еслиподстановка корректна, формулы могут не быть эквивалентными,как в случае формул∀ξ B(ξ, η) и∀η B(η, η).Как же сформулировать утверждение правильно?Нагляднее всего, видимо, сделать так.
Давайте заключим в рамкувсе связанные вхождения всех переменных (в том числе вхожденияпосле кванторов). После этого соединим линиями переменную послеквантора и все её вхождения, связанные именно этим вхождениемквантора. Свободные вхождения переменных остаются при этом безрамок. Получится что-то вроде∀ x (∃ z B( x , z ) ∧ C( x )) ∧ D(x, y, z).[п. 6]Переименование переменных155Если теперь стереть переменные внутри рамок, останется схема формулы, которая содержит всю существенную информацию о ней.
Будем называть две формулы подобными (отличающимися лишь именами связанных переменных), если они имеют одну и ту же схему.Теорема 52 (о переименовании связанных переменных). Подобныеформулы доказуемо эквивалентны. Докажем две простые леммы.Лемма 1. Если формула ϕ не содержит переменной η (ни связанно, ни свободно), то формулы∀ξ ϕи∀η ϕ(η/ξ)доказуемо эквивалентны.Доказательство.
В самом деле, подстановка корректна, так какв ϕ нет кванторов по η. Поэтому выводима формула∀ξ ϕ → ϕ(η/ξ).Левая часть её не содержит переменной η, поэтому по правилу Бернайса можно вывести∀ξ ϕ → ∀η ϕ(η/ξ).В обратную сторону: подстановка ξ вместо η в формулу ϕ(η/ξ)корректна (поскольку η была подставлена вместо свободных вхождений ξ, при обратной подстановке переменная ξ не попадёт в областьдействия кванторов по ней) и даёт формулу ϕ.
Поэтому формула∀η ϕ(η/ξ) → ϕ(η/ξ)(ξ/η)или, что то же самое,∀η ϕ(η/ξ) → ϕявляется аксиомой. Осталось применить правило Бернайса, заметив,что в левую часть переменная ξ свободно не входит (все свободныевхождения были заменены на η). Лемма 1 доказана.Аналогичное утверждение для квантора существования доказывается точно так же.Лемма 2. Замена подформулы на доказуемо эквивалентную даётдоказуемо эквивалентную формулу.Доказательство. Как мы видели на с. 140, доказуемая эквивалентность сохраняется после навешивания квантора: если α ' α0 ,156Исчисление предикатов[гл.
4]то ∀ξ α ' ∀ξ α0 и ∃ξ α ' ∃ξ α0 (символ ' здесь обозначает доказуемую эквивалентность). Кроме того, из α ' α0 и β ' β 0 следует,что (α ∧ β) ' (α0 ∧ β 0 ), (α ∨ β) ' (α0 ∨ β 0 ), (α → β) ' (α0 → β 0 ) и¬α ' ¬α0 . (В этом легко убедиться, написав подходящие пропозициональные тавтологии.)Теперь утверждение леммы легко доказать индукцией (начав сзаменённой подформулы и рассматривая всё более длинные частиформулы). Лемма 2 доказана.Леммы 1 и 2 позволяют нам заменять переменные внутри рамоксхемы на новые (ранее не использованные) переменные, получая доказуемо эквивалентную и подобную исходной формулу.
Такими заменами можно из двух подобных формул получить третью, используя для замены одни и те же переменные. При этом обе исходныеформулы доказуемо эквивалентны третьей, а значит, и друг другу.(Использование третьей формулы существенно: нельзя преобразовать первую формулу сразу во вторую, так как при замене переменных в рамках может не выполняться условие леммы 1.) Аккуратное обращение со связанными и свободными переменными — традиционная головная боль авторов учебников по логике.Наиболее радикальный подход — вообще изгнать связанные переменные, заменив их квадратиками со связями между ними.
Тогдапри подстановке можно ни о чём не заботиться. Зато формулы перестают быть последовательностями символов, а становятся объектамисо сложной структурой. (Этот подход использован в книге БурбакиТеория множеств [3].)Менее радикальный вариант состоит в том, чтобы разделить переменные на два типа — свободные и связанные. Так делается, например, в классической книге Гильберта и Бернайса Основания математики [8]. Тогда можно смело подставлять терм вместо свободной переменной, зато при навешивании квантора надо заменять свободную переменную на связанную.Ещё один вариант — договориться, что при подстановке термавместо свободной переменных автоматически происходит переименование связанных переменных, создающих коллизии.Всё это, конечно, мелочи — но досадные, особенно если стремиться к краткости, ясности и наглядности. Следы мучительных раздумий на подобные темы видны в примечании на с. 101 – 102 книгиКлини Математическая логика [16]: «Гильберт и Бернайс h .
. . i идругие авторы используют для обозначения свободных и связанныхпеременных разные буквы h . . . i Мы следовали этому правилу в те-[п. 7]Предварённая нормальная форма157чение десятилетия h . . . i Сейчас же мы твёрдо убеждены, что использование единого списка переменных для свободных и замкнутыхвхождений даёт небольшое, но чувствительное преимущество».С этим связан и другой выбор: как определять истинность формул. Тут есть две возможности: можно определять истинность формулы на оценке (при данных значениях параметров), а можно говорить только о замкнутых формулах, вводя константы для всех элементов интерпретации.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
