Предыдущий:
https://2ch.hk/math/res/109635.html (М)
Что за дебил шапку писал?
Очевидный конструктивный петух, как и все треды до этого. Предлагаю в этот раз создать альтернативный непетушиный тред оснований, а петушню бойкотировать.
Это тред тусовочки из какой-нибудь конфы, или тут могут накидать литературы для общего развития?
для общего развития можно и школьные учебники почитать (ну, без шуток, какую-нибудь биологию для продвинутых классов), так что конкретизируй
>накидать литературы для общего развития
https://libgen.rs/book/index.php?md5=DB5FD04D3AB9ECD89E5CFB7A2A9D0268
https://homotopytypetheory.org/book/
https://groupoid.github.io/formal.one/
Спасибо
>>2873
>так что конкретизируй
Ну вот в заголовке висит:
"Дежурное напоминание - абстракция не может быть первичнее примеров, содержащих абстрагируемое свойство, а метаязык строится только над объектным языком, и так же не может быть первичнее него". Это что-то из теории моделей или что это?
> "Дежурное напоминание - абстракция не может быть первичнее примеров, содержащих абстрагируемое свойство, а метаязык строится только над объектным языком, и так же не может быть первичнее него". Это что-то из теории моделей или что это?
Это базовые свойства абстракции и метаязыка как явлений. Один из местных клоунов, известный как N петух, просто игнорирует эти моменты в своих жалких попытках "доказать", что аксиомы Пеано якобы не определяют множество натуральных чисел. Вычитал он это у Успенского, в целом там логика уровня того мультфильма про олимпиаду, где "баба Яга против", а вся "аргументация" строится на игнорировании сути абстракции и метаязыка.
Все ZFC-шные множества в такой теории оказываются деревьями (из-за фундированности). Но теория Aczel'а этими множествами не ограничивается и постулирует, что любой связный ориентированный граф является картинкой какого-нибудь множества. В том числе - граф с циклами.
Например, граф, состоящий из одной точки и висящей в ней петельки является картинкой множества x = {x}.
Такая теория множеств оказывается неожиданно интересной и вполне согласующейся со здравым смыслом. Поэтому интерес рассматривать анти-фундированные множества есть. И не стоит всегда предполагать, что x и {x,y} - разные множества априори.
Снова в шапку забыл закинуть картинку, характерезующую тред... Плохой перекат.
Общее развитие продвигается полным ходом.
>Это что-то из теории моделей или что это?
это просто какое-то околоматематическое ШУЕ, как по ссылке https://groupoid.github.io/formal.one/ из >>2878, такое нужно игнорировать
Это ДРУГОЕ!!!111 Да и вообще, было бы странно ожидать чего-то содержательного от деятеля, который мало того, что не знал разницы между конструктивизмом и ультрафинитизмом, так ещё и пытался перемагивать первое вторым. Интересно, с Успенским они вместе выступали на одной сцене? Биба и Боба - два великих математика.
не знаю, не хочется смотреть часовое видео по ссылке от тех, кто рекомендует почитать Сохацкого
Как минимум, он на голову выше всяких совковых образованцев, на которых тут дрочат, и которые в математику пошли ради того, чтобы на завод не погнали. Ты просто вслушайся, что несёт деятель с видоса >>2891 про связь текста и математики, это же полный пиздец. Ну можно же было что-то в тему почитать, ладно, я не говорю про Скиннера, там букв много и они нерусские какие-то, но зачем придумывать какую-то хуйню из головы? Ну просто скажи, что не знаешь темы. Но нет, надо с умным видом кринжа наваливать, профессор же типа. А потом всякие N петухи этой шизой индоктринируются и серят здесь годами.
Кто индоктринировал тебя, конструктивный петух?
>Как минимум, он на голову выше всяких совковых образованцев
Он полуграмотный шарлатан, который разводит неопытных, что не могут самостоятельно увидеть в его писанине грубые ошибки, о чём уже неоднократно писали, но ты упрямо продолжаешь пиарить разводилу.
> Он полуграмотный шарлатан,
До вышеупомянутых деятелей в вопросах ШУЕ ему очень далеко, тем не менее.
Если есть кто-то хуже, это не повод пиарить шарлатана.
> неопытных, что не могут самостоятельно увидеть в его писанине грубые ошибки,
Их там и нет. Пример ты все равно не приведешь, даже один.
> о чём уже неоднократно писали
Кто-то что-то пукнул без единого пруфа.
Наверное нужно указать, что он эти свои тексты не публиковал, а при распространении среди своих студентов просил их дальше не рассылать. Они совершенно точно имеют элемент преувеличения с художественной целью и троллинга в целом, что довольно трудно не заметить при чтении.
>Кто-то что-то пукнул без единого пруфа.
Ага, здрасьте, приехали, уже забыл что ли?
>Их там и нет. Пример ты все равно не приведешь, даже один.
Открываю https://groupoid.github.io/formal.one/, кликаю по ссылке «Математичні компоненти» (https://groupoid.space/misc/library/), смотрю в его «определение» «inf_grpd» и тихо охуеваю от полного непонимания им темы (даже в HoTT-буке есть про ∞-усечённые типы).
В обмен на твой анус только потом не жалуйся могу на его любимом cubicaltt пруф написать, что этот его inf_grpd эквивалентен стягиваемости (isContr, лол!) типа. И это только самое дегенеративное, что вспомнилось сходу.
>>2907
>что он эти свои тексты не публиковал
https://www.researchgate.net/profile/Maksym-Sokhatskyi-2#publications
>а при распространении среди своих студентов просил их дальше не рассылать
Неправда. Пруфов не будет, пруфы проёбаны.
>Они совершенно точно имеют элемент преувеличения с художественной целью и троллинга в целом
Всё так.
>что довольно трудно не заметить при чтении
Ну, как показывает практика, некоторым хоть ссы в глаза, всё конструктивная роса.
>Открываю https://groupoid.github.io/formal.one/, кликаю по ссылке «Математичні компоненти» (https://groupoid.space/misc/library/), смотрю в его «определение» «inf_grpd» и тихо охуеваю от полного непонимания им темы (даже в HoTT-буке есть про ∞-усечённые типы).
Ну так напиши ему в issue, пусть оправдывается. В чем проблема? Здесь ты максимум напугаешь N-петуха украинскими словами, опять весь тред засерит.
>Ну так напиши ему в issue, пусть оправдывается. В чем проблема?
Так это бессмысленно: он в issue прокричит что-нибудь про агентов КГБ, удалит его через пару минут и заблочит на гитхабе. Прецеденты уже были.
Тебе буквально несколько тредов назад показали, что "спектральная категория языков" это бессмысленная хуйня.
Не было такого. Разговор был о том, что идея недопилена, и все. Остальное ты сам себе напридумывал.
Как похожая типизация с разными названиями опровергает идею спектральной категории формальных мов?
Какая ещё похожая типизация с разными названими?
>идею спектральной категории формальных мов
У Сохацкого никакого вразумительного определения нет, что выяснили два треда назад.
> У Сохацкого никакого вразумительного определения нет,
Есть и определения, и код.
> что выяснили два треда назад.
Кто выяснил? Ты и твои воображаемые друзья? Они там сейчас с тобой, в одной комнате?
Это откуда? Ссылку бы принёс
Ну ё-моё, опять за старое?
>определения
Это вот эти определения, да? Что язык только с Π-питом в язык только с Σ-типом разумным образом не вкладывается не надо опять рассказывать, надеюсь?
>код
Это вот этот код? https://github.com/groupoid/anders/blob/main/lib/foundations/mltt/mltt.anders
Универсумы там найдёшь? А индуктивные типы? А как связано «Π-form» с остальной структурой, объяснишь? А «Σ-form», кстати, тоже как? Да и «=-form», впрочем.
>Кто выяснил? Ты и твои воображаемые друзья? Они там сейчас с тобой, в одной комнате?
Забыл уже всё? Так сейчас напомним.
> Это вот эти определения, да? Что язык только с Π-питом в язык только с Σ-типом разумным образом не вкладывается не надо опять рассказывать, надеюсь?
То есть, ты даже нотацию не осилил? Там нет никаких "языков только с П типом", это сокращённые названия для разных типизированных лямбд, прямо на твоей же картинке это есть. "Язык только с П типом" это PTS, pure type system Барендрегта итд. Читать бы научился для начала...
Ты чё, Сохацкий что ли? У него такая же дегенеративная манера вести дискуссии.
>Там нет никаких "языков только с П типом",
А? На первой картинке что? Как вот эту ΠΣ понимать?
А на второй картинке что такое? Зачем же в (неком) MLTT-72 в синтаксисе и Π, и Σ?
>"Язык только с П типом" это PTS, pure type system Барендрегта итд
Да, правда что ли? Таблицу (картинка 3) его же открой (где он, помимо прочего, каким-то образом связывает Σ с неким MLTT-72).
> А? На первой картинке что?
PTS это, на третьей же картинке прямо написано.
> Как вот эту ΠΣ понимать?
MLTT 72, опять же, это там прямо написано. Если и этого мало, дальше есть полная типизация.
> А на второй картинке что такое? Зачем же в (неком) MLTT-72 в синтаксисе и Π, и Σ?
Затем, что в MLTT 72 есть оба этих зависимых типа. Ты даже нотацию не понял, зато спорить зачем-то лезешь.
>PTS это, на третьей же картинке прямо написано.
ΠΣ — это PTS? Или что ты хотел сказать?
>MLTT 72, опять же, это там прямо написано.
А, так ΠΣ — это MLTT-72? Я тебе говорю: раз Сохацкий использует O_ΠΣ там, где подразумевает использование обеих конструкций (именно подразумевает, потому что никаких синтаксических деревьев он строить почему-то не хочет), то O_Σ — это, очевидно, синтаксис лишь с Σ. И, далее, где (MLTT-72) Сохацкий подразумевает использование и Π, и Σ, он пишет и O_Π, и O_Σ. Так откуда стрелки из O_Π в O_Σ?
>Затем, что в MLTT 72 есть оба этих зависимых типа.
Да, а теперь см. выше.
>Ты даже нотацию не понял, зато спорить зачем-то лезешь.
Кто тут не понял-то, ёпт?
То есть будем неудобные вопросы просто игнорировать? А с кодом-то там что, всё нормально?
Зачем ты вообще оправдываешься за этого проходимца? Лучше бы нормально в тему вкатился, чтобы не плавать в материале как Максимка, что советовали два треда назад ещё.
Могу ещё добавить, что в другом разделе (внезапно), можно найти эти самые O_Π и O_Σ, и там, оказывается, в O_Π только лишь Π-тип, а в O_Σ, да, только Σ-тип.
>Описание ко второй картинке прочитай и не неси дичь.
Там написано, что если к языку с O_Π добавить O_Σ, получится MLTT-72 (або O_ΠΣ). В чём проблема?
Вот тебе, короче говоря, заготовка: https://pastebin.com/u70gz6Dk
Заполняй отмеченное место построением обсуждаемой стрелки.
> Там написано, что если к языку с O_Π добавить O_Σ, получится MLTT-72 (або O_ΠΣ). В чём проблема?
Проблема в том, что ты требуешь стрелку из PTS не в MLTT 72, а в сигма тип, который просто добавляется к PTS для получения MLTT 72. Либо это троллинг тупостью, либо ты правда не понимаешь о чем речь вообще.
> module dvach where
> data nat
> = zero
> | succ (n : nat)
И тут N петуха порвало.
>Проблема в том, что ты требуешь стрелку из PTS не в MLTT 72, а в сигма тип, который просто добавляется к PTS для получения MLTT 72.
Ну правильно, а у Сохацкого что на пике, алло?
> Ну правильно, а у Сохацкого что на пике, алло?
У тебя часть пика. У Сохацкого там то же, что я описал, а именно, что каждая последующая мова в списке содержит в себе предыдущую.
Речь сейчас про первую часть пика (которая каким-то образом должна порождать вторую часть).
Нет, он пишет, что послідовність синтаксичних дерев (первая часть пика) генерує (!) відповідну послідовність мов програмування.
На первом пике самостоятельная послідовність (объекты + стрелки), которую и обсуждаем.
Давай все-таки не будем из контекста что-то дергать и обсуждать как вещь в себе? Там все определения приведены, читай.
Какую, блядь, вещь в себе, ты гуманитарий что ли?
Тебе Сохацкий чёрным по белому написал, что есть вот такая послідовність, а ты делаешь вид, что он такого не писал.
Возможно имеется в виду "последовательность" в таком же смысле в каком "хуй - пизда - джигурда" последовательность слов.
Да, конечно, а следом почему последовательность уже настоящая, в категории? Или там тоже?
Можно миллион оправданий придумать (зачем?), а настоящий ответ один: Максим нарисовал стрелочек, чтобы нарисовать стрелочек, чтоб пацаны зауважали; никакого глубокого смысла в этих стрелках просто нет.
Или непонятно? Мне продолжить и в https://groupoid.github.io/formal.one/ и https://github.com/groupoid/anders/ ещё перлов найти?
"A derivation in type theory is a finite tree in which each node is a valid rule of inference"
Давай. Я не понимаю чего вообще этот хохол пытается показать. Вроде выстраивает какую то мета-теорию языков в своем собственном собранном на коленке язычке. План надежный просто как швейцарские часы.
https://github.com/groupoid/anders/commit/91bc9537b1b19ef7f539f5afa67ede207690c24a#diff-325adff688f303388bbc224312d23307967c735971ccbc5627237b256fa81146R6
Вот ему понадобился вектор типов Vec (bool × U₀) three, но он, конечно, получил ошибку, потому там был «Vec (A : U) : ℕ → U», а «bool × U₀ : U₁». Чтобы исправить положение, он меняет «A : U» на «A : U₁», и получает очередную ошибку, потому что справа в определении Vec терм не в U₀. Даже не понимая, что а) вектор типов сам должен лежать в U₁, б) ℕ-iter принимает аргументы из другого универсума, он просто включает «option girard true», которое выключает различение универсумов (а также позволяет доказать ложь).
https://github.com/groupoid/anders/commit/07aaa7ce1ee975f4d755914c0901f28a8506d9b0
Вот он пытается изобрести комонадическую модальность, не понимая, что такие модальности «require changes to the judgements of the type theory» (то есть замки; о чём в статье, ссылку на которую он сам же оставил, и написано). Его «♯ A» просто эквивалентнен A.
https://github.com/groupoid/CCHM/blob/40a6e91e8e5240653b2cbb282406cfdab84f99f3/src/real.ctt#L115-L116
Вот ещё одна попытка определить комонадическую модальность. То есть это не случайность какая-то, он этот конкретный момент совсем не понимает.
https://github.com/groupoid/anders/commit/993919ad3abe82ac1d0756bac18785dcda151723
Вот он ломает собственный прувер.
https://github.com/groupoid/anders/commit/b842e71e24a32d30409641434523f60650203430
А вот он его героически чинит.
https://github.com/groupoid/anders/blob/66c592c6246da96c5f32581460142b057425faaf/lib/mathematics/categories/cartesian.anders#L10-L16
А вот как у него определения декартово замкнутая категория: стрелки есть, никаких условий на них нет.
https://github.com/groupoid/CCHM/blob/40a6e91e8e5240653b2cbb282406cfdab84f99f3/src/category.ctt#L124
Вот от не может отличить универсум от одноэлементного типа и дописывает его в конец структуры. Получается, конечно, крайне проблемное определение.
А вот ещё занимательная дискуссия с участием нашего героя: https://gist.github.com/effectfully/2e23858032b8d5dd6ca2d65d0bd7c133
https://github.com/groupoid/anders/commit/91bc9537b1b19ef7f539f5afa67ede207690c24a#diff-325adff688f303388bbc224312d23307967c735971ccbc5627237b256fa81146R6
Вот ему понадобился вектор типов Vec (bool × U₀) three, но он, конечно, получил ошибку, потому там был «Vec (A : U) : ℕ → U», а «bool × U₀ : U₁». Чтобы исправить положение, он меняет «A : U» на «A : U₁», и получает очередную ошибку, потому что справа в определении Vec терм не в U₀. Даже не понимая, что а) вектор типов сам должен лежать в U₁, б) ℕ-iter принимает аргументы из другого универсума, он просто включает «option girard true», которое выключает различение универсумов (а также позволяет доказать ложь).
https://github.com/groupoid/anders/commit/07aaa7ce1ee975f4d755914c0901f28a8506d9b0
Вот он пытается изобрести комонадическую модальность, не понимая, что такие модальности «require changes to the judgements of the type theory» (то есть замки; о чём в статье, ссылку на которую он сам же оставил, и написано). Его «♯ A» просто эквивалентнен A.
https://github.com/groupoid/CCHM/blob/40a6e91e8e5240653b2cbb282406cfdab84f99f3/src/real.ctt#L115-L116
Вот ещё одна попытка определить комонадическую модальность. То есть это не случайность какая-то, он этот конкретный момент совсем не понимает.
https://github.com/groupoid/anders/commit/993919ad3abe82ac1d0756bac18785dcda151723
Вот он ломает собственный прувер.
https://github.com/groupoid/anders/commit/b842e71e24a32d30409641434523f60650203430
А вот он его героически чинит.
https://github.com/groupoid/anders/blob/66c592c6246da96c5f32581460142b057425faaf/lib/mathematics/categories/cartesian.anders#L10-L16
А вот как у него определения декартово замкнутая категория: стрелки есть, никаких условий на них нет.
https://github.com/groupoid/CCHM/blob/40a6e91e8e5240653b2cbb282406cfdab84f99f3/src/category.ctt#L124
Вот от не может отличить универсум от одноэлементного типа и дописывает его в конец структуры. Получается, конечно, крайне проблемное определение.
А вот ещё занимательная дискуссия с участием нашего героя: https://gist.github.com/effectfully/2e23858032b8d5dd6ca2d65d0bd7c133
А вот ещё определение окружности через пустой тип, конечно же: https://github.com/groupoid/anders/commit/447eff7b6ebd5f51a3af4d2d00aa8861d082f3f5#diff-91d9514806ff2092e37976b0bf8c79e48410ea90f57143009e962e5cf82d69ecR387
Ну и вот ещё несколько раз путает U с одноэлементным типом: https://github.com/groupoid/anders/blob/66c592c6246da96c5f32581460142b057425faaf/lib/mathematics/categories/abelian.anders#L11
Чекнул их "введение в матлогику", у них "дерево вывода" это "дерево формул" с доп.условием. Но поскольку в книжице по теории типов нет введения понятия формулы, а Автор постоянно используют обороты типо we express this as\they are introduced as follow, уточняя что это всё inference по inference rule которые образуют derivation. Дерево вывода оказывается более уместней, чем дерево формул без формул.
Вот ещё в переводе HoTT book переводчик пишет «выведение» (приложение, пункт A.2). Не самый авторитетный источник, наверное, но всё же.
https://henrychern.wordpress.com/2017/11/03/%d0%b3%d0%be%d0%bc%d0%be%d1%82%d0%be%d0%bf%d0%b8%d1%87%d0%b5%d1%81%d0%ba%d0%b0%d1%8f-%d1%82%d0%b5%d0%be%d1%80%d0%b8%d1%8f-%d1%82%d0%b8%d0%bf%d0%be%d0%b2/
"Выведение" хороший вариант. Звучит естественно в контексте с древом\выводом и к тому-же укладывается в одно слово.
wSEMYSLI, KOTORYEMOGUTPRIJTIW GOLOWUPRI^TENII DANNOJKNIGI,QWLQ@TSQINTELLEKTUALXNOJSOBSTWENNOSTX@ AWTORAIOB_EKTOMAWTORSKOGOPRAWA.iHNELICENZIROWANNOE OBDUMYWANIEZAPRE]AETSQ.
Бля, зачем ты саммонил хохла, поток дерьма теперь на пару тредов не остановать :С
> инфоциган
Значение знаешь?
> сохацкий достоин моего внимания?
Думаю, нет, ведь ты у него даже нотацию не осилил.
Моя терминология предельно точна, он именно инфоциган который пиарится на хайповой теме, даже не математик а кодерок из занюханного хуторского говновузика с кафедры прикладной математики (т.е. даже ни математик ни программист).
Так какие там морфизмы между O_Π и O_Σ синтаксическими деревьями например?
Инфоциганство это не пиар на чем-то, а продажа успешного успеха в виде курсов, наставничества, гивов итп шлака. К Сохацкому можно по-разному относиться, но он не инфоциган, это факт.
Так он свою псевдонаучную хуергу продаёт под видом математики. Просто аудитория специфическая, но сути это не меняет.
Так он же успех и наставничество и продаёт. Ты его ТОПОВОГО ПРОГОММИСТА видел? А ведь ему донатили (и, вероятно, всё ещё донатят) за такое.
Хули ты боевыми картиночками кидаешься, уёбище? Где построение стрелки?
Обпучкался с пикчи.
Неплохо.
Ты дееспособный вообще? Весь код есть в anders, там смотри. Если нотацию осилишь, что маловероятно.
Я этот Anders писал, так что получше тебя знаю, где какой там код. Этой конкретной стрелки там нет.
>Где он что-то продает, поридж? Все бесплатно на гитхабе.
Ты совсем чтоли дебил? Себя продает, свои высеры.
>Из PTS в MLTT 72? Хуевый ты писатель значит.
Даже мимокроку уже понятно, что тебе говорят про стрелку из синтаксического дерева O_Π в синтаксическое дерево O_Σ.
Тебе само название "спектральная категория формальных мов" о чем-нибудь говорит? Стрелки там между формальными языками. О чем там прямо написано в определениях из главы 2.3. В общем, я тебя услышал, скибидитуалетикс, теперь уебывай
>Тебе само название "спектральная категория формальных мов" о чем-нибудь говорит?
Очевидно она говорит что автор "мов" сказочный долбоёб наципятак которому во время не дали таблеток.
Ты даже нотацию не осилил. Но долбаебом называешь не себя, что было бы правдой, а кого-то другого. Типичный пердеж
>Пруфанешь?
Оставляй фейкопочту.
>Из PTS в MLTT 72?
Из O_Π в O_Σ, ну ёпт.
>Хуевый ты писатель значит.
Я-то тут причём вообще? Я прувер писал, а не диссер Сохацкому и/или его формализацию; о наличии той или иной формализации в репозитории я могу говорить, поскольку сам прувер, стандартная библиотека к нему, а также кое-какой код Сохацкого, включая обрывочные формализации диссера, находятся в одном репозитории.
Сохацкий вообще эту, кхм, монографию о категорії формальних мов начал писать ещё до начала любых работ над Anders.
>>2991
Вообще-то речь о послідовності синтаксичних дерев (смотрим на пик), которая генерує послідовність мов, и стрелки в обсуждаемом фрагменте между деревьями/синтаксисами.
> Из O_Π в O_Σ, ну ёпт.
> Вообще-то речь о послідовності синтаксичних дерев (смотрим на пик), которая генерує послідовність мов, и стрелки в обсуждаемом фрагменте между деревьями/синтаксисами.
А где там в тексте прямо написано, что между индуктивными типами именно морфизмы в категорном смысле, а не просто отношение следования?
> То есть в одном и том же предложении одно и то же слово означает разные вещи?
Спектральная категория формальных мов прямо заявлена, а спектральная категория индуктивных типов - нет.
> Между синтаксическими деревьями.
То есть, индуктивными типами, см. визначення 23 и 24.
>а спектральная категория индуктивных типов - нет.
И стрелок между ними совсем нет, да?
>То есть, индуктивными типами, см. визначення 23 и 24.
Так это не любые индуктивные типы.
> И стрелок между ними совсем нет, да?
Так где там написано, что стрелки между индуктивными типами это морфизмы?
То есть, ты не рассматриваешь вариант, что это просто стрелочные типы функций в пределах одной мовы, содержащей эти типы?
То есть функции в cubicaltt? Заготовка выше.
>Дежурное напоминание - абстракция не может быть первичнее примеров, содержащих абстрагируемое свойство, а метаязык строится только над объектным языком, и так же не может быть первичнее него.
Зайдём с другого конца. Предположим это так, тогда на каком основании ты используешь абстракцию которую не принял как аксиому (у тебя ебанька по твоим же слоам есть только несколько конкретных примеров, тебе кто разрешал переходить к следующему примеру и т.д)? И тем более опираться на метаязык при обосновании понятий объектного языка если он вторичен? Ты ебанько задним числом математематические понятия определяешь чтоли?
> (у тебя ебанька по твоим же слоам есть только несколько конкретных примеров, тебе кто разрешал переходить к следующему примеру и т.д)?
N-петух, какой еще "переход к следующему примеру"? Аксиомы Пеано это и есть пример, содержащий абстракцию потенциальной бесконечности.
Мовный газнюх, ты в своих газах запутался или что? Сам же предлагал обосновать абстракцию (которая вторична) фиксированной серией примеров (которые в понимании твоего пропитанного газами мозга первичны). Вот тебе и вопрос, как ты ебло на одних примерах собрался с потенциально неограниченными структурами работать? Ты это технически не можешь сделать т.к. еще не ввёл "вторичную" абстракцию. Про Пеано в очередной раз в лужу пёрнул - аксиомы сами собой ничего не обосновывают, они работают только если принята абстракция потенциальной осуществимости.
Что ты трясёшься, у тебя синдром Туретта?
> аксиомы сами собой ничего не обосновывают, они работают только если принята абстракция потенциальной осуществимости.
Абстракция потенциальной осуществимости - это свойство аксиом Пеано и других подобных аксиоматик, правил построения итд. Это следует из самого определения абстракции, она не висит в воздухе, а вторична по отношению к конкретным примерам, имеющим это свойство. Тут вообще не о чем спорить итд, это элементарные вещи.
>Что ты трясёшься, у тебя синдром Туретта?
Трясу яичками по лбу твоей мамаши.
> Абстракция потенциальной осуществимости - это свойство аксиом Пеано и других подобных аксиоматик, правил построения итд. Это следует из самого определения абстракции, она не висит в воздухе, а вторична по отношению к конкретным примерам, имеющим это свойство. Тут вообще не о чем спорить итд, это элементарные вещи.
Ты через "вторичность" пытался отрицать что абстракция потенциальной осуществимости принимается как исходное неопределяемое понятие, теперь ты говоришь что всегда её предполагал (таблетки помогли?).
При её наличии натуральное число это базовый объект плюс абстракция, определение аксиомами Пеано использует ту же базу только более сложное, а поэтому нинужно. Ты или более простое определение принеси или признай себя петухом коим ты являешься.
Перечитай ещё раз оп-пост, я там все изложил, и к этому нечего добавить ни мне, ни тебе. Абстракция не может быть "исходным неопределяемым понятием", у этого термина есть общепринятое определение. Натуральное число это никакой не "базовый объект", это элемент множества. Считаю этот вопрос закрытым.
>Перечитай ещё раз оп-пост, я там все изложил, и к этому нечего добавить ни мне, ни тебе.
Там шизофазия написана, как и вся твоя писанина.
> Абстракция не может быть "исходным неопределяемым понятием"
Опять таблетки кончились, шиз? Абстракция всегда неопределяемое понятие, т.к. не сводится к элементарным вещами иначе бы это было бы обычное определение.
>Натуральное число это никакой не "базовый объект", это элемент множества.
Базовый объект это единица, а всё множество формируется из 1 на основе абстракции потенциальной осущетвимости. Аксиоматика Пеано лишь постфактум описывает построенный таким образом объект, сама по себе она ничего не определяет. Ну и как уже говорилось в принципе не может определять т.к. даже в своей формулировке опирается на абстракцию потенциальной осуществимости в метаязыке.
>Считаю этот вопрос закрытым.
Ты своё безпруфное мнение лечащим врачам изливай, всем остальным на него похую. Ты или доказательство давай или корректное определение без скрытых замкнутых кругов и прочих логических ошибок которые в твоём пиздедже на каждом шагу.
А давай-ка ты источники своей шизы приведешь. И нет, той статейкой Успенского на одностраничном сайтике типа укоз ру можешь подтереться. Конкретно:
> Абстракция всегда неопределяемое понятие,
> Базовый объект это единица, а всё множество формируется из 1 на основе абстракции потенциальной осущетвимости. Аксиоматика Пеано лишь постфактум описывает построенный таким образом объект
Где это написано? Если это хуйня из головы, так и пиши. Я приводил общепринятые определения понятия абстракции и метаязыка. Теперь ты давай пруфы, что твоя писанина это не шиза совкового скуфидона, а принятые в математике вещи.
Источник не мой, а твой. Просто ты читать не умеешь, копипастишь рандомные фрагменты не понимая что за ними стоит, зачем они вводятся и что (и при каких условиях) определяют.
Успенский хотя бы работающий математик в топовом универе, а на твоей стороне только фрики вроде мовного говнокодерка воннаби математика из провициального быдловузика для нациков в какой-то щитхол кантри, который даже матфак не осилил.
Причем тут укоз, дебил, там просто пиратская копия его книжки хостится.
Ещё про это писали как минимум Пуанкаре и Кронекер, но ты хуйло пиздливое специально как баран упёрся в одного Успенского в попытках съехать на дебильных шуточках (типа гыгы, совок успенский чета спизданул).
>Где это написано? Если это хуйня из головы, так и пиши. Я приводил общепринятые определения понятия абстракции и метаязыка.
Везде, я ж за тебя дебила не могу прочитать. Ты привёл только нерелевантуню хуйню которая вообще никак не обосновывала N, точнее скопипастил то что сам нихуя не понял.
Хуйня из больной головы это мовная шизофазия твоего протыка уёбка сохацкого.
>Теперь
Ты не одного пруфа не показал, какое блять "теперь"? Хоть за одно своё слово ответь, мразь тупая. Ты же спиздянул якобы аксиомы Пеано что-то там определяют, вот и тащи доказательства, как.
>ты давай пруфы, что твоя писанина это не шиза совкового скуфидона, а принятые в математике вещи.
Пруфы тебе даны неоднократно: 1) аксиомы Пеано формулируются как конкретная формальная система, любая ФС необходимо использует абстракцию потенциальной осуществимости. 2) Для доказательства существования множества удовлетворяющего этим аксиомам ты опять вынужден ссылаться на абстракцию осуществимости когда доберешься до аксиомы индукции.
> Ещё про это писали как минимум Пуанкаре и Кронекер,
Цитаты.
> Везде,
Ссылки где?
> Пруфы тебе даны неоднократно:
Пока что от тебя поступала только хуйня из головы.
> любая ФС необходимо использует абстракцию потенциальной осуществимости.
Неси цитаты, где ты это взял.
> 2) Для доказательства существования множества удовлетворяющего этим аксиомам ты опять вынужден ссылаться на абстракцию осуществимости когда доберешься до аксиомы индукции.
Это не пруфы, а "твое мнение". Абстракция потенциальной осуществимости это свойство, а не какая-то высшая истина, существующая вне примеров, содержащих её. По первой же ссылке в Википедии:
> https://ru.m.wikipedia.org/wiki/%D0%90%D0%B1%D1%81%D1%82%D1%80%D0%B0%D0%BA%D1%86%D0%B8%D1%8F
> Абстра́кция (лат. abstractio «отвлечение»[1]) — процесс отвлечения (абстрагирования) от тех или иных характеристик объекта для их избирательного анализа;
> обобщающая абстракция — даёт обобщённую картину явления, отвлечённую от частных отклонений. В результате такой абстракции выделяется общее свойство исследуемых объектов или явлений. Данный вид абстракции считается основным в математике и математической логике.
Нигде нет хуйни о том, что абстракция это какое-то "неопределяемое понятие", к которому нужно возноситься в молитве для определения чего-то, содержащего абстрагируемое свойство. Один из таких примеров - аксиомы Пеано.
> Thus, intuitionistically, truth is identified with provability, though of course not (because of Godel's incompleteness theorem) with derivability within any particular formal system.
Так как МЛ тогда предлагает доказать что-либо если не в формальной системе? Уверовать?
> поридж начинает подозревать, что конструктивизм чем-то неуловимо отличается от формализма, но вот чем? Сможет ли пердикс понять, в чем тут дело и почему интуиционизм со времён Брауэра рассматривался как отдельное направление в основаниях, а не как часть формализма? Продолжаем зоонаблюдения
>почему интуиционизм со времён Брауэра рассматривался как отдельное направление в основаниях, а не как часть формализма
Что бы не осквернять шизой в принципе вменяемую программу формализации математики?
Я читал Сохацкого в подлиннике.
Результаты, связанные с нашей способностью осуществлять конструктивные процессы, в математике часто формулируются в виде теорем существования, утверждающих существование объектов, удовлетворяющих таким-то требованиям.
В конструктивной математике под этим подразумевается, что построение таких объектов потенциально осуществимо, т, е.что мы владеем способом их построения.
Это конструктивное понимание теорем существования расходится с тем, как их понимают в классической математике. Правда, „классики" не любят объяснять свое понимание таких теорем. Однако из того, как они обходятся со словом «существует», следует, что их понимание этого слова отлично от конструктивного. Они, например, считают возможным утверждать, существование конструктивного объекта, удовлетворяющего данному требованию, уже тогда, когда им удается путем «приведения к нелепости» опровергнуть предположение о том, что ни один объект не удовлетворяет этому требованию. Способ построения искомого объекта может при этом и небыть известен. Таким образом, конструктивное понимание высказываний о существовании отлично от классического.
Абстракция потенциальной осуществимости позволяет нам рассуждать о сколь угодно длинных конструктивных процессах и сколь угодно больших конструктивных объектах. Их осуществимость потенциальна: они были бы осуществимы практически, располагай мы достаточными пространством, временем и материалом.
Абстракция потенциальной осуществимости, как и всякая абстракция, вносит туда, куда она привлекается, элемент фантазии. Он неизбежно присутствует во всякой абстрактной науке, в том числе и в математике. Классическая математика привлекает абстракции, идущие гораздо дальше абстракций конструктивной математики. В частности, она пользуется абстракцией актуальной бесконечности, т. е. позволяет себе рассуждать о „бесконечных множествах" как о законченных неконструктивных „объектах". Различие между „классиками" и„конструктивистами" состоит в том, что они привлекают раз-разные абстракции, т. е. фантазируют по-разному.
А что такое конструктивный процесс, и вообще процесс?
> Да и к написанному есть вопросики.
Вопросики у него есть, а. Вейп вытащи из жопы, или что ты туда засовываешь, потом хотя бы пару статей из Википедии осиль вместо тиктака. Откуда вы сюда лезете такие?
Мовный петух получает образование на википедии, лул.
Шо, у вас на хуторе универы и книжки не завезли?
-1/12
кто за конструктивизм, тот петух
все остальные — конструктивисты
>Базовый объект это единица, а всё множество формируется из 1 на основе абстракции потенциальной осущетвимости. Аксиоматика Пеано лишь постфактум описывает построенный таким образом объект, сама по себе она ничего не определяет.
Аксиоматика Пеано содержится в его труде Arithmetices principia, nova methodo exposita, его перевод на английский язык приведен в книге Selected works of Giuseppe Peano translated from the Italian (https://www.pdfdrive.com/selected-works-of-giuseppe-peano-translated-from-the-italian-e186125668.html ).
Похоже, что АП как раз-таки определяет "свойство быть числом". О бесконечности речи не идет. И если бы речь о бесконечности заходила, то бесконечность была бы актуальной. То есть существуют такие объекты, как числа, а их свойства описаны конечным набором конечных схем.
> Ну и как уже говорилось в принципе не может определять т.к. даже в своей формулировке опирается на абстракцию потенциальной осуществимости в метаязыке.
Имеется в виду возможность рассмотрения сколь угодно длинных формул? Почему бы вместо формул не рассматривать сам конечный набор конечных схем (схем правильно построенных формул), а получаемые из них формулы - считать лишь вспомогательными средствами некоего отдельного метода исследования схем? И конечно же верно, что никто никогда не может рассмотреть слишком большой набор формул, а тем более бесконечный, иначе как найдя абстрактный подход через рассмотрение вместо них заключающего их множества. Множества точно так же описываются конечным набором конечных схем. Нарушается ли финитизм где-либо в ходе таких исследований?
Проблема N петуха в том, что он не осилил определения абстракции и метаязыка в принципе. Конкретно, тот факт, что эти явления вторичны по отношению к примерам, содержащим абстрагируемое свойство и обьектному языку соответственно. Он не понимает, что абстракция не может существовать сама по себе, вне примеров, содержащих её, а метаязык может быть только надстройкой над объектным языком. Все это описано буквально на каждом углу, начиная с Википедии, однако же у N петуха какое-то "свое" (на самом деле взятое у Успенского) понимание абстракции и метаязыка. Учитывая, что там ШУЕ уровня Рыбникова и "основ православной арифметики", имеем что имеем - долбаеб вместо того чтобы хотя бы ПОПЫТаться разобраться в вопросе, с 2015(!) года серит шизой, что оказывается, аксиомы Пеано якобы не определяют множество натуральных чисел. Короче говоря, спорить там бесполезно, всё что можно сделать - тыкать дауна в общепринятые (а не ШУЕшные) определения абстракции и метаязыка.
>не осилил определения абстракции и метаязыка
>метаязык может быть только надстройкой над объектным языком
Конструшок, как тебе удается обосраться даже в совершенно очевидных понятиях и перевернуть их с ног на голову? То универсальная машина Тьюринга у тебя это обобщение МТ вообще, то вот этот бред.
Я так понимаю, возражений по существу нет? Или дальше будешь игнорировать общепринятые определения абстракции и метаязыка? Абстракция это свойство примеров, собственно и содержащих абстрагируемое свойство. Будешь с этим спорить? Зачем?
> Метаязы́к — язык, предназначенный для описания другого языка, называемого объектным языком
https://ru.m.wikipedia.org/wiki/%D0%9C%D0%B5%D1%82%D0%B0%D1%8F%D0%B7%D1%8B%D0%BA
Вот так просто, N петух. Нет объектного языка - нет и метаязыка для его описания.
> Универсальной машиной Тью́ринга называют машину Тьюринга, которая может заменить собой любую машину Тьюринга. Получив на вход программу и входные данные, она вычисляет ответ, который вычислила бы по входным данным машина Тьюринга, чья программа была дана на вход.
https://ru.m.wikipedia.org/wiki/%D0%A3%D0%BD%D0%B8%D0%B2%D0%B5%D1%80%D1%81%D0%B0%D0%BB%D1%8C%D0%BD%D0%B0%D1%8F_%D0%BC%D0%B0%D1%88%D0%B8%D0%BD%D0%B0_%D0%A2%D1%8C%D1%8E%D1%80%D0%B8%D0%BD%D0%B3%D0%B0#:~:text=%D0%A3%D0%BD%D0%B8%D0%B2%D0%B5%D1%80%D1%81%D0%B0%D0%BB%D1%8C%D0%BD%D0%BE%D0%B9%20%D0%BC%D0%B0%D1%88%D0%B8%D0%BD%D0%BE%D0%B9%20%D0%A2%D1%8C%D1%8E%CC%81%D1%80%D0%B8%D0%BD%D0%B3%D0%B0%20%D0%BD%D0%B0%D0%B7%D1%8B%D0%B2%D0%B0%D1%8E%D1%82%20%D0%BC%D0%B0%D1%88%D0%B8%D0%BD%D1%83,%D0%BF%D1%80%D0%BE%D0%B3%D1%80%D0%B0%D0%BC%D0%BC%D0%B0%20%D0%B1%D1%8B%D0%BB%D0%B0%20%D0%B4%D0%B0%D0%BD%D0%B0%20%D0%BD%D0%B0%20%D0%B2%D1%85%D0%BE%D0%B4.
А ты читать разучился, N петух? Универсальная потому так и называется, что способна заменить любой конкретный пример машины Тьюринга. Что сказать-то хотел?
Но я тебя не спрашивал кто кого может заменить, а
>Какое понятие более общее
Я вообще ору. Как с таким уровнем понимания чего либо ты можешь листать своего Браузера с Мартином-Лефом и искренне считать что ты чего то там понимаешь?
У тебя может пизда между ног, и ты на самом деле не петух и курица? Просто такой уровень отсутствия логического мышления у человека за гранью моего понимания.
>>3095
Просто проходил мимо, решил погонять тупого петуха по старым темам.
> Просто проходил мимо, решил погонять тупого петуха по старым темам.
То есть, ты не N петух? Это не проблема, и тебя вылечим. С машиной Тьюринга ты таки обосрался, так что официально обьявляешься опущенным. Возьми антистресс и проследуй к параше.
> Но я тебя не спрашивал кто кого может заменить, а
> >Какое понятие более общее
То есть, само понятие "универсальная" тебе ни о чем не говорит? Хорошо, Я тебя услышал. Универсальная машина Тьюринга - более общая потому что может заменить любой частный случай. Я на твой вопрос ответил?
>Универсальная машина Тьюринга - более общая потому что может заменить любой частный случай. Я на твой вопрос ответил?
Ну ответить ты ответил. Но пиздец, конечно, что теперь с этим делать непонятно...
Какое понятие более общее - "автомобиль" или "зеленый автомобиль"?
>The problem of too many equalities in HoTT can be understood as a problem of underspecification of the mathematical objects. N and Z as sets are isomorphic but are not if we consider them as monoids with usual addition. So, monoid of N is really the data of N together with structure and property of a monoid, which cannot be canonically isomorphic to the Z monoid.
Что скажете?
Тоже что и всегда, HOTT даже N не может определить, кому нужно такое "основание"? А всё остальное и в теории множеств нормально сидит.
> HOTT даже N не может определить,
N петух, в HoTT N определено. По абстракции потенциальной бесконечности тебя уже сто раз еблом ткнули в определение абстракции - это свойство примеров, а не наоборот.
> define succ
N петух, это отношение следования. Абстракция потенциальной бесконечности это свойство succ, но не наоборот.
А потом спрашиваешь у анонов откуда берется инъективность конструкторов и они начинают что-то невнятно блеять про теорию категорий прикрываясь первым попавшимся пейпером по coic. Тру стори.
В то, что ты Сохацкому понаписал в андерс хуйни без половины морфизмов, мы поверим. Ну, почти. Но к HoTT какие претензии? Ее поумнее тебя писали, там даже Мартин-Леф в соавторах. Чего ты там ниспровергать собрался?
> Петух, ты что тупее дошкольника?
Тупее тебя нет никого. Уебывай и свои задачки для коррекционной группы детского сада забирай. Чё вас деградантов так сюда тянет? В другом месте пердежируй, аниме
Ору с убогого. Петух не справился со школьной программой, это известно. Теперь взят новый уровень - вопросы для дошколят оказывается петуху тоже не по зубам. Что дальше? Попытка вырабатывать условные рефлексы? Кто умнее конструктивный петух или обезьяна?
> чморидж обосрался с универсальной машиной Тьюринга, теперь кукарекает на самоподдуве, пытаясь закукарекать свой обсер
Не стыдно тебе таким дебилом быть?
Потешный не может ответить на вопрос для дошкольника, но уверен что обосрался не он. Какая форма неполноценности у тебя?
>Какая форма неполноценности у тебя?
Конструктивизм в затяжной стадии. С каждым годом его интеллект всё падает и падает. В первых тредах, он ещё пытался что-то аргументировать и аватарил Брауэрем. Теперь он уже не пытается и просто срёт картинками с зумерами.
Инъективность можно получить из построения односторонней обратной или, например, возможности элиминировать в универсум повыше. Почти все, кто с DTT знаком, в курсе, но причём тут инъективность вообще?
Кто ты-то? Ты вообще не тому анону про андерс пишешь. Разберись уже, кто кому что писал, что такое этот самый Anders и какое он имеет отношение к текстам Сохацкого.
Конкретно меня интересует почему 0≠1. Потому что в аксиомах Пеано это постулируется явно, а в MLTT берется хуй знает откуда. Несколько тредов в прошлом задавал этот вопрос и получал только дрист под себя от конструктивного петуха. Потом случайно наткнулся на то что для доказательства этого факта необходим универсум.
Это все при том, что coic очень сложная система и правила ее хуй где нормально описаны. Об этом еще Воеводский говорил.
>Конкретно меня интересует почему 0≠1.
Конкретно «0 ≠ 1» вроде как называется дизъюнктивностью конструкторов, под инъективностью понимают стандартную инъективность (то есть succ(n) = succ(m) → n = m). Впрочем, это вопросы названий, конечно.
>Потому что в аксиомах Пеано это постулируется явно, а в MLTT берется хуй знает откуда. Несколько тредов в прошлом задавал этот вопрос и получал только дрист под себя от конструктивного петуха. Потом случайно наткнулся на то что для доказательства этого факта необходим универсум.
Да, нужен универсум. Стандартный аргумент такой: мы строим функцию f из ℕ в универсум U такую, что f(0) ≡ 𝟏 (одноэлементный тип), а f(succ(n)) ≡ 𝟎 (пользуясь частным случаем индукции). Теперь если у нас есть 0 = 1, то и 𝟏 ≡ f(0) = f(1) ≡ 𝟎. Потом нужно ещё применить индукцию для равенства, чтобы из 𝟏 = 𝟎 получить функцию 𝟏 → 𝟎. Ну а 𝟏 населён, откуда мы получаем элемент типа 𝟎. Сводя всё вместе, получаем импликацию 0 = 1 → 𝟎, что и есть отрицание равенства, по стандартному определению.
Вот тут ещё пишут, что без универсума «0 ≠ 1» в MLTT не выводится: https://proofassistants.stackexchange.com/a/2626/310
>дизъюнктивностью конструкторов, под инъективностью
Не спорю, но еще хотелось бы термин объединяющий эти два свойства. Особенно забавным мне кажется то что в coic это свойство подается чуть ли не как само-собой разумеющееся, в то время как в большинстве языков программирования (не функциональных) конструктор конструирует что угодно и как угодно.
Видел это доказательство, но все равно оно какой то странный привкус оставляет. Подозрительно что прувер до всего этого додумывается автоматически.
>it is well-known that Martin-Löf type theory without univeres does not prove 0≠1.
И теперь мне стало интересно кто и как это доказал. Вроде где-то видел строятся модели для этого соответствующие.
>конструктор конструирует что угодно и как угодно
Просто один и тот же термин (конструктор) в ООП и теориях типов используют для разных понятий.
>Подозрительно что прувер до всего этого додумывается автоматически.
Неудивительно, тактики как раз под такие стандартные случаи и забиты. А подозревать не в чем, например, в Lean тактики генерируют термы отдельно от ядра, ядро же проверяет только то, что тактика сгенерировала. То есть пруф от кривой тактики принят не будет. Можно даже посмотреть, какой конкретно пруф тактика сгенерировала (пик).
>И теперь мне стало интересно кто и как это доказал. Вроде где-то видел строятся модели для этого соответствующие.
Вот нагуглилось что-то: https://www.cse.chalmers.se/~smith/JSLPeano.pdf
Там вместо "означает" должно быть "увтерждает" как во втором примере суждения или чо?
Терм a имеет тип A / терм a населяет тип A / терм a является элементом типа A.
Опечатки в переводе, вот это пиздос, да, никогда такого не было.
Хм. Пока ты явно не указал, я и не заметил что там элемент является типом. Видать у меня реально низкий айкю.
Спасибо, почитаю.
Вот предельно упрощенный терм на coq который доказывает тезис. Осталось только его осмыслить как следует.
Почему используешь lean? Да еще на немецком, кек.
>Почему используешь lean?
Синтаксис приятнее (чем в Agda/Coq) кажется, метапрограммирование отличное и плагины проверяют код на лету.
>Да еще на немецком, кек.
Системная локаль.
>>The problem of too many equalities in HoTT can be understood as a problem of underspecification of the mathematical objects. N and Z as sets are isomorphic but are not if we consider them as monoids with usual addition. So, monoid of N is really the data of N together with structure and property of a monoid, which cannot be canonically isomorphic to the Z monoid.
>Что скажете?
Я не знаю особенности HoTT, но мне интересно ответить и оживить доску.
Буду считать, что цитата использует HoTT как обозначение математической теории, в которой интерпретируемы теория множеств и арифметики N и Z. То есть HoTT - особая основная теория, выступающая в основании математики и обосновывающая многие другие ее теории.
Далее, о чем идет речь?
>The problem of too many equalities in HoTT
Присутствуют отношения равенства, различающиеся между собой, что ли?
>N and Z as sets are isomorphic but are not if we consider them as monoids with usual addition
Мол, по одному изоморфизму они изоморфны, а по другому - нет?
>So, monoid of N is really the data of N together with structure and property of a monoid, which cannot be canonically isomorphic to the Z monoid.
(Будем считать, что речь идет об аддитивном моноиде.) Так ведь, насколько я понимаю, это полностью соответствует обычным результатам конвенциональной математики. В Z: a = a + (1 + [-1]). Тогда для любого f, если f - биекция из Z в N: f1 != f(-1), значит один из них ненулевой, и тогда fa != fa + f1 + f(-1), то есть никакая биекция f не является гомоморфизмом.
>Присутствуют отношения равенства, различающиеся между собой, что ли?
Да, как разные изоморфизмы.
>Мол, по одному изоморфизму они изоморфны, а по другому - нет?
Типы (ℕ и ℤ) изоморфны, структуры (то есть n-ки, тип + операция + свойства) над ними — уже нет.
>Я не знаю особенности HoTT
Может тогда не стоит отвечать?
HoTT (по видимому) предлагает считать N и Z тождественными понятиями, что противоречит интуиции и устоявшейся практике.
Странно он пишет
> Intuitively, φ(A) =⊤ means that the interpretation of the type A is a set with one element and φ(A) =⊥ means that A is interpreted as the empty set.
а потом
> φ(Eq(A, a, b)) = φ(A)
Но населенность равенства очевидно должна зависеть от того что сравнивается. Продолжу наблюдения.
В этой интерпретации любой тип либо пустой, либо одноэлементный.
В одноэлементном типе все элементы равны, причём одним образом (даже в HoTT), поэтому равенство там всегда, вне зависимости от a и b, — одноэлементный тип.
А в пустом типе чтобы Eq(A, a, b) просто построить, нужно найти a/b в нём, то есть его естественно интерпретировать как пустой тип.
То есть как раз φ(Eq(A, a, b)) = φ(A).
>причём одним образом (даже в HoTT)
А он и может быть только одним образом. Это чисто в HoTT придумали, что якобы может быть не одним образом.
Да нет, понятие равенства задолго до HoTT вызывало много вопросов. Это просто ты кроме тиктака ничего не знаешь.
>А давайте придумаем модель, где желаемое является действительным? А давайте!
Действительно, кек.
А есть какие-то богом данные модели что ли?
1) изоморфизм Карри-Говарда и тезис Чёрча;
2) содержание диссертации Брауэра в переводе Гейтинга;
3) пять уровней языка и четыре способа отрицания по Маннури;
4) интерпретацию логических констант по Брауэру-Гейтингу-Колмогорову;
5) теорию статистического обучения Вапника и модель spikgram Миколова;
6) отличия машины Тьюринга от машины Поста.
Конструктивист обязан:
1) отрицать закон исключённого третьего;
2) отрицать любую математику, не выразимую через типизированную лямбду в MLTT или нормальные алгорифмы Маркова;
3) переписать на прувере AUTOMATH де Брауна книгу "Основы математического анализа" Ландау;
4) представить все формальные теории в терминах алфавитов, термов и манипуляций с ними;
5) свести гомологическую алгебру к исчислению предикатов, используя нумерацию Гёделя.
Ну придумали же множества. Оказалось полезным.
Про алгтоп целая восьмая глава.
>>3258
HoTT+аксиома выбора+универсум (вроде как) взаимно интерпретируема с ZFC+недостижимые кардиналы, так что всё, что можно сделать в "стандартной" математике, можно сделать и в HoTT. Требовать "определение пучка в HoTT" это то же самое, что требовать "определение пучка в ZFC".
И вообще, практически для всей математики (в том числе для пучков) скорее всего хватит даже подсистемы арифметики второго порядка.
0) Основания математики должны быть $(n,r)§-категорными, где $n,r \in \mathbb{N} \cup \{ -2,-1,\infty\}$.
1) Споры об аксиоме выбора не имеют смысла. Действительно, категория $\mathrm{Set}_{\mathrm{AC}}$ множеств и отображений между ними, где все эпиморфизмы обратимы справа, и категория $\mathrm{Set}$, где это условие не обязательно выполняется, обе являются абсолютно валидными категориями. С какой именно из них работать -- зависит от конкретной ситуации.
0) Основания математики должны быть $(n,r)$-категорными, где $n,r \in \mathbb{N} \cup \{ -2,-1,\infty\}$.
1) Споры об аксиоме выбора не имеют смысла. Действительно, категория $\mathrm{Set}_{\mathrm{AC}}$ множеств и отображений между ними, где все эпиморфизмы обратимы справа, и категория $\mathrm{Set}$, где это условие не обязательно выполняется, обе являются абсолютно валидными категориями. С какой именно из них работать -- зависит от конкретной ситуации.
поправил
Дополню. Натуральные числа определяются как инициальная алгебра эндофунктора $X \mapsto \ast \coprod X$ на произвольном топосе. Кроме того, естественно рассматривать не только натуральные числа, но и конатуральные числа (конатуральные кочисла? натуральные кочисла?) и коиндукцию.
> не только натуральные числа, но и конатуральные числа
Отрицательные что ли? Хуя ты демон, множество Z открыл.
Нет, как заметил анон >>3318 , конатуральные кочисла это терминальная коалгебра на указанном мной функторе. Я не уверен, что ты понимаешь под "отрицательными числами", но подозреваю, что это двойственная категория к категории предпорядка ассоциированной к $\mathbb{N}$ как моноиду, или возможно сам $\mathbb{N}$ как комоноид. Не знаю, как ты мог перепутать это с конатуральными кочислами.
>множество Z
Как правильно определять $\mathbb{Z}$ я, к сожалению, пока не понял, для меня это открытый вопрос. Предлагаю отталкиваться от "свободный $k$-кортежный моноидальный $n$-группоид на одном объекте".
Интересно, как ты собрался определить натуральные числа без абстракции поенциальной осуществимости? А если с ней, то зачем мудрить а не просто взять и определить палочками как у Маркова?
>как ты собрался определить натуральные числа
Вот тут >>3306 написал.
>абстракции поенциальной осуществимости
Прости, не знаю, что это такое. Звучит как что-то связанное с модальной логикой и теорией моделей. Это очень интересно, но к математике (разделу линейной алгебры) и ее основаниям отношения не имеет.
>определить палочками
Не знаю, что такое "палочки". Если ты имеешь в виду терминальный объект в топосе, то это соответствует моему >>3306 определению.
> Интересно, как ты собрался определить натуральные числа без абстракции поенциальной осуществимости?
N петух опять завел свою ШУЕ шарманку. Абстракция потенциальной осуществимости - это свойство аксиом Пеано, а не что-то что может "существовать" отдельно от примеров, содержащих абстрагируемое свойство.
Cам то понял что сказал? Ты свою ШУЕ шизу как чат бот высираешь даже не задумываясь.
> Cам то понял что сказал?
Понял. А вот ты походу нет.
> Ты свою ШУЕ шизу как чат бот высираешь даже не задумываясь.
Это общепринятое определение абстракции, N петух. А вот у тебя реально ШУЕ.
>Не знаю, что такое "палочки". Если ты имеешь в виду терминальный объект в топосе
Похоже на начало пути нового петушка. Напомнило времена раннего конструктивного петуха когда он еще мог что то кроме шитпостинга чмориджами, благоговейно цитировал писания швятых Браузера и пророка его Мартина-Лефа.
Я по сути просто пересказываю позицию всех великих математиков второй половины двадцатого и двадцать первого веков, от Гротендика и Квиллена до Шольце и Лури.
N-петух - ты ультрафинитист или що? Просто если так, то очень бы хотелось увидеть какую-нибудь валидную ультрафинитную программу оснований математики
> А можно с нормального Западного источника?
Ну да, у Сохацкого есть ссылки. Вообще под гамалогии у него запилен так называемый "стек де Рама - Черубини - Шрайбера", где-то к нему и ссылки на нормальные источники чтобы обпучкаться.
Брауэра цитировать местным ебланам типа тебя бессмысленно, вы в Википедию-то не можете, все ваше ШУЕ и просто весь набор слов контрится первой же ссылкой оттуда. Вот ты же обосрался с универсальной машиной Тьюринга, а мог бы не обсираться а просто прочитать определение в Википедии. Как и N петух, к слову. Успенский ещё ладно, дедушка старый, ему все равно. Рано вам ещё Брауэра и Мартин-Лефа, дети тиктака.
>Вот ты же обосрался с универсальной машиной Тьюринга
Кек. Ты обосрался даже с зелеными машинками.
Я ответил на весь класс подобных вопросов, но ты этого ожидаемо не увидел, дединсайд. То есть, обосрался и в этом.
Твои любимые мемасы с чмориджами это универсальный ответ на все только в твоем деградировавшем мозгу.
Ты как-то слишком отстраненно пишешь про чмориджей, хотя сам - ярчайший представитель вида, судя по дегенеративности твоих постов.
(Ко)гомологии в HoTT можно и без модальностей считать (см. https://guillaumebrunerie.github.io/pdf/LIPIcs-CSL-2022-11.pdf, https://arxiv.org/pdf/2212.04182.pdf или https://arxiv.org/pdf/1706.01540.pdf), модальности нужны ради варианта SDG (https://ncatlab.org/nlab/show/synthetic+differential+geometry).
Имхо это плохая аналогия, и вопрос "какое понятие более общее" не очень хорошо определен для мат объектов. Попробуй лучше с абстрактной группой и подгруппой группы симметрий.
мимо
Чем аналогия плоха? Предельно ясная аналогия доступная даже детсадовцам чтобы навести петуха на правильный ответ.
> не очень хорошо определен для мат объектов
не в данном случае
Так, а это уже реально база. Там можно сделать алгеом? Кинь пожалуйста еще такое. Завтра скачаю Agda если есть алгеом. Помню в 2017 пробовал, но там даже не было когомологий.
Это же она?
>>3357
Я просто пошутил, извини. Пытаюсь троллингом вытянуть истину. Мне реально нужен теоретико-типовой пучок.
>не в данном случае
Какое "понятие" более общее, абстрактной группы или подгруппы группы симметрий? Для меня этот вопрос не имеет смысла, потому что абстрактная группа (т.е. по сути синтаксическая теория) и конкретные группы (т.е. по сути ее модели) живут в разных категориях. То же с машинами Тьюринга.
Вообще, по-моему здесь происходит путаница между отношением абстрактное-конкретное и отношением общее-частное.
>Чем аналогия плоха?
Я не уверен, в каком смысле зеленая машина (эта конкретная зелена машина? понятие зеленой машины?) моделирует любую машину (любую конкретную машину? понятие машины?).
>Какое "понятие" более общее, абстрактной группы или подгруппы группы симметрий?
Ну я сразу понял ты предлагаешь сравнить два несравнимых понятия и доказать таким образом что любые два понятия невозможно сравнить. Это какая то форма конструктивизма головного мозга?
>Я не уверен, в каком смысле зеленая машина
очень на то похоже...
>Мне реально нужен теоретико-типовой пучок
Определяется пучок в HoTT так же, как везде: как предпучок на сайте, удовлетворяющий ряду свойств. Чтобы увидеть, как это определение выглядит в агде, достаточно загуглить "sheaf agda" и посмотреть, например, сюда https://github.com/jonsterling/constructive-sheaf-semantics
>>3362
>что любые два понятия невозможно сравнить
Я не знаю, что такое "понятие" в математике. Объекты двух разных категорий действительно нельзя сравнить, поэтому вопрос о том, что более "общее", машина Тьюринга, моделирующая любую конкретную машину Тьюринга, или абстрактная синтаксическая теория машины Тьюринга, для меня не имеет смысла.
>Это какая то форма конструктивизма головного мозга?
Я не конструктивист.
>Объекты двух разных категорий действительно нельзя сравнить
О! так ты новый категориальный петушок. Милости просим.
426x240, 0:07
Давай так -- дай мне множество понятий и определи на нем отношение порядка, которое моделировало бы отношение "x есть более общее понятие, чем y". Потом расскажи, где во всей этой структуре относительно друг друга будут находиться понятия "универсальная машина Тьюринга", "машина Тьюринга", "группа", "подгруппа группы симметрий", "машина" и "зеленая машина" и почему. Или предложи альтернативную модель. Тогда может получиться какой-то разговор.
Ну или загугли хотя бы "aristotle ontological square" и помедитируй над разницей между exemplify, instantiate и inhere.
>>3365
Возьми два множества с определенными на них предпорядками (можешь рассматривать их как категории). Как "сравнить" (каким (би)функтором?) элемент первого предпорядка с элементом второго? inb4: (ко)произведение не это делает.
На что это ответ?
Раньше конструшок такой же напористый был, только предлагал перечитывать все писания швятого Браузера и пророка его Мартина-Лефа. Если тебе все это нужно чтобы ответить на вопрос на который легко ответит даже ребенок пяти лет, то куда то ты не туда свернул.
Сомневаюсь, что типичный ребенок пяти лет хорошо понимает, что такое "более общее понятие". Еще сомневаюсь, что типичный ребенок пяти лет хорошо понимает разницу между синтаксической теорией и ее моделью. Еще сомневаюсь, что мы в строгости должны ориентироваться на детей. Еще прошу заметить, что я никого читать не предлагаю, а прошу описать отношение предпорядка, с чем у умного ребенка пяти лет проблем действительно возникнуть не должно.
352x640, 0:14
>Там можно сделать алгеом?
Вопрос не совсем верно задан. Как верно выше замечали, HoTT с выбором интерпретирует ZFC (теорема 10.5.11 в HoTT book’е), так что раз в ZFC можно сделать алгеом, то и в HoTT тоже.
Ты, вероятно, спрашивал о синтетическом алгеоме (то есть чтобы с ℝ не пердолиться; иначе можно задать справедливый вопрос: для чего нужны кубические теории типов). Тогда как раз можешь почитать, что пишут Черубини и Шрайбер: https://www.math.kit.edu/iag3/~wellen/media/diss.pdf, https://arxiv.org/pdf/1806.05966.pdf, https://arxiv.org/pdf/2307.00073.pdf и вообще https://arxiv.org/find/math/1/au:+Schreiber_U/0/1/0/all/0/1 и https://felix-cherubini.de/ (тут ссылки на Agda-код есть).
Если очень надо пердолиться с ℝ, при этом пользоваться синтетическими расчётами, можешь почитать https://arxiv.org/pdf/1509.07584.pdf, но, правда, насколько я знаю, это в пруверах ещё никто не реализовывал.
>Кинь пожалуйста еще такое.
Майер — Вьеторис для когомологий: https://staff.math.su.se/evan.cavallo/works/mayer-vietoris.pdf, https://staff.math.su.se/evan.cavallo/works/oxford.pdf
Вот тут подробнее: https://ncatlab.org/nlab/files/Cavallo-CohomologyInHoTT.pdf
Вот когомологии Чеха сделать пытаются: https://www.felix-cherubini.de/chech.pdf (тут тоже SDG).
Гомологии для CW-комплексов: https://arxiv.org/pdf/1802.02191.pdf
Спектральные последовательности: https://github.com/cmu-phil/Spectral, https://ncatlab.org/nlab/show/spectral+sequences+in+homotopy+type+theory, https://florisvandoorn.com/talks/17Pitt_SSS.pdf
Теорема Гуревича: https://arxiv.org/pdf/2007.05833.pdf
Тут пятая глава про когомологии: https://arxiv.org/pdf/1606.05916.pdf
Свежая статья про когомологии на агде: https://arxiv.org/pdf/2401.16336.pdf
>Это же она?
В статьях про когомологии? Да, Agda.
Такое-то окормление говном модульного деда. Годами квакал, что нематематика потому что гамалогий нет, а оказалось что давно уже есть.
Это кал, качай Anders там всё есть, в том числе и абстракции созданные на основе примеров (но и в коем случае не наоборот!).
Тут тема несколько сложнее, чем обычно в Википедии пишут. Но против твоих кукареканий и Википедии более чем достаточно. Ты просто знай своё место (оно у параши) и смирись с этим.
Я знаю, мой дом здесь, я все треды перекатываю.
База уровня выше 9000.
Спасибо, анон. Загрузил плейлист по Агде и буду постепенно вкатываться опять.
Что это? Я вроде видел его мельком если не ошибаюсь, но синтаксис Агды пока топ для математика. Чистый, без всяких проггерских штук.
>Что это?
Это тебя жирно троллят. Чуть более продвинутая чем cubicaltt (но всё ещё экспериментальная) имплементация кубической теории типов.
В сравнении, в кубической агде библиотека значительно больше и много готовой автоматизации.
>синтаксис Агды пока топ для математика
В агде нельзя использовать «=» для равенства…
Скибиди-петух, а тебе что интересно не позволяет ответить на вопрос? Тебе же не нужно как категориальному петуху выписать категорию всего на свете чтобы было вообще о чем говорить. Подозреваю дело в том что МЛ не завез сабтайпинг и другим отношения на типах строить не велел и теперь для петуха это не доступная концепция так что от одного вопроса у него разрывает пердак. Сейчас порватыш еще чмориджей подкинет.
460x380, 0:17
- доломали N петуха, не осилившего пару определений из Википедии
- совершенно случайно доломали модульного деда, оказалось что гамалогии давно реализованы в агде
- попутно опетушили то ли какого-то подсиралу N петуха, то ли самого N петуха, мимикрирующего под собственного подсиралу, так же не осилившего определение машины Тьюринга из Википедии.
И только конструктивный петух щебечет все так же резво как и раньше. Уникальный случай в истории когда петух совсем без мозга живет уже больше десятка лет.
Рад, что ты сам себя из вменяемых выписал только что. Можешь и сам отсюда танцевать нахуй. Только одно замечание - опровержение N петушества по существу (конкретными ссылками), это не шиза, как бы неприятно тебе от этого не было.
1280x720, 0:02
Уважаемый (на самом деле нет), ты в своих анальных половых партнёрах уже запутался. Кто там тебя в анус сношал мне фиолетово ;)
По существу ты шизик, это медицинский факт, но что ты от меня хочешь, петушарий? Я не из этих, ваших, если что.
> По существу ты шизик, это медицинский факт,
Это кукареканье долбаеба, а не факт, тем более "медицинский".
> что ты от меня хочешь,
> сам мне безостановочно написывает одну хуйню за другой
?
Поциэнт, это ваш диагноз а не хуйня. Не занимайтесь самолечением, обратитесь к специалистам.
https://youtu.be/lXTuJL_VaSI?si=hSXsgV4UAF52bfR7
>Поясните, плиз, логики отдельно от математиков обучаются, вместе с философами или как?
Есть специальность "логика" у философов (ака 5.7.5 в номенклатуре ВАК) и есть специальность "математическая логика" у математиков (ака 1.1.5).
Соответственно, часто есть кафедра (лаборатория, институт, группа...) логики (и, обычно, чего-то еще) на математическом факультете, и кафедра (лаборатория, институт, группа...) логики на философском. Учатся математики-логики и философы-логики раздельно, если не считать возможные межфакультетские и междисциплинарные курсы/семинары.
>Но непонятно, как можно о современной математике говорить, если ты ей не занимаешься
Очевидно, он в математике, о которой он говорит, разобрался достаточно, чтобы заниматься философией математики. Разобрался он, вероятно, так же, как разбираются все остальные люди - читая книжки и разговаривая с людьми, работающими в области (вот https://philomatica.org/wp-content/uploads/2013/02/colin.pdf пример такого разговора). В принципе, самоучки, которые освоили какой-то материал в достаточной степени, чтобы понимать, что пишут другие, - это не какое-то редкое явление. Собственно производством новой математики он не занимается и, вроде как, не претендует.
>Насколько это все котируется в научном сообществе
Философия математики это существующая область, и вопросы, которые он обсуждает, в ней обсуждает не только он. Он где-то преподает и пишет статьи. В этом смысле, то, что он делает, вполне себе "котируется".
Нашел кстати где-то у МЛ тезис о том что действительно мы не знаем что такое доказательство, если бы мы знали что такое доказательство, но мы не знаем что это такое...
Но при этом утверждается что единственный способ доказать конъюнкцию это предъявить пару доказательств. Почему нельзя это сделать еще каким то окольным путем? Или почему не учитываются возможные проблемы, например если имеются ресурсные ограничения - та самая "чернильная дыра", у человека заканчивается бумага чтобы выписать оба доказательства вместе, в формальной системе не хватает свободных переменных.
Еще интереснее тезис о применении функций к доказательствам при построении импликации. Т.е. мы не знаем что такое доказательство но мы будем применять к нему функции. Приехали.
> Нашел кстати где-то у МЛ тезис о том что действительно мы не знаем что такое доказательство,
Цитату неси.
https://archive-pml.github.io/martin-lof/pdfs/Truth-of-a-Proposition-Evidence-of-a-Judgment-1987.pdf
>Now, there can be no proof, no conclusive proof, that a proof really proves its conclusion, because, if such a miraculous means were available to us, we would of course always use it and be guaranteed against mistakes.
>So, clearly, there can be no proof in the proper sense of the word that a proof really proves its conclusion: the most there can be is a discussion as to whether a proof is correct or not, and such discussion arises precisely when we make mistakes, or when we have insufficient grounds or evidence for what we are doing.
>As should be clear from what I have just said, this notion of validity or conclusiveness or correctness of a proof is a very fundamental notion. Indeed, it is the most fundamental one of all, the one of all the notions that I have digcussed which has no other notion before it
в конце какая то хуйня-малофья идет про хлеб и ненастоящий сладкий хлеб и про то что можно считать доказательством то что кажется достаточно убедительным лично тебе (или не считать, тут я не понял мнение лично МЛ на этот счет)
Петух, ты разобрался какое понятие более общее "зеленые автомобили" или "автомобили" или для тебе это все еще неподъемная задача, кек?
Хуй там, это ебанько даже определение абстракции не осилило, теперь вот бегает как опущенный со своей википедией. Такая вот абсиракция, лол.
N петух, общепринятое определение абстракции я цитировал. Но ты его не осилил, зато уверовал в рандомной ШУЕ.
Ты копипастил нерелевантуню хуйню которую даже нормально прочитать и понять не смог. Ты даже отрицал что абстракция это понитие, т.е. у тебя мозги отшиблены на прочь от слова совсем, тебе с школьной программы нужно начинать а потом уже в основания лезть. О чём с тобой после этого говорить? Эта болезнь головного мозга (асемасия) описана у Манина в "доказумом и не доказуемом", он там приводил примеры как больные с частиным поражением мозга могли копипастить относительно сложные фразы (как например делаешь ты, хотя ни Мартин Лёфа ни Маркова ты не читал) при этом путались в элементарных понятиях. Если будет второе издание книги, тебя нужно в пример поставить, с цитатами, как канонического ебанька.
764x720, 0:03
Энпе Тух, ты просто клоун. Все твои кукареканья - это всего лишь защитная реакция. А все твои маняаргументы контрятся первой же ссылкой из Википедии. Ты пытаешься приплести какую-то нерелевантную хуйню, какую-то "сасимасию Манина" (чего?), какие-то выдуманные "диагнозы", которые с готовностью приписываешь несогласным с твоим ШУЕ итд. Все это просто чтобы не признавать своего обсера в простейшем вопросе - определении абстракции. А это определение есть на каждом углу начиная с Википедии. Ты это прекрасно понимаешь. И тебе от этого никуда не деться, терпи Энпе Тух, терпи.
Ничего, стадия отрицания у тебя скоро закончится и придёт сирение, мовный петух. Как говорили в одном фильме "...и тебя вылечат".
Твоя уровень это детские книжки с соовтествующими "определениями" для детей, что бы не травмировать психику раньше времени. Только непонятно, если ты дебил, зачем во взрослые треды лезешь со своим свиным рылом, ась? Отвечай, мовная петушара.
> Ты пытаешься приплести какую-то нерелевантную хуйню, какую-то "сасимасию Манина" (чего?)
Ты бы лучше вместо ШУЕ уёбка сохацкого что нибудь путное почитал, того же Манина например.
Ведь один в один твой случай, как будто с тебя писали:
«Мл. лейтенант Засецкий, 23 лет, получил 2 марта 1943 года пулевое проникающее ранение черепа левой теменно-затылочной области. Ранение... осложнилось воспалительным процессом, вызвавшим слипчивый процесс в оболочках мозга и выраженные изменения в окружающих тканях мозгового вещества».
Нарушения психики Засецкого поначалу ужасны. Над всем доминирует асемасия — разрывы связей между знаком и его значением.
Первая встреча Засецкого с врачом: «Попробуйте прочитать эту страничку! «—»... Нет, что это? ... не знаю ... я не понимаю, что это ... Нет ... какое это? ... — «Ну, попробуйте посчитать что-нибудь простое, например сложите семь и шесть! ...»— «Семь ... шесть .. .как же это ... семь... нет, я не могу ... нет,-я совсем не знаю ...».
Утрачено понимание простейших предикатов:
«Что бывает перед зимой?» — «Перед зимой... или после зимы .. . лето ... или что-нибудь ... нет. Это у меня не выходит ...» — «А перед весной?» — «Перед весной ... сейчас весна ... а вот до ... или после ... я уже теряюсь ... нет ... у меня не выходит . . .»
Нарушается интерпретация смыслоорганизующих кодов синтаксиса:
«В школу, где училась Дуня, с фабрики пришла работница, чтобы сделать доклад». Что это? Кто же сделал доклад? Дуня? Работница? А где училась Дуня? И кто пришел с фабрики? И куда?»
Это трудный пример (текст А. Р. Лурия), но вот что пишет сам Засецкий: «А еще: «слон больше мухи» и «муха больше слона» ... Я понимал только, что «муха» маленькая, а «слон» большой, но разобраться в этих словах и ответить на вопрос, муха меньше слона или больше, я почему-то не мог. Главная же беда была в том, что я не мог понять, к чему относится слово «меньше» (или «больше») — к мухе или слону . . .».
Обращает на себя внимание сложность метаязыкового текста, описывающего языковые нарушения. Точность анализа нарушений кажется несовместимой с грубостью нарушений, которые анализируются. Это можно было бы объяснить тем, что анализ ретроспективен, но вот описание в настоящем времени, еще более глубокое: «... Я снова припоминаю про понятия «муха меньше слона» или «муха больше слона». Берусь думать над ними, как они должны правильно пониматься и как неправильно. От перестановки слов в этих понятиях изменяется смысл понятия. Мне же они кажутся на первый взгляд одинаковыми, словно ничего не изменяется от перестановки этих слов. А подольше подумаешь, заме-
чаешь, что or перестановки слов изменяется смысл указанных четырех слов (слон, муха, меньше, больше). Но мой мозг, моя память после ранения и до сих пор не в силах сразу охватить, к кому отнести слово меньше (или больше) — к слону или к мухе? Перестановок даже в этих четырех словах очень много».
Это сохранение сложных психических способностей при утрате «простых» видно и на образцах творческого воображения Засец-кого, близких к литературно-психологическим этюдам: «Вот-я врач. Я осматриваю больного, сердечно обеспокоен его состоянием, болею за него всей душой, ну как же, ведь это же человек, такой же, как и все, но только он сильно болен, ему надо помочь. Ведь я тоже могу болеть, и мне тоже кто-то должен помочь, а теперь вот надо помочь этому больному. Иначе нельзя. А вот я другой врач. Ох, и надоели мне эти больные со своими жалобами. Я не знаю, зачем я связался с этой медициной. Мне не хочется ничего делать, не хочется никому помогать. Правда, я. помогаю больше тем, кто и мне оказывает какую-нибудь помощь. И не беда, если умрет какой-нибудь больной, не в первый раз они умирали и умирают».
Все это показывает полную неосновательность мнения Дж. Россера [6]: «Когда доказательство открыто и записано на языке символической логики, его может проверить любой слабоумный (moron)».
> Ты пытаешься приплести какую-то нерелевантную хуйню, какую-то "сасимасию Манина" (чего?)
Ты бы лучше вместо ШУЕ уёбка сохацкого что нибудь путное почитал, того же Манина например.
Ведь один в один твой случай, как будто с тебя писали:
«Мл. лейтенант Засецкий, 23 лет, получил 2 марта 1943 года пулевое проникающее ранение черепа левой теменно-затылочной области. Ранение... осложнилось воспалительным процессом, вызвавшим слипчивый процесс в оболочках мозга и выраженные изменения в окружающих тканях мозгового вещества».
Нарушения психики Засецкого поначалу ужасны. Над всем доминирует асемасия — разрывы связей между знаком и его значением.
Первая встреча Засецкого с врачом: «Попробуйте прочитать эту страничку! «—»... Нет, что это? ... не знаю ... я не понимаю, что это ... Нет ... какое это? ... — «Ну, попробуйте посчитать что-нибудь простое, например сложите семь и шесть! ...»— «Семь ... шесть .. .как же это ... семь... нет, я не могу ... нет,-я совсем не знаю ...».
Утрачено понимание простейших предикатов:
«Что бывает перед зимой?» — «Перед зимой... или после зимы .. . лето ... или что-нибудь ... нет. Это у меня не выходит ...» — «А перед весной?» — «Перед весной ... сейчас весна ... а вот до ... или после ... я уже теряюсь ... нет ... у меня не выходит . . .»
Нарушается интерпретация смыслоорганизующих кодов синтаксиса:
«В школу, где училась Дуня, с фабрики пришла работница, чтобы сделать доклад». Что это? Кто же сделал доклад? Дуня? Работница? А где училась Дуня? И кто пришел с фабрики? И куда?»
Это трудный пример (текст А. Р. Лурия), но вот что пишет сам Засецкий: «А еще: «слон больше мухи» и «муха больше слона» ... Я понимал только, что «муха» маленькая, а «слон» большой, но разобраться в этих словах и ответить на вопрос, муха меньше слона или больше, я почему-то не мог. Главная же беда была в том, что я не мог понять, к чему относится слово «меньше» (или «больше») — к мухе или слону . . .».
Обращает на себя внимание сложность метаязыкового текста, описывающего языковые нарушения. Точность анализа нарушений кажется несовместимой с грубостью нарушений, которые анализируются. Это можно было бы объяснить тем, что анализ ретроспективен, но вот описание в настоящем времени, еще более глубокое: «... Я снова припоминаю про понятия «муха меньше слона» или «муха больше слона». Берусь думать над ними, как они должны правильно пониматься и как неправильно. От перестановки слов в этих понятиях изменяется смысл понятия. Мне же они кажутся на первый взгляд одинаковыми, словно ничего не изменяется от перестановки этих слов. А подольше подумаешь, заме-
чаешь, что or перестановки слов изменяется смысл указанных четырех слов (слон, муха, меньше, больше). Но мой мозг, моя память после ранения и до сих пор не в силах сразу охватить, к кому отнести слово меньше (или больше) — к слону или к мухе? Перестановок даже в этих четырех словах очень много».
Это сохранение сложных психических способностей при утрате «простых» видно и на образцах творческого воображения Засец-кого, близких к литературно-психологическим этюдам: «Вот-я врач. Я осматриваю больного, сердечно обеспокоен его состоянием, болею за него всей душой, ну как же, ведь это же человек, такой же, как и все, но только он сильно болен, ему надо помочь. Ведь я тоже могу болеть, и мне тоже кто-то должен помочь, а теперь вот надо помочь этому больному. Иначе нельзя. А вот я другой врач. Ох, и надоели мне эти больные со своими жалобами. Я не знаю, зачем я связался с этой медициной. Мне не хочется ничего делать, не хочется никому помогать. Правда, я. помогаю больше тем, кто и мне оказывает какую-нибудь помощь. И не беда, если умрет какой-нибудь больной, не в первый раз они умирали и умирают».
Все это показывает полную неосновательность мнения Дж. Россера [6]: «Когда доказательство открыто и записано на языке символической логики, его может проверить любой слабоумный (moron)».
Энпе Тух, приведи свое петушиное определение абстракции, противоречащее общепринятому. Со ссылками, разумеется.
Тебе и из википедии сойдёт, ты только его читать нучись без своей ШУЕ примеси.
А главное, это ты поясни почему оно не является понятием и кто тебе разрешал испльзовать в математике понятия без определения и одновременно не считать их исходными неопределямыми.
Меня оно устраивает если без твоих ШУЕ-интерпретаций, на остальную часть поста отвечай.
> асемасией
Асисяй? Так какие претензии к определению абстракции в Википедии? Это приказ Израиля, чи шо?
>>3568
> детские книжки с соовтествующими "определениями" для детей, что бы не травмировать психику раньше времени
А у тебя какое-то тайноведение, закрытые оккультные писания не для всех, где абстракция определяется как-то иначе чем в общепринятом её понимании?
Местные основатели тоже терминов из книжек и разговоров нахватались и тоже получается философией математики занимаются тут.
То что ты привёл из википедии никакого отношения к нашему дискурсу не имеет, более того нисколько не противоречит тому что я писал. Просто ты как и подобает болезному умом простейший текст осилить не можешь, только бегаешь как опущенный с копипастами.
Это у тебя тупого ГСМ-ебанька абстракция магически сама себя определяет, в математике напротив, есть либо исходные понятия (аксиомы или доказательства/редукция к более простым понятиям). Касательно N ты ни первый способ ни второй не продемонстрировал, а значит можно в очередной раз сделать вывод что ты пиздливое хуйло.
10 дней обтекал? Лови тогда ещё струю мочи в ебало.
> абстракция магически сама себя определяет,
Абстракция это свойство примеров, собственно, содержащих её. В случае N, абстракция потенциальной осуществимости является свойством аксиом Пеано.
> Касательно N ты ни первый способ ни второй не продемонстрировал
N определяется аксиомами Пеано, абстракция потенциальной осуществимости это свойство аксиом Пеано. Следовательно, N определено. Свободен, клоун.
> О, в треде есть реально полезный контент, чаю
"А что, так можно было?!" Прикинь, можно. Достаточно писать что-то по теме треда, а не только выгуливать тут шизу, пытаясь "ниспровергать" общепризнанные давно доказанные вещи писаниями ноунейм ШУЕшников.
Стандартно. Вот если бы через преобразование Фурье, вот это была бы настоящая чмондель-техника.
А с сохацким есть?
Как же так? Ведь эллиптическая кривая и есть пучок. Но так уж и быть, можно ссылку?
Ты загуглить не осилил, буквально. Кто тебе сказал, что ты криптографию в агде осилишь?
Я хочу создать криптографический пучок, чтобы только я знал, как ему дать формальное определение в теории типов Мартина-Лефа.
Но пучок - понятие первичное.
Пук Бернедектта на свiдомых мовах.
Бернадектт одобряет.
> А если серьезно, без шуток?
Читать научиться для начала. Стек де Рама - Черубини - Шрайбера тут неоднократно упоминали.
так это для алгтопа
>теория множеств
Может лучше сжечь книгу? Есть же теория категорий, ну или теория типов на крайний случай.
>теория категорий
Не дает интуиции, просто язык для описания некоторых свойств. Чтобы понять почему эти свойства верны нужно заглядывать внутрь структуры или строить ее модели.
>теория типов
Удобно как если на беговую дорожку прийти в латексном костюме. Может можно будет о чем то говорить когда компуктер-саентисты разберутся с десятками взаимоисключающих способов определить равенства, структуры, высказывания.
Теория множеств - оптимальная золотая середина на данный момент.
>Не дает интуиции, просто язык для описания некоторых свойств.
А теория множеств какую интуицию даёт?
>Удобно как если на беговую дорожку прийти в латексном костюме.
Ты аксиоматическую теорию множеств видел? Как там удобно функции строить, например, знаешь?А когда с десятками взаимоисключающих способов определить категорию Set разберутся?
Для математика, который не занимается вознёй в основаниях, в целом, не очень важно, в какой системе работать, а те, кто возятся, в любом случае окажутся по уши в сотне технических проблем.
> когда компуктер-саентисты разберутся с десятками взаимоисключающих способов определить равенства, структуры, высказывания.
Они-то давно разобрались, это ты разберись.
> Не дает интуиции, просто язык для описания некоторых свойств. Чтобы понять почему эти свойства верны нужно заглядывать внутрь структуры или строить ее модели.
Заодно разберись, что такое теория категорий. Судя по вышенаписанному, у тебя вообще нет понимания, что это и зачем.
Функция определяется тем как действует на элементы. Определи мне возведение в квадрат в терминах теории категорий, а я над тобой поржу. Что такое топос определяется через аналогии с SET; вот если бы было наоборот тогда бы к мокрым мечтам категорщиков не было никаких вопросов.
Пока что потуги перевести основания на альтернативный формализм категорий или типов напоминают мне лисперов которым синтаксис ненужон.
>>4081
Иди терм отредуцируй, клоунесса конструктивная.
>Функция определяется тем как действует на элементы.
Ты же в курсе, что функция из A в B в теории множеств стандартно определяется как подмножество A × B с рядом условий, да?
>Определи мне возведение в квадрат в терминах теории категорий, а я над тобой поржу.
Возведение в квадрат чего? Натурального числа? Вещественного числа? Множества? Группы?
>Что такое топос определяется через аналогии с SET
Причём тут топос? Какие аналогии? Ты же в курсе, что для категории Set нужны классы или там, например, универсум Гротендика, да?
А ты в курсе как функция определяется в ТК? Никак
Допустим я хочу понять что из себя представялет возведение в квадрат и я смотрю:
1 - 1
2 - 4
3 - 9
...
поэлементно
Твои действия в аналогичной ситуации в рамках категориального подхода?
>А ты в курсе как функция определяется в ТК?
Ты про какое-нибудь ETCS, да? А как тогда множество определяется в теории множеств? А отношение принадлежности там же? А как тип определяется в теории типов? А как определяется число в арифметике Пеано? А отношение «лежать между» в https://en.wikipedia.org/wiki/Tarski%27s_axioms?
>Допустим я хочу понять что из себя представялет возведение в квадрат и я смотрю:
Начнём с того, что функцией возведения в квадрат будет множество упорядоченных пар вида {(0, 0), (1, 1), (2, 4), (3, 9), …}.
В теории множеств известно, как определить функцию умножения натуральных чисел (пусть будет Π), поэтому возведение в квадрат естественно определить через неё как {(x, Π(x, x)) | x ∈ ℕ}, которое на самом деле сокращение к {(x, y) ∈ ℕ × ℕ | y = Π(x, x)}, которое на самом деле сокращение к {w ∈ ℕ × ℕ | ∃ x ∈ ℕ: ∃ y ∈ ℕ ∧ (x, y) = w ∧ ((x, x), y) ∈ Π}, если не пользоваться ε-оператором и сокращением для полного образа. Ой, сколько машинерии-то вдруг понадобилось для квадрата, а это мы даже не обсуждали, как произведение определить, в том числе и произведение множеств.
>Твои действия в аналогичной ситуации в рамках категориального подхода?
В ETCS, внезапно, тоже можно определить произведение Π, которое будет стрелкой из ℕ × ℕ в ℕ, а также диагональ Δ из ℕ в ℕ × ℕ, которая n ↦ (n, n). Возведение в квадрат, неожиданно, окажется композицией Π ∘ Δ. Более того, что тоже крайне неожиданно, такой же композицией его можно определить в теории множеств (надо лишь не забыть определить композицию функций, которая там напрямую не дана, да).
После точно так же можно посмотреть значение этой функции на конкретном числе, которое стрелка из терминального объекта в ℕ: есть стрелка 0 из терминального объекта в ℕ и стрелка succ из ℕ в ℕ, а Π ∘ Δ ∘ succ ∘ succ ∘ … ∘ succ ∘ 0, например, значением и будет.
>поэлементно
В детский сад.
>>поэлементно
>В детский сад.
Ясн. Ни для чего не пригодный формализм. Разве что только чтобы "переоткрывать" то что уже давно доказано через множества.т
> тоже крайне неожиданно
Да нет, крайне ожидаемо - категорщики пытаются одевать штаны через голову - смешно смотреть.
Ты, долбоёбина, функцию Аккермана тоже поэлементно исследовать будешь? А функции из ℝ в ℝ, особенно разрывные?
>Ни для чего не пригодный формализм.
У тебя, блядь, формализмами являются и теории множеств, и ETCS, дегенерат ебучий.
>У тебя, блядь, формализмами являются и теории множеств, и ETCS, дегенерат ебучий.
Это противоречит чему именно? Только тому что ты не тупая ебанашка, не пиши мне больше.
Сука, уёбок, у тебя в двух формализмах квадрат примерно одинаково определяется, но ты продолжаешь верещать, что один формализм априори лучше, а другой вообще не нужен, не разбираясь, блядь, ни в каком из них. Иди просто нахуй отсюда.
>Не дает интуиции,
Вся моя интуиция строится как раз на ней и теории типов, а не на теории множеств.
>Ты же в курсе, что для категории Set нужны классы или там, например, универсум Гротендика, да?
NBG равнонепротиворечива с ZFC, а люди всё ещё ссут кровавой мочой от классов..
Гоша?
>Почему по поводу аксиомы выбора возникают такие споры?
Всегда удивляло тоже, ведь самое проблемное место теории множеств - это схема выделения..
>Что это вообще с точки зрения Гротендика и теории категорий?
Что у тебя эпи в Set расщепимы, т.е. почти тоже самое, что любой модуль над F_1 проективен..
>Знаю, что Гротендик был недоволен состоянием топологии и её привязки к анализу.
У меня скорее ощущение, что общей топологии быть не должно..
Просто так совпало, что мы изобрели настолько слабый концепт, что он работает в случаях, где мы используем совершенно разные методы
над F2
Ты хочешь своровать категорные интуиции?
Не колхозная, а природная. Пучки отражают естественную красоту мира и связь локального с глобальным.
Подозреваю, что какой-то не математик?
ПУЧК ПУЧК ПУЧК ПУЧК ПУЧК
Потому что из неё следует что движением можно клонировать шарики.
>Ты же в курсе, что функция из A в B в теории множеств стандартно определяется как подмножество A × B с рядом условий, да?
Ну это так себе определение, по сути эквивалентно самой упорядоченной паре т.к. если ты определил пару ты уже фиксировал соответствие. Тут как множество это совокупность, а совокупность это множество. Один хер с разных сторон.
Подпесалсо. Проблема в том что все альтернативы теории множеств контринтуитивны и при этом не дают ничего нового в в том плане что все равно по сути повторяют конструкции в теории множеств только на более сложном языке.
А почему не?
Спектральный пук.
Да, это тот самый Успенский.
>>4073
Бурбаки с того света продолжают писать книги. В 2016 начала выходить Алгебраическая топология, там есть зайчатки теорката "по Бурбаки".
>>4083
На самом деле связи топосов с SET довольно спорны. По моему скромному мнению, гораздо более правильным является установление связей топосов с геометрией эйлеровых кругов на плоскости.
Сначала хотел сделать персонажей объектами, а их отношения морфизмами, но потом понял, что какая-то тривиальная категория получается. Мне кажется, нужно брать отдельную категорию для каждого аспекта произведения, например - категория Сюжет(𝔸), Темы(𝔸) и т.д. Что думаете, братья категористы?
я тоже
Можно сделать морфизмы "тропами" а ля tvtropes, а любой объект это простр "болванка", полностью определённая морфизмами из и в, т.е. всеми применимыми "тропами".
namdak trompa spoq
В принципе идея неплохая, гораздо лучше моей, но вижу проблему. Думаю тоже будет тривиальная категория или некий скелет высшей категории. Некоторые персонажи в аниме/визуальных новеллах обладают глубиной, которая выше тропов заложенных в них, т.е. тут есть некая высшая структура которая описуема только условными 2-морфизмами в этой категории.
Она не захватывает всей структуры.
Или может нужно использовать интуицию теории пучков и алгема? Локально персонаж определен полностью тропами, но глобально может быть что-то нетривиальное.
Ну у меня получилось немного нестандартно.
>программирование - теория типов - гомотопическая теория типов - теоркат - алгтоп - алгем и ПУЧКИ
Самое нормальное:
>база логики - теоркат и теория типов одновременно - алгем, алгтоп, высший теоркат и т.д.
Главное не останавливаться только на одном теоркате или теории типов, там точно с ума можно сойти. И множества вообще не трогай, можно навсегда стать инвалидом в математическом плане. И разбавляй нормальную первокультурную математику теоркатом и теорией типов, чтобы понимать глубинные смыслы.
>>114625 →
Лучше сначала объясни, какие «противоречия, найдённые Гёделем» и как именно решила «типология Рассела»?
Нет, нельзя. И дело не в Гёделе. Формализация всей математики упирается в проблему разрешимости Гильберта, которая неразрешима, что доказал Тьюринг.
Неразрешимость означает, что в общем случае нельзя алгоритмически доказательства искать; возможность загнать всё в одну большую систему и доказать её непротиворечивость она не исключает (исключает теорема Гёделя в известных случаях).
Всё, сам нашёл. ZFC/NBG.
Это конструктивный петух, он у нас особенный. Так что лучше приготовься к потоку шитпостов если хочешь ему чего то доказать.
Думаю уёбок сохацкий за последние пару лет на своей жопе почувствовал её существование, лол.
Проиграл.
ультрафинитисты насрали
Раньше любил троллить с помощью неё на других бордах финитистов, математиков, алгемщиков пучкистов, и много кого.
Какой тип у 1?
Алсо достаточно глянуть на конструктивного петуха чтобы отпало желание заниматься теорией типов и вообще основаниями.
"X имеет тип Y" это же не предикат в теории типов, а утверждение мета уровня. В твоём случае вопрос не имеет смысла, потому что не существует абстрактного объекта в вакууме без типа. Дай определение 1, и сразу поймешь какой у него тип.
За счёт этого и хорошо получается троллить притворяясь ярым сторонником теории типов. Приверженцы других теорий оснований и математики сильно горят от неё, хотя по сути о ней знают очень мало.
>утверждение мета уровня
Бла-бла-бла, бред. Не более "мета" чем существование пустого множества в теории множеств. От того что дурачки повторяют заученные швятые писание они не становятся правдой.
>не существует абстрактного объекта в вакууме без типа
Ты сказал?
На самом деле подвох был в том что 1 это натуральное число. А так же это целое число. И нечетное число. Это очевидно любому здравомыслящему человеку как и то что теория типов ущербна.
Когда будешь тролить в следующий раз расскажи еще про пятьдесят оттенков равенства в теории типов. Тогда ты точно будешь у мамки главным тралом.
Существование пустого множества выразимо в самой теории типов. x : A это не предикат, как предикат существования или принадлежности множеству. В теории типов любая точка принадлежит какому-то пространству, без этого невозможно даже говорить об этой точке.
Но это сказал не я, а Мартин Лёв. Если хочешь доказать его неправоту, покажи хоть один объект без типа в теории типов. 1 не имеет смысла в контексте оснований без более глубокого объяснения того, о чём мы говорим. 1 натуральное число, если мы говорим о типе натуральных чисел определенных индуктивно, также это и целое число, если мы говорим о Дедекиновых сечениях.
Понимаешь, запись концепта не равна концепту, который она описывает. 1 может быть даже терминальным объектом в категории.
Про разные равенства кстати математики хорошо понимают интуитивно, но вот именно то, о чём мы сейчас говорим вызывает у них диссонанс. Норм почва для троллинга и финитистов, и теоретико-множественников. Прочитал HoTT и можно троллить почти весь математический контингент, да даже программистов.
>Но это сказал не я, а Мартин Лёв.
Почему мне должно быть не похуй?
>покажи хоть один объект без типа в теории типов
>В Писании написано что Бог есть - шах и мат аметисты
Всех затралил лалок, переиграл и уничтожил.
Вообще смешно как МЛ придумал концепцию "джаджментов" - это как аксиомы, но только аксиому другую можно выкинуть нахуй (как это провернул пришвятой Браузер например) а вот "джаджмент" это нечто "совершенно фундаментальное и само-собой разумеющееся" и если будешь в этом сомневаться то незримый дух конструктивизма тебя покарает. При этой разумеющности МЛ несколько раз менял фундаментальные "джаджменты" своей теории типов, обсираясь в процессе с парадоксами. Но дурачки хавают. just sayin.
(И это еще петух похоже еще где то гуляет на каникулах, а то уже весь тред в его перьях бы был)
>При этой разумеющности МЛ несколько раз менял фундаментальные "джаджменты" своей теории типов
Я слушал только одну его лекцию и не читал книги, он говорит эти джаджменты отражают объективную реальность или они работают только в пределах его теории типов? Если второе, то думаю они могут меняться.
>>5677
Тайп классы это ведь что-то из проггерства? Там вообще непонятно что происходит, у них там и вымышленная категория типов хаскеля есть.
>Про разные равенства кстати математики хорошо понимают интуитивно
Ты наверно и аксиому унивалетности выпишешь с закрытыми глазами? Только не перепутай equivalence, equality и isomorphism.
Я да, недавно даже думал про неё в обычной жизни. Нормальные математики (то есть алгебраисты, пучкисты и прочие первокультурщики) интуитивно понимают различие изоморфизма и равенства. Им только нужно объяснить judgemental equality.
Добавили новую аксиому Брауэра-Вайлдбергера о неконструктивности множества целых чисел и уникальности единицы.
>В чем состоит "говнотроллинг"?
В унылых доёбах до технических деталей каких-то теорий.
Точно так же можно визжать про то, почему в теории множеств зачастую 1 ∈ 3 и иногда (0, 0) = 2. Здравомыслящим людям там как, нормально вообще?
Можно повизжать про малые и большие множества, а заодно про классы, про необходимость городить универсум (Гротендика) ради теории категорий. А без теоремы о дедукции много доказать сможешь в Hilbert-style системе? Как, удобно?
>observational equality
Не знаю что это, я читал только HoTT. Интересный концепт? Пригоден для троллинга?
>В унылых доёбах до технических деталей каких-то теорий.
Я говорю что то что тейк про то что у чего угодно должон быть один само-собой разумеющийся тип хуйня и это не очевидно только промытым адептам теории типов. Каким хуем это техническая деталь ТТ когда это ее самая основа, ты совсем чтоли ебанько тупое?
>>5692
Пытаюсь разобраться, иногда возвращаюсь в него потыкать. Можно тралить унылых типизаторов тем что у них овер50 различных сортов равенств с которыми они сами разобраться не могут. Можно этот пассаж с ncatlab скидывать как пруф:
https://ncatlab.org/nlab/show/extensional+type+theory
Note: For a while, the nLab incorrectly used “extensional type theory” to refer to what we now call set-level type theory. If you encounter uses of this sort, please correct them.
>скучная проггерская тема
Как же у меня печет с ебанашки. HoTT это и есть скучная проггерская тема. А "математики" используют ZFC и вообще про основания не парятся.
>Я говорю что то что тейк про то что у чего угодно должон быть один само-собой разумеющийся тип хуйня и это не очевидно только промытым адептам теории типов. Каким хуем это техническая деталь ТТ когда это ее самая основа, ты совсем чтоли ебанько тупое?
А я говорю тебе, что ты хуесос и пидорас, благодаря единственности типа проще добиться завершимости алгоритма проверки типов, а в теориях, где у терма может быть много типов (ничего себе, а так не один такой умник, да?), за этим надо отдельно следить (Coq).
>проще добиться
Пффф проблемы типоманек, страдайте - добивайтесь, проще должно быть нормальным людям.
>завершимости алгоритма проверки типов
А кто тебе сказал что он должон завершатся? (ты ведь о разрешимости тайпчекинга) Опять транслируешь догматы швятых отцов или можешь привести какие то аргументы?
>у терма может быть много типов
>Coq
Разве там есть такое? Не припомню.
Кстати, обрати внимани я использовал оборот "я говорю" т.к. ссылался на раннее написанное в треде. Но ты этого не понял, но решил повторить этот оборот за мной, т.к. ты и есть тупой хуесос и пидорас у которого разорвало сраку.
>Пффф проблемы типоманек, страдайте - добивайтесь, проще должно быть нормальным людям.
Добейтесь тогда, чтобы в теории множеств не было хуйни вроде «1 ∈ 2». (Ты долбоёб?)
>А кто тебе сказал что он должон завершатся? (ты ведь о разрешимости тайпчекинга) Опять транслируешь догматы швятых отцов или можешь привести какие то аргументы?
Очевидно, при реализации завершающегося алгоритма можно опираться на пруф завершимости. Поэтому если такой алгоритм зацикливается, то проблема не в теории, а в реализации. Значит уровень доверия к такому чекеру выше.
>Разве там есть такое? Не припомню.
Доброе утро.
>>5699
Какой же ты дегенерат ебанутый.
>Добейтесь тогда, чтобы в теории множеств не было хуйни вроде «1 ∈ 2».
Нахуя?
>(Ты долбоёб?)
Пичот?
>Очевидно, при реализации завершающегося алгоритма можно опираться на пруф завершимости.
Напиши по-человечески что там тебе очевидно.
>Поэтому если такой алгоритм зацикливается, то проблема не в теории, а в реализации. Значит уровень доверия к такому чекеру выше.
Т.е. ты представляешь себе такую гипотетическую ситуацию что - ты скармливаешь чекеру свою теорему. Он начинает чего то там бздеть-пердеть. И тут у тебя есть только два варианта - либо чекер говно, либо ты написал хуйню. Так? И вообще никаких способов выбрать одно или другое у тебя нет. Но вот если чекер исправно тебе выдает да/нет, то
> Значит уровень доверия к такому чекеру выше.
(при том что на практике чекер может точно так же сколько угодно бздеть-пердеть потому что "за конечное время" еще не значит что ты его сможешь дождаться за свою жизнь)
У тебя кашка в голове.
>Доброе утро.
Ну это мы уже реально дошли
>до технических деталей каких-то теорий
>Though Set and Type are different in Coq, this is mostly due to historical reasons
>Какой же ты дегенерат ебанутый.
Твоей мамке норм, вчера орала как последняя сучка.
>Нахуя?
А ради твоих хотелок кто чего добиваться должен, петушок?
>Т.е. ты представляешь себе такую гипотетическую ситуацию что - ты скармливаешь чекеру свою теорему. Он начинает чего то там бздеть-пердеть. И тут у тебя есть только два варианта - либо чекер говно, либо ты написал хуйню. Так? И вообще никаких способов выбрать одно или другое у тебя нет. Но вот если чекер исправно тебе выдает да/нет, то
Тупой хуесос не может понять, что ситуация «скормили терм чекеру, он зациклился, но мы не знаем, проблема в реализации или терме» предпочтительнее ситуации «скормили терм чекеру, он зациклился, но мы не знаем, проблемы в реализации, теории или терме».
>при том что на практике чекер может точно так же сколько угодно бздеть-пердеть потому что "за конечное время" еще не значит что ты его сможешь дождаться за свою жизнь
Правда что ли? Вот это да! Никогда такого не было!
>Ну это мы уже реально дошли
>>Though Set and Type are different in Coq, this is mostly due to historical reasons
Причём тут отличия Set и Type, хуесосина тупая? Ты видишь, что там красным подчёркнуто, потому что слева и справа от равенства стоят термы разных типов?
>А ради твоих хотелок кто чего добиваться должен, петушок?
Такая смешная тупая обиженка. А ты - А ты - А ты. Аргументов нет т.к. всякая мыслительная деятельность заменена на цитирование швятых отцов.
Должен потому что типизаторы хотят чтобы их построениями пользовались мейнстримные математики, а те в свою очередь в своей работе не различают 1:N и 1:Z и им типы только мешают. Все то надо дауненку разжевывать.
(И чтоб дауненок не квакал еще - нет 1 ∈ 2 математики не доказывают и ровно поэтому им это не мешает ничем, стрелочка не поворачивается)
>ситуация
Ты скормил терм тайпчекеру, он бздит уже второй день. Твои действия?
>Правда что ли? Вот это да! Никогда такого не было!
У долбоебушки ничего сложнее a+b=b+a не доказывавшего безусловно. Out of memory это тоже народные придания.
Напомню мы говорим про
>Значит уровень доверия к такому чекеру выше.
Т.е. ты продолжаешь настаивать что ты больше веруешь в тайпчекер потому что можно доказать что он обязательно рано или поздно остановится на любом входе. Потому что?... Даже если бы он представлял из себя миллион строк говнокода. Ну долбоебушка.
>Причём тут отличия Set и Type, хуесосина тупая? Ты видишь, что там красным подчёркнуто
Конечно я же слетал на машине времени чтобы глянут в картинку которую ты запостишь в будущем. Значит ты все таки говоришь про Universe polymorphism, который кстати тоже меняли в coq разок-другой. Чем он вообще релевантен дискуссии? Ты просто решил притащить какого то невнятного говна чтобы все думали какой ты умный. Ты случайно не конструктивный клоун? Нужно срочно проверить.
Ответь пожалуйста на простой вопрос: какое понятие более общее - Машина Тьюринга или Универсальная Машина Тьюринга.
>Должен потому что типизаторы хотят чтобы их построениями пользовались мейнстримные математики
Мейнстримные математики ими пользуются, несмотря на твоё кудахтанье.
>У долбоебушки ничего сложнее a+b=b+a не доказывавшего безусловно. Out of memory это тоже народные придания.
В отличие от тебя, диванного тупого хуесоса, я OOM в разных чекерах видел не раз.
>Т.е. ты продолжаешь настаивать что ты больше веруешь
Понимаешь, петушок, веруешь тут только ты, у тебя есть мантры (типов у терма должно быть много), ересь (тип должен быть один), святые отцы (настоящие™ мейнстримные математики) и отступники (проклятые программисты). В реальном же мире бывает и так (MLTT), и сяк (теории типов с subtyping), и даже в Coq’е иногда доказывают False, а в Lean так вообще фундаментальные проблемы с разрешимостью, но мейнстримные математики, о ужас, им всё равно пользуются.
И да, это не означает, что разрешимость нинужна.
>Значит ты все таки говоришь про Universe polymorphism
Значит ты тупой пидорас-хуесос, который не может разглядеть, блядь, кумулятивность, которая в коке была до модного полиморфизма.
>Чем он вообще релевантен дискуссии?
Тупая опущенная пидорасина, если ты пролистаешь чуть вверх, то увидишь, что я писал тебе, как в Coq’е у терма два разных типа бывает, пример чего я тебе и привёл.
>Ответь пожалуйста на простой вопрос: какое понятие более общее - Машина Тьюринга или Универсальная Машина Тьюринга.
Машина Тьюринга.
>Дежурное напоминание - абстракция не может быть первичнее примеров, содержащих абстрагируемое свойство, а метаязык строится только над объектным языком, и так же не может быть первичнее него.
Получается, так и не было дано определение порядка, на котором здесь даётся определение первичности. Понятное дело, что для метаязыка как прессуппозиция подразумевается язык-объект подобно тому как пресуппозицией для вопроса "перестали ли вы пить коньяк по утрам?" является утверждение "вы пили коньяк" или для "является ли король Франции лысым?" утверждение "Франция не является республикой". Но я здесь не ставлю задачей себе логический анализ языка, а ставлю задачей выставить автора тупым долбоёбом и хохлом. Поэтому я добавлю, что для целых чисел отношение "больше" абсолютно изморфно отношению "меньше", и лишь если мы добавим аксиому, что "0<1", то мы сможешь сказать, что единица меньше минус-едницы, а не наоборот. Чисто экстенционально, без учёта смысла слов "больше" и "меньше", эти отношения одинаковые. Поэтому понять, какой смысл автор-хохол вкладывает в свои слова представляется затруднительным, а сам он его сформулировать не в состоянии в силу врождённой тупости и регидности мышления.
Опа, дежурный петух опять вылез. Санитарам объявляется выговор.
Я бы вообще этот вопрос ставил таким образом, что это не бог-из-машины, а вот как лично я могу написать программу, например, на питоне чтобы считать свои формулы, например, на латексе. Что я должен знать? Какими принципами руководствоваться? И банально какие аксиомы как правила преобразования строк мне нужны?
То есть это банальное требование воспроизводимости эксперимента, а не i+1 i-1
Ты для начало понятие строки попробуй определить строго, многие вопросы отпадут.
Понятия не имею, что ты подразумеваешь под строкой. Вот у меня текстовый редактор видит \n - значит дальше новая строка. У каждого свой взгляд.
А вот давай погорим, что такое вообще ЗНАК. Вот в отношении SRC - MSG - DST. Вот в этих рамках. И посмотрим, что ты ск4ажешь.
>Мейнстримные математики ими пользуются
А про 1 ∈ 2 нечего не спизданешь еще? Ну пользуются конечно поплевываясь, куда деваться.
Только совершенно ебанутый будет утверждать что нет никаких трудностей при переносе неформальной математики в формальную когда надо дохуя всего переиначить чтобы просто запихнуть в прувер то что тебе надо. Будешь отрицать?
>OOM в разных чекерах видел не раз.
А к чему тогда были твои восклицания. Анивей, как к такому повороту отнеслись в твоей церкви Швятой Разрешимости?
>В реальном же мире бывает и так (MLTT), и сяк
Но сначала один анон спизданул что 1 это только если 1:N а по другому никак и быть не может в сам целый Мартин Леф так сказал. А потом ты закукарекал про разрешимость и... без нее тоже наверное никак?
Но если бывает и так и сяк, то у меня больше вопросов нет.
расшифруй только еще
>Очевидно, при реализации завершающегося алгоритма можно опираться на пруф завершимости.
>Coq’е у терма два разных типа бывает
Как это поможет мне определять существенно разные типы для одного терма - 1:N, 1:Z. Давай по-новой, чего ты там хотел доказать принеся какую то обскурную
>The status of Universe Polymorphism is experimental.
фичу из coq. То что чем больше фичей в теории типов тем она сложнее? Ну охуеть ты мне глаза открыл.
Ну хотя бы не конструктивный петух, так что диалог в принципе возможен.
Знак это клеймо на жопе мовно-конструктивной петушары.
>куда деваться.
Заставляют, надо понимать, жрать теорию типов?
>Только совершенно ебанутый будет утверждать что нет никаких трудностей при переносе неформальной математики в формальную
А я такое утверждал что ли?
>когда надо дохуя всего переиначить чтобы просто запихнуть в прувер то что тебе надо
Ты, наверное, охуеешь, но если запихивать пруф в прувер с теорией множеств, то тоже придётся переиначивать.
>Будешь отрицать?
Я же не ебанутый.
>Но сначала один анон спизданул что 1 это только если 1:N а по другому никак и быть не может в сам целый Мартин Леф так сказал.
Это проблемы одного анона.
>А потом ты закукарекал про разрешимость и... без нее тоже наверное никак?
Как никак, если я тебе сам же привёл в пример Lean, у которого с ней проблемы. Разрешимость тайпчекинга — одно из хороших свойств, как непрерывность — хорошее свойство функции. Зачем вообще нужна непрерывность, без непрерывности нельзя что ли? Иногда можно, иногда нужно, точно так же как и с разрешимостью тайпчекинга (да и разрешимостью предикатов вообще). Или зачем группе коммутативность?
>расшифруй только еще
Я же уже писал. Точно так же Lean, ядро которого хорошо отделено от фронтенда (в виде парсера, elaborator’а и прочего), вызывает больше доверия, чем ядро Coq, которое перемешано с языком (языками) тактик.
Как выше верно писали, такое ещё позволяет проще «воспроизвести эксперимент». У Lean, например, есть экспортный формат, то есть ты можешь написать свой независимый чекер термов в этом формате и проверить, действительно ли пруфы из Mathlib (https://github.com/leanprover-community/mathlib4) пруфы, а не наёбка, не занимаясь восстановлением алгоритма вывода типов и сотен тактик, как это было бы в Coq’е.
Что, собственно, уже не раз делали, одна из последних попыток, например: https://github.com/digama0/lean4lean
>Как это поможет мне определять существенно разные типы для одного терма - 1:N, 1:Z. Давай по-новой, чего ты там хотел доказать принеся какую то обскурную
А разные юниверсы — это несущественно разные типы что ли, ёбаный в рот? Где проходит граница существенности?
Впрочем, то, чего именно ты хочешь, называется subtyping; хотя эти проблемы реально неплохо решаются продвинутым парсером вместе с тайпклассами (и нет, обычно их частью синтаксиса теории не делают, предвосхищая вскукареки про две разные теории на бумаге и в реализации).
>>The status of Universe Polymorphism is experimental.
Сука, блядь, какой polymorphism? Ну ты мне объясни, блядь, причём тут polymorphism? Нахуя ты его приплетаешь?
Фича, о которой я говорю, которая ломает единственность типа, называется universe cumulativity.
>куда деваться.
Заставляют, надо понимать, жрать теорию типов?
>Только совершенно ебанутый будет утверждать что нет никаких трудностей при переносе неформальной математики в формальную
А я такое утверждал что ли?
>когда надо дохуя всего переиначить чтобы просто запихнуть в прувер то что тебе надо
Ты, наверное, охуеешь, но если запихивать пруф в прувер с теорией множеств, то тоже придётся переиначивать.
>Будешь отрицать?
Я же не ебанутый.
>Но сначала один анон спизданул что 1 это только если 1:N а по другому никак и быть не может в сам целый Мартин Леф так сказал.
Это проблемы одного анона.
>А потом ты закукарекал про разрешимость и... без нее тоже наверное никак?
Как никак, если я тебе сам же привёл в пример Lean, у которого с ней проблемы. Разрешимость тайпчекинга — одно из хороших свойств, как непрерывность — хорошее свойство функции. Зачем вообще нужна непрерывность, без непрерывности нельзя что ли? Иногда можно, иногда нужно, точно так же как и с разрешимостью тайпчекинга (да и разрешимостью предикатов вообще). Или зачем группе коммутативность?
>расшифруй только еще
Я же уже писал. Точно так же Lean, ядро которого хорошо отделено от фронтенда (в виде парсера, elaborator’а и прочего), вызывает больше доверия, чем ядро Coq, которое перемешано с языком (языками) тактик.
Как выше верно писали, такое ещё позволяет проще «воспроизвести эксперимент». У Lean, например, есть экспортный формат, то есть ты можешь написать свой независимый чекер термов в этом формате и проверить, действительно ли пруфы из Mathlib (https://github.com/leanprover-community/mathlib4) пруфы, а не наёбка, не занимаясь восстановлением алгоритма вывода типов и сотен тактик, как это было бы в Coq’е.
Что, собственно, уже не раз делали, одна из последних попыток, например: https://github.com/digama0/lean4lean
>Как это поможет мне определять существенно разные типы для одного терма - 1:N, 1:Z. Давай по-новой, чего ты там хотел доказать принеся какую то обскурную
А разные юниверсы — это несущественно разные типы что ли, ёбаный в рот? Где проходит граница существенности?
Впрочем, то, чего именно ты хочешь, называется subtyping; хотя эти проблемы реально неплохо решаются продвинутым парсером вместе с тайпклассами (и нет, обычно их частью синтаксиса теории не делают, предвосхищая вскукареки про две разные теории на бумаге и в реализации).
>>The status of Universe Polymorphism is experimental.
Сука, блядь, какой polymorphism? Ну ты мне объясни, блядь, причём тут polymorphism? Нахуя ты его приплетаешь?
Фича, о которой я говорю, которая ломает единственность типа, называется universe cumulativity.
>Заставляют, надо понимать, жрать теорию типов?
Да, можно и так сказать. Когда математику надоедает марать бумагу он лезет посмотреть какие там пруверы самые модные и молодежные. И видит там - coq, agda, lean... Приходится жрать что дают.
Видел тезис что если бы в безтиповые пруферы вливали бы столько же средств то и они бы были тоже вполне конкурентны.
>Разрешимость тайпчекинга — одно из хороших свойств, как непрерывность — хорошее свойство функции.
Пример у тебя абсолютно ебанутый. Даже не знаю что еще сказать.
>Точно так же Lean, ядро которого хорошо отделено от фронтенда
Да какое блядь это имеет отношение к разрешимости. Ты совсем дурачек и не понимаешь что никакого или просто пишешь хуйню лишь бы написать побольше хуйни?
Тебе часто в детстве говорили что ты какой то тупенький?
>А разные юниверсы — это несущественно разные типы что ли, ёбаный в рот?
Но ведь ты прекрасно понял о чем я, зачем тогда опять включаешь дурачка? Или это дефолтный режим.
>Сука, блядь, какой polymorphism?
Кек знал что у тебя опять подорвет. Я мог бы написать как одно отменяет другое, ну да похуй. Я еще раз повторяю - нахуя ты его притащил, чудик? Чего хотел этим доказать?
>Видел тезис что если бы в безтиповые пруферы вливали бы столько же средств то и они бы были тоже вполне конкурентны.
Тут спорить не буду, вполне возможно, да.
>Пример у тебя абсолютно ебанутый. Даже не знаю что еще сказать.
Ну и в чём разница? У теорий типов точно так же есть синтаксис, как у, например, групп, и точно так же есть модели. Если ты воспринимаешь теорию типов как заповеди, спущенные святым (ну или наоборот, как тебе там надо?) Мартином-Лёфом, то это исключительно твои проблемы.
>Да какое блядь это имеет отношение к разрешимости. Ты совсем дурачек и не понимаешь что никакого или просто пишешь хуйню лишь бы написать побольше хуйни?
Сука, ну такая же мотивация, блядь, что ядро маленьким делать, что разрешимости добиваться. Ты реально не понимаешь?
>Тебе часто в детстве говорили что ты какой то тупенький?
У тебя комплексы какие-то?
>Я мог бы написать как одно отменяет другое, ну да похуй.
Что кого? Без (universe) полиморфизма не бывает кумулятивности? Без кумулятивности не бывает полиморфизма? Так ты же дегенерат.
>Но ведь ты прекрасно понял о чем я, зачем тогда опять включаешь дурачка?
Так это не ты верещал, что всем директивно спустили необходимость иметь каждому терму ровно один тип?
>Чего хотел этим доказать?
>>в Coq’е у терма может быть много типов
>>привожу пример
>аррряяя ПОЛИМОРФИЗМ аррряяяя
Я пишу тебе, блядь, бывает у терма много типов, даже в, казалось бы, Coq’е (но не только там), хоть и не в той форме, какой тебе надо, но у тебя почему-то от этого истошный визг.
>>Пример у тебя абсолютно ебанутый. Даже не знаю что еще сказать.
>Ну и в чём разница? У теорий типов точно так же есть синтаксис, как у, например, групп, и точно так же есть модели.
А у кошки четыре ноги и позади длинный хвост. Какой же ты ебанутый. Я хотел обсудить должна ли теория типов быть разрешимой или не обязательно и какие плюсы и минусы. Вроде удалось донести мысль что не должна. Напомню мы начали с тезиса
>А я говорю тебе, что ты хуесос и пидорас, благодаря единственности типа проще добиться завершимости алгоритма проверки типов, а в теориях, где у терма может быть много типов (ничего себе, а так не один такой умник, да?), за этим надо отдельно следить (Coq).
Теперь при более детальном рассмотрении я вижу что в нем столько нонсеквитуров что даже лениво их все разбирать.
>Сука, ну такая же мотивация, блядь, что ядро маленьким делать, что разрешимости добиваться. Ты реально не понимаешь?
Тяжело понять бред от безмозглого дебила. Маленькое ядро может реализовывать неразрешимую систему типов. Это вообще ортогональные консерны, можешь ты это уже понять ебаклак?
>>Я мог бы написать как одно отменяет другое, ну да похуй.
>Что кого? Без (universe) полиморфизма не бывает кумулятивности? Без кумулятивности не бывает полиморфизма? Так ты же дегенерат.
Сам себе напридумывал. Сам же себе и подибил. Главное по плечу себя не забудь похлопать какой ты у мамки молодец.
>хоть и не в той форме, какой тебе надо
>но у тебя почему-то от этого истошный визг.
Ору с даунича. Может потому что
>не в той форме, какой тебе надо
Не? Может попробуешь в какой надо форме принести чтобы не было никаких визгов? Но я понял твой модус-операнди это спиздануть какую то слайтли-релейтед хуету и пытаться делать умный вид.
Какой же ты непрошибаемо тупой хуесос.
>Я хотел обсудить должна ли теория типов быть разрешимой или не обязательно и какие плюсы и минусы.
Я уже написал, что необязательно, ты это прочитал, но уже, видимо, забыл.
>Теперь при более детальном рассмотрении я вижу что в нем столько нонсеквитуров что даже лениво их все разбирать.
А, так это ты, хуесосина полуграмотная? Иди нахуй отсюда, уёбок тупой.
>Маленькое ядро может реализовывать неразрешимую систему типов.
А где я писал обратное, дебилушка? Покажешь?
>Это вообще ортогональные консерны, можешь ты это уже понять ебаклак?
Опять ты жопой прочитал, но сделал далеко идущие выводы.
>Сам себе напридумывал.
Так ты напишешь, кто кого отменяет? Зачем-то начал верещать про полиморфизм, а теперь загадочно умалчиваешь, зачем, делая вид дохуя специалиста.
>Может попробуешь в какой надо форме принести чтобы не было никаких визгов?
Верещал нагло придуманную хуйню про
>У каждого объекта должен быть только один тип и задается он при определении? Вы че ебанутые?
А теперь оправдывается, что он, видите ли, на самом деле, про subtyping говорил. Просто говна поешь.
>А, так это ты
Кто? У тебя делирий?
>>Маленькое ядро может реализовывать неразрешимую систему типов.
>А где я писал обратное, дебилушка? Покажешь?
Нахуй ты вообще притащил свое маленькое ядро, клоунесса ебаная.
>Зачем-то начал верещать про полиморфизм, а теперь загадочно умалчиваешь, зачем, делая вид дохуя специалиста.
Очевидно чтобы сральню тебе разворотить. Как видишь план удался.
>>У каждого объекта должен быть только один тип и задается он при определении? Вы че ебанутые?
>А теперь оправдывается, что он, видите ли, на самом деле, про subtyping говорил.
> на самом деле, про subtyping говорил.
Чего блядь? Энивей, я же тебе говорю показывай теорию типов в которой рутинно объявляют один объект с разными типами вроде
>1 это натуральное число. А так же это целое число. И нечетное число.
А свой исторический флюк с coq'овским Set-Prop-Type-MProp(?)-сабтайпами для них и чего они там еще нахуевертели засунь себе в разорванную сральню откуда ты их вынул.
Можешь не продолжать, я уже узнал тебя по твоим неуместным латинизмами, долбоёб.
>Энивей, я же тебе говорю показывай теорию типов в которой рутинно объявляют один объект с разными типами вроде
Хули тебе показывать, если ты всё равно нихуя не понимаешь.
>А свой исторический флюк с coq'овским Set-Prop-Type-MProp(?)-сабтайпами для них и чего они там еще нахуевертели засунь себе в разорванную сральню откуда ты их вынул.
Что вот это предложение ярко и демонстрирует. Исторический флюк у него, блядь, во дегенерат.
>Можешь не продолжать, я уже узнал тебя по твоим неуместным латинизмами, долбоёб.
Реально заинтриговал. Но думаю ты снова обосрался по причине - обсерытышь по жизни. Вообще 21 век идет, привыкай дедуль.
>Хули тебе показывать, если ты всё равно нихуя не понимаешь.
На самом интересном месте слился, жаль.
>Что вот это предложение ярко и демонстрирует. Исторический флюк у него, блядь, во дегенерат.
Контр-аргументы? Будешь утверждать что в coq не нахуевертели говна? Ты похоже еще на десяток ийсикю пунктов отупел от бессильной злобы.
Продолжай мриять, что не насрал хуйни, а филигранно затроллил.
>Будешь утверждать что в coq не нахуевертели говна?
Хули ты на ходу придумываешь тезисы, пидорас-хуесос-говноед? Вот где про это речь шла?
Чет маня совсем слилась. Думал манька будет получше. Но очень плохая манька попалась, некачественная к сожалению.
Чего не скажешь о Сохацком подцепившем сифилис в ТЦК.