В.Б. Шехтман - Курс лекций по логике и теории алгоритмов (1161807), страница 6
Текст из файла (страница 6)
¬ ∃ x ¬ϕ → ∀ x ¬¬ϕ — по уже доказанному2. ¬¬ϕ → ϕ163. ∀ x ¬¬ϕ → ∀ x ϕ — монотонность4. ¬ ∃ x ¬ϕ → ∀ x ϕ — два раза МР5. ¬ ∀ x ϕ → ∃ x ¬ϕ — правило контрапозицииТеперь лемма доказана полностью. 2.1.5. Теорема корректности исчисления предикатовВ этом разделе нашей основной целью будет доказательство теоремы корректности для исчисления предикатов, а именно,⊢PCΩ ϕ ⇒ ϕ.Доказательство мы разобъём на много-много промежуточных лемм. Итак, вперёд.Лемма 2.9. Пусть дана формула ϕ ∈ FmΩ и FV(ϕ) ⊆ {x1 , . . .
, xn }. Тогда в любой интерпретации Mсигнатуры ΩM ∀ ϕ ⇔ для всех a1 , . . . , an ∈ M M [a1 , . . . , an /x1 , . . . , xn ]ϕ.Индукцией по n:| ∀ x 1 . . . ∀ x n ϕ|M = 1 ⇔ для всех a1 ∈ M|[a1 /x1 ] ∀ x 2 . . . ∀ x n ϕ|M = 1.Лемма 2.10. Пусть α — одна из первых 11ти аксиом. Тогда α.
Почти очевидно. Берём произвольный набор переменных, подставляем в формулы, фигурирующие ваксиоме. Считаем их (формул) значения в интерпретации. Подставляем, получаем аксиому логики высказываний — а про них нам известно, что они все — тавтологии. Лемма 2.11. Пусть α — 14я аксиома. Тогда α. Итак, есть утверждение вида∀ x ϕ(x) → ψ → ∃ x ϕ(x) → ψ ,x 6∈ FV(ψ).Пусть FV(α) = {y1 , . .
. , yn }. Ясно, что x 6∈ FV(α). Пусть ψ1 и ϕ1 (x) — формулы, полученные в результатеподстановки в ψ и ϕ некоторых значений переменных yi . Тогдаα1 = ∀ x ϕ1 (x) → ψ1 → ∃ x ϕ1 (x) → ψ1 .Полагаем, что | ∀ x ϕ1 (x) → ψ1 | = 1 и | ∃ x ϕ1 (x)| = 1, нужно доказать, что |ψ1 | = 1. То есть, мы знаем, чтодля некоторого a ∈ M |ϕ(a1 )| = 1 и |ϕ1 (a) → ψ1 | = 1. По МР (в рамках логики высказываний) получаем, что|ψ1 | = 1. Следующая лемма доказывается полностью аналогично.Лемма 2.12. Пусть α — 15я аксиома. Тогда α.А это и вовсе очевидно:Лемма 2.13. α, α → β ⇒ β.Лемма 2.14. ϕ ⇒ ∀ x ϕ.По определению, M ϕ ⇔ M ∀ ϕ. Лемма 2.15 (о двойной подстановке в терм). Даны термы r ∈ TmΩ∪M , FV(r) ⊆ {x} и t ∈ TmΩ , FV(t) ⊆{z1 , .
. . , zn } и элементы носителя c1 , . . . , cn ∈ M . Обозначим a = |t(c)|M . Тогда|[c/z][t/x]r|M = |[a/x]r|M .Очевидно (индукция по длине терма, то есть по числу функциональных символов в нём). Лемма 2.16 (о двойной подстановке в формулу). Дана формула термы ψ ∈ FmΩ∪M , FV(r) ⊆ {x} итерм t ∈ TmΩ , FV(t) ⊆ {z1 , . . .
, zn }, а также элементы носителя c1 , . . . , cn ∈ M , причём подстановка [t/x]свободна в ψ. Обозначим a = |t(c)|M . Тогда|[c/z][t/x]ψ|M = |[a/x]ψ|M .17 Опят-таки индукция по длине формулы. Здесь тоже всё достаточно очевидно, отдельного рассмотрениязаслуживает лишь случай с квантором: ψ(x) = ∃ u ψ1 (u, x), u 6= x. Тогда FV(ψ1 ) = {u, x}, причём u 6∈ z (поусловию подстановка свободна). Нам нужно доказать равенство|[c/z][t/x] ∃ u ψ1 | = |[a/x] ∃ u ψ1 |.Пусть слева единица, докажем, что и справа получим один.Итак, для некоторого m ∈ M имеем:|[c/z][t/x][m/u]ψ1 | = 1.Обозначим ψ2 = [m/u]ψ1 .
ψ2 короче, чем ψ, следовательно, к этой формуле можно применить предположениеиндукции:1 = |[c/z][t/x][m/u]ψ1 | = |[c/z][t/x]ψ2 | = |[a/x]ψ2 | = |[a/x][m/u]ψ1 |,а значит |[a/x] ∃ u ψ1 | = 1, что и требовалось. Все рассуждения обратимы, поэтому окончательно получаем|[c/z][t/x] ∃ u ψ1 | = 1 ⇔ |[a/x] ∃ u ψ1 | = 1.Случай с квантором всеобщности разбирается полностью аналогично. Случай замкнутой формулы очевиден.Лемму можно считать доказанной. Лемма 2.17. Пусть α — 13я аксиома.
Тогда α. Нужно доказать, чтоM α = [t(z)/x]ϕ(x, y) → ∃ x ϕ(x, y).По определению, для этого нужно доказать, что M ∀ α, то есть M [b, c/y, z]α для произвольных элементовносителя b, c. При подстановке ещё надо учитывать, что наборы переменных y и z могут пересекаться, но мыне станем вдаваться в такие подробности. Итак, имеем|[b, c/y, z]α| = |[b, c/y, z][t, x]ϕ(x, y) → [b/z] ∃ x ϕ(x, y)| = |α1 → α2 |,то есть нужно доказать, что |α1 | = 1 ⇒ |α2 | = 1. Доказываем:|α1 | = |[c/z][t/x]ϕ(x, b)| = |[a/x]ϕ(x, b)| ⇒ | ∃ x ϕ(x, b)| = 1,где a = |t(c)|. Вот и всё. Лемма 2.18.
Пусть α — 12я аксиома. Тогда α. Полностью аналогично предыдущей лемме. Тем самым, доказательство теоремы корректности для исчисления предикатов завершено.2.1.6. Теорема корректности и теорема непротиворечивостидля теорий первого порядкаОпределение. Будем говорить, что формула ϕ логически следует из теории T (T ϕ), если ϕ истинна влюбой модели этой теории. Для незамкнутых формул, как обычно, речь идёт об их универсальном замыкании.Теорема 2.19 (корректности для теорий первого порядка).T ⊢ ϕ ⇒ T ϕ.Как обычно, индукция по длине вывода. База — очевидно. Шаг — теорема дедукции.
Определение. Теория T противоречива, если найдётся такая формула ϕ, что T ⊢ ϕ и T ⊢ ¬ϕ.Теорема 2.20 (о непротиворечивости для теорий первого порядка). Выполнимая теория непротиворечива. Предположим обратное. Тогда в некоторой модели M ϕ и M ¬ϕ, что невозможно (если ϕ незамкнута,берём ∀ ϕ и приходим к такому же противоречию).
182.1.7. Теории с равенствомВ исчислении предикатов с равенством (PC=Ω ) всякая сигнатура снабжается дополнительным предикатнымсимволом «=», а список аксиом пополняется следующими пятью:16) ∀ x x = x17) ∀ x ∀ y (x = y → y = x)18) ∀ x ∀ y ∀ z (x = y & y = z → x = z)19) ∀ (x1 = y1 & . . .
xn = yn → f n (x1 , . . . , xn ) = f n (y1 , . . . , yn )) , f n ∈ Fn20) ∀ (x1 = y1 & . . . xn = yn → P n (x1 , . . . , xn ) = P n (y1 , . . . , yn )) , P n ∈ PrПонятия выводимости и логического следования вводятся аналогично обычному исчислению предикатов.Определение.
Интерпретация M теории с равенством нормальна, еслиM a = b ⇔ a = b,причём равенство справа понимается как совпадение соответствующих элементов носителя.Лемма 2.21.1) ⊢PC=t1 = r1 & . . . & tn = rn → f (t1 , . . . , tn ) = f (r1 , . . . , rn )Ω2) ⊢PC=t1 = r1 & . . . & tn = rn → P (t1 , .
. . , tn ) = P (r1 , . . . , rn )Ω2.2. Теории Хенкина2.2.1. Экзистенциальная полнотаОпределение. Теория T экзистенциально полна ( ∃ – полна) в сигнатуре Ω, если для любой формулыϕ(x) ∈ FmΩ выполнено следующее следствие: если T ⊢ ∃ x ϕ(x), то существует такой замкнутый терм t ∈ TmΩ ,что T ⊢ ϕ(t).Замечание наборщика.
Говоря неформально, это означает, что квантор существования всегда реализуется в теории T .Пример 2.1. Пусть задана сигнатура Ω1 = ({0, 1}, {+}, ∅, γ1) со стандартной интерпретацией N1 (натуральные числа со сложением). В ней рассмотрим теорию Th(N1 ), состоящую из множества всех формул, истинныхв этой интерпретации (её элементарную теорию). Несложно понять, что эта теория экзистенциально полна.Действительно, по определению нашей теории имеем:Th(N1 ) ⊢ ∃ x ϕ(x) ⇔ N1 ∃ x ϕ(x),а это означает, опять же, по определению, что найдётся натуральное число n, для которого N1 ϕ(n).Пример 2.2.
А вот обратный пример. Рассмотрим сигнатуру Ω1 = (∅, ∅, {<}, γ1), интерпретируемую какнатуральные числа со стандартным упорядочением (N2 ). В качестве теории вновь возьмём элементарную теориюданной интерпретации. Ясно, однако, что никакой экзистенциальной полноты здесь быть не может: так какмножества констант и функциональных символов пусты, замкнутых термов в данной сигнатуре просто нет, иподставлять в формулу будет нечего.2.2.2. Свойство ХенкинаОпределение. Будем говорить, что формула ϕ(x) обладает свойством Хенкина относительно теории T , еслисуществует такая константа данной сигнатуры c ∈ Cnst, чтоT ⊢ ∃ x ϕ(x) → ϕ(c).Определение.
Теория T является теорией Хенкина, если любая формула обладает одноимённым свойствомотносительно этой теории.Лемма 2.22. Любая теория Хенкина экзистенциально полна. Очевидно. 2.2.3. Вложение непротиворечивых теорий в полные теории ХенкинаЛемма 2.23 (о свежих константах). Пусть дана формула ϕ(x) ∈ FmΩ и некоторая константа c ∈ Cnst,не входящая в эту формулу, причём ⊢PC(=) ϕ(c). Тогда ⊢PC(=) ϕ(x).ΩΩ Пусть ⊢ ϕ(c), докажем, что ⊢ ϕ(z), где z — некоторая переменная, не встречающаяся в выводе ϕ(c).Доказательство будем проводить по индукции по длине вывода ϕ(c).1. ϕ(c) — аксиома. В таком случае ϕ(z) — также аксиома.192. ϕ(c) получается по правилу МР:ψ(c), ψ(c) → ϕ(c)ϕ(c)и вывод формул ψ(c) и ψ(c) → ϕ(c) короче, чем вывод ϕ(c).
Тогда по предположению индукции имеем⊢ ψ(z) и ⊢ ψ(z) → ϕ(z), откуда по МР получаем ϕ(z).3. ϕ(c) получается по правилу обобщения: рассуждаем аналогично предыдущему случаю.Итак, мы научились выводить ϕ(z), а значит, по правилу обощения, и ⊢ ∀zϕ(z). По построению эта подстановкасвободна, что даёт нам право воспользоваться 12й аксиомой:⊢ ∀zϕ(z) → ϕ(x),откуда по МР получаем требуемое. Лемма 2.24.
Пусть T — непротиворечивая теория в «счётной» (то есть не более чем счётной) сигнатуреΩ. Тогда существует такая сигнатураΩ′ = Ω ∪ {cn |n ∈ N},и непротиворечивая теория Хенкина T ′ в ней, что T ⊆ T ′ . Пронумеруем все замкнутые формулы сигнатуры Ω′ вида ∃ xn ϕn (xn ). Построим индуктивно последовательность теорий Tn . Положим T0 = T, Ω0 = Ω иTn+1 = Tn ∪ { ∃ x n ϕn (xn ) → ϕn (dn )},где dn — первая константа, не попавшая в Ωn .Замечание наборщика. Поясню идею этого построения (как я её понимаю). У нас есть теория T . Мы для каждой формулывида ∃ x ϕ(x) → ϕ(c) проверяем, выводима ли она из нашей теории хоть для какой-нибудь константы c.
Если такой константы ненашлось, мы добавляем в сигнатуру новую константу (dn ), а к теории — новую формулу ( ∃ x n ϕn (xn ) → ϕn (dn )).Убедимся (опять таки индуктивно), что построенные таким образом теории будут непротиворечивы. База унас есть (исходная теория была непротиворечива по условию), будем доказывать шаг. Итак, считаем, что протеорию Tn известно, что она непротиворечива. Следует убедиться в непротеворечивости теории Tn+1 .
Предположим обратное (то есть противоречивость Tn+1 ). Мы знаем, что эта теория имеет вид Tn+1 = Tn , α, и еёпротиворечивость означает, чтоTn , α ⊢ ψ, Tn , α ⊢ ¬ψ.По теореме дедукции получаемTn ⊢ α → ψ,Tn ⊢ α → ¬ψ.Теперь воспользуемся 10й аксиомой и получим Tn ⊢ ¬α. Это означает, что в теории Tn найдутся формулыr1 , . . . , rk такие, что r1 & . . . & rk ⊢ ¬α.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
