2018-09-27 Формалізація Буддизму

Формалізація Буддизму

Зараз я дам вам відчути смак формальної філософії по-справжньому! А то вам може здатися, що це канал з формальної математики, а не формальної філософії. Я ж вважаю, що якщо формальна філософія не спирається на формальну математику, то гріш ціна такій формальній філософії.


 module buddhism where
 import path

Сьогодні ми будемо формалізувати поняття недвоїстості в буддизмі, яке пов'язане одразу з багатьма концепціями на рівнях Сутри, Тантри та Дзогчена: поняттям взаємозалежного виникнення та поняттям порожнечі всіх феноменів (Сутра Праджняпараміти). Класичний приклад із розчленовуванням тіла ставить питання, коли тіло перестає бути людиною-істотою, якщо від нього почати відрубувати шматки м'яса (ми буддисти любимо і лілеєм такі уявні образи-експерименти) або іншими словами, щоб відрізнити тіло від не-тіла, нам потрібен двомісний предикат (родина типів), функція, яка може ідентифікувати конректні два еклемпляри тіла. Практично йдеться про ідентифікацію двох об'єктів, тобто про звичайний тип-рівность Мартіна-Льофа.

За фреймворк візьмемо концепти Готтлоба Фреге, згідно з визначенням, концепт - це предикат над об'єктом або, іншими словами, Пі-тип Мартіна-Льофа, індексований тип, сім'я типів, тривіальне розшарування тощо. Де об'єкт x з o належить концепту, якщо сам концепт, параметризований цим об'єктом, населений p(o) : U (де p : concept o).


 concept (o: U): U
   = o -> U

Концепт p повинен надавати приклад чи контрприклад розрізнення, тобто щоб визначити тіло це чи не тіло ще, поки ми його розчленовуємо, нам потрібно як мінімум два шматки: тіло і не тіло як приклади ідентифікації. Таким чином, недвоїстість може бути представлена як рівність між усіма розшаруваннями (предекатами над об'єктами).


 nondual (o: U) (p: concept o): U
   = (x y: o) -> Path U (p x) (p y)

Отже, недвоїстість усуває різницю між прикладами і контрприкладами на примордіальному рівні мандали MLTT, тобто ідентифікує всі концепти. Сама ж ідентифікація класів об'єктів, які належать різним концептам — це умова, що стискає всі об'єкти в точку, або стягуваний простір, вершина конуса мандали MLTT, або, іншими словами, порожнеча всіх феноменів виражена як тип логічної одиниці, який містить лише один елемент.


 allpaths (o: U): U
   = (x y: o) -> Path o x y

Формулювання буддійської теореми недвоїстості, яка поширюється всі типи учнів (тупих, середніх і тямущих), може звучати так: недвоїстість концепту є спосіб ідентифікації його об'єктів. Сформулюємо цю саму теорему в інший бік: спосіб ідентифікації об'єктів задає предикат неподвоїстості концептів. Туди - ((p: concept o) -> nondual o p) -> allpaths o, Сюди - allpaths o -> ((p: concept o) -> nondual o p). І доведемо її! Як видно з сигнатур нам лише треба побудувати функцію транспорту між двома просторами шляхів: (p x) =_U (p y) і x =_o y. Скористаємося приведенням шляху до стрілки (coerce) та конгруентності (cong) з базової бібліотеки.


 forward (o:U): ((p: concept o) -> nondual o p) -> allpaths o
   = \(nd: (p: concept o) -> nondual o p) (a b: o) ->
      coerce (Path o a a) (Path o a b) (nd (\(z:o)->Path o a z) a b) (refl o a)

 backward (o:U): allpaths o -> ((p: concept o) -> nondual o p)
   = \(all: allpaths o)(p: concept o)(x y: o) -> cong o U p x y (all x y)

Як бачите, теоремка про порожнечу всіх феноменів вийшла на кілька рядків, які демонструють: 1) основи формальної філософії та швидке занурення в область математичної філософії; 2) гарний приклад до першого розділу HoTT на простір шляхів та модуль path.

[1]. Kuen-Bang Hou (Favonia), 2017, Higher-Dimensional Types in the Mechanization of Homotopy Theory https://favonia.org/files/thesis.pdf