Брауэр — Urintuition
Статус
[И].
Брауэр (1881-1966)
Голландский математик и философ. Основатель интуиционизма.
Биографический контекст
- 1881: родился в Роттердаме.
- 1904: степень доктора философии.
- 1907: диссертация «Over de Grondslagen der Wiskunde» — основы интуиционизма.
- 1911: теоремы о fixed points (классика).
- 1912-1951: профессор в Амстердаме.
- 1966: смерть.
Значение для математики
- Основатель интуиционизма.
- Предшественник конструктивной математики.
- Топология: fixed point theorem, invariance of dimension.
- Основы математики: alternative to classical foundations.
Urintuition
Пра-интуиция двойственности:
В самом основании сознания лежит способность различать «момент сейчас» и «момент до».
Из этого различения — натуральные числа: сейчас, сейчас-после-сейчас, ...
Детализация
Формулировка Брауэра (из диссертации 1907):
«Das der Mathematik eigentümliche Ding, die Urintuition, ist die «Zweieinigkeit».»
«Особенное для математики — Urintuition, это «Двоединство».»
Структура Urintuition
- Момент сейчас: current moment of consciousness.
- Момент до: immediately prior moment, retained.
- Различение между ними: первый акт математики.
- Соединение их в единство: «two-in-one».
Zweieinigkeit — нем. «двоединство» — одновременное различение и соединение.
Феноменологическая природа
- Непосредственность: Urintuition дан непосредственно в сознании.
- Универсальность: каждый математик имеет к нему доступ.
- Основа: всё остальное строится отсюда.
От Urintuition к математике
- Urintuition → ℕ.
- ℕ → арифметика.
- Арифметика → анализ (через конструкции).
- И так далее.
Вся математика — построена из Urintuition конструктивными операциями.
Детализация построения
Urintuition → ℕ:
- 1 = первое различение (момент сейчас).
- 2 = Urintuition примененный к 1.
- 3 = Urintuition примененный к 2.
- ... и так далее.
ℕ → арифметика:
- Сложение: повторение Urintuition.
- Умножение: повторение сложения.
- Конструктивные определения operations.
Арифметика → анализ:
- Рациональные как пары целых.
- Реальные как choice sequences (spreads и species).
- Анализ через конструктивные построения.
Ключевые принципы конструктивной математики
- Экзистенция через конструкцию: ∃x. P(x) требует построения конкретного x.
- Отказ от LEM: закон исключённого третьего (A ∨ ¬A) не принимается глобально.
- Отказ от double negation: ¬¬A не влечёт A.
- Continuum: интуиционистская версия (Брауэр's theorem about continuity).
Параллель с Diakrisis
| Брауэр | Diakrisis |
|---|---|
| Urintuition | Διάκрисίς (акт) |
| Различение сейчас/до | первое применение Διάκрисις |
| ℕ как результат | α_ℕ ∈ Trace(𝖠) |
| Конструктивная математика | часть Diakrisis-каталога |
Расширенная таблица
| Брауэр | Diakrisis | Тип соответствия |
|---|---|---|
| Urintuition | Διάκрисіс | первичный акт |
| Zweieinigkeit | моменты 1+3 (расщепление+соотнесение) | структура акта |
| Temporal structure | ординалы в 𝖬 | time-like ordering |
| Choice sequences | gauge-выборы | free variability |
| Intuitionistic logic | α_int | один из gauge-классов |
| Continuity theorem | свойства α_int | конкретные теоремы |
Глубинные параллели
Акт как primitive:
- Брауэр: Urintuition — primitive.
- Diakrisis: Διάκрисίс — primitive.
- Общее: акт предшествует объектам.
Конструктивизм:
- Брауэр: каждое мат-утверждение — через конструкцию.
- Diakrisis: каждая α выражается через Trace.
- Общее: explicit building, не ontological existence.
Отличие
Брауэр:
- Субъективизм (Urintuition = акт индивидуального математика).
- Ограничение на конструктивную логику.
- Отказ от закона исключённого третьего.
Diakrisis:
- Δиакрисис — имперсонален (не зависит от конкретного «я»).
- Логико-нейтрален (не привилегирует конструктивную логику).
- Допускает классическую математику как gauge-вариант.
Детализация отличий
Субъективизм vs имперсональность:
- Брауэр: Urintuition связан с конкретным сознанием.
- Diakrisis: Διάκрисίς универсален, структурен.
- Следствие: Брауэр требует «живого математика»; у нас — formal structure.
Логика:
- Брауэр: ограничение на intuitionistic.
- Diakrisis: любая логика — gauge-выбор.
- Следствие: мы охватываем и classical, и intuitionistic.
Отношение к ZFC:
- Брауэр: ZFC — «не настоящая» математика (из-за LEM).
- Diakrisis: ZFC — одна из α, равноправная с HoTT.
Точки схождения
Несмотря на отличия:
- Обе теории — структурные.
- Обе признают акт как primary.
- Обе обеспечивают формальную работу.
Что ценно
- Идея, что математика выводится из одного акта.
- Феноменологическая доступность этого акта.
Детализация ценного
Математика из одного акта:
- Брауэр: вся ℕ → арифметика → анализ → ... из Urintuition.
- Diakrisis: все α ∈ Trace(𝖠) из initial α_0.
- Значение: редукционность в хорошем смысле.
Феноменологическая доступность:
- Urintuition — проверяемо (каждый может заметить).
- Διάκрисіс — также проверяемо.
- Следствие: математика укоренена в опыте.
Что отвергается
- Ограничение на конструктивность.
- Субъективизм как онтологическая позиция.
Детализация отвергнутого
Ограничение на конструктивность:
- Принуждает отказаться от многих классических теорем.
- Ограничивает математику.
- В Diakrisis: ограничение — gauge-выбор, не обязательство.
Субъективизм:
- Математика становится зависимой от индивидуального сознания.
- Проблематично для универсальности.
- В Diakrisis: имперсональность — сохраняет универсальность.
Связь с интуиционистской логикой α_int
Интуиционистская логика — gauge-вариант в каталоге /04-extractions/06-logics-catalog. Брауэр-теория — один из путей (не единственный).
В Diakrisis
- α_int: артикуляция интуиционистской логики.
- Брауэр's position: соответствует конкретному выбору в α_int.
- Другие варианты: classical (α_cl), linear (α_lin), и т.д.
Gauge-equivalence
- α_int и α_cl — разные gauge-классы (не эквивалентны).
- α_int Морита-эквивалентен α_topos (toposes).
- α_int ⊂ α_constructive в целом.
Наследие Брауэра
Современное интуиционистское движение
- Гейтинг: формализация intuitionistic logic.
- Мартин-Лёф: MLTT.
- Бишоп: constructive analysis.
- Эводи, Воеводский: HoTT (с intuitionistic base).
Computational impact
- Curry-Howard isomorphism: propositions as types.
- Proof assistants: Coq, Agda, Lean — все intuitionistic.
- Functional programming: из intuitionistic идей.
В современной физике
- Isham и другие: intuitionistic подход к квантовой механике.
- Topos physics: через intuitionistic logic.