Формализация

Каждое утверждение теории доводится до машинной проверки: доказательство принимает компилятор Rocq (Coq). Проверить можно самостоятельно: https://github.com/Horsocrates/theory-of-systems-coq


27 004	теоремы (Qed)
0	недоказанных мест (Admitted)
2 021	файл
Rocq 9	компилятор

Что такое формализация

Формализация — запись определений и доказательств на формальном языке, в котором каждый шаг проверяет программа, а не доверие читателя. Доказательство либо собирается целиком, либо не принимается вовсе.

CIC (исчисление индуктивных конструкций) — логическое ядро этого языка: каждое определение — точная конструкция, каждый шаг вывода — применение явного правила. Rocq (прежнее имя — Coq) — компилятор, который этот язык проверяет: файл принимается только тогда, когда каждое доказательство в нём завершено. Отметка Qed в конце доказательства означает: проверено машиной.

Проекту это даёт две вещи. Первое — надёжность: за каждым утверждением теории, доведённым до этого слоя, стоит проверенное доказательство, а не авторитет автора. Второе — честность границ: по коду точно видно, что доказано, что принято как условие и что остаётся открытым.

Основание

В ядре объявлены две аксиомы: исключённое третье (classic, файл Distinction.v) и конструктивный свидетель существования (L4_witness, файл ToS_Axioms.v). Это технические аксиомы, а не основания системы: в самой теории оба закона выводятся и обосновываются — от акта различения. Логическое ядро Rocq конструктивно и не содержит их встроенными, поэтому в код они входят как явные допущения — требование инструмента, а не основание теории.

Сама цепь основания — акт различения → законы → принципы → E/R/R — выведена сквозняком, и вывод проверен машиной. Законы L1–L5 — теоремы о структуре различения (LawsFromDistinction.v, five_laws_from_distinction); исключённое третье на различениях — структурный факт, не допущение: различение по построению кладёт каждый предмет по одну из сторон. Принципы P1–P4 — теоремы из законов (PrinciplesFromLaws.v, derivation_chain: P1 — из L1 и L5, P2 — из L5, P3 — из L1 и L4, P4 — из L5); из принципов строится метод E/R/R (PrinciplesToERR.v). Постулатов в этой цепи нет ни одного звена. Две аксиомы кода — не звенья цепи, а цена переноса выведенного в чужое ядро: classic — формализация L3-как-тотальности (теорема L3_independence показывает точное совпадение), L4_witness — извлечение свидетеля по P4.

Сам L3 при этом расщеплён машинно (BinarityVsTotality.v): бинарность — «третьего не дано» — теорема без аксиом в трёх формах (side_binarity, L3_binarity, pending_binarity — верна уже для незавершённого акта), и лишь тотальность — «назначение всегда уже состоялось» — требует classic (totality_completes). Незавершённый акт получил формальный тип (PendingDistinction — «может быть, но нет»), актуализация — событие со свидетелем (Достаточное Основание вшито в тип перехода), и канонический distinction_of равен актуализации тотальностью по чистой конверсии (distinction_of_is_actualization): аксиома входит в конструктор ровно в аргументе назначения. У тотальности нет онтологического прочтения — «может быть» не значит «будет»: потенциал истекает нереализованным (яблоки сгнили — сок не сделан), тотальность всегда о «сейчас» и никогда о будущем; будущее — не функция настоящего, оба продолжения законны — это поле свободы (TotalityNow.v: potential_expires, eternalism_refuted, totality_now, future_not_readable — 0 аксиом). Принимающий classic принимает режим счёта, не тезис о мире.

Сравнение с ZFC

Классическое основание математики — ZFC — держится на аксиомах существования: бесконечность постулируется завершённым множеством, степень — совокупностью всех подмножеств, выбор — функцией по произвольному семейству. Здесь путь другой: структура выводится из законов логики, и каждый принцип делает работу аксиомы — теоремой, а не постулатом:

Принцип	из закона	делает работу аксиомы ZFC
P1 — нет `S ∈ S` (иерархия уровней)	L5	Фундирования
P2 — определение раньше запроса (нет круговых определений)	L5	дисциплины Выделения (Рассел снят)
P4 — конечная актуальность (всё — процесс, не завершённый объект)	L5	Бесконечности
P3 — тождество по критерию	L1 + L4	Объёмности
детерминированный выбор по порядку	L5	Выбора

