Формальна Філософія

2022-02-13 15:02:41 https://tonpa.guru/stream/2022/2022-01-17%20Anders.htm Відкрити / Коментувати

2020-03-25 00:14:12 https://tonpa.guru/stream/2020/2020-03-24%20Modal%20Homotopy%20Type%20Theory.htm Відкрити / Коментувати

2019-07-25 03:43:42 https://tonpa.guru/stream/2019/2019-07-24%20Психофизическое%20расслоение.htm Відкрити / Коментувати

2018-09-29 08:31:55 Немного разбавлю стрим безумного монаха своей шизофренией. Идея классификации сознания по себе является очень значимой и обсуждаемой темой для философов всех времен. Я в свою очередь чувствую огромное подавление при какой-либо попытке написать этот пост со стороны интенсивности дифференциации той информации, которую я сам же и хочу преподнести. Дабы не раскидываться termes d’arts, начнём с точки зрения квантового психоанализа, т.к. эта тема будет чаще всего проявляться в дальнейших исследованиях, которую также не получится умалкивать в любом случае. Я постараюсь не ограничивать читателей копенгангенской (самой распиливаемой) интерпретацией (ведь с многомировой теорией Эверетта мы можем доказать квантовое бессмертие!). Ее цель также предоставлять фреймворк собственного поведения как траектория, позволяющая реализировать единый разум (что в данном контексте называем Гиперкосмическим Богом, отдельный пост о котором слишком крутой, чтобы его увидели остальные), сознание (Разум Будды, Тихе, Аннутара). Такие парадоксы как квантовая запутанность, нелокальность, ЭПР и наблюдателя играют очень важную роль в понимании тамошнего. И без того было очень бурное обсуждение в научной сфере о квантовой структуре сознания, однако пришли к выводу, что самоопределение системы более-менее стабильно чтобы можно было утверждать о неизвестных происхождениях самоосознанности. Было доказано, что мы не можем полностью вычислить состояние квантовой системы (отличный пример перспективы Йонеды, которая гласит, что любой объект определяется только благодаря его взаимоотношениям, id est сами объекты мы можем опустить и оставить одни взаимоотношения, что само по себе есть концепция естественности, что есть основное достижение теории категорий и то главное переосмысление математиков ХХ века, о котором напишу пост в другом канале когда-нибудь) не теряя о ней информацию. Собственно и вселенную определяют не люди, а единый гиперкосмический наблюдатель, дающий нам только почву для размышлений. В эклектическое время подобная имманентность и независимость от времени была хорошо отображена на триптихе, который сам по себе есть прообраз современного интерфейса. Где на иконе внутри триптиха изображён тот наблюдатель, с точки зрения которого и нарисован весь сюжет? Он дисперсен и рассеян по полотну так, что с любой точки можно было бы предположить его существование — почему объекты, отображённые на иконе имеют тенденцию увеличиваться по мере их отдаления от потенциального наблюдателя? Стоит также помнить, что сложность встречи с сакральным заключается в том, что оно не требует поиска вовне и вовсе. Оно требует сделать шаг, длиною с жизнь, ему навстречу. В чем заключается сея причина этого вижения? Подпитка собственного чсв? Высший гнозис? Тот, кто возносится — не сталкивается с сакральным напрямую, что бы ему ни казалось. Когда действительно сталкиваешься с потоками, они сами снимают вуаль самомнения и проявляют собой, что и оно — не такое, как ты ожидал, и ты — не велик или ничтожен, а просто такой, какой есть, и полно в тебе море несоответствий ему и самому себе. Відкрити / Коментувати

2018-09-29 07:19:50 Где R — это модель вещественной прямой. Еще его называют фундаментальный инфинити групоид. Обратный оператор (бемоль или флэт модалити) соотвественно переводит из гомотопического определения (для чего HoTT и была придумана) в теоретико-множественное определение, наделяя это множество топологией, заданной покрытием, сформированным из гомотопической информации по HIT типу (или другими словами на основе его гомогенной структуры композиции). Если представить бемоль в теории типов, то ничего интересного не получится, так как это будет просто коиндуктивный процесс ретопологизации:

data flat (A: U)
= con (x: flat A)

flatInd (A: U) (C: flat A -> U)
(f: (u: flat A) -> C (con u))
: (x: flat A) -> C x
= split con x -> f x

