Сейчас я дам вам почувствовать вкус формальной философии по-на | Формальна Філософія

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

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.