Полный поаксиомный разбор машинно сведён в реестр ZFCAxiomLedger.v: все девять аксиом ZFC классифицированы функцией tos_verdict, и каждый вердикт «заменена» цитирует свой 0-аксиомный файл устранения:

Аксиома ZFC	Вердикт	Позиция
Бесконечности	заменена P4	ℕ — индуктивный тип; бесконечность — только процесс
Степени	role-limit	единственная цена: конечный булеан — Element (ровно 2ⁿ подмножеств, явно перечислимо), полный 2^ℕ — role-limit (несчётность)
Фундирования	заменена P1	иерархия уровней фундирована: `S ∈ S` невозможно
Выделения (схема)	заменена P4	предикативная — разрешимая — выделимость; парадокс Рассела — ошибка типа
Подстановки (схема)	заменена P4	ограниченные процесс-семейства; трансфинитный охват — осознанный отказ
Пары	тривиальна	зависимая пара даётся самой структурой типов
Объединения	тривиальна	структурно-конструктивна, отдельная аксиома не нужна
Выбора	заменена L5	детерминированный выбор по индексу вместо произвольного (L5 назначает статусы)
Объёмности	тривиальна	структурное равенство, без глобальной аксиомы

Итог реестра — теорема only_powerset_is_role_limit: ровно одна аксиома из девяти — Степени — попадает на дальнюю сторону границы финитизации; восемь остальных тривиальны или заменены именованным законом. И даже Степени отвергается не как операция: на конечной стороне булеан явно строится, цена — только его примыкание к завершённой бесконечности.

Честная калибровка. Мы не заявляем «у нас меньше аксиом»: спор о количестве малосодержателен. Честное сравнение — по субстратам: ZFC — классическая логика первого порядка плюс аксиомы существования множеств; здесь — конструктивное ядро CIC плюс два явных допущения инструмента (classic — режим тотальности, чья бинарностная половина выведена теоремой без аксиом, и L4_witness — извлечение свидетеля по P4; раздел «Основание» выше). Постулатов система не принимает ни на одном шаге: то, что в ZFC вводится аксиомой, здесь либо выведено, либо построено. Ни одно из двух допущений — не утверждение существования.

Том «Математика»: развёрнутое чтение

Формальная база и том «Математика» — две стороны одного корпуса: том разворачивает прозой то, что здесь стоит кодом, и каждая его часть опирается на свои файлы src/. Опорные точки:

Аксиоматический минимум — как статус «Закон/Принцип» отличается от статуса «аксиома» и что именно принимается поверх CIC: Часть I, глава 6.
Действительные числа как процессы — RealProcess := nat → Q в прозе: Часть IV.
Теория множеств без аксиомы выбора — множество как система; счётность конструктивна, несчётность — правило о процессах; Шрёдер—Бернштейн и Кантор без выбора; двойная судьба самой аксиомы выбора — запрет и переинтерпретация: Часть X.
Иллюзорные конструкции ZFC — что именно теряется — и что не теряется — без её аксиом: Часть XIX, глава 6.
Граница финитизации — итоговая линия корпуса: процесс либо завершается (Element), либо доказуемо никогда (role-limit); одна граница разом — конструктивности, мощности и спектра: Часть XX, глава 1.

Ключевые результаты

Действительное число определено как процесс: RealProcess := nat → Q — последовательность рациональных приближений с условием Коши. На этом основании доказаны:

Несчётность отрезка [0, 1] — ни одно перечисление процессов Коши не покрывает отрезок (диагональ тройным делением интервалов). Print Assumptions выдаёт единственное допущение — classic: несчётность доказана без аксиомы бесконечности и без аксиомы выбора.
Теорема об экстремуме (23 Qed, 0 Admitted) — argmax определён L5-резолюцией: статус максимума назначается первой подходящей позиции (L5 назначает статусы), потому сходимость держится и на плато.
Теорема о промежуточном значении (23 Qed) — в ε-форме: для всякого ε > 0 найдётся x с |f(x)| < ε. Точный ноль над ℚ недостижим — и это не слабость, а честная граница: точного нуля над ℚ не существует.

Чего формализация не использует — и почему: поаксиомный разбор в разделе «Сравнение с ZFC» выше.

Честные границы

