Математический анализ · Теория моделей · Обратная математика
Сравнение выразительной силы и метатеоретических свойств: , предикативный анализ Вейля и
Язык и онтология
Переменные пробегают только элементы ; сигнатура: . Символ между числами отсутствует — внутреннее устройство чисел синтаксически невыразимо. Функции — только многочлены. Квантификация по подмножествам и последовательностям невозможна; предел, непрерывность, интеграл в общем виде невыразимы (только для многочленов). По теореме Тарского теория полна и разрешима; по теореме Лёвенгейма–Сколема у неё есть модели любой бесконечной мощности.
Два сорта: числа (тип 0: ) и множества чисел (тип 1: ). Схема свёртывания — только по числовым формулам (без кванторов ). вводится аксиоматически как наименьшее индуктивное. Сепарабельные пространства (, , ) кодируются через подмножества . Несепарабельные () и произвольные функционалы требуют третьего сорта. Теория является «синтаксическим сахаром» над (консервативное расширение). Как перечислимо аксиоматизированная двусортная теория она укладывается в стандартную семантику Хенкина (полнота), без требования единственности модели (см. строку «Уникальность модели» в таблице).
Работаем внутри , но весь язык редуцирован к кумулятивной иерархии , стартующей с (по той же схеме, что порождает универсум фон Неймана). На базовом уровне иерархии элементы рассматриваются как эффективные атомы, свойства которых исчерпываются полной теорией модели в сигнатуре упорядоченного поля (в отличие от уровня II, где язык лишь перечислимо аксиоматизируется — см. «Уникальность модели» в таблице). Это исключает из рассмотрения внутреннюю -структуру самих чисел. При этом над базой доступны все конструкции : ординалы, кардиналы, трансфинитная индукция и пространства функций. Формы выбора добавляются по потребности: счётный выбор (), зависимый выбор () или полная .
| Характеристика / Знаковые теоремы | Уровень I RCF 1-й порядок над | Уровень II Вейль предикат. 2-й порядок над | Уровень III атомы + формы выбора |
|---|
В первой колонке пометка не определимо совпадает по смыслу с «невыразимо в языке»: после точки указана типичная причина — нет II порядка (подмножества ℝ, последовательности, произвольные покрытия и т. п.); нет ℕ; коды и σ-алгебра — здесь под σ-алгеброй имеется в виду нужда в семействе подмножеств ℝ, замкнутом по счётным операциям (дополнение, счётное объединение): так задаются измеримые множества и мера Лебега; на языке I нет переменной для произвольных таких семейств и для самой меры как функции на них.
Под кодами — представление объектов анализа (числа, функции на отрезке, классы функций, элементы Lp) последовательностями натуральных чисел или другими объектами арифметики второго порядка при ограничениях предикативности; без этого даже постановка теорем о мере и банаховых пространствах в том виде, как в таблице, недоступна.
Отдельно для аксиоматики: нет объектов-множеств, ℕ не выделяется.
Строка Уникальность модели: на уровне I — теорема Лёвенгейма–Сколема для счётной сигнатуры первого порядка; на уровне II формализация двусортная и перечислима, так что в игру входят семантика Хенкина (полнота для такого языка) и возможны попарно неизоморфные модели; на уровне III к ZF добавляется полная элементарная теория модели ℝ на атомах, и интендированная структура фиксируется с точностью до изоморфизма.
© Nikolai Kazimirov · mathem.at