Интерактивная иллюстрация к доказательству теоремы Гёделя о полноте исчисления предикатов первого порядка.
Что здесь происходит
Теорема Гёделя о полноте утверждает: если множество формул \(\Gamma\) непротиворечиво,
то у него есть модель. Доказательство конструктивно строит эту модель в три шага.
1
Расширение языка.
Для каждой формулы \(\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\).
Это константы Хенкина.
2
Лемма Линденбаума.
Перечислим все замкнутые формулы расширенного языка \(\mathcal{L}_\omega\).
На каждом шаге добавляем очередную формулу \(\varphi_k\) к теории, если это не создаёт противоречия,
иначе добавляем \(\lnot\varphi_k\). В итоге получаем полное непротиворечивое множество \(\Delta\):
для каждой формулы в \(\Delta\) лежит ровно одна из \(\varphi, \lnot\varphi\).
3
Термовая модель.
Носитель модели — классы эквивалентности замкнутых термов по \((s \sim t) \iff (s{=}t) \in \Delta\).
Предикат \({<}\) интерпретируется по определению: \([s] < [t]\) iff \((s{<}t)\in\Delta\).
Лемма об истинности (индукция по формуле) гарантирует, что модель удовлетворяет \(\Gamma\).
Пример на этой странице.
Язык \(\mathcal{L} = \{=,\,{<},\,0\}\) с теорией линейного порядка и аксиомой минимальности
\(\forall x\,(0{=}x \vee 0{<}x)\). Константа \(0\) даёт первый замкнутый терм, поэтому
конструкция Хенкина стартует сразу: уже в \(\mathcal{L}_0\) осмыслена формула \(\exists x\,(0{<}x)\).
Ползунок n управляет числом итераций расширения языка, ползунок k — числом шагов Линденбаума.