Принцип: граница возможного — часть результата. В статье-опоре формализация честно несла 8 недоказанных мест (Admitted) — не пробелов, а пограничных маркеров трёх родов:

ℚ-ограничение — теоремы, требующие полноты ℝ, над ℚ ложны (вложенные интервалы над ℚ могут сходиться к иррациональному — которого в ℚ нет): маркер границы ℚ/ℝ. Они не доказаны, потому что не должны быть доказуемы над ℚ.
Уровень универсумов — система типов Coq отвергает само-референтные конструкции: ошибка «Universe Inconsistency» и есть доказательство — P1 (Иерархия) принуждается типами.
Стабильность цифр — Qfloor разрывен; интервальный подход (167 Qed, 0 Admitted) вытеснил цифровой целиком.

Каждая непровалка — успех понимания. Позже все эти места закрыты — ослаблением формулировок и явными допущениями (Гейне—Борель доказан с явной гипотезой числа Лебега: над ℚ отрезок и вправду некомпактен); текущее состояние базы — 0 Admitted.

Теория Знания: карта машинной проверки

Теория Знания не только рассуждена, но и формально выведена — без единого допущения сверх самих законов логики. Ниже по темам сборки: что проверено и в каком файле каталога src/foundation/ репозитория.

Познаваемость

Познаваемость в принципе — всякое определённое разрешимо в одну из сторон: KnowledgeDistinctionGrounding.v (knowable_in_principle).
Познаваемо ≠ познано — определённость дана с вещью, а запись требует конкретного познающего: KnowledgeDistinctionGrounding.v (knowable_not_yet_known), KnowledgeSubject.v (knowable_not_known_witness).
Знать — значит уладить различение — атомы знания суть законы первичного Различения: KnowledgeDistinctionGrounding.v (knowledge_is_distinction), заземлено в Distinction.v.
Корень и синтез ветви — одна граница (обучаемое = финитизируемое = конструируемое, KnowledgeFinitization.v), одна диагональ (необучаемое = неразрешимое = несчётное — одна инстанция теоремы Ловера, KnowledgeDiagonalBridge.v: Кантор = остановка = Гёдель), карта четырёх столпов как одного (KnowledgeSynthesis.v).

Знание

Лестница данные → информация → запись — водораздел двойствен по носителю: данные несёт источник, информация добавляет свидетеля: KnowledgeInformation.v.
Знание-о и его источники — знание-о источено из присутствия (извне или изнутри; изнутри — знание-как); передача — вторых рук, дистиллят; встреча необходима: KnowledgeSourceOrder.v.
Знание-как есть процесс и несводимо — за всякой стадией есть следующая, шага «пройдено всё» нет: KnowledgeProcess.v (as_object_fails); разрыв расходится без предела: KnowledgeGap.v (deficit_diverges); умение не сводится к своду фактов (регресс Райла): KnowledgeIrreversible.v (how_underdetermined_by_that).
Зазор: догнать нельзя по построению — теорема о неубывающем зазоре self_deepening_gap_nondecreasing (KnowledgeGap.v): каждая новая запись открывает нового знаемого не меньше, чем закрывает, — разность «поле − срез» не убывает ни при какой скорости записи.
Фазовый переход — исход гонки решает порог: ограниченное поле запись настигает (knowledge_completes_when_bounded), необъятное даёт расходящийся разрыв (knowledge_race_phase_transition, KnowledgeGap.v); взаимодействие как ярус со следом — KnowledgeInteraction.v.
Нет завершённого свода как объекта — всеохватность по ходу есть, готового свода нет: KnowledgeProcess.v (knowledge_process_capstone, as_object_fails).

Свидетель

Свидетель — позиционная роль, не вещь — одна система может стоять по обе стороны познания: KnowledgeSubject.v (subject_is_positional, same_system_both_positions).
Конститутивное ядро — порог ≥ 1, хотя бы один канал, избирательное внимание; рефлексия и память не необходимы: KnowledgeSubject.v (minimal_subject_without_reflection).
Нет внешнего само-взгляда — познавая себя, познающий внутри системы, которую познаёт: KnowledgeSubject.v (no_external_self_view). Разбор роли — Метафизика, раздел «Свидетель как роль».

Восприятие