Один из примеров связующих топосов — это категории рефлексивных графов, как предпучок над категорией множеств. Если G — такой граф, то shape(G) — это граф компонентной связности G, flat(G) — это граф с теми же вершинами, что G, но только лишь с рефлексивными стрелками, sharp(G) — это полная сеть на множестве вершин графа G.

Теперь перейдем к дифференциальной геометории и тройке сопряженным модальных операторов связующего дифференциального топоса:

re (coerflection) ⊣ im (reflection) ⊣ etale.

Средний модальный оператор — это коредукция, стек де Рама, или инфинитезимальная форма, она позволяет моделироват бесконечно-малые окресности вокруг точек, скрывая комонадические вычисления за 5 аксиомами теории типов: формация, интро, элиминатор, бета и эта правила. С ее помощью мы будем моделировать картановую геометрию в HoTT в следующих выпусках.

Im : U -> U
ImUnit (A: U) : A -> Im A
isCoreduced (A:U): U = isEquiv A (Im A) (ImUnit A)
ImCoreduced (A:U): isCoreduced (Im A)
ImRecursion (A B: U) (c: isCoreduced B) (f: A -> B) : Im A -> B

Про связующие топосы вы можете почитать в работах Уильяма Ловера, Майкла Шульмана, Урса Шрайбера, Феликса Веллена, Дэна Ликаты. Последние два также есть на youtube. Відкрити / Коментувати

2018-09-29 07:19:50 Для тех, кто попал сюда случайно, хочу напомнить, что необходимый прекурсор для этого журнала — "перинатальная топология" t.me/systemflow. Я и сам хотел всё это писать, но поскольку Адам, очевидно, ориентируется в математике лучше меня, оставляю для себя возможность писать более прозаически, помня о том, что большинство термов, про которые я говорю, находятся в репозитории groupoid/infinity. Желающие формальных определений могут уже ознакомиться с основами математики и программирования в виде 10 выпусков о гомотопической теории типов на сайте groupoid.space. Пока сформированы только 3 выпуска: 1-й (MLTT), 3-й (HoTT) и 8-й (Topoi). Почему я про них вспомнил, потому что сегодня речь пойдет о cohesive (связующих модальных) топосах, как важном расширении теории типов вообще и гомотопической теории типов в частности. Про cohesive топосы вы можете также прочитать у Адама в "перинатальной топологии", я же расширю это видение, чтобы читатель мог заняться компаративистикой, ведь два источника всегда лучше чем один!

Связующие модальные топосы были придуманы Ловером, как мощное средство построения сопряженных преобразований между теориями. Вообще, топосы — это про соединение категорной и топологической информации. Если быть формальным, то связанный топос — это геометрический морфизм, который генерирует сопряженную тройку модальных операторов

∫ (shape) ⊣ ♭(flat) ⊣ # (sharp).

Геометрический мортфизм — это пара функторов между категориями пучков, пучек — это предпучек с сайтом Гротендика, сайт Гротендика — это запакованная модель топологии через покрытия (я встречал в литературе три модели).

Co (C: precategory) (cod: carrier C) : U
= (dom: carrier C) ∗ (hom C dom cod)

Delta (C: precategory) (d: carrier C) : U
= (index: U) ∗ (index −> Co C d)

Coverage (C: precategory ): U
= (cod: carrier C)
∗ (fam: Delta C cod)
∗ (coverings: carrier C −> Delta C cod −> U)
∗ (coverings cod fam)

Предпучек — это просто функтор из обратной категории в категорию множеств! Тут впервые можно упомянуть зоопарк теорий множеств. Я же советую ознакомится только с тремя теориями множеств: ZFC, NBG, ETCS. Последняя теория — это категорная модель теории множеств построенная самим Ловером, чтобы пальцами можно было поводить по коммутативных диаграммах и показать что всё аксиомы теории множеств берутся из топоса.

site (C: precategory ): U
= (C: precategory )
∗ Coverage C

presheaf (C: precategory ): U
= catfunctor (opCat C) Set

sheaf (C: precategory ): U
= (S: site C)
∗ presheaf S.1

