Конструкция Хенкина: пошаговая демонстрация

Интерактивная иллюстрация к доказательству теоремы Гёделя о полноте исчисления предикатов первого порядка.

Что здесь происходит

Теорема Гёделя о полноте утверждает: если множество формул \(\Gamma\) непротиворечиво, то у него есть модель. Доказательство конструктивно строит эту модель в три шага.

Расширение языка. Для каждой формулы \(\exists x\,\varphi(x)\) вводится новая константа-«свидетель» \(c\) и аксиома \(\exists x\,\varphi(x) \to \varphi(c)\). Поскольку добавление констант порождает новые экзистенциальные формулы, процедура итерируется: \(\mathcal{L}_0 \subseteq \mathcal{L}_1 \subseteq \cdots \subseteq \mathcal{L}_\omega\). Это константы Хенкина.

Лемма Линденбаума. Перечислим все замкнутые формулы расширенного языка \(\mathcal{L}_\omega\). На каждом шаге добавляем очередную формулу \(\varphi_k\) к теории, если это не создаёт противоречия, иначе добавляем \(\lnot\varphi_k\). В итоге получаем полное непротиворечивое множество \(\Delta\): для каждой формулы в \(\Delta\) лежит ровно одна из \(\varphi, \lnot\varphi\).

Термовая модель. Носитель модели — классы эквивалентности замкнутых термов по \((s \sim t) \iff (s{=}t) \in \Delta\). Предикат \({<}\) интерпретируется по определению: \([s] < [t]\) iff \((s{<}t)\in\Delta\). Лемма об истинности (индукция по формуле) гарантирует, что модель удовлетворяет \(\Gamma\).

Та же теорема о полноте — причина, по которой арифметика второго порядка как формальная система остаётся первопорядковой: её моделями оказываются общие (хенкиновские) структуры, где второй сорт — произвольное семейство «множеств», а не настоящий булеан \(\mathcal{P}(\mathbb{N})\). Что из этого следует для \(\mathsf{ACA}_0\), \(\mathsf{Z}_2\) и категоричности — в материале «Иерархия теорий арифметики второго порядка».

Пример на этой странице. Язык \(\mathcal{L} = \{=,\,{<},\,0\}\) с теорией линейного порядка и аксиомой минимальности \(\forall x\,(0{=}x \vee 0{<}x)\). Константа \(0\) даёт первый замкнутый терм, поэтому конструкция Хенкина стартует сразу: уже в \(\mathcal{L}_0\) осмыслена формула \(\exists x\,(0{<}x)\). Ползунок n управляет числом итераций расширения языка, ползунок k — числом шагов Линденбаума.

↓ Полный текст доказательства теоремы Гёделя о полноте (PDF)

итерация языка — \(n\)

\(\mathcal{L}_0 \subseteq \mathcal{L}_1 \subseteq \mathcal{L}_2 \subseteq \mathcal{L}_3 = \mathcal{L}_\omega\)

шаг Линденбаума — \(k\)

добавить аксиому \(\forall x\,\forall y\,\forall z\;(x{=}y \vee y{=}z \vee z{=}x)\)

исходная теория \(\Gamma\)

язык \(\mathcal{L}_n\)

аксиомы Хенкина \(H\)

ПН-множество \(\Delta\) — первые \(k\) шагов Линденбаума

термовая модель \(\mathfrak{M} = T/{\sim}\)

На карте оснований математики (MathLogic Nexus): Теорема о полноте · Алгебра Линденбаума