Считывание: данные → информация — различие становится информацией лишь для свидетеля (активное взятие, не зеркало): KnowledgeInformation.v; канал и избирательное внимание: KnowledgeSubject.v. Феноменальная сторона — фильтр, иллюзия, ожидание — эмпирическая и честно оставлена прозе (Восприятие).
Два поля, каналы и потенциал воли — данные — ступень объективного поля, информация и запись — субъективного (rung_field); перехода нет без канала (no_channel_no_transition), обозначение канала не требует, лестница без пропусков (ladder_no_skip); потенциал воли — разность полей — не падает ниже старта и не иссякает (will_inexhaustible), выделение участка возможно на всяком шаге (selection_always_possible): KnowledgeMentalField.v (27 Qed, 0 аксиом). Разбор — Метафизика, «Ментальное поле».
Модальный квадрат поля — три слоя исчерпывают свидетельствуемое (witnessable_three_layers); необходимое — в поле, но без порождающего шага (necessary_no_generating_step), порождено ровно актуализированное (generated_iff_actual); время приложимо ровно к порождённому — к необходимому неприменимо (necessary_timeless, timed_iff_generated); отрицание бытия — инволюция, крайние углы переходят друг в друга (non_being_involutive, square_extremes): KnowledgeMentalField.v.

Интуиция

Интуиция — канал знания-о, не присутствия — несёт знание-о, взятое целым; присутствие каналом не добывается: KnowledgeInsight.v (usmotrenie_is_a_that_channel).
Метод и позиция — две оси — усмотрение/дискурсия (метод) отделены от снаружи/изнутри (позиция): KnowledgeInsight.v (position_method_disentangled, both_positions_yield_that, usmotrenie_unique_up).
Целое сразу, понимание — по порядку — схватить целое можно одним актом, понять — лишь по ярусам: KnowledgeInsight.v. Полный разбор — Интуиция.

Глубина

Эффективная глубина = минимум трёх ограничителей — предмет × канал × порог: KnowledgeDepth.v; вертикаль двунаправленна (порог отказывает вниз и вверх): там же.
Пороги осваиваются по порядку — ярус не вместить, не освоив нижний: KnowledgeDepth.v (tiers_mastered_in_order).
Меж-вертикальное сравнение — частично — глобальной числовой шкалы глубины нет: KnowledgeDepthCrossVertical.v.

Вопрос