Дифференциальный связующий топос — это топос с двумя такими сопряженными тройками. Если первая тройка относится к алгебраической топологии, то вторая тройка модальных операторов относится к дифференциальной геометрии. Левый модальный оператор первой тройки, shape модалити оператор, переводит теоретико-множественные геометрические места точек (например, для S^1 =_{SET} { (x,y) \in R \times R \| x^2 + y^2 = 1} ) в гомотопическую информацию (для окружности, например, S^1 =_{HIT} { base : S^1, loop: base = base }. Таким образом, можно сказать, что шейп оператор делает из множества групоид, вытаскивая информацию о группах из топологии покрытий, которая находится в топосах. Вот как в HoTT выглядит определение этого оператора и его рекурсор:

data shape (A: U)
= sig' (_: A)
| kap (_: R -> shape A)
| kap' (_: R -> shape A)

shapeRec (A B: U) (f: A -> B)
(k: (R -> B) -> B)
(k': (R -> B) -> B)
(p1': (g: R -> B) (x: R) -> Path B (g x) (k g))
(p2': (x: B) -> Path B x (k' (\(_:R) -> x)))
: shape A -> B = split
sig' a -> f a
kap g -> k (\(x:R) -> shapeRec A B f k k' p1' p2' (g x))
kap' g -> k' (\(x:R) -> shapeRec A B f k k' p1' p2' (g x)) Відкрити / Коментувати

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

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. Відкрити / Коментувати

2018-09-25 16:02:50 Вообще у теории симплициальных множеств есть много изоморфизмов: теория инфинити категорий (сразу несколько моделей, квазикатегории, о них пойдет речь в следующих постах), теория струн, и т.д. Обеспечение открытого бесконечного глобулярного (n-размерного) когерентного (аналог композиции на n-уровнях) пространства — чистая геометрия. Вообще в геометрию мы выходим всегда если что-то обобщаем на бесконечности. Например в теоретической информатике, а именно теории типов — у нас есть два раздела: теория типов и их полиномиальные функторы (обычные индуктивные типы) с одной стороны, и, с другой стороны — гомотопическая теория типов (где есть глобулярные равенства, благодаря выброшенному эта-правилу Id типа) и их высших индуктивных типов (или CW-комплексов, так как любой CW-комплекс можно выразить через HIT и наоборот). Відкрити / Коментувати

2018-09-25 15:45:30 Возьмем человеческий мозг. Пускай каждый нейрон — это вершина симплициального комплекса (триангулированного пространства), даже не комплекса, а симплициального множества (тоже что комплекс, только с информацией об ориентации, тут ориентация — это категорная дуальность, переворачивание n-стрелок), так как разница потенциалов передается по дендрону от нейрона к нейрону в определенном направлении. Берем радиоактивные изотопы (лучше всего взять помеченый ЛСД), пропускаем через энцефалический барьер и строим симплициальный комплекс. Почему мы взяли симплициальные множества, а не направленные графы, потому что группы нейронов образуют сгустки, в которых энергия связи настольно сильная, что можно говорить об компактности клеток на n-уровнях. Если попытаться сгенерировать рендомный мозг, на основе статистических данных, то мы получим симплициальный комплекс размерности 3 (три) в среднем. Если же мы возьмем ожидание размерности по реальным конкретным мозгам, то мы получим число измерений комплекса равным приблизительно 8 (восьми). Привет Калаби Яу, Слоения Хопфа и Е8. Моделирование нейросетей многомерными комплексами это маст хев современного теоретического АI, как в симуляции (медицине), так и в прикладном моделировании. В компьютер вижине уже, кстати, во всю. Критерий Сохацкого: если комплекс нейросети имеет размерность меньше 8, ожидать самозарожденного АI там глупо. В процессе обучения мы сможем наблюдать изменение комплекса в реальном времени и возможно даже повышение размерностей. Відкрити / Коментувати

2018-09-13 23:07:53 Вообще хорошая модель мышления, мне думается, должна содержать все основные аспекты математики, из которых я перечислил только три основные глубины (в духе старой школы). Ясно, что такая планка формальной философии будет взята не скоро, а жизнь наша быстротечна и коротка как последний день бархатного сезона. Поэтому, в рамках концепции накопления полезного знания, которое может пригодится для формальных художников будушего, мы можем оцифровывать основные идеи или модели эзотерического знания, чисто для того, чтобы убедится в том что они или: 1) примитивны или шизофреничны до комичности, тем не менее являются инсайтами большого мета-существа; 2) действительно содержат некие глубокие паттерны, которые содержат в себе исключительные объекты и законы абстракции, которые смогут пригодится или быть интересными. Відкрити / Коментувати