10.9: Теорема компактності
Одним з важливих наслідків теореми повноти є теорема компактності. Теорема компактності стверджує, що якщо кожна скінченна підмножина множини речень задовольняється, вся множина є задовільною, навіть якщо сама множина нескінченна. Це далеко не очевидно. Ніщо, здається, не виключає, принаймні, на перший погляд, можливість існування нескінченних наборів речень, які суперечливі, але протиріччя виникає лише, так би мовити, з нескінченного числа. Теорема компактності говорить про те, що такий сценарій можна виключити: немає незадовільних нескінченних множин пропозицій, кожне скінченне підмножина яких задовольняється. Як і теорема повноти, вона має версію, пов'язану з тягненням: якщо нескінченний набір речень тягне за собою щось, вже кінцева підмножина робить.
Визначення10.9.1
НабірΓ формул кінцево задовольняється тоді і тільки тоді, коли коженΓ0⊆Γ скінченний задовольняється.
Теорема10.9.1: Compactness Theorem
Наступне утримання для будь-яких реченьΓ іA:
-
Γ\EntailsAякщо є кінцевеΓ0⊆Γ таке, щоΓ0\EntailsA.
-
Γє задовільним тоді і тільки тоді, коли він кінцево задовольняється.
Доказ. Доводимо (2). ЯкщоΓ задовольняється, то є будова\StructM така, що\SatMA для всіхA∈Γ. Звичайно, це\StructM також задовольняє кожну скінченну підмножинуΓ, так щоΓ це кінцево задовольняється.
Тепер припустимо, щоΓ це остаточно задовольняється. Тоді кожне скінченне підмножинаΓ0⊆Γ задовольняється. За обґрунтованості (Слідства 9.11.2 та 8.12.3) кожна кінцева підмножина є послідовною. ТодіΓ сама повинна відповідати Пропозиціям 8.8.5 та 9.7.5. За повнотою (теорема 10.8.1), оскількиΓ є послідовним, вона задовольняється. ◻
Проблема10.9.1
Доведіть (1) теореми10.9.1.
Приклад10.9.1
У кожній моделі\StructM теорії кожен термінΓ,t звичайно, виділяє елемент\DomainM. Чи можемо ми гарантувати, що це також правда, що кожен елемент\DomainM вибирається тим чи іншим терміном? Іншими словами, чи існують теорії,Γ всі моделі яких висвітлюються? Теорема компактності показує, що це не так, якщоΓ має нескінченні моделі. Ось як це побачити: Дозвольте\StructM бути нескінченною моделлюΓ, і нехайc буде постійним символом не мовоюΓ. ΔДозволяти множина всіх речень\eqN[c][t] дляt терміна мовою\LangLΓ, тобтоΔ=\Setabs\eqN[c][t]t∈\Trm[L].
Приклад10.9.2
Розглянемо мову,\LangL що містить символ присудка<, постійні символи\Obj0\Obj1, і символи функції+,×,−,÷. ΓДозволяти бути сукупністю всіх речень в цій мові істинно в\StructQ області\Rat і очевидних тлумачень. Γце сукупність всіх речень\LangL істинних про раціональні числа. Звичайно, в\Rat (і навіть в\Real), немає чисел, які більше,0 але менше, ніж1/k для всіхk∈\PosInt. Таке число, якби воно існувало, було б нескінченно малим: ненульовим, але нескінченно маленьким. Теорема компактності показує, що існують моделі,Γ в яких існують нескінченності:Δ Дозволяти бути{0<c}∪\Setabsc<(\Obj1÷\numk)k∈\PosInt (де\numk=(\Obj1+(\Obj1+⋯+(\Obj1+\Obj1)…)) зk\Obj1). Для будь-якогоΔ0 скінченного підмножиниΔ існуєK таке, що всі пропозиціїc<(\Obj1÷\numk) вΔ0 havek<K. Якщо ми розширимо\StructQ до\StructQ′ з\AssigncQ′=1/K ми маємо\SatQ′Γ∪Δ0, що, і так кінцевоΓ∪Δ задовольняється (Вправа: доведіть це детально). За компактності,Γ∪Δ задовольняється. Будь-яка модель\StructSΓ∪Δ містить нескінченно мале, а саме\AssigncS.
Проблема10.9.2
У стандартній моделі арифметики немає елемента\StructN,k∈\DomainN який задовольняє кожну формулу\numn<x (де\numn\Obj0′…′n′ with's). Використовуйте теорему компактності, щоб показати, що набір речень в мові арифметики, які є істинними в стандартній моделі арифметики, також\StructN вірні в структурі\StructN′, яка містить елемент, який задовольняє кожній формулі. \numn<x.
Приклад10.9.3
Ми знаємо, що логіка першого порядку з присудком ідентичності може висловити, що розмір домену повинен мати якийсь мінімальний розмір: реченняA≥n (яке говорить «є принаймніn різні об'єкти») вірно лише в структурах, де\DomainM має принаймні nоб'єкти. Так що, якщо ми візьмемо,Δ=\SetabsA≥nn≥1
Таким чином, логіка першого порядку може виражати нескінченність. Теорема компактності показує, що вона не може виражати кінцевість, однак. Бо припустимо, що деякі сукупності пропозиційΛ були задоволені у всіх і тільки кінцевих структурах. ТодіΔ∪Λ кінцево задовольняється. Чому? ПрипустимоΔ′∪Λ′⊆Δ∪Λ, є кінцевим зΔ′⊆Δ іΛ′⊆Λ. nДозволяти найбільшу кількість таких, щоA≥n∈Δ′. Λ, будучи задоволеним у всіх кінцевих структурах, має модель\StructM з скінченно багатьма, але≥n елементами. Але потім\SatMΔ′∪Λ′. За компактності,Δ∪Λ має нескінченну модель, що суперечить припущенню, щоΛ задовольняється тільки в скінченних структурах.