В.Б. Шехтман - Курс лекций по логике и теории алгоритмов (1161807), страница 7
Текст из файла (страница 7)
Вновь применим теорему дедукции:⊢ r1 & . . . & rk → ¬α.Вспомним, что α = ∃ x n ϕn (xn ) → ϕn (dn ) и применим предыдущую лемму:⊢ r1 & . . . & rk → ¬( ∃ x n ϕn (xn ) → ϕn (dn )) ⇒⊢ r1 & . . . & rk → ¬( ∃ x n ϕn (xn ) → ϕn (x)),то естьTn ⊢ ¬( ∃ x n ϕn (xn ) → ϕn (x)).Осталось понять, почему это невозможно. Нам известно, что¬(α → β) → α & ¬β.В нашем случае это означает следующее:Tn ⊢ ∃ x ϕ(x) & ¬ϕ(x).Воспользуемся правилом обобщения:Tn ⊢ ∀ x ( ∃ x ϕ(x) & ¬ϕ(x)).Теперь остаётся «раскрыть скобки». С одной стороны, получимTn ⊢ ∃ x ϕ(x),20так как∀ x ( ∃ x ϕ(x) & ¬ϕ(x)) → ∀ x ∃ x ϕ(x),∀ x ∃ x ϕ(x) → ∃ x ϕ(x),а с другой стороны, пользуясь тем, что ∀ x ¬ϕ(x) → ¬ ∃ x ϕ(x), имеемTn ⊢ ¬ ∃ x ϕ(x).Это не согласуется с непротиворечивостью теории Tn , а значит, наше предположении о противоречивости Tn+1было ошибочным.
Таким образом, все теории Tn будут непротиворечивы, а значит, непротиворечивой теориейбудет и их объединение:[T ′ :=Tn .nПо построению, эта теория будет содержать исходную и являться теорией Хенкина, что и требовалось. Лемма 2.25. Пусть T — непротиворечивая теория в «счётной» (то есть не более чем счётной) сигнатуреΩ.
Тогда существует такая сигнатураΩ′ = Ω ∪ {cn |n ∈ N},и полная непротиворечивая теория Хенкина S в ней, что S ⊆ T ′ . Достаточно применить предыдущую лемму и лемму Линденбаума. 2.3. Существование модели2.3.1. Случай теории без равенстваЛемма 2.26. Пусть T — непротиворечивая, полная, экзистенциально полная теория без равенства в неболее чем счётной сигнатуре Ω. Тогда теория T имеет счётную модель.
Рассмотрим множество D всех замкнутых термов сигнатуры Ω (ясно, что оно не пусто, раз уж у наснашлась экзистенциально полная теория, и не более чем счётно). Определим на это множестве модель:M = (D, I).Константы и функциональные символы I будет отображать в себя, а предикатные символы интерпретироватьтак:(1, T ⊢ P (t1 , . . .
, tn )MP (t1 , . . . , tn ) :=0, иначе.Покажем, что в такой интерпретации для любого терма имеем tM = t. Проведём индукцию по числу функциональных символов, входящих в терм. Если их нет (база индукции), требование, очевидно, выполнено. Пустьтеперь t = f (t1 , . . . , tk ), тогда по предположению индукцииMtM = f M (tM1 , . . . , tk ) = f (t1 , . . . , tk ) = t,что и требовалось.Теперь осталось убедиться, что для любой замкнутой формулы ϕM ϕ ⇔ T ⊢ ϕ.Как обычно, используем индукцию, на этот раз — по числу логических связок, входящих в ϕ.
Если их нет(атомарная формула), утверждение следует из определения оценки для предикатных символов. Для формулвида ϕ & ψ, ϕ ∨ ψ и т. п. проверка тривиальна. Рассмотрим несколько более сложный случай формулы ϕ =∃ x ψ(x). В силу экзистенциальной полноты M ∃ x ψ(x) тогда и только тогда, когда существует замкнутыйтерм t, такой что M ψ(t), а по предположению индукции это возможно лишь в том случае, если T ⊢ ψ(t).Это доказывает шаг индукции, а вместе с ним и всю лемму, так как теперь уже ясно, что построенная модельявляется требуемой.
Теорема 2.27 (о существовании модели). Пусть T — непротиворечивая теория без равенства в неболее чем счётной сигнатуре Ω. Тогда теория T имеет счётную модель. Непротиворечивые теории мы умеем вкладывать в полные теории Хенкина, для которых можно применить только что доказанную лемму.
Теорема 2.28 (Гёделя о полноте). ϕ ⇒⊢PCΩ ϕ. Ясно, что формулу ϕ можно считать замкнутой. Пусть 6⊢ ϕ. Тогда теория {¬ϕ} непротиворечива, азначит, у неё существует счётная модель: M ¬ϕ. Следовательно, 6 ϕ, что и требовалось доказать. Следствие 2.1 (теорема Лёвенгейма – Сколема). Если теория 1го порядка без равенства имеет модель, то она имеет счётную модель.212.3.2. Случай теории с равенствомПример 3.1.
Рассмотрим теорию с равенством из одной формулы:∀ x ∀ y x = y.Ясно, что модель этой теории не может состоять из более чем одного элемента. Этот пример показывает, чтодля теорий с равенством существование (нормальной) счётной модели не является обязательным.Теорема 2.29. Пусть T — непротиворечивая теория с равенством в не более чем счётной сигнатуре Ω.Тогда теория T имеет не более чем счётную модель. Положим T = = T ∪ {аксиомы равенства 16 – 20}. У этой теории существует счётная модель M = (M, I),однако она не обязательно нормальна. Введём на этой модели отношение эквивалентности:a ∼ b := M a = b.Утверждение 2.30.
Такое определение отношения эквивалентности является корректным. Все необходимые свойства следуют из аксиом равенства 16 – 18. Утверждение 2.31. Пустьai ∼ b i ,i = 1, . . . , n.Тогдаf M (a1 , . . . , an ) = f M (b1 , . . . , bn ).Достаточно воспользоваться аксиомой 19. Утверждение 2.32. Пустьai ∼ b i ,i = 1, . . . , n.ТогдаP M (a1 , . . . , an ) = P M (b1 , .
. . , bn ). Достаточно воспользоваться аксиомой 20. f возьмём фактор прежнего носителя по построенномуИтак, в качестве предметной области новой модели Mfвыше отношению эквивалентности: M := M/ ∼. Элементами этого носителя являются классы эквивалентностиe А именно, положимea элементов из M . Теперь определим новую интерпретирующую функцию I. fMfMc := cfM (a , . .
. , a )f M (ea1 , . . . , ean ) := fg1n MfMP (ea1 , . . . , ean ) := P (a1 , . . . , an ).Такая модель будет нормальна по построению. Нужно, однако, ещё доказать, что это действительно модельтеории T .Замечание наборщика. В дальнейшем для класса эквивалентности будет также использоваться обозначение ∼ [·].Утверждение 2.33. Пусть t ∈ TmΩ и FV(t) ⊆ {x1 , . . . , xn }. Тогда ∼ [|t(a1 , . . . , an )|M ] = |t(ea1 , . . . , ean )|Mf. Доказываем индукцией по числу функциональных символов в терме t. База (когда их нет) — очевидна(в этом случае терм — это переменная либо константа). Докажем шаг:∼ [|t(a1 , .
. . , an )|M ] =∼ [|f (r1 (a1 , . . . , an ), . . . , rm (a1 , . . . , am ))|M ] = |f (r1 (ea1 , . . . , ean ), . . . , rn (ea1 , . . . , ean ))|Mf =ffM= f M (|r1 (ea1 , . . . , ean )|Ma1 , . . . , ean )|Mf, . . . , |rn (ef) = f (∼ [|r1 (a1 , . . . , an )|M ], . . . , ∼ [|rn (a1 , . . . , an )|M ]) ==∼ [f M (|r1 (a1 , . . . , an )|M , . . . , |rn (a1 , . . . , an )|M )].Лемма 2.34. Пусть ϕ ∈ FmΩ и FV(ϕ) ⊆ {x1 , . .
. , xn }. Тогдаf ϕ(eM ϕ(a1 , . . . , an ) ⇔ Ma1 , . . . , ean ). В который раз — индукция по длине формулы. База — предикатный символ, он же атомарная формула,выполняется по определению. Проверим шаг. Пусть, к примеру, ϕ = ϕ1 & ϕ2 . ТогдаM ϕ ⇔ M ϕ1 и M ϕ2 ,22а для каждой из них выполнено предположение индукции.
Случаи дизъюнкции, импликации и отрицания проверяются аналогично. Остановимся отдельно на случае с квантором. Пусть ϕ(a1 , . . . , an ) = ∃ y ψ(y, a1 , . . . , an ).Истинность этой формулы в модели M означает, что в этой модели найдётся элемент носителя b, такой чтоf ψ(eb, eM ψ(b, a1 , . . . , an ). Применяя предположение индукции, получим Ma1 , . . . , ean ), откуда следует, чтоfM ϕ(ea1 , . . .
, ean ). Тем самым лемма доказана. f T . Это завершает доказательство теоремы. Таким образом, мы показали, что M T = ⇒ MТеперь точно так же, как в случае теорий без равенства, можно доказать следующую теорему.Теорема 2.35 (Гёделя о полноте для исчисления предикатов с равенством). ϕ ⇒⊢PC=ϕ.ΩСледствие 2.2 (теорема Лёвенгейма – Сколема). Если теория 1го порядка с равенством выполнима,то она имеет не более чем счётную нормальную модель.Теорема 2.36 (компактности Гёделя – Мальцева). Если всякое конечное подмножество теории T выполнимо, то теория T имеет модель. Предположим обратное. Это означает, что теория T противоречива. Однако, в доказательстве её противоречивости будет присутствовать лишь конечное число формул, то есть в ней найдётся конечное подмножество,не имеющее модели.
Получили противеоречие, которое и доказывает теорему. Следствие 2.3. Если теория имеет модели сколь угодно большой конечной мощности, то она имеет ибесконечную модель. Итак, пусть теория T в сигнатуре Ω имеет модели сколь угодно большой конечной мощности. Построимсигнатуру Ω′ := Ω∪{cn |n > 1}, то есть просто добавим к сигнатуре Ω счётное множество констант. В ней возьмёмтеорию T ′ := T ∪ {ci 6= cj |i < j}. Покажем, что каждое конечное подмножество T ′′ ⊂ T ′ этой теории выполнимо.Для любого конечного подмножества имеем T ′′ ⊆ Tn := T ∪ {ci 6= cj |1 6 i < j 6 n}. По условию теоремы,существует модель M T, |M | = n. Это означает, что из неё можно сделать модель теории Tn , сопоставивновым константам попарно различные элементы из M .
Таким образом, в силу теоремы компактности, теорияT ′ имеет модель, и эта модель бесконечна, так как сама теория требует наличия в ней счётного множествапопарно различных элементов. Однако, эта же модель будет моделью исходной теории T , что и доказываеттеорему. Пример 3.2. Не существует теории первого порядка в сигнатуре групп, такой что M T тогда и толькотогда, когда M — конечная группа.2.4. Изоморфизм и элементарная эквивалентность интерпретаций2.4.1. Определения и основные свойстваОпределение.
Пусть M и M ′ — две интерпретации сигнатуры Ω. Будем говорить, что π : M ∼= M′ —изоморфизм этих интерпретаций, если π — биекция, сохраняющая все операции и предикаты.Лемма 2.37. Значения термов сохраняются при изоморфизме:π(|t(a1 , . . . , an )|M ) = |t(πa1 , . . . , πan )|M ′ .Доказательство проводится по индукции и полностью аналогично доказательству утверждения 2.33. Лемма 2.38. Выводимость формул сохраняется при изоморфизме:M ϕ(a1 , . . . , an ) ⇔ M ′ ϕ(πa1 , . . . , πan ).Доказательство полностью аналогично доказательству леммы 2.34.