Перейти к содержимому
Topos Uranos
Русский

Теорема компактности

Краткое содержание

Вывод есть конечная последовательность и использует лишь конечное число посылок; выполнимость же бесконечного множества формул требует одной-единственной оценки, которая придаёт значение 11 бесконечному числу формул сразу, и ничто в её определении не говорит, что достаточно рассмотреть конечные части. Теорема компактности утверждает, что достаточно: множество формул выполнимо тогда и только тогда, когда выполнимо каждое из его конечных подмножеств. Этот урок доказывает её прямым семантическим рассуждением, не проходя через выводимость: значения переменных v1,v2,…v_1, v_2, \ldots фиксируются одно за другим, и на каждом шаге сохраняется инвариант, состоящий в том, что всякое конечное подмножество множества остаётся выполнимым оценкой, согласованной с уже зафиксированным; если бы ни один из двух возможных выборов его не сохранял, объединение двух конечных свидетелей этой неудачи противоречило бы предыдущему инварианту, а в конце каждая формула оказывается выполненной по лемме о совпадении, поскольку содержит конечное число переменных. Так как переменные занумерованы, построение не нуждается в аксиоме выбора. Из компактности следуют её эквивалентные формы (множество невыполнимо тогда и только тогда, когда невыполнима некоторая его конечная часть; формула есть следствие множества тогда и только тогда, когда она есть следствие некоторой его конечной части), а вместе с полнотой для конечных посылок из предыдущего урока и сильная полнота: Γ⊨φ\Gamma \models \varphi влечёт Γ⊢φ\Gamma \vdash \varphi для всякого множества Γ\Gamma, откуда выводимость и семантическое следование всегда совпадают. Урок завершается комбинаторными приложениями: раскраской бесконечных графов по раскраскам их конечных частей, конечными границами, скрытыми в бесконечных утверждениях, и пределами того, что может выразить множество формул.

Цели обучения

  1. Определять конечно выполнимые множества и доказывать теорему компактности последовательной фиксацией значений переменных, объясняя роль инварианта, рассуждения о двух свидетелях и леммы о совпадении, а также то, почему построение не нуждается в аксиоме выбора.
  2. Формулировать, доказывать и применять эквивалентные формы компактности, форму невыполнимости и форму следования, и переходить от каждой из них к остальным.
  3. Выводить сильную полноту из компактности, полноты для конечных множеств посылок и монотонности, и получать из неё совпадение выводимости с семантическим следованием и непротиворечивости с выполнимостью.
  4. Кодировать множествами формул комбинаторные задачи о бесконечных множествах (раскраски, порядки, паросочетания) и решать их с помощью компактности, отличая то, что теорема гарантирует, от того, чего она не гарантирует.

Что используется из предыдущих уроков

Этот урок работает почти целиком в семантике и использует из неё следующее. Оценка есть функция v ⁣:V→{0,1}v\colon V \to \{0, 1\} на множестве VV переменных v1,v2,v3,…v_1, v_2, v_3, \ldots, которая единственным образом продолжается на все формулы; оценка выполняет множество Γ\Gamma формул, v⊨Γv \models \Gamma, если придаёт значение 11 каждой из них, и Γ\Gamma выполнимо, если его выполняет некоторая оценка, и невыполнимо в противном случае. Всё это есть в уроке о семантике логики высказываний вместе с центральным инструментом этого урока, леммой о совпадении: если две оценки совпадают на переменных формулы φ\varphi, которые образуют конечное множество V(φ)V(\varphi), то они придают формуле φ\varphi одно и то же значение.

Из урока о семантическом следовании и эквивалентности используются определение Γ⊨φ\Gamma \models \varphi (всякая оценка, выполняющая Γ\Gamma, выполняет φ\varphi), его структурные свойства, в частности монотонность (если Γ⊆Δ\Gamma \subseteq \Delta и Γ⊨φ\Gamma \models \varphi, то Δ⊨φ\Delta \models \varphi) и пятое свойство (из невыполнимого множества следует всякая формула), и теорема «Следование и невыполнимость»: Γ⊨φ\Gamma \models \varphi тогда и только тогда, когда Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} невыполнимо. Из урока об обобщённых законах де Моргана и дистрибутивности используется лемма о значении: ⋀i=1nφi\bigwedge_{i=1}^{n} \varphi_i имеет значение 11 тогда и только тогда, когда все её члены имеют значение 11, а ⋁i=1nφi\bigvee_{i=1}^{n} \varphi_i тогда и только тогда, когда некоторый член имеет значение 11. Наконец, ⊤:=(v1→v1)\top := (v_1 \rightarrow v_1) есть тавтология, а ⊥:=¬⊤\bot := \neg\top есть противоречие.

Со стороны выводимости урок о формальных дедуктивных системах доказал монотонность (Мон: если Γ⊆Δ\Gamma \subseteq \Delta и Γ⊢φ\Gamma \vdash \varphi, то Δ⊢φ\Delta \vdash \varphi) и конечность (Кон: если Γ⊢φ\Gamma \vdash \varphi, то некоторое конечное подмножество Γ0\Gamma_0 множества Γ\Gamma удовлетворяет условию Γ0⊢φ\Gamma_0 \vdash \varphi), а урок о четырёх приёмах вывода проверил, что оба свойства выполняются в системе курса (схемы A1, A2 и A3, modus ponens и замена двойного отрицания, ЗДО), к которой в дальнейшем относится знак ⊢\vdash. Наконец, урок о корректности и полноте доказал теорему о корректности (Γ⊢φ\Gamma \vdash \varphi влечёт Γ⊨φ\Gamma \models \varphi для всякого Γ\Gamma) и полноту для конечных множеств посылок: если {γ1,…,γk}⊨φ\{\gamma_1, \ldots, \gamma_k\} \models \varphi, то {γ1,…,γk}⊢φ\{\gamma_1, \ldots, \gamma_k\} \vdash \varphi.