Вопрос — указывающий акт, не зазор: KnowledgeInquiry.v (question_is_pointing_not_access, gap_not_sufficient).
Кольцо поля — корректный вопрос живёт в среднем слое границы: KnowledgeInquiry.v (three_zones, well_founded_question).
Указание ≠ доступ — корректный вопрос не обещает ответа: KnowledgeInquiry.v (question_without_road, question_access_independent); при этом ответ существует и дорога конкретна: KnowledgeAnswerExists.v (answer_exists, road_is_concrete). Разбор — Вопрос.
Структура вопроса: цель · направление · основание — дефекты постановки (группа 1.A каталога) суть порча частей, классификация полна (ill_formed_classified); конститутивный порядок цель → направление → основание (complete_passed_goal); три вида цели по мере данности с закрывающими актами (closers_injective) — направление вопросов факта и решения стоит в знаемом, восполняющего — в кольце (wf_filling_on_ring); путь к ответу build → select → verify с инвариантом полярного закрытия (path_closes_polar); основание двулико — содержательное и деятельное, лица независимы (grounds_two_faces; деятельное = внимание + удержанный интерес: act_ground_needs_both): KnowledgeQuestion.v (37 Qed, 0 аксиом).
Лестница вопросов, корень, связность, этика входа — три яруса вопрошания, отвлечение вне закона (legal_two); иерархия: Источник внутри Логики (source_inside_logic), вершина самообоснована и единственна (self_grounded_unique), путь вовне конечен для всякой системы (chain_to_root), любые две точки связаны через общую мета-систему (path_via_common_meta), свод систем невозможен (no_svod_of_systems); двойственность: всё, что ответ, несёт корень, софист скрывает существующий корень (answer_has_root, sophistry_conceals); все дефекты 1.A искажают намерение и уводят с корня (all_defects_distort, defect_leaves_root); ходьба по ярусам без перескока (no_skip), поля вопросов вложены транзитивно (within_trans): KnowledgeQuestionPath.v (26 Qed, 0 аксиом).
Шкала воли и счёт сознаний — воля никогда не нуль, значений ровно два по числу статусов (will_never_zero, will_injective), seedless — минимум (seedless_minimum), возврат гарантирован (no_extinction); статус × позиция — 6 состояний свидетеля (states_complete); сознаний = различий + 1, Логика не воспринимается ни в каком опыте (consc_eq_diff_plus_one, logic_never_perceived): KnowledgeWillStatus.v (17 Qed, 0 аксиом).
Не-правда и ложь: двойной корень — не-правда — статус содержания, ложь — статус акта: тот же контент, два акт-статуса (same_content_two_acts, untruth_without_intent_not_lie); всякий акт имеет корень акта, корень содержания есть только у правды — ложь укоренена лишь как акт (lie_rooted_only_as_act); софист скрывает оба дефицита (sophistry_double_concealment); проекция законна, ложь = модальная подмена «возможное как сущее» (projection_itself_legal, substitution_dishonest); поле не портится — портится чужая запись (objective_field_undamaged); отказ уводит вектор, не стирает запись (refusal_turns_away_not_erases); поверх-структура стоит лишь пока держат — одна брешь роняет (overlay_needs_every_moment, overlay_falls_at_first_gap), правда самоносима (truth_needs_no_effort): KnowledgeTruthLie.v (21 Qed, 0 аксиом).
Лестница представления и два пути не-правды — две оси представления: связь (мнение · знание-что · понимание) × соответствие; титулы знания — успех-термины: неправое «знание» есть иллюзия знания (know_that_never_wrong, wrong_link_is_illusion); Геттиер растворён — правота без цепочки не знание, связка Менона = путь (gettier_dissolved, meno_binding); истина о потенциальном двулика — структура открыта рассуждению, наполнение без встречи даёт лишь проекцию (structure_always_open, no_meeting_only_projection); непротиворечивость — допуск, не мерило (consistency_not_truth, possibility_not_guarantee); не знающий истины может лишь замещать — потому замещение массово (ignorant_only_substitutes); искажение падает при первой непокрытой чужой встрече, замещение — при первой собственной, правда стоит без усилия (distortion_falls_at_first_gap, substitution_falls_at_own_meeting, truth_stands_free): KnowledgeTruthLadder.v (29 Qed, 0 аксиом). Разбор — глава «Правда и истина».
Вопросы × домены: цикл реализует путь — цикл доменов монотонен по ступеням пути и, свёрнутый, есть в точности полный путь build → select → verify (cycle_monotone, cycle_is_full_path); построение прежде всякого выбора, выбор прежде проверки (build_before_select, select_before_verify); решение входит в рассуждение ровно один раз — рамкой, и закрывает его воля (unique_decision_domain, will_closes_frame); проверка единственна и последняя (unique_verifier, verifier_is_last); цели формируются до всякого выбора (goals_before_every_choice); рефлексия — единственная смена предмета: путь сам становится предметом (unique_reflexive, world_before_path): KnowledgeDomainCycle.v (16 Qed, 0 аксиом).

Понимание

Порядок-источник — присутствие — корень, знание-о — сток: KnowledgeSourceOrder.v (presence_is_root, that_is_sink).
Знание-о = потерийный дистиллят встречи — дистиллят строго тоньше, встреча необходима: KnowledgeSourceOrder.v (that_is_distillate, no_meeting_no_that).
Необратимость — присутствия из пропозиции не вернуть, прохождение не свести к фактам: KnowledgeIrreversible.v (presence_underdetermined_by_that, no_section_for_distillation).
Определённость решает потерю при передаче — вполне определённое передаётся без убыли, неопределённое теряется тем больше, чем шире поле прочтений: KnowledgeDeterminacy.v (determined_transmits_losslessly, logic_lossless, indeterminate_can_lose).

Философия

Единственное формальное утверждение — что завершённой мудрости (целостности понятого) не существует как объекта — есть уже доказанное «нет завершённого свода»: KnowledgeProcess.v (as_object_fails), приложённое к мудрости (глава о философии).

Репозиторий

Весь код открыт: github.com/Horsocrates/theory-of-systems-coq. Каждое доказательство можно прочитать и проверить самостоятельно — компилятор не принимает недоказанное.

Опора: Horsocrates, Theory of Systems: A First-Principles Foundation for Mathematics (2026) — philpapers.org/rec/HORTOS.

Путь Мудрости

Проводник