Склейка математики, онтологии, физики и computer science

Есть работы, которые склеивают математику, естественные (физику, химию, биологию и т.п.) науки, компьютеры, онтологию (в том числе 4D экстенсиональную), онтологию собственно математики (основания математики, foundational ontology), а также дают намётки на то, как это всё совместно развивать, а также разъясняют, почему нельзя этого делать с текущей математической классикой, унаследованной из работ 20 века. Например, работа Андрея Родина^[1] «Venus Homotopically»^[2] (2016), а также его разбор естественнонаучной программы Владимира Воеводского «Voevodsky's Unachieved Project» (2020)^[3].

В этих работах объясняется, что логика первого порядка, которая традиционно используется как foundational ontology для выражения объектов и отношений в онтологической работе, оказывается не самым фундаментальным способом выражать математические объекты, особенно если помнить про то, что в какой-то момент эти математические объекты будут использованы для утверждений о физическом мире. Вместо идеи о множествах как коллекциях каких-то других объектов и построения логики на этих «алгебраических» основаниях более фундаментальной оказывается идея геометрическая: минимальным объектом объявляется точка, затем точка рассматривается в пространстве и становятся возможными утверждения (пропозиции), и только потом на базе этих пропозиций мы формулируем утверждения теории множеств.

В качестве примера тут берётся Венера, которая в некоторых странах называется Утренней звездой, а в некоторых странах называется Вечерней звездой. Отождествление объектов, обозначаемых терминами Венера и Утренняя звезда, а также Венера и Вечерняя звезда решается семантикой (в статьях отсылка идёт к «лингвистике», это вопрос языка, знаковой системы — каким знаком обозначаем объект). А вот для отождествления Утренней звезды и Вечерней звезды нужна более сложная операция, включающая какие-то доказательства, понимаемые как вычисления/математические выкладки/выполнение компьютерной программы. У нас есть «какой-то объект», который скрывается за горизонтом, а потом вдруг выплывает из-за горизонта, или наблюдается в другом месте планеты — и как узнать, это новый объект, или тот же самый объект? Даже Солнце, которое каждый день восходит почти в одном и том же месте — это одно и то же физическое Солнце, или каждый раз новое?

Тем самым управление вниманием к физическим объектам может быть описано в терминах указания на место в пространстве, занимаемое точками объекта, а также пути, который составляют эти точки, а доказательство того, что мы наблюдаем тот же самый объект, который просто прошёл некоторый путь в многомерном пространстве (возможно, более чем трёхмерном, или даже четырёхмерном пространстве-времени) ведётся в этих геометрических, или как об этом говорят математики, гомотопических терминах. Основная аксиома, которая позволяет обсуждать такую эквивалентность как «типы» (тигр и мышь в каком-то смысле эквивалентны/одинаковы/равноценны, ибо принадлежат к одному типу, Утренняя и Вечерняя звезда — эквивалентны/одинаковы, и дальше можно говорить об отнесении этой эквивалентности к эквивалентным термам/лексическим единицам разговора об объектах) — это унивалентная аксиома^[4], предложенная Владимиром Воеводским в 2006-2007 годах. На этой аксиоме и ряде других выстраиваются унивалентные основания математики^[5] примерно так же, как на базе аксиом были выстроены основания геометрии Евклида, его труд так и назывался «Начала/основания/elements/foundations геометрии»^[6].

Статья М.Атья более чем двадцатилетней давности (2000 год) про перспективы развития математики «Математика в двадцатом веке»^[7] говорит о теме многомасштабности (переход от локальных «бесконечно малых» к крупмномасштабным описаниям) и ведущей в этой теме роли топологии, а ещё про повышение размерности до бесконечных, переходе от коммутативного к некоммутативному умножению (квантовая физика вся на этом), переход от линейного к нелинейному (и там тоже примеры из физики), и главная тема дихотомии в математике: геометрия с поддержкой физики как описания законов природы против алгебры с целью создания «алгебраической машины». Вот Арнольд поддерживает геометрическую традицию, а Бурбаки — алгебру.

Атья пишет как раз про особенности мышления, которые поддерживают эти две «большие традиции»: геометрия (размерность) связана с пространством, а алгебра (последовательность операций) связана со временем. Чтобы описывать что-то связанное с пространством и временем, нужно использовать и геометрическое описание, и алгебраическое. И вот это уже очень близко к тому, что я хотел бы обсуждать в части общематематического (для всех, а не для профессиональных математиков!) образования. Для меня это та же линия обсуждения разницы 3D и 4D в онтологических описаниях^[8]: описания мира в 3D были статичными-геометричными, а добавка их изменчивости как «последовательности состояний» вроде должна была давать «алгебраичность», компьютерную последовательность операций, но пока 4D онтологии (выражаемые, впрочем, как и 3D онтологии обычно в насквозь алгебраичной FOL как knowledge graph^[9]) не очень распространены. В любом случае эти ходы от «пространств с возможными состояниями» к «последовательностям состояний» можно описывать как ходы на синтез «геометрии» и «алгебры».

Та же весьма и весьма условная линия может быть в различении членораздельного (алгебраического, «западного») и голографического (геометрического, «восточного») в социологии в работе Вячеслава Широнина (2016 год) и даже в глубоком обучении (представление многомерных пространств в нейросетях как «геометрическое» и символьное текстовое представление как «алгебраическое»)^[10]. Та же линия в работах Владимира Мартынова по линии различения «письменной музыки» как «геометрической» и «аудиального джаза» с приматом развёртки во времени как «алгеброической» для джазовой импровизационной безнотной традиции^[11] (хотя что-то подсказывает, что тут это противопоставление геометрии и алгебры как работы с пространством и временем может сломаться — ибо тексты-нотации обычно оказываются как раз алгебраическими, а не геометрическими по природе своей), но всё одно интересно подумать и в этом направлении — мы же ищем универсальные различения, помогающие думать. Сюда же я бы добавил «The geometry of musical rhythm. What makes a good rhythm good» by Godfried T. Toussaint (2020)^[12], и обзор 2017 года по связи ритма и движения^[13].

В том числе Атья говорит об алгебраике как об искушении Фауста: отказаться от геометрической интуиции и надеяться на «алгебраическую машинку» — это продать душу дьяволу. И (это ещё 20 лет назад!) признание того, что наибольший вклад в собственно математику внесла квантовая теория поля, идущая от физиков^[14]. И вот прогноз на 21 век (можно поглядеть, как он выполняется, уже ведь 22% прошло от 21 века): «XXI век может стать эпохой квантовой математики или, если угодно, бесконечномерной математики». При этом суть математики по Атья в том, что «найдены вполне строгие доказательства всех тех замечательных фактов, о которых размышляли физики».

Подход к унификации математики на чисто алгебраических принципах (основания математики от Бурбаки^[15] по опоре всей математики на теорию множеств Цермело как самую базовую математическую идею, из которой можно вывести все остальные положения математики) в конечном итоге провалился, искушение Фауста не сработало. Математика, как её описывали Бурбаки, оказалась не в состоянии описать многие интересные типы объектов топологии, ибо оперировала с уже довольно крупными/составными объектами, «множествами», а не более мелкими, как «точка». Стало понятно, что аксиоматический подход с описывающими геометрически задаваемые объекты аксиомами надо объединять с алгебраическими идеями конструктивизма. В конструктивной математике математический объект считается понятым, когда понятен способ его построения/конструирования из более мелких, и этот способ можно считать вычислением согласно доказательству или компьютерной программе на языке, способном записывать доказательства. Компьютерные системы, в которых возможны доказательства, были созданы^[16] — и хотя они оказались крайне сложны в использовании, тем не менее появился способ использовать компьютер для проверки математических доказательств, и это «алгебраический способ работы с основанными на геометрии понятиями», синтез двух разных математических подходов в самом основании математики.

Традиционно математики работают с «неформальными доказательствами», которые напоминают, скорее, «псевдокод», чем формальную компьютерную программу, которая может быть исполнена на каком-то вычислителе. Системы проверки доказательств, подразумевающие формальную запись доказательств и затем компьютерную проверку этих доказательств должны давать гарантии в том, что математическое знание согласовано между собой, то есть там нет ошибок. Ибо если в каком-то доказательстве ошибка, а на результаты такой работы ссылаются другие математики, то и эти работы становятся ошибочными, на них нельзя опереться. Поэтому кроме формальной теории типов, базирующейся на унивалентных основаниях математики, предлагается неформальная теория типов^[17], в рамках которой доказательства пишут «как обычно, неформально», но в которой в случае затруднений легко провести формализацию и затем проверить результат формализации компьютером.

Тем самым унивалентные основания математики позволяют:

• Работать с доказательствами по практически всем типам математических объектов, которые были «невидимы» для предыдущих формальных/логических теорий. Грубо говоря, предложены кирпичи, которые позволяют описывать не только прямые стены, но и стены самых разных форм: переход к более мелким объектам даёт дополнительную выразительность. Тем самым через переформулирование в терминах более мелких объектов можно связывать между собой результаты в самых разных областях математики.
• Предотвращать ошибки за счёт использования компьютеров для доказательств.
• Обсуждать онтологические проблемы, в том числе проблемы задания объектов в физическом мире (базисные понятия геометричны, они связаны с обсуждением широко понимаемых форм/shapes, поэтому задействуют геометрическую интуицию, неотъемлемо присущую интеллекту, см. идеи Chollet^[18]. В том числе легко решаются проблемы типа «отождествить Утреннюю и Вечернюю звёзды»).
• Удобно стыковать основания математики (нужны для надёжного описания формализма), основной корпус идей «чистой математики» (придумывание новых типов математических объектов, которые обладают интересным нетривиальным поведением) и прикладную математику, которая после отождествления каких-то математических объектов с физическими объектами в плане поведения (то есть после моделирования) позволяет провести вычисление над математическими объектами для того, чтобы предсказать поведение физических объектов.

Теория типов даёт машинку «исчисления» (вычислений) как синтаксис, а теория категорий придаёт смысл теории типов (семантика) — что и для чего вычислять, там дуализм синтаксиса и семантики^[19].

---

1. https://philomatica.org ↩︎

2. https://philomatica.org/wp-content/uploads/2013/01/vh3.pdf ↩︎

3. https://arxiv.org/abs/2012.01150, слайды и видео рассказа от декабря 2022, https://philomatica.org/2022/12/univalent-foundations-and-applied-mathematics/ ↩︎

4. https://ncatlab.org/nlab/show/univalence+axiom ↩︎

5. https://ncatlab.org/nlab/show/univalent+foundations+for+mathematics ↩︎

6. https://ru.wikipedia.org/wiki/Начала_(Евклид) ↩︎

7. http://www.mccme.ru/free-books/matpros/i8005024.pdf.zip ↩︎

8. The simplification in integration architecture that 4D supports https://gateway.newton.ac.uk/sites/default/files/asset/doc/2105/Ian Bailey.pdf ↩︎

9. https://en.wikipedia.org/wiki/Knowledge_graph ↩︎

10. https://ailev.livejournal.com/1281819.html ↩︎

11. https://polit.ru/article/2007/10/05/martynov/ ↩︎

12. https://disk.yandex.ru/i/1nkR_3XD6xUlMg ↩︎

13. https://disk.yandex.ru/i/d_qwMqXLReRIlw ↩︎

14. https://disk.yandex.ru/d/WbIxH66UCgQfRw ↩︎

15. https://ru.wikipedia.org/wiki/Никола_Бурбаки ↩︎

16. https://coq.inria.fr/, https://en.wikipedia.org/wiki/Agda_(programming_language) ↩︎

17. https://planetmath.org/informaltypetheory, и такие тексты, как "свобода от логики", https://golem.ph.utexas.edu/category/2012/11/freedom_from_logic.html, traditional mathematics is usually written in natural language (with some additional helpful symbols), but in a way that all mathematicians can nevertheless recognize as “sufficiently rigorous” — and it’s generally understood that anyone willing to undertake the tedium could fully formalize it in a formal system like material set theory, structural set theory, or extensional type theory. By analogy, therefore, we would like an “informal” way to write mathematics in natural language which we can all agree could be fully formalized in homotopy type theory, by anyone willing to undertake the tedium. ↩︎

18. On the Measure of Intelligence, https://arxiv.org/abs/1911.01547, 2019 ↩︎

19. https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory ↩︎