Теория моделей и теорема полноты

1930 год: 23-летний Курт Гёдель доказывает теорему полноты в своей диссертации. На следующий год он опровергает себя же - теоремой неполноты. Эти два результата вместе определили границы формального мышления.

• **Верификация программ:** model checking - это буквально проверка M ⊨ φ, где M - модель системы, φ - спецификация на темпоральной логике (LTL/CTL)
• **Нестандартный анализ:** теория бесконечно малых Робинсона (1961) построена через теорему компактности - нестандартные модели R возникают именно так
• **Криптография и протоколы:** автоматические проверщики (Tamarin, ProVerif) рассуждают в логике первого порядка, опираясь на теорему полноты

Предварительные знания

• Пропозициональная логика
• Теория первого порядка

• Логика первого порядка

Структуры и истинность формул

Формула сама по себе - это синтаксический объект, строка символов. Истинность или ложность появляется только когда мы указываем **структуру** (модель), в которой её интерпретируем.

**Структура** M для сигнатуры σ = {f, R, c} содержит: носитель (непустое множество |M|), интерпретацию каждой функции f^M: |M|^n → |M|, каждого предиката R^M ⊆ |M|^n, каждой константы c^M ∈ |M|. Пишем M ⊨ φ, если формула φ истинна в структуре M.

Два объекта могут быть **изоморфны** (совпадать как структуры) или только **элементарно эквивалентны** (совпадать по всем формулам первого порядка, но не быть изоморфными). Например, (Q, <) и (R, <) как линейные порядки элементарно эквивалентны - ни одна формула первого порядка в сигнатуре {<} не отличает плотное линейное упорядочение без концов от другого такого же. (Внимание: как упорядоченные поля Q и R уже не эквивалентны - в R корень из 2 существует, в Q нет.)

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

Теорема компактности - один из самых мощных инструментов в логике. Она говорит: если каждое **конечное** подмножество теории имеет модель, то вся теория имеет модель.

**Теорема компактности (Гёдель-Мальцев):** Теория T имеет модель тогда и только тогда, когда каждое конечное подмножество T имеет модель. Эквивалентная формулировка: если Γ ⊨ φ (φ семантически следует из Γ), то существует конечное Δ ⊆ Γ такое, что Δ ⊨ φ.

Другое применение: теорема Лёвенгейма-Скулема следует из компактности. Если теория имеет бесконечную модель, она имеет модели любой бесконечной мощности. Это значит: никакая теория первого порядка не может зафиксировать мощность своих моделей - нельзя «в первом порядке» сказать «существует несчётно много элементов».

Теорема полноты Гёделя (1930)

1930 год: 23-летний Гёдель в своей диссертации доказывает, что синтаксис и семантика логики первого порядка совпадают. Если что-то истинно во всех моделях - его можно вывести формально. Через год он опровергает себя же - но только для арифметики.

**Теорема полноты (Гёдель, 1930):** Для любой теории Γ и формулы φ: Γ ⊨ φ (φ истинна во всех моделях Γ) тогда и только тогда, когда Γ ⊢ φ (φ выводима из Γ). То есть: семантическое следование = синтаксическая выводимость. **Теорема неполноты (Гёдель, 1931):** В любой непротиворечивой формальной арифметике есть истинные утверждения, которые нельзя доказать (⊨ φ, но ⊬ φ). Противоречия нет: неполнота 1931 говорит о конкретной теории PA, полнота 1930 говорит о правиле вывода логики в целом.

Теорема полноты 1930 утверждает, что правила логики первого порядка **не упускают ничего** - если что-то истинно во всех моделях, формальный вывод это докажет. Теорема неполноты 1931 утверждает, что аксиомы арифметики **не описывают всего** - есть истины натуральных чисел, которые из PA не следуют. Это разные уровни утверждений.

Итог

• **Структура M** интерпретирует сигнатуру: носитель + функции + предикаты + константы. M ⊨ φ - φ истинна в M
• **Теорема компактности:** T выполнима ⟺ каждое конечное подмножество T выполнимо. Следствие - нестандартные модели (R*, нестандартная арифметика)
• **Теорема полноты 1930:** Γ ⊨ φ ⟺ Γ ⊢ φ - семантика и синтаксис первого порядка совпадают. Это не противоречит неполноте 1931, которая говорит о конкретной теории PA, а не о правилах вывода

Связанные темы

Теория моделей - точка, где логика встречается с алгеброй и анализом:

• Исчисление предикатов — Предоставляет синтаксическую сторону - правила вывода ⊢, над которыми теорема полноты устанавливает соответствие с ⊨
• Арифметика Пеано и неполнота — Теорема неполноты 1931 - главное следствие: PA не описывает N полностью, существуют нестандартные модели

Вопросы для размышления

• Теорема компактности говорит, что нельзя выразить «множество счётное» в логике первого порядка. Почему? Что это говорит о выразительности первого порядка?
• Если PA имеет нестандартные модели - как мы вообще «знаем», что говорим о натуральных числах, а не о какой-то другой модели PA?
• Теорема полноты гарантирует: всё, что истинно во всех моделях, выводимо. Но вывод может быть сколь угодно длинным. Что это говорит о практике доказательств?

Связанные уроки

• plt-06-lambda-calculus