Двач.hk не отвечает.
Вы видите копию треда, сохраненную 17 сентября в 13:36.
Скачать тред: только с превью, с превью и прикрепленными файлами.
Второй вариант может долго скачиваться. Файлы будут только в живых или недавно утонувших тредах. Подробнее
Если вам полезен архив М.Двача, пожертвуйте на оплату сервера.
Вы видите копию треда, сохраненную 17 сентября в 13:36.
Скачать тред: только с превью, с превью и прикрепленными файлами.
Второй вариант может долго скачиваться. Файлы будут только в живых или недавно утонувших тредах. Подробнее
Если вам полезен архив М.Двача, пожертвуйте на оплату сервера.
Очередной тред, посвященный первой культуре - основаниям математики. Дежурное напоминание - абстракция не может быть первичнее примеров, содержащих абстрагируемое свойство, а метаязык строится только над объектным языком, и так же не может быть первичнее него. Просьба воздержаться от срачей на эту тему, так как тут и сраться не о чем.
Предыдущий:
https://2ch.hk/math/res/109635.html (
М)
Предыдущий:
https://2ch.hk/math/res/109635.html (
М)Не забываем определять N.
>>2865 (OP)
Что за дебил шапку писал?
Что за дебил шапку писал?
>>2870
Очевидный конструктивный петух, как и все треды до этого. Предлагаю в этот раз создать альтернативный непетушиный тред оснований, а петушню бойкотировать.
Очевидный конструктивный петух, как и все треды до этого. Предлагаю в этот раз создать альтернативный непетушиный тред оснований, а петушню бойкотировать.
>>2865 (OP)
Это тред тусовочки из какой-нибудь конфы, или тут могут накидать литературы для общего развития?
Это тред тусовочки из какой-нибудь конфы, или тут могут накидать литературы для общего развития?
>>2872
для общего развития можно и школьные учебники почитать (ну, без шуток, какую-нибудь биологию для продвинутых классов), так что конкретизируй
для общего развития можно и школьные учебники почитать (ну, без шуток, какую-нибудь биологию для продвинутых классов), так что конкретизируй
>>2872
https://libgen.rs/book/index.php?md5=DB5FD04D3AB9ECD89E5CFB7A2A9D0268
https://homotopytypetheory.org/book/
https://groupoid.github.io/formal.one/
>накидать литературы для общего развития
https://libgen.rs/book/index.php?md5=DB5FD04D3AB9ECD89E5CFB7A2A9D0268
https://homotopytypetheory.org/book/
https://groupoid.github.io/formal.one/
>>2878
Спасибо
>>2873
Ну вот в заголовке висит:
"Дежурное напоминание - абстракция не может быть первичнее примеров, содержащих абстрагируемое свойство, а метаязык строится только над объектным языком, и так же не может быть первичнее него". Это что-то из теории моделей или что это?
Спасибо
>>2873
>так что конкретизируй
Ну вот в заголовке висит:
"Дежурное напоминание - абстракция не может быть первичнее примеров, содержащих абстрагируемое свойство, а метаязык строится только над объектным языком, и так же не может быть первичнее него". Это что-то из теории моделей или что это?
>>2879
Это базовые свойства абстракции и метаязыка как явлений. Один из местных клоунов, известный как N петух, просто игнорирует эти моменты в своих жалких попытках "доказать", что аксиомы Пеано якобы не определяют множество натуральных чисел. Вычитал он это у Успенского, в целом там логика уровня того мультфильма про олимпиаду, где "баба Яга против", а вся "аргументация" строится на игнорировании сути абстракции и метаязыка.
> "Дежурное напоминание - абстракция не может быть первичнее примеров, содержащих абстрагируемое свойство, а метаязык строится только над объектным языком, и так же не может быть первичнее него". Это что-то из теории моделей или что это?
Это базовые свойства абстракции и метаязыка как явлений. Один из местных клоунов, известный как N петух, просто игнорирует эти моменты в своих жалких попытках "доказать", что аксиомы Пеано якобы не определяют множество натуральных чисел. Вычитал он это у Успенского, в целом там логика уровня того мультфильма про олимпиаду, где "баба Яга против", а вся "аргументация" строится на игнорировании сути абстракции и метаязыка.
373 Кб, 1498x1984А про аксиому фундирования сделаю некоторое дополнение, чтобы не казалось, что претензия искусственная. Есть теория множеств Aczel'а, в которой множества рассматриваются как графы. Точки - элементы, стрелочки - отношение "быть элементом". Пикрелейтед - иллюстрация.
Все ZFC-шные множества в такой теории оказываются деревьями (из-за фундированности). Но теория Aczel'а этими множествами не ограничивается и постулирует, что любой связный ориентированный граф является картинкой какого-нибудь множества. В том числе - граф с циклами.
Например, граф, состоящий из одной точки и висящей в ней петельки является картинкой множества x = {x}.
Такая теория множеств оказывается неожиданно интересной и вполне согласующейся со здравым смыслом. Поэтому интерес рассматривать анти-фундированные множества есть. И не стоит всегда предполагать, что x и {x,y} - разные множества априори.
Все ZFC-шные множества в такой теории оказываются деревьями (из-за фундированности). Но теория Aczel'а этими множествами не ограничивается и постулирует, что любой связный ориентированный граф является картинкой какого-нибудь множества. В том числе - граф с циклами.
Например, граф, состоящий из одной точки и висящей в ней петельки является картинкой множества x = {x}.
Такая теория множеств оказывается неожиданно интересной и вполне согласующейся со здравым смыслом. Поэтому интерес рассматривать анти-фундированные множества есть. И не стоит всегда предполагать, что x и {x,y} - разные множества априори.
597 Кб, 1000x568>>2865 (OP)
Снова в шапку забыл закинуть картинку, характерезующую тред... Плохой перекат.
Снова в шапку забыл закинуть картинку, характерезующую тред... Плохой перекат.
>>2865 (OP)
Общее развитие продвигается полным ходом.
Общее развитие продвигается полным ходом.
>>2879
это просто какое-то околоматематическое ШУЕ, как по ссылке https://groupoid.github.io/formal.one/ из >>2878, такое нужно игнорировать
>Это что-то из теории моделей или что это?
это просто какое-то околоматематическое ШУЕ, как по ссылке https://groupoid.github.io/formal.one/ из >>2878, такое нужно игнорировать
>>2891
Это ДРУГОЕ!!!111 Да и вообще, было бы странно ожидать чего-то содержательного от деятеля, который мало того, что не знал разницы между конструктивизмом и ультрафинитизмом, так ещё и пытался перемагивать первое вторым. Интересно, с Успенским они вместе выступали на одной сцене? Биба и Боба - два великих математика.
Это ДРУГОЕ!!!111 Да и вообще, было бы странно ожидать чего-то содержательного от деятеля, который мало того, что не знал разницы между конструктивизмом и ультрафинитизмом, так ещё и пытался перемагивать первое вторым. Интересно, с Успенским они вместе выступали на одной сцене? Биба и Боба - два великих математика.
>>2891
не знаю, не хочется смотреть часовое видео по ссылке от тех, кто рекомендует почитать Сохацкого
не знаю, не хочется смотреть часовое видео по ссылке от тех, кто рекомендует почитать Сохацкого
>>2898
Как минимум, он на голову выше всяких совковых образованцев, на которых тут дрочат, и которые в математику пошли ради того, чтобы на завод не погнали. Ты просто вслушайся, что несёт деятель с видоса >>2891 про связь текста и математики, это же полный пиздец. Ну можно же было что-то в тему почитать, ладно, я не говорю про Скиннера, там букв много и они нерусские какие-то, но зачем придумывать какую-то хуйню из головы? Ну просто скажи, что не знаешь темы. Но нет, надо с умным видом кринжа наваливать, профессор же типа. А потом всякие N петухи этой шизой индоктринируются и серят здесь годами.
Как минимум, он на голову выше всяких совковых образованцев, на которых тут дрочат, и которые в математику пошли ради того, чтобы на завод не погнали. Ты просто вслушайся, что несёт деятель с видоса >>2891 про связь текста и математики, это же полный пиздец. Ну можно же было что-то в тему почитать, ладно, я не говорю про Скиннера, там букв много и они нерусские какие-то, но зачем придумывать какую-то хуйню из головы? Ну просто скажи, что не знаешь темы. Но нет, надо с умным видом кринжа наваливать, профессор же типа. А потом всякие N петухи этой шизой индоктринируются и серят здесь годами.
>>2899
Кто индоктринировал тебя, конструктивный петух?
Кто индоктринировал тебя, конструктивный петух?
>>2899
Он полуграмотный шарлатан, который разводит неопытных, что не могут самостоятельно увидеть в его писанине грубые ошибки, о чём уже неоднократно писали, но ты упрямо продолжаешь пиарить разводилу.
>Как минимум, он на голову выше всяких совковых образованцев
Он полуграмотный шарлатан, который разводит неопытных, что не могут самостоятельно увидеть в его писанине грубые ошибки, о чём уже неоднократно писали, но ты упрямо продолжаешь пиарить разводилу.
>>2902
До вышеупомянутых деятелей в вопросах ШУЕ ему очень далеко, тем не менее.
> Он полуграмотный шарлатан,
До вышеупомянутых деятелей в вопросах ШУЕ ему очень далеко, тем не менее.
>>2903
Если есть кто-то хуже, это не повод пиарить шарлатана.
Если есть кто-то хуже, это не повод пиарить шарлатана.
>>2902
Их там и нет. Пример ты все равно не приведешь, даже один.
Кто-то что-то пукнул без единого пруфа.
> неопытных, что не могут самостоятельно увидеть в его писанине грубые ошибки,
Их там и нет. Пример ты все равно не приведешь, даже один.
> о чём уже неоднократно писали
Кто-то что-то пукнул без единого пруфа.
>>2902
Наверное нужно указать, что он эти свои тексты не публиковал, а при распространении среди своих студентов просил их дальше не рассылать. Они совершенно точно имеют элемент преувеличения с художественной целью и троллинга в целом, что довольно трудно не заметить при чтении.
Наверное нужно указать, что он эти свои тексты не публиковал, а при распространении среди своих студентов просил их дальше не рассылать. Они совершенно точно имеют элемент преувеличения с художественной целью и троллинга в целом, что довольно трудно не заметить при чтении.
>>2906
Ага, здрасьте, приехали, уже забыл что ли?
Открываю 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-буке есть про ∞-усечённые типы).
В обмен на твой анус только потом не жалуйся могу на его любимом cubicaltt пруф написать, что этот его inf_grpd эквивалентен стягиваемости (isContr, лол!) типа. И это только самое дегенеративное, что вспомнилось сходу.
>>2907
>что он эти свои тексты не публиковал
https://www.researchgate.net/profile/Maksym-Sokhatskyi-2#publications
>а при распространении среди своих студентов просил их дальше не рассылать
Неправда. Пруфов не будет, пруфы проёбаны.
>Они совершенно точно имеют элемент преувеличения с художественной целью и троллинга в целом
Всё так.
>что довольно трудно не заметить при чтении
Ну, как показывает практика, некоторым хоть ссы в глаза, всё конструктивная роса.
>>2908
Ну так напиши ему в issue, пусть оправдывается. В чем проблема? Здесь ты максимум напугаешь N-петуха украинскими словами, опять весь тред засерит.
>Открываю https://groupoid.github.io/formal.one/, кликаю по ссылке «Математичні компоненти» (https://groupoid.space/misc/library/), смотрю в его «определение» «inf_grpd» и тихо охуеваю от полного непонимания им темы (даже в HoTT-буке есть про ∞-усечённые типы).
Ну так напиши ему в issue, пусть оправдывается. В чем проблема? Здесь ты максимум напугаешь N-петуха украинскими словами, опять весь тред засерит.
>>2909
Так это бессмысленно: он в issue прокричит что-нибудь про агентов КГБ, удалит его через пару минут и заблочит на гитхабе. Прецеденты уже были.
>Ну так напиши ему в issue, пусть оправдывается. В чем проблема?
Так это бессмысленно: он в issue прокричит что-нибудь про агентов КГБ, удалит его через пару минут и заблочит на гитхабе. Прецеденты уже были.
>>2906
Тебе буквально несколько тредов назад показали, что "спектральная категория языков" это бессмысленная хуйня.
Тебе буквально несколько тредов назад показали, что "спектральная категория языков" это бессмысленная хуйня.
>>2912
Не было такого. Разговор был о том, что идея недопилена, и все. Остальное ты сам себе напридумывал.
Не было такого. Разговор был о том, что идея недопилена, и все. Остальное ты сам себе напридумывал.
>>2918
Как похожая типизация с разными названиями опровергает идею спектральной категории формальных мов?
Как похожая типизация с разными названиями опровергает идею спектральной категории формальных мов?
>>2919
Какая ещё похожая типизация с разными названими?
У Сохацкого никакого вразумительного определения нет, что выяснили два треда назад.
Какая ещё похожая типизация с разными названими?
>идею спектральной категории формальных мов
У Сохацкого никакого вразумительного определения нет, что выяснили два треда назад.
>>2920
Есть и определения, и код.
Кто выяснил? Ты и твои воображаемые друзья? Они там сейчас с тобой, в одной комнате?
> У Сохацкого никакого вразумительного определения нет,
Есть и определения, и код.
> что выяснили два треда назад.
Кто выяснил? Ты и твои воображаемые друзья? Они там сейчас с тобой, в одной комнате?
>>2922
Это откуда? Ссылку бы принёс
Это откуда? Ссылку бы принёс
102 Кб, 1036x510>>2921
Ну ё-моё, опять за старое?
Это вот эти определения, да? Что язык только с Π-питом в язык только с Σ-типом разумным образом не вкладывается не надо опять рассказывать, надеюсь?
Это вот этот код? https://github.com/groupoid/anders/blob/main/lib/foundations/mltt/mltt.anders
Универсумы там найдёшь? А индуктивные типы? А как связано «Π-form» с остальной структурой, объяснишь? А «Σ-form», кстати, тоже как? Да и «=-form», впрочем.
Забыл уже всё? Так сейчас напомним.
Ну ё-моё, опять за старое?
>определения
Это вот эти определения, да? Что язык только с Π-питом в язык только с Σ-типом разумным образом не вкладывается не надо опять рассказывать, надеюсь?
>код
Это вот этот код? https://github.com/groupoid/anders/blob/main/lib/foundations/mltt/mltt.anders
Универсумы там найдёшь? А индуктивные типы? А как связано «Π-form» с остальной структурой, объяснишь? А «Σ-form», кстати, тоже как? Да и «=-form», впрочем.
>Кто выяснил? Ты и твои воображаемые друзья? Они там сейчас с тобой, в одной комнате?
Забыл уже всё? Так сейчас напомним.
>>2925
То есть, ты даже нотацию не осилил? Там нет никаких "языков только с П типом", это сокращённые названия для разных типизированных лямбд, прямо на твоей же картинке это есть. "Язык только с П типом" это PTS, pure type system Барендрегта итд. Читать бы научился для начала...
> Это вот эти определения, да? Что язык только с Π-питом в язык только с Σ-типом разумным образом не вкладывается не надо опять рассказывать, надеюсь?
То есть, ты даже нотацию не осилил? Там нет никаких "языков только с П типом", это сокращённые названия для разных типизированных лямбд, прямо на твоей же картинке это есть. "Язык только с П типом" это PTS, pure type system Барендрегта итд. Читать бы научился для начала...
>>2927
Ты чё, Сохацкий что ли? У него такая же дегенеративная манера вести дискуссии.
А? На первой картинке что? Как вот эту ΠΣ понимать?
А на второй картинке что такое? Зачем же в (неком) MLTT-72 в синтаксисе и Π, и Σ?
Да, правда что ли? Таблицу (картинка 3) его же открой (где он, помимо прочего, каким-то образом связывает Σ с неким MLTT-72).
Ты чё, Сохацкий что ли? У него такая же дегенеративная манера вести дискуссии.
>Там нет никаких "языков только с П типом",
А? На первой картинке что? Как вот эту ΠΣ понимать?
А на второй картинке что такое? Зачем же в (неком) MLTT-72 в синтаксисе и Π, и Σ?
>"Язык только с П типом" это PTS, pure type system Барендрегта итд
Да, правда что ли? Таблицу (картинка 3) его же открой (где он, помимо прочего, каким-то образом связывает Σ с неким MLTT-72).
>>2928
PTS это, на третьей же картинке прямо написано.
MLTT 72, опять же, это там прямо написано. Если и этого мало, дальше есть полная типизация.
Затем, что в MLTT 72 есть оба этих зависимых типа. Ты даже нотацию не понял, зато спорить зачем-то лезешь.
> А? На первой картинке что?
PTS это, на третьей же картинке прямо написано.
> Как вот эту ΠΣ понимать?
MLTT 72, опять же, это там прямо написано. Если и этого мало, дальше есть полная типизация.
> А на второй картинке что такое? Зачем же в (неком) MLTT-72 в синтаксисе и Π, и Σ?
Затем, что в MLTT 72 есть оба этих зависимых типа. Ты даже нотацию не понял, зато спорить зачем-то лезешь.
>>2929
ΠΣ — это PTS? Или что ты хотел сказать?
А, так ΠΣ — это MLTT-72? Я тебе говорю: раз Сохацкий использует O_ΠΣ там, где подразумевает использование обеих конструкций (именно подразумевает, потому что никаких синтаксических деревьев он строить почему-то не хочет), то O_Σ — это, очевидно, синтаксис лишь с Σ. И, далее, где (MLTT-72) Сохацкий подразумевает использование и Π, и Σ, он пишет и O_Π, и O_Σ. Так откуда стрелки из O_Π в O_Σ?
Да, а теперь см. выше.
Кто тут не понял-то, ёпт?
>PTS это, на третьей же картинке прямо написано.
ΠΣ — это PTS? Или что ты хотел сказать?
>MLTT 72, опять же, это там прямо написано.
А, так ΠΣ — это MLTT-72? Я тебе говорю: раз Сохацкий использует O_ΠΣ там, где подразумевает использование обеих конструкций (именно подразумевает, потому что никаких синтаксических деревьев он строить почему-то не хочет), то O_Σ — это, очевидно, синтаксис лишь с Σ. И, далее, где (MLTT-72) Сохацкий подразумевает использование и Π, и Σ, он пишет и O_Π, и O_Σ. Так откуда стрелки из O_Π в O_Σ?
>Затем, что в MLTT 72 есть оба этих зависимых типа.
Да, а теперь см. выше.
>Ты даже нотацию не понял, зато спорить зачем-то лезешь.
Кто тут не понял-то, ёпт?
>>2931
То есть будем неудобные вопросы просто игнорировать? А с кодом-то там что, всё нормально?
Зачем ты вообще оправдываешься за этого проходимца? Лучше бы нормально в тему вкатился, чтобы не плавать в материале как Максимка, что советовали два треда назад ещё.
То есть будем неудобные вопросы просто игнорировать? А с кодом-то там что, всё нормально?
Зачем ты вообще оправдываешься за этого проходимца? Лучше бы нормально в тему вкатился, чтобы не плавать в материале как Максимка, что советовали два треда назад ещё.
>>2932
Могу ещё добавить, что в другом разделе (внезапно), можно найти эти самые O_Π и O_Σ, и там, оказывается, в O_Π только лишь Π-тип, а в O_Σ, да, только Σ-тип.
Могу ещё добавить, что в другом разделе (внезапно), можно найти эти самые O_Π и O_Σ, и там, оказывается, в O_Π только лишь Π-тип, а в O_Σ, да, только Σ-тип.
>>2934
Там написано, что если к языку с O_Π добавить O_Σ, получится MLTT-72 (або O_ΠΣ). В чём проблема?
Вот тебе, короче говоря, заготовка: https://pastebin.com/u70gz6Dk
Заполняй отмеченное место построением обсуждаемой стрелки.
>Описание ко второй картинке прочитай и не неси дичь.
Там написано, что если к языку с O_Π добавить O_Σ, получится MLTT-72 (або O_ΠΣ). В чём проблема?
Вот тебе, короче говоря, заготовка: https://pastebin.com/u70gz6Dk
Заполняй отмеченное место построением обсуждаемой стрелки.
>>2935
Проблема в том, что ты требуешь стрелку из PTS не в MLTT 72, а в сигма тип, который просто добавляется к PTS для получения MLTT 72. Либо это троллинг тупостью, либо ты правда не понимаешь о чем речь вообще.
И тут N петуха порвало.
> Там написано, что если к языку с O_Π добавить O_Σ, получится MLTT-72 (або O_ΠΣ). В чём проблема?
Проблема в том, что ты требуешь стрелку из PTS не в MLTT 72, а в сигма тип, который просто добавляется к PTS для получения MLTT 72. Либо это троллинг тупостью, либо ты правда не понимаешь о чем речь вообще.
> module dvach where
> data nat
> = zero
> | succ (n : nat)
И тут N петуха порвало.
18 Кб, 753x129>>2937
Ну правильно, а у Сохацкого что на пике, алло?
>Проблема в том, что ты требуешь стрелку из PTS не в MLTT 72, а в сигма тип, который просто добавляется к PTS для получения MLTT 72.
Ну правильно, а у Сохацкого что на пике, алло?
68 Кб, 1036x510>>2938
У тебя часть пика. У Сохацкого там то же, что я описал, а именно, что каждая последующая мова в списке содержит в себе предыдущую.
> Ну правильно, а у Сохацкого что на пике, алло?
У тебя часть пика. У Сохацкого там то же, что я описал, а именно, что каждая последующая мова в списке содержит в себе предыдущую.
>>2939
Речь сейчас про первую часть пика (которая каким-то образом должна порождать вторую часть).
Речь сейчас про первую часть пика (которая каким-то образом должна порождать вторую часть).
>>2941
Нет, он пишет, что послідовність синтаксичних дерев (первая часть пика) генерує (!) відповідну послідовність мов програмування.
На первом пике самостоятельная послідовність (объекты + стрелки), которую и обсуждаем.
Нет, он пишет, что послідовність синтаксичних дерев (первая часть пика) генерує (!) відповідну послідовність мов програмування.
На первом пике самостоятельная послідовність (объекты + стрелки), которую и обсуждаем.
86 Кб, 772x495>>2942
Давай все-таки не будем из контекста что-то дергать и обсуждать как вещь в себе? Там все определения приведены, читай.
Давай все-таки не будем из контекста что-то дергать и обсуждать как вещь в себе? Там все определения приведены, читай.
>>2943
Какую, блядь, вещь в себе, ты гуманитарий что ли?
Тебе Сохацкий чёрным по белому написал, что есть вот такая послідовність, а ты делаешь вид, что он такого не писал.
Какую, блядь, вещь в себе, ты гуманитарий что ли?
Тебе Сохацкий чёрным по белому написал, что есть вот такая послідовність, а ты делаешь вид, что он такого не писал.
>>2925
Возможно имеется в виду "последовательность" в таком же смысле в каком "хуй - пизда - джигурда" последовательность слов.
Возможно имеется в виду "последовательность" в таком же смысле в каком "хуй - пизда - джигурда" последовательность слов.
>>2945
Да, конечно, а следом почему последовательность уже настоящая, в категории? Или там тоже?
Можно миллион оправданий придумать (зачем?), а настоящий ответ один: Максим нарисовал стрелочек, чтобы нарисовать стрелочек, чтоб пацаны зауважали; никакого глубокого смысла в этих стрелках просто нет.
Или непонятно? Мне продолжить и в https://groupoid.github.io/formal.one/ и https://github.com/groupoid/anders/ ещё перлов найти?
Да, конечно, а следом почему последовательность уже настоящая, в категории? Или там тоже?
Можно миллион оправданий придумать (зачем?), а настоящий ответ один: Максим нарисовал стрелочек, чтобы нарисовать стрелочек, чтоб пацаны зауважали; никакого глубокого смысла в этих стрелках просто нет.
Или непонятно? Мне продолжить и в https://groupoid.github.io/formal.one/ и https://github.com/groupoid/anders/ ещё перлов найти?
Как переводится derivation на Русский? Или это от лингвистического понятия деревации и прям так и писать?
"A derivation in type theory is a finite tree in which each node is a valid rule of inference"
"A derivation in type theory is a finite tree in which each node is a valid rule of inference"
>>2946
Давай. Я не понимаю чего вообще этот хохол пытается показать. Вроде выстраивает какую то мета-теорию языков в своем собственном собранном на коленке язычке. План надежный просто как швейцарские часы.
Давай. Я не понимаю чего вообще этот хохол пытается показать. Вроде выстраивает какую то мета-теорию языков в своем собственном собранном на коленке язычке. План надежный просто как швейцарские часы.
>>2948
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
>>2948
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
>>2950
А вот ещё определение окружности через пустой тип, конечно же: https://github.com/groupoid/anders/commit/447eff7b6ebd5f51a3af4d2d00aa8861d082f3f5#diff-91d9514806ff2092e37976b0bf8c79e48410ea90f57143009e962e5cf82d69ecR387
А вот ещё определение окружности через пустой тип, конечно же: https://github.com/groupoid/anders/commit/447eff7b6ebd5f51a3af4d2d00aa8861d082f3f5#diff-91d9514806ff2092e37976b0bf8c79e48410ea90f57143009e962e5cf82d69ecR387
>>2953
Ну и вот ещё несколько раз путает U с одноэлементным типом: https://github.com/groupoid/anders/blob/66c592c6246da96c5f32581460142b057425faaf/lib/mathematics/categories/abelian.anders#L11
Ну и вот ещё несколько раз путает U с одноэлементным типом: https://github.com/groupoid/anders/blob/66c592c6246da96c5f32581460142b057425faaf/lib/mathematics/categories/abelian.anders#L11
91 Кб, 686x591>>2956
Чекнул их "введение в матлогику", у них "дерево вывода" это "дерево формул" с доп.условием. Но поскольку в книжице по теории типов нет введения понятия формулы, а Автор постоянно используют обороты типо we express this as\they are introduced as follow, уточняя что это всё inference по inference rule которые образуют derivation. Дерево вывода оказывается более уместней, чем дерево формул без формул.
Чекнул их "введение в матлогику", у них "дерево вывода" это "дерево формул" с доп.условием. Но поскольку в книжице по теории типов нет введения понятия формулы, а Автор постоянно используют обороты типо we express this as\they are introduced as follow, уточняя что это всё inference по inference rule которые образуют derivation. Дерево вывода оказывается более уместней, чем дерево формул без формул.
>>2959
Вот ещё в переводе 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/
Вот ещё в переводе 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/
>>2960
"Выведение" хороший вариант. Звучит естественно в контексте с древом\выводом и к тому-же укладывается в одно слово.
"Выведение" хороший вариант. Звучит естественно в контексте с древом\выводом и к тому-же укладывается в одно слово.
Где достать последние версии конспектов Вавилова? Гуглятся какие-то огрызки да ещё с такой херотенью:
wSEMYSLI, KOTORYEMOGUTPRIJTIW GOLOWUPRI^TENII DANNOJKNIGI,QWLQ@TSQINTELLEKTUALXNOJSOBSTWENNOSTX@ AWTORAIOB_EKTOMAWTORSKOGOPRAWA.iHNELICENZIROWANNOE OBDUMYWANIEZAPRE]AETSQ.
wSEMYSLI, KOTORYEMOGUTPRIJTIW GOLOWUPRI^TENII DANNOJKNIGI,QWLQ@TSQINTELLEKTUALXNOJSOBSTWENNOSTX@ AWTORAIOB_EKTOMAWTORSKOGOPRAWA.iHNELICENZIROWANNOE OBDUMYWANIEZAPRE]AETSQ.
>>2948
Бля, зачем ты саммонил хохла, поток дерьма теперь на пару тредов не остановать :С
Бля, зачем ты саммонил хохла, поток дерьма теперь на пару тредов не остановать :С
>>2965
Значение знаешь?
Думаю, нет, ведь ты у него даже нотацию не осилил.
> инфоциган
Значение знаешь?
> сохацкий достоин моего внимания?
Думаю, нет, ведь ты у него даже нотацию не осилил.
>>2966
Моя терминология предельно точна, он именно инфоциган который пиарится на хайповой теме, даже не математик а кодерок из занюханного хуторского говновузика с кафедры прикладной математики (т.е. даже ни математик ни программист).
Моя терминология предельно точна, он именно инфоциган который пиарится на хайповой теме, даже не математик а кодерок из занюханного хуторского говновузика с кафедры прикладной математики (т.е. даже ни математик ни программист).
>>2966
Так какие там морфизмы между O_Π и O_Σ синтаксическими деревьями например?
Так какие там морфизмы между O_Π и O_Σ синтаксическими деревьями например?
>>2967
Инфоциганство это не пиар на чем-то, а продажа успешного успеха в виде курсов, наставничества, гивов итп шлака. К Сохацкому можно по-разному относиться, но он не инфоциган, это факт.
Инфоциганство это не пиар на чем-то, а продажа успешного успеха в виде курсов, наставничества, гивов итп шлака. К Сохацкому можно по-разному относиться, но он не инфоциган, это факт.
>>2969
Так он свою псевдонаучную хуергу продаёт под видом математики. Просто аудитория специфическая, но сути это не меняет.
Так он свою псевдонаучную хуергу продаёт под видом математики. Просто аудитория специфическая, но сути это не меняет.
>>2969
Так он же успех и наставничество и продаёт. Ты его ТОПОВОГО ПРОГОММИСТА видел? А ведь ему донатили (и, вероятно, всё ещё донатят) за такое.
Так он же успех и наставничество и продаёт. Ты его ТОПОВОГО ПРОГОММИСТА видел? А ведь ему донатили (и, вероятно, всё ещё донатят) за такое.
25 Кб, 464x305>>2978
Хули ты боевыми картиночками кидаешься, уёбище? Где построение стрелки?
Хули ты боевыми картиночками кидаешься, уёбище? Где построение стрелки?
>>2980
Обпучкался с пикчи.
Обпучкался с пикчи.
>>2980
Неплохо.
Неплохо.
>>2979
Ты дееспособный вообще? Весь код есть в anders, там смотри. Если нотацию осилишь, что маловероятно.
Ты дееспособный вообще? Весь код есть в anders, там смотри. Если нотацию осилишь, что маловероятно.
>>2983
Я этот Anders писал, так что получше тебя знаю, где какой там код. Этой конкретной стрелки там нет.
Я этот Anders писал, так что получше тебя знаю, где какой там код. Этой конкретной стрелки там нет.
>>2976
Ты совсем чтоли дебил? Себя продает, свои высеры.
>Где он что-то продает, поридж? Все бесплатно на гитхабе.
Ты совсем чтоли дебил? Себя продает, свои высеры.
Лол, конструктивный петух снова схватился за боевые картиночки.
>>2987
Даже мимокроку уже понятно, что тебе говорят про стрелку из синтаксического дерева O_Π в синтаксическое дерево O_Σ.
>Из PTS в MLTT 72? Хуевый ты писатель значит.
Даже мимокроку уже понятно, что тебе говорят про стрелку из синтаксического дерева O_Π в синтаксическое дерево O_Σ.
133 Кб, 919x750>>2990
Тебе само название "спектральная категория формальных мов" о чем-нибудь говорит? Стрелки там между формальными языками. О чем там прямо написано в определениях из главы 2.3. В общем, я тебя услышал, скибидитуалетикс, теперь уебывай
Тебе само название "спектральная категория формальных мов" о чем-нибудь говорит? Стрелки там между формальными языками. О чем там прямо написано в определениях из главы 2.3. В общем, я тебя услышал, скибидитуалетикс, теперь уебывай
>>2991
Очевидно она говорит что автор "мов" сказочный долбоёб наципятак которому во время не дали таблеток.
>Тебе само название "спектральная категория формальных мов" о чем-нибудь говорит?
Очевидно она говорит что автор "мов" сказочный долбоёб наципятак которому во время не дали таблеток.
>>2992
Ты даже нотацию не осилил. Но долбаебом называешь не себя, что было бы правдой, а кого-то другого. Типичный пердеж
Ты даже нотацию не осилил. Но долбаебом называешь не себя, что было бы правдой, а кого-то другого. Типичный пердеж
20 Кб, 835x133>>2987
Оставляй фейкопочту.
Из O_Π в O_Σ, ну ёпт.
Я-то тут причём вообще? Я прувер писал, а не диссер Сохацкому и/или его формализацию; о наличии той или иной формализации в репозитории я могу говорить, поскольку сам прувер, стандартная библиотека к нему, а также кое-какой код Сохацкого, включая обрывочные формализации диссера, находятся в одном репозитории.
Сохацкий вообще эту, кхм, монографию о категорії формальних мов начал писать ещё до начала любых работ над Anders.
>>2991
Вообще-то речь о послідовності синтаксичних дерев (смотрим на пик), которая генерує послідовність мов, и стрелки в обсуждаемом фрагменте между деревьями/синтаксисами.
>Пруфанешь?
Оставляй фейкопочту.
>Из PTS в MLTT 72?
Из O_Π в O_Σ, ну ёпт.
>Хуевый ты писатель значит.
Я-то тут причём вообще? Я прувер писал, а не диссер Сохацкому и/или его формализацию; о наличии той или иной формализации в репозитории я могу говорить, поскольку сам прувер, стандартная библиотека к нему, а также кое-какой код Сохацкого, включая обрывочные формализации диссера, находятся в одном репозитории.
Сохацкий вообще эту, кхм, монографию о категорії формальних мов начал писать ещё до начала любых работ над Anders.
>>2991
Вообще-то речь о послідовності синтаксичних дерев (смотрим на пик), которая генерує послідовність мов, и стрелки в обсуждаемом фрагменте между деревьями/синтаксисами.
>>2997
А где там в тексте прямо написано, что между индуктивными типами именно морфизмы в категорном смысле, а не просто отношение следования?
> Из O_Π в O_Σ, ну ёпт.
> Вообще-то речь о послідовності синтаксичних дерев (смотрим на пик), которая генерує послідовність мов, и стрелки в обсуждаемом фрагменте между деревьями/синтаксисами.
А где там в тексте прямо написано, что между индуктивными типами именно морфизмы в категорном смысле, а не просто отношение следования?
71 Кб, 744x360>>3013
Спектральная категория формальных мов прямо заявлена, а спектральная категория индуктивных типов - нет.
То есть, индуктивными типами, см. визначення 23 и 24.
> То есть в одном и том же предложении одно и то же слово означает разные вещи?
Спектральная категория формальных мов прямо заявлена, а спектральная категория индуктивных типов - нет.
> Между синтаксическими деревьями.
То есть, индуктивными типами, см. визначення 23 и 24.
>>3014
И стрелок между ними совсем нет, да?
Так это не любые индуктивные типы.
>а спектральная категория индуктивных типов - нет.
И стрелок между ними совсем нет, да?
>То есть, индуктивными типами, см. визначення 23 и 24.
Так это не любые индуктивные типы.
>>3015
Так где там написано, что стрелки между индуктивными типами это морфизмы?
> И стрелок между ними совсем нет, да?
Так где там написано, что стрелки между индуктивными типами это морфизмы?
>>3017
То есть, ты не рассматриваешь вариант, что это просто стрелочные типы функций в пределах одной мовы, содержащей эти типы?
То есть, ты не рассматриваешь вариант, что это просто стрелочные типы функций в пределах одной мовы, содержащей эти типы?
>>3018
То есть функции в cubicaltt? Заготовка выше.
То есть функции в cubicaltt? Заготовка выше.
>>2865 (OP)
Зайдём с другого конца. Предположим это так, тогда на каком основании ты используешь абстракцию которую не принял как аксиому (у тебя ебанька по твоим же слоам есть только несколько конкретных примеров, тебе кто разрешал переходить к следующему примеру и т.д)? И тем более опираться на метаязык при обосновании понятий объектного языка если он вторичен? Ты ебанько задним числом математематические понятия определяешь чтоли?
>Дежурное напоминание - абстракция не может быть первичнее примеров, содержащих абстрагируемое свойство, а метаязык строится только над объектным языком, и так же не может быть первичнее него.
Зайдём с другого конца. Предположим это так, тогда на каком основании ты используешь абстракцию которую не принял как аксиому (у тебя ебанька по твоим же слоам есть только несколько конкретных примеров, тебе кто разрешал переходить к следующему примеру и т.д)? И тем более опираться на метаязык при обосновании понятий объектного языка если он вторичен? Ты ебанько задним числом математематические понятия определяешь чтоли?
>>3024
N-петух, какой еще "переход к следующему примеру"? Аксиомы Пеано это и есть пример, содержащий абстракцию потенциальной бесконечности.
> (у тебя ебанька по твоим же слоам есть только несколько конкретных примеров, тебе кто разрешал переходить к следующему примеру и т.д)?
N-петух, какой еще "переход к следующему примеру"? Аксиомы Пеано это и есть пример, содержащий абстракцию потенциальной бесконечности.
>>3025
Мовный газнюх, ты в своих газах запутался или что? Сам же предлагал обосновать абстракцию (которая вторична) фиксированной серией примеров (которые в понимании твоего пропитанного газами мозга первичны). Вот тебе и вопрос, как ты ебло на одних примерах собрался с потенциально неограниченными структурами работать? Ты это технически не можешь сделать т.к. еще не ввёл "вторичную" абстракцию. Про Пеано в очередной раз в лужу пёрнул - аксиомы сами собой ничего не обосновывают, они работают только если принята абстракция потенциальной осуществимости.
Мовный газнюх, ты в своих газах запутался или что? Сам же предлагал обосновать абстракцию (которая вторична) фиксированной серией примеров (которые в понимании твоего пропитанного газами мозга первичны). Вот тебе и вопрос, как ты ебло на одних примерах собрался с потенциально неограниченными структурами работать? Ты это технически не можешь сделать т.к. еще не ввёл "вторичную" абстракцию. Про Пеано в очередной раз в лужу пёрнул - аксиомы сами собой ничего не обосновывают, они работают только если принята абстракция потенциальной осуществимости.
>>3035
Что ты трясёшься, у тебя синдром Туретта?
Абстракция потенциальной осуществимости - это свойство аксиом Пеано и других подобных аксиоматик, правил построения итд. Это следует из самого определения абстракции, она не висит в воздухе, а вторична по отношению к конкретным примерам, имеющим это свойство. Тут вообще не о чем спорить итд, это элементарные вещи.
Что ты трясёшься, у тебя синдром Туретта?
> аксиомы сами собой ничего не обосновывают, они работают только если принята абстракция потенциальной осуществимости.
Абстракция потенциальной осуществимости - это свойство аксиом Пеано и других подобных аксиоматик, правил построения итд. Это следует из самого определения абстракции, она не висит в воздухе, а вторична по отношению к конкретным примерам, имеющим это свойство. Тут вообще не о чем спорить итд, это элементарные вещи.
>>3039
Трясу яичками по лбу твоей мамаши.
Ты через "вторичность" пытался отрицать что абстракция потенциальной осуществимости принимается как исходное неопределяемое понятие, теперь ты говоришь что всегда её предполагал (таблетки помогли?).
При её наличии натуральное число это базовый объект плюс абстракция, определение аксиомами Пеано использует ту же базу только более сложное, а поэтому нинужно. Ты или более простое определение принеси или признай себя петухом коим ты являешься.
>Что ты трясёшься, у тебя синдром Туретта?
Трясу яичками по лбу твоей мамаши.
> Абстракция потенциальной осуществимости - это свойство аксиом Пеано и других подобных аксиоматик, правил построения итд. Это следует из самого определения абстракции, она не висит в воздухе, а вторична по отношению к конкретным примерам, имеющим это свойство. Тут вообще не о чем спорить итд, это элементарные вещи.
Ты через "вторичность" пытался отрицать что абстракция потенциальной осуществимости принимается как исходное неопределяемое понятие, теперь ты говоришь что всегда её предполагал (таблетки помогли?).
При её наличии натуральное число это базовый объект плюс абстракция, определение аксиомами Пеано использует ту же базу только более сложное, а поэтому нинужно. Ты или более простое определение принеси или признай себя петухом коим ты являешься.
>>3041
Перечитай ещё раз оп-пост, я там все изложил, и к этому нечего добавить ни мне, ни тебе. Абстракция не может быть "исходным неопределяемым понятием", у этого термина есть общепринятое определение. Натуральное число это никакой не "базовый объект", это элемент множества. Считаю этот вопрос закрытым.
Перечитай ещё раз оп-пост, я там все изложил, и к этому нечего добавить ни мне, ни тебе. Абстракция не может быть "исходным неопределяемым понятием", у этого термина есть общепринятое определение. Натуральное число это никакой не "базовый объект", это элемент множества. Считаю этот вопрос закрытым.
>>3043
Там шизофазия написана, как и вся твоя писанина.
Опять таблетки кончились, шиз? Абстракция всегда неопределяемое понятие, т.к. не сводится к элементарным вещами иначе бы это было бы обычное определение.
Базовый объект это единица, а всё множество формируется из 1 на основе абстракции потенциальной осущетвимости. Аксиоматика Пеано лишь постфактум описывает построенный таким образом объект, сама по себе она ничего не определяет. Ну и как уже говорилось в принципе не может определять т.к. даже в своей формулировке опирается на абстракцию потенциальной осуществимости в метаязыке.
Ты своё безпруфное мнение лечащим врачам изливай, всем остальным на него похую. Ты или доказательство давай или корректное определение без скрытых замкнутых кругов и прочих логических ошибок которые в твоём пиздедже на каждом шагу.
>Перечитай ещё раз оп-пост, я там все изложил, и к этому нечего добавить ни мне, ни тебе.
Там шизофазия написана, как и вся твоя писанина.
> Абстракция не может быть "исходным неопределяемым понятием"
Опять таблетки кончились, шиз? Абстракция всегда неопределяемое понятие, т.к. не сводится к элементарным вещами иначе бы это было бы обычное определение.
>Натуральное число это никакой не "базовый объект", это элемент множества.
Базовый объект это единица, а всё множество формируется из 1 на основе абстракции потенциальной осущетвимости. Аксиоматика Пеано лишь постфактум описывает построенный таким образом объект, сама по себе она ничего не определяет. Ну и как уже говорилось в принципе не может определять т.к. даже в своей формулировке опирается на абстракцию потенциальной осуществимости в метаязыке.
>Считаю этот вопрос закрытым.
Ты своё безпруфное мнение лечащим врачам изливай, всем остальным на него похую. Ты или доказательство давай или корректное определение без скрытых замкнутых кругов и прочих логических ошибок которые в твоём пиздедже на каждом шагу.
>>3049
А давай-ка ты источники своей шизы приведешь. И нет, той статейкой Успенского на одностраничном сайтике типа укоз ру можешь подтереться. Конкретно:
Где это написано? Если это хуйня из головы, так и пиши. Я приводил общепринятые определения понятия абстракции и метаязыка. Теперь ты давай пруфы, что твоя писанина это не шиза совкового скуфидона, а принятые в математике вещи.
А давай-ка ты источники своей шизы приведешь. И нет, той статейкой Успенского на одностраничном сайтике типа укоз ру можешь подтереться. Конкретно:
> Абстракция всегда неопределяемое понятие,
> Базовый объект это единица, а всё множество формируется из 1 на основе абстракции потенциальной осущетвимости. Аксиоматика Пеано лишь постфактум описывает построенный таким образом объект
Где это написано? Если это хуйня из головы, так и пиши. Я приводил общепринятые определения понятия абстракции и метаязыка. Теперь ты давай пруфы, что твоя писанина это не шиза совкового скуфидона, а принятые в математике вещи.
333 Кб, 781x794Вумные мысли о N
>>3050
Источник не мой, а твой. Просто ты читать не умеешь, копипастишь рандомные фрагменты не понимая что за ними стоит, зачем они вводятся и что (и при каких условиях) определяют.
Успенский хотя бы работающий математик в топовом универе, а на твоей стороне только фрики вроде мовного говнокодерка воннаби математика из провициального быдловузика для нациков в какой-то щитхол кантри, который даже матфак не осилил.
Причем тут укоз, дебил, там просто пиратская копия его книжки хостится.
Ещё про это писали как минимум Пуанкаре и Кронекер, но ты хуйло пиздливое специально как баран упёрся в одного Успенского в попытках съехать на дебильных шуточках (типа гыгы, совок успенский чета спизданул).
Везде, я ж за тебя дебила не могу прочитать. Ты привёл только нерелевантуню хуйню которая вообще никак не обосновывала N, точнее скопипастил то что сам нихуя не понял.
Хуйня из больной головы это мовная шизофазия твоего протыка уёбка сохацкого.
Ты не одного пруфа не показал, какое блять "теперь"? Хоть за одно своё слово ответь, мразь тупая. Ты же спиздянул якобы аксиомы Пеано что-то там определяют, вот и тащи доказательства, как.
Пруфы тебе даны неоднократно: 1) аксиомы Пеано формулируются как конкретная формальная система, любая ФС необходимо использует абстракцию потенциальной осуществимости. 2) Для доказательства существования множества удовлетворяющего этим аксиомам ты опять вынужден ссылаться на абстракцию осуществимости когда доберешься до аксиомы индукции.
Источник не мой, а твой. Просто ты читать не умеешь, копипастишь рандомные фрагменты не понимая что за ними стоит, зачем они вводятся и что (и при каких условиях) определяют.
Успенский хотя бы работающий математик в топовом универе, а на твоей стороне только фрики вроде мовного говнокодерка воннаби математика из провициального быдловузика для нациков в какой-то щитхол кантри, который даже матфак не осилил.
Причем тут укоз, дебил, там просто пиратская копия его книжки хостится.
Ещё про это писали как минимум Пуанкаре и Кронекер, но ты хуйло пиздливое специально как баран упёрся в одного Успенского в попытках съехать на дебильных шуточках (типа гыгы, совок успенский чета спизданул).
>Где это написано? Если это хуйня из головы, так и пиши. Я приводил общепринятые определения понятия абстракции и метаязыка.
Везде, я ж за тебя дебила не могу прочитать. Ты привёл только нерелевантуню хуйню которая вообще никак не обосновывала N, точнее скопипастил то что сам нихуя не понял.
Хуйня из больной головы это мовная шизофазия твоего протыка уёбка сохацкого.
>Теперь
Ты не одного пруфа не показал, какое блять "теперь"? Хоть за одно своё слово ответь, мразь тупая. Ты же спиздянул якобы аксиомы Пеано что-то там определяют, вот и тащи доказательства, как.
>ты давай пруфы, что твоя писанина это не шиза совкового скуфидона, а принятые в математике вещи.
Пруфы тебе даны неоднократно: 1) аксиомы Пеано формулируются как конкретная формальная система, любая ФС необходимо использует абстракцию потенциальной осуществимости. 2) Для доказательства существования множества удовлетворяющего этим аксиомам ты опять вынужден ссылаться на абстракцию осуществимости когда доберешься до аксиомы индукции.
>>3052
Цитаты.
Ссылки где?
Пока что от тебя поступала только хуйня из головы.
Неси цитаты, где ты это взял.
Это не пруфы, а "твое мнение". Абстракция потенциальной осуществимости это свойство, а не какая-то высшая истина, существующая вне примеров, содержащих её. По первой же ссылке в Википедии:
Нигде нет хуйни о том, что абстракция это какое-то "неопределяемое понятие", к которому нужно возноситься в молитве для определения чего-то, содержащего абстрагируемое свойство. Один из таких примеров - аксиомы Пеано.
> Ещё про это писали как минимум Пуанкаре и Кронекер,
Цитаты.
> Везде,
Ссылки где?
> Пруфы тебе даны неоднократно:
Пока что от тебя поступала только хуйня из головы.
> любая ФС необходимо использует абстракцию потенциальной осуществимости.
Неси цитаты, где ты это взял.
> 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.
Так как МЛ тогда предлагает доказать что-либо если не в формальной системе? Уверовать?
208 Кб, 968x733>>3054
> поридж начинает подозревать, что конструктивизм чем-то неуловимо отличается от формализма, но вот чем? Сможет ли пердикс понять, в чем тут дело и почему интуиционизм со времён Брауэра рассматривался как отдельное направление в основаниях, а не как часть формализма? Продолжаем зоонаблюдения
4 Кб, 81x433>>3055
Что бы не осквернять шизой в принципе вменяемую программу формализации математики?
>почему интуиционизм со времён Брауэра рассматривался как отдельное направление в основаниях, а не как часть формализма
Что бы не осквернять шизой в принципе вменяемую программу формализации математики?
>>3058
Я читал Сохацкого в подлиннике.
Я читал Сохацкого в подлиннике.
>>3054
Результаты, связанные с нашей способностью осуществлять конструктивные процессы, в математике часто формулируются в виде теорем существования, утверждающих существование объектов, удовлетворяющих таким-то требованиям.
В конструктивной математике под этим подразумевается, что построение таких объектов потенциально осуществимо, т, е.что мы владеем способом их построения.
Это конструктивное понимание теорем существования расходится с тем, как их понимают в классической математике. Правда, „классики" не любят объяснять свое понимание таких теорем. Однако из того, как они обходятся со словом «существует», следует, что их понимание этого слова отлично от конструктивного. Они, например, считают возможным утверждать, существование конструктивного объекта, удовлетворяющего данному требованию, уже тогда, когда им удается путем «приведения к нелепости» опровергнуть предположение о том, что ни один объект не удовлетворяет этому требованию. Способ построения искомого объекта может при этом и небыть известен. Таким образом, конструктивное понимание высказываний о существовании отлично от классического.
Результаты, связанные с нашей способностью осуществлять конструктивные процессы, в математике часто формулируются в виде теорем существования, утверждающих существование объектов, удовлетворяющих таким-то требованиям.
В конструктивной математике под этим подразумевается, что построение таких объектов потенциально осуществимо, т, е.что мы владеем способом их построения.
Это конструктивное понимание теорем существования расходится с тем, как их понимают в классической математике. Правда, „классики" не любят объяснять свое понимание таких теорем. Однако из того, как они обходятся со словом «существует», следует, что их понимание этого слова отлично от конструктивного. Они, например, считают возможным утверждать, существование конструктивного объекта, удовлетворяющего данному требованию, уже тогда, когда им удается путем «приведения к нелепости» опровергнуть предположение о том, что ни один объект не удовлетворяет этому требованию. Способ построения искомого объекта может при этом и небыть известен. Таким образом, конструктивное понимание высказываний о существовании отлично от классического.
>>3061
Абстракция потенциальной осуществимости позволяет нам рассуждать о сколь угодно длинных конструктивных процессах и сколь угодно больших конструктивных объектах. Их осуществимость потенциальна: они были бы осуществимы практически, располагай мы достаточными пространством, временем и материалом.
Абстракция потенциальной осуществимости, как и всякая абстракция, вносит туда, куда она привлекается, элемент фантазии. Он неизбежно присутствует во всякой абстрактной науке, в том числе и в математике. Классическая математика привлекает абстракции, идущие гораздо дальше абстракций конструктивной математики. В частности, она пользуется абстракцией актуальной бесконечности, т. е. позволяет себе рассуждать о „бесконечных множествах" как о законченных неконструктивных „объектах". Различие между „классиками" и„конструктивистами" состоит в том, что они привлекают раз-разные абстракции, т. е. фантазируют по-разному.
Абстракция потенциальной осуществимости позволяет нам рассуждать о сколь угодно длинных конструктивных процессах и сколь угодно больших конструктивных объектах. Их осуществимость потенциальна: они были бы осуществимы практически, располагай мы достаточными пространством, временем и материалом.
Абстракция потенциальной осуществимости, как и всякая абстракция, вносит туда, куда она привлекается, элемент фантазии. Он неизбежно присутствует во всякой абстрактной науке, в том числе и в математике. Классическая математика привлекает абстракции, идущие гораздо дальше абстракций конструктивной математики. В частности, она пользуется абстракцией актуальной бесконечности, т. е. позволяет себе рассуждать о „бесконечных множествах" как о законченных неконструктивных „объектах". Различие между „классиками" и„конструктивистами" состоит в том, что они привлекают раз-разные абстракции, т. е. фантазируют по-разному.
>>3062
А что такое конструктивный процесс, и вообще процесс?
А что такое конструктивный процесс, и вообще процесс?
187 Кб, 273x392>>3064
Вопросики у него есть, а. Вейп вытащи из жопы, или что ты туда засовываешь, потом хотя бы пару статей из Википедии осиль вместо тиктака. Откуда вы сюда лезете такие?
> Да и к написанному есть вопросики.
Вопросики у него есть, а. Вейп вытащи из жопы, или что ты туда засовываешь, потом хотя бы пару статей из Википедии осиль вместо тиктака. Откуда вы сюда лезете такие?
>>3067
Мовный петух получает образование на википедии, лул.
Шо, у вас на хуторе универы и книжки не завезли?
Мовный петух получает образование на википедии, лул.
Шо, у вас на хуторе универы и книжки не завезли?
формализм крута
55 Кб, 900x1200Можем договориться :)
>>3074
-1/12
-1/12
кто против конструктивизма, тот петух
кто за конструктивизм, тот петух
все остальные — конструктивисты
кто за конструктивизм, тот петух
все остальные — конструктивисты
256 Кб, 1291x2123>>3049
Аксиоматика Пеано содержится в его труде 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 ).
Похоже, что АП как раз-таки определяет "свойство быть числом". О бесконечности речи не идет. И если бы речь о бесконечности заходила, то бесконечность была бы актуальной. То есть существуют такие объекты, как числа, а их свойства описаны конечным набором конечных схем.
Имеется в виду возможность рассмотрения сколь угодно длинных формул? Почему бы вместо формул не рассматривать сам конечный набор конечных схем (схем правильно построенных формул), а получаемые из них формулы - считать лишь вспомогательными средствами некоего отдельного метода исследования схем? И конечно же верно, что никто никогда не может рассмотреть слишком большой набор формул, а тем более бесконечный, иначе как найдя абстрактный подход через рассмотрение вместо них заключающего их множества. Множества точно так же описываются конечным набором конечных схем. Нарушается ли финитизм где-либо в ходе таких исследований?
>Базовый объект это единица, а всё множество формируется из 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 ).
Похоже, что АП как раз-таки определяет "свойство быть числом". О бесконечности речи не идет. И если бы речь о бесконечности заходила, то бесконечность была бы актуальной. То есть существуют такие объекты, как числа, а их свойства описаны конечным набором конечных схем.
> Ну и как уже говорилось в принципе не может определять т.к. даже в своей формулировке опирается на абстракцию потенциальной осуществимости в метаязыке.
Имеется в виду возможность рассмотрения сколь угодно длинных формул? Почему бы вместо формул не рассматривать сам конечный набор конечных схем (схем правильно построенных формул), а получаемые из них формулы - считать лишь вспомогательными средствами некоего отдельного метода исследования схем? И конечно же верно, что никто никогда не может рассмотреть слишком большой набор формул, а тем более бесконечный, иначе как найдя абстрактный подход через рассмотрение вместо них заключающего их множества. Множества точно так же описываются конечным набором конечных схем. Нарушается ли финитизм где-либо в ходе таких исследований?
>>3083
Проблема N петуха в том, что он не осилил определения абстракции и метаязыка в принципе. Конкретно, тот факт, что эти явления вторичны по отношению к примерам, содержащим абстрагируемое свойство и обьектному языку соответственно. Он не понимает, что абстракция не может существовать сама по себе, вне примеров, содержащих её, а метаязык может быть только надстройкой над объектным языком. Все это описано буквально на каждом углу, начиная с Википедии, однако же у N петуха какое-то "свое" (на самом деле взятое у Успенского) понимание абстракции и метаязыка. Учитывая, что там ШУЕ уровня Рыбникова и "основ православной арифметики", имеем что имеем - долбаеб вместо того чтобы хотя бы ПОПЫТаться разобраться в вопросе, с 2015(!) года серит шизой, что оказывается, аксиомы Пеано якобы не определяют множество натуральных чисел. Короче говоря, спорить там бесполезно, всё что можно сделать - тыкать дауна в общепринятые (а не ШУЕшные) определения абстракции и метаязыка.
Проблема N петуха в том, что он не осилил определения абстракции и метаязыка в принципе. Конкретно, тот факт, что эти явления вторичны по отношению к примерам, содержащим абстрагируемое свойство и обьектному языку соответственно. Он не понимает, что абстракция не может существовать сама по себе, вне примеров, содержащих её, а метаязык может быть только надстройкой над объектным языком. Все это описано буквально на каждом углу, начиная с Википедии, однако же у N петуха какое-то "свое" (на самом деле взятое у Успенского) понимание абстракции и метаязыка. Учитывая, что там ШУЕ уровня Рыбникова и "основ православной арифметики", имеем что имеем - долбаеб вместо того чтобы хотя бы ПОПЫТаться разобраться в вопросе, с 2015(!) года серит шизой, что оказывается, аксиомы Пеано якобы не определяют множество натуральных чисел. Короче говоря, спорить там бесполезно, всё что можно сделать - тыкать дауна в общепринятые (а не ШУЕшные) определения абстракции и метаязыка.
>>3085
Конструшок, как тебе удается обосраться даже в совершенно очевидных понятиях и перевернуть их с ног на голову? То универсальная машина Тьюринга у тебя это обобщение МТ вообще, то вот этот бред.
>не осилил определения абстракции и метаязыка
>метаязык может быть только надстройкой над объектным языком
Конструшок, как тебе удается обосраться даже в совершенно очевидных понятиях и перевернуть их с ног на голову? То универсальная машина Тьюринга у тебя это обобщение МТ вообще, то вот этот бред.
>>3087
Я так понимаю, возражений по существу нет? Или дальше будешь игнорировать общепринятые определения абстракции и метаязыка? Абстракция это свойство примеров, собственно и содержащих абстрагируемое свойство. Будешь с этим спорить? Зачем?
Я так понимаю, возражений по существу нет? Или дальше будешь игнорировать общепринятые определения абстракции и метаязыка? Абстракция это свойство примеров, собственно и содержащих абстрагируемое свойство. Будешь с этим спорить? Зачем?
>>3087
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%9C%D0%B5%D1%82%D0%B0%D1%8F%D0%B7%D1%8B%D0%BA
Вот так просто, N петух. Нет объектного языка - нет и метаязыка для его описания.
>>3089
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.
> Универсальной машиной Тью́ринга называют машину Тьюринга, которая может заменить собой любую машину Тьюринга. Получив на вход программу и входные данные, она вычисляет ответ, который вычислила бы по входным данным машина Тьюринга, чья программа была дана на вход.
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.
Срочно таблеток мовному петуху, он щас весь тред википедией засрет.
>>3093
А ты читать разучился, N петух? Универсальная потому так и называется, что способна заменить любой конкретный пример машины Тьюринга. Что сказать-то хотел?
А ты читать разучился, N петух? Универсальная потому так и называется, что способна заменить любой конкретный пример машины Тьюринга. Что сказать-то хотел?
Не совсем понял маневр N петуха в сторону машины Тьюринга. С аксиомами Пеано, абстракцией и метаязыком обосрался, теперь хочешь с машинами Тьюринга обосраться?
>>3094
Но я тебя не спрашивал кто кого может заменить, а
Я вообще ору. Как с таким уровнем понимания чего либо ты можешь листать своего Браузера с Мартином-Лефом и искренне считать что ты чего то там понимаешь?
У тебя может пизда между ног, и ты на самом деле не петух и курица? Просто такой уровень отсутствия логического мышления у человека за гранью моего понимания.
>>3095
Просто проходил мимо, решил погонять тупого петуха по старым темам.
Но я тебя не спрашивал кто кого может заменить, а
>Какое понятие более общее
Я вообще ору. Как с таким уровнем понимания чего либо ты можешь листать своего Браузера с Мартином-Лефом и искренне считать что ты чего то там понимаешь?
У тебя может пизда между ног, и ты на самом деле не петух и курица? Просто такой уровень отсутствия логического мышления у человека за гранью моего понимания.
>>3095
Просто проходил мимо, решил погонять тупого петуха по старым темам.
55 Кб, 900x1200>>3096
То есть, ты не N петух? Это не проблема, и тебя вылечим. С машиной Тьюринга ты таки обосрался, так что официально обьявляешься опущенным. Возьми антистресс и проследуй к параше.
То есть, само понятие "универсальная" тебе ни о чем не говорит? Хорошо, Я тебя услышал. Универсальная машина Тьюринга - более общая потому что может заменить любой частный случай. Я на твой вопрос ответил?
> Просто проходил мимо, решил погонять тупого петуха по старым темам.
То есть, ты не N петух? Это не проблема, и тебя вылечим. С машиной Тьюринга ты таки обосрался, так что официально обьявляешься опущенным. Возьми антистресс и проследуй к параше.
> Но я тебя не спрашивал кто кого может заменить, а
> >Какое понятие более общее
То есть, само понятие "универсальная" тебе ни о чем не говорит? Хорошо, Я тебя услышал. Универсальная машина Тьюринга - более общая потому что может заменить любой частный случай. Я на твой вопрос ответил?
>>3097
Ну ответить ты ответил. Но пиздец, конечно, что теперь с этим делать непонятно...
Какое понятие более общее - "автомобиль" или "зеленый автомобиль"?
>Универсальная машина Тьюринга - более общая потому что может заменить любой частный случай. Я на твой вопрос ответил?
Ну ответить ты ответил. Но пиздец, конечно, что теперь с этим делать непонятно...
Какое понятие более общее - "автомобиль" или "зеленый автомобиль"?
>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.
Что скажете?
>>3139
Тоже что и всегда, HOTT даже N не может определить, кому нужно такое "основание"? А всё остальное и в теории множеств нормально сидит.
Тоже что и всегда, HOTT даже N не может определить, кому нужно такое "основание"? А всё остальное и в теории множеств нормально сидит.
>>3140
N петух, в HoTT N определено. По абстракции потенциальной бесконечности тебя уже сто раз еблом ткнули в определение абстракции - это свойство примеров, а не наоборот.
> HOTT даже N не может определить,
N петух, в HoTT N определено. По абстракции потенциальной бесконечности тебя уже сто раз еблом ткнули в определение абстракции - это свойство примеров, а не наоборот.
>>3143
N петух, это отношение следования. Абстракция потенциальной бесконечности это свойство succ, но не наоборот.
> define succ
N петух, это отношение следования. Абстракция потенциальной бесконечности это свойство succ, но не наоборот.
>>3145
А потом спрашиваешь у анонов откуда берется инъективность конструкторов и они начинают что-то невнятно блеять про теорию категорий прикрываясь первым попавшимся пейпером по coic. Тру стори.
А потом спрашиваешь у анонов откуда берется инъективность конструкторов и они начинают что-то невнятно блеять про теорию категорий прикрываясь первым попавшимся пейпером по coic. Тру стори.
>>3154
В то, что ты Сохацкому понаписал в андерс хуйни без половины морфизмов, мы поверим. Ну, почти. Но к HoTT какие претензии? Ее поумнее тебя писали, там даже Мартин-Леф в соавторах. Чего ты там ниспровергать собрался?
В то, что ты Сохацкому понаписал в андерс хуйни без половины морфизмов, мы поверим. Ну, почти. Но к HoTT какие претензии? Ее поумнее тебя писали, там даже Мартин-Леф в соавторах. Чего ты там ниспровергать собрался?
133 Кб, 919x750>>3165
Тупее тебя нет никого. Уебывай и свои задачки для коррекционной группы детского сада забирай. Чё вас деградантов так сюда тянет? В другом месте пердежируй, аниме
> Петух, ты что тупее дошкольника?
Тупее тебя нет никого. Уебывай и свои задачки для коррекционной группы детского сада забирай. Чё вас деградантов так сюда тянет? В другом месте пердежируй, аниме
>>3166
Ору с убогого. Петух не справился со школьной программой, это известно. Теперь взят новый уровень - вопросы для дошколят оказывается петуху тоже не по зубам. Что дальше? Попытка вырабатывать условные рефлексы? Кто умнее конструктивный петух или обезьяна?
Ору с убогого. Петух не справился со школьной программой, это известно. Теперь взят новый уровень - вопросы для дошколят оказывается петуху тоже не по зубам. Что дальше? Попытка вырабатывать условные рефлексы? Кто умнее конструктивный петух или обезьяна?
127 Кб, 627x598>>3167
Не стыдно тебе таким дебилом быть?
> чморидж обосрался с универсальной машиной Тьюринга, теперь кукарекает на самоподдуве, пытаясь закукарекать свой обсер
Не стыдно тебе таким дебилом быть?
>>3168
Потешный не может ответить на вопрос для дошкольника, но уверен что обосрался не он. Какая форма неполноценности у тебя?
Потешный не может ответить на вопрос для дошкольника, но уверен что обосрался не он. Какая форма неполноценности у тебя?
>>3169
Конструктивизм в затяжной стадии. С каждым годом его интеллект всё падает и падает. В первых тредах, он ещё пытался что-то аргументировать и аватарил Брауэрем. Теперь он уже не пытается и просто срёт картинками с зумерами.
>Какая форма неполноценности у тебя?
Конструктивизм в затяжной стадии. С каждым годом его интеллект всё падает и падает. В первых тредах, он ещё пытался что-то аргументировать и аватарил Брауэрем. Теперь он уже не пытается и просто срёт картинками с зумерами.
>>3154
Инъективность можно получить из построения односторонней обратной или, например, возможности элиминировать в универсум повыше. Почти все, кто с DTT знаком, в курсе, но причём тут инъективность вообще?
Инъективность можно получить из построения односторонней обратной или, например, возможности элиминировать в универсум повыше. Почти все, кто с DTT знаком, в курсе, но причём тут инъективность вообще?
>>3162
Кто ты-то? Ты вообще не тому анону про андерс пишешь. Разберись уже, кто кому что писал, что такое этот самый Anders и какое он имеет отношение к текстам Сохацкого.
Кто ты-то? Ты вообще не тому анону про андерс пишешь. Разберись уже, кто кому что писал, что такое этот самый Anders и какое он имеет отношение к текстам Сохацкого.
>>3172
Конкретно меня интересует почему 0≠1. Потому что в аксиомах Пеано это постулируется явно, а в MLTT берется хуй знает откуда. Несколько тредов в прошлом задавал этот вопрос и получал только дрист под себя от конструктивного петуха. Потом случайно наткнулся на то что для доказательства этого факта необходим универсум.
Это все при том, что coic очень сложная система и правила ее хуй где нормально описаны. Об этом еще Воеводский говорил.
Конкретно меня интересует почему 0≠1. Потому что в аксиомах Пеано это постулируется явно, а в MLTT берется хуй знает откуда. Несколько тредов в прошлом задавал этот вопрос и получал только дрист под себя от конструктивного петуха. Потом случайно наткнулся на то что для доказательства этого факта необходим универсум.
Это все при том, что coic очень сложная система и правила ее хуй где нормально описаны. Об этом еще Воеводский говорил.
>>3183
Конкретно «0 ≠ 1» вроде как называется дизъюнктивностью конструкторов, под инъективностью понимают стандартную инъективность (то есть succ(n) = succ(m) → n = m). Впрочем, это вопросы названий, конечно.
Да, нужен универсум. Стандартный аргумент такой: мы строим функцию 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
>Конкретно меня интересует почему 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
>>3186
Не спорю, но еще хотелось бы термин объединяющий эти два свойства. Особенно забавным мне кажется то что в coic это свойство подается чуть ли не как само-собой разумеющееся, в то время как в большинстве языков программирования (не функциональных) конструктор конструирует что угодно и как угодно.
Видел это доказательство, но все равно оно какой то странный привкус оставляет. Подозрительно что прувер до всего этого додумывается автоматически.
И теперь мне стало интересно кто и как это доказал. Вроде где-то видел строятся модели для этого соответствующие.
>дизъюнктивностью конструкторов, под инъективностью
Не спорю, но еще хотелось бы термин объединяющий эти два свойства. Особенно забавным мне кажется то что в coic это свойство подается чуть ли не как само-собой разумеющееся, в то время как в большинстве языков программирования (не функциональных) конструктор конструирует что угодно и как угодно.
Видел это доказательство, но все равно оно какой то странный привкус оставляет. Подозрительно что прувер до всего этого додумывается автоматически.
>it is well-known that Martin-Löf type theory without univeres does not prove 0≠1.
И теперь мне стало интересно кто и как это доказал. Вроде где-то видел строятся модели для этого соответствующие.
28 Кб, 572x221>>3188
Просто один и тот же термин (конструктор) в ООП и теориях типов используют для разных понятий.
Неудивительно, тактики как раз под такие стандартные случаи и забиты. А подозревать не в чем, например, в Lean тактики генерируют термы отдельно от ядра, ядро же проверяет только то, что тактика сгенерировала. То есть пруф от кривой тактики принят не будет. Можно даже посмотреть, какой конкретно пруф тактика сгенерировала (пик).
Вот нагуглилось что-то: https://www.cse.chalmers.se/~smith/JSLPeano.pdf
>конструктор конструирует что угодно и как угодно
Просто один и тот же термин (конструктор) в ООП и теориях типов используют для разных понятий.
>Подозрительно что прувер до всего этого додумывается автоматически.
Неудивительно, тактики как раз под такие стандартные случаи и забиты. А подозревать не в чем, например, в Lean тактики генерируют термы отдельно от ядра, ядро же проверяет только то, что тактика сгенерировала. То есть пруф от кривой тактики принят не будет. Можно даже посмотреть, какой конкретно пруф тактика сгенерировала (пик).
>И теперь мне стало интересно кто и как это доказал. Вроде где-то видел строятся модели для этого соответствующие.
Вот нагуглилось что-то: https://www.cse.chalmers.se/~smith/JSLPeano.pdf
511 Кб, 1306x532Тут недавно выкладывали ссылку на русский перевод HoTT book. Пикрил просто первое, что бросилось в глаза, сколько там подобной параши, неизвестно. Смысла читать этот перевод, конечно же, нет.
44 Кб, 900x900>>3190
Там вместо "означает" должно быть "увтерждает" как во втором примере суждения или чо?
Там вместо "означает" должно быть "увтерждает" как во втором примере суждения или чо?
58 Кб, 1152x222>>3191
Терм a имеет тип A / терм a населяет тип A / терм a является элементом типа A.
Опечатки в переводе, вот это пиздос, да, никогда такого не было.
Терм a имеет тип A / терм a населяет тип A / терм a является элементом типа A.
Опечатки в переводе, вот это пиздос, да, никогда такого не было.
>>3193
Хм. Пока ты явно не указал, я и не заметил что там элемент является типом. Видать у меня реально низкий айкю.
Хм. Пока ты явно не указал, я и не заметил что там элемент является типом. Видать у меня реально низкий айкю.
9 Кб, 513x212>>3189
Спасибо, почитаю.
Вот предельно упрощенный терм на coq который доказывает тезис. Осталось только его осмыслить как следует.
Почему используешь lean? Да еще на немецком, кек.
Спасибо, почитаю.
Вот предельно упрощенный терм на coq который доказывает тезис. Осталось только его осмыслить как следует.
Почему используешь lean? Да еще на немецком, кек.
>>3197
Синтаксис приятнее (чем в Agda/Coq) кажется, метапрограммирование отличное и плагины проверяют код на лету.
Системная локаль.
>Почему используешь lean?
Синтаксис приятнее (чем в Agda/Coq) кажется, метапрограммирование отличное и плагины проверяют код на лету.
>Да еще на немецком, кек.
Системная локаль.
>>3139
Я не знаю особенности HoTT, но мне интересно ответить и оживить доску.
Буду считать, что цитата использует HoTT как обозначение математической теории, в которой интерпретируемы теория множеств и арифметики N и Z. То есть HoTT - особая основная теория, выступающая в основании математики и обосновывающая многие другие ее теории.
Далее, о чем идет речь?
Присутствуют отношения равенства, различающиеся между собой, что ли?
Мол, по одному изоморфизму они изоморфны, а по другому - нет?
(Будем считать, что речь идет об аддитивном моноиде.) Так ведь, насколько я понимаю, это полностью соответствует обычным результатам конвенциональной математики. В Z: a = a + (1 + [-1]). Тогда для любого f, если f - биекция из Z в N: f1 != f(-1), значит один из них ненулевой, и тогда fa != fa + f1 + f(-1), то есть никакая биекция f не является гомоморфизмом.
>>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 не является гомоморфизмом.
>>3199
Да, как разные изоморфизмы.
Типы (ℕ и ℤ) изоморфны, структуры (то есть n-ки, тип + операция + свойства) над ними — уже нет.
>Присутствуют отношения равенства, различающиеся между собой, что ли?
Да, как разные изоморфизмы.
>Мол, по одному изоморфизму они изоморфны, а по другому - нет?
Типы (ℕ и ℤ) изоморфны, структуры (то есть n-ки, тип + операция + свойства) над ними — уже нет.
>>3199
Может тогда не стоит отвечать?
HoTT (по видимому) предлагает считать N и Z тождественными понятиями, что противоречит интуиции и устоявшейся практике.
>Я не знаю особенности HoTT
Может тогда не стоит отвечать?
HoTT (по видимому) предлагает считать N и Z тождественными понятиями, что противоречит интуиции и устоявшейся практике.
>>3189
Странно он пишет
а потом
Но населенность равенства очевидно должна зависеть от того что сравнивается. Продолжу наблюдения.
Странно он пишет
> 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)
Но населенность равенства очевидно должна зависеть от того что сравнивается. Продолжу наблюдения.
>>3202
В этой интерпретации любой тип либо пустой, либо одноэлементный.
В одноэлементном типе все элементы равны, причём одним образом (даже в HoTT), поэтому равенство там всегда, вне зависимости от a и b, — одноэлементный тип.
А в пустом типе чтобы Eq(A, a, b) просто построить, нужно найти a/b в нём, то есть его естественно интерпретировать как пустой тип.
То есть как раз φ(Eq(A, a, b)) = φ(A).
В этой интерпретации любой тип либо пустой, либо одноэлементный.
В одноэлементном типе все элементы равны, причём одним образом (даже в HoTT), поэтому равенство там всегда, вне зависимости от a и b, — одноэлементный тип.
А в пустом типе чтобы Eq(A, a, b) просто построить, нужно найти a/b в нём, то есть его естественно интерпретировать как пустой тип.
То есть как раз φ(Eq(A, a, b)) = φ(A).
>>3203
А он и может быть только одним образом. Это чисто в HoTT придумали, что якобы может быть не одним образом.
>причём одним образом (даже в HoTT)
А он и может быть только одним образом. Это чисто в HoTT придумали, что якобы может быть не одним образом.
>>3230
Да нет, понятие равенства задолго до HoTT вызывало много вопросов. Это просто ты кроме тиктака ничего не знаешь.
Да нет, понятие равенства задолго до HoTT вызывало много вопросов. Это просто ты кроме тиктака ничего не знаешь.
>>3233
Действительно, кек.
>А давайте придумаем модель, где желаемое является действительным? А давайте!
Действительно, кек.
>>3251
А есть какие-то богом данные модели что ли?
А есть какие-то богом данные модели что ли?
Конструктивист должен знать:
1) изоморфизм Карри-Говарда и тезис Чёрча;
2) содержание диссертации Брауэра в переводе Гейтинга;
3) пять уровней языка и четыре способа отрицания по Маннури;
4) интерпретацию логических констант по Брауэру-Гейтингу-Колмогорову;
5) теорию статистического обучения Вапника и модель spikgram Миколова;
6) отличия машины Тьюринга от машины Поста.
Конструктивист обязан:
1) отрицать закон исключённого третьего;
2) отрицать любую математику, не выразимую через типизированную лямбду в MLTT или нормальные алгорифмы Маркова;
3) переписать на прувере AUTOMATH де Брауна книгу "Основы математического анализа" Ландау;
4) представить все формальные теории в терминах алфавитов, термов и манипуляций с ними;
5) свести гомологическую алгебру к исчислению предикатов, используя нумерацию Гёделя.
1) изоморфизм Карри-Говарда и тезис Чёрча;
2) содержание диссертации Брауэра в переводе Гейтинга;
3) пять уровней языка и четыре способа отрицания по Маннури;
4) интерпретацию логических констант по Брауэру-Гейтингу-Колмогорову;
5) теорию статистического обучения Вапника и модель spikgram Миколова;
6) отличия машины Тьюринга от машины Поста.
Конструктивист обязан:
1) отрицать закон исключённого третьего;
2) отрицать любую математику, не выразимую через типизированную лямбду в MLTT или нормальные алгорифмы Маркова;
3) переписать на прувере AUTOMATH де Брауна книгу "Основы математического анализа" Ландау;
4) представить все формальные теории в терминах алфавитов, термов и манипуляций с ними;
5) свести гомологическую алгебру к исчислению предикатов, используя нумерацию Гёделя.
>>3249
Ну придумали же множества. Оказалось полезным.
Ну придумали же множества. Оказалось полезным.
>>3258
Про алгтоп целая восьмая глава.
Про алгтоп целая восьмая глава.
>>3229
>>3258
HoTT+аксиома выбора+универсум (вроде как) взаимно интерпретируема с ZFC+недостижимые кардиналы, так что всё, что можно сделать в "стандартной" математике, можно сделать и в HoTT. Требовать "определение пучка в HoTT" это то же самое, что требовать "определение пучка в ZFC".
И вообще, практически для всей математики (в том числе для пучков) скорее всего хватит даже подсистемы арифметики второго порядка.
>>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}$, где это условие не обязательно выполняется, обе являются абсолютно валидными категориями. С какой именно из них работать -- зависит от конкретной ситуации.
>>3303
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}$, где это условие не обязательно выполняется, обе являются абсолютно валидными категориями. С какой именно из них работать -- зависит от конкретной ситуации.
поправил
>>3305
Дополню. Натуральные числа определяются как инициальная алгебра эндофунктора $X \mapsto \ast \coprod X$ на произвольном топосе. Кроме того, естественно рассматривать не только натуральные числа, но и конатуральные числа (конатуральные кочисла? натуральные кочисла?) и коиндукцию.
Дополню. Натуральные числа определяются как инициальная алгебра эндофунктора $X \mapsto \ast \coprod X$ на произвольном топосе. Кроме того, естественно рассматривать не только натуральные числа, но и конатуральные числа (конатуральные кочисла? натуральные кочисла?) и коиндукцию.
>>3306
Отрицательные что ли? Хуя ты демон, множество Z открыл.
> не только натуральные числа, но и конатуральные числа
Отрицательные что ли? Хуя ты демон, множество Z открыл.
>>3316
Нет, как заметил анон >>3318 , конатуральные кочисла это терминальная коалгебра на указанном мной функторе. Я не уверен, что ты понимаешь под "отрицательными числами", но подозреваю, что это двойственная категория к категории предпорядка ассоциированной к $\mathbb{N}$ как моноиду, или возможно сам $\mathbb{N}$ как комоноид. Не знаю, как ты мог перепутать это с конатуральными кочислами.
Как правильно определять $\mathbb{Z}$ я, к сожалению, пока не понял, для меня это открытый вопрос. Предлагаю отталкиваться от "свободный $k$-кортежный моноидальный $n$-группоид на одном объекте".
Нет, как заметил анон >>3318 , конатуральные кочисла это терминальная коалгебра на указанном мной функторе. Я не уверен, что ты понимаешь под "отрицательными числами", но подозреваю, что это двойственная категория к категории предпорядка ассоциированной к $\mathbb{N}$ как моноиду, или возможно сам $\mathbb{N}$ как комоноид. Не знаю, как ты мог перепутать это с конатуральными кочислами.
>множество Z
Как правильно определять $\mathbb{Z}$ я, к сожалению, пока не понял, для меня это открытый вопрос. Предлагаю отталкиваться от "свободный $k$-кортежный моноидальный $n$-группоид на одном объекте".
>>3323
Интересно, как ты собрался определить натуральные числа без абстракции поенциальной осуществимости? А если с ней, то зачем мудрить а не просто взять и определить палочками как у Маркова?
Интересно, как ты собрался определить натуральные числа без абстракции поенциальной осуществимости? А если с ней, то зачем мудрить а не просто взять и определить палочками как у Маркова?
>>3324
Вот тут >>3306 написал.
Прости, не знаю, что это такое. Звучит как что-то связанное с модальной логикой и теорией моделей. Это очень интересно, но к математике (разделу линейной алгебры) и ее основаниям отношения не имеет.
Не знаю, что такое "палочки". Если ты имеешь в виду терминальный объект в топосе, то это соответствует моему >>3306 определению.
>как ты собрался определить натуральные числа
Вот тут >>3306 написал.
>абстракции поенциальной осуществимости
Прости, не знаю, что это такое. Звучит как что-то связанное с модальной логикой и теорией моделей. Это очень интересно, но к математике (разделу линейной алгебры) и ее основаниям отношения не имеет.
>определить палочками
Не знаю, что такое "палочки". Если ты имеешь в виду терминальный объект в топосе, то это соответствует моему >>3306 определению.
>>3324
N петух опять завел свою ШУЕ шарманку. Абстракция потенциальной осуществимости - это свойство аксиом Пеано, а не что-то что может "существовать" отдельно от примеров, содержащих абстрагируемое свойство.
> Интересно, как ты собрался определить натуральные числа без абстракции поенциальной осуществимости?
N петух опять завел свою ШУЕ шарманку. Абстракция потенциальной осуществимости - это свойство аксиом Пеано, а не что-то что может "существовать" отдельно от примеров, содержащих абстрагируемое свойство.
>>3326
Cам то понял что сказал? Ты свою ШУЕ шизу как чат бот высираешь даже не задумываясь.
Cам то понял что сказал? Ты свою ШУЕ шизу как чат бот высираешь даже не задумываясь.
>>3327
Понял. А вот ты походу нет.
Это общепринятое определение абстракции, N петух. А вот у тебя реально ШУЕ.
> Cам то понял что сказал?
Понял. А вот ты походу нет.
> Ты свою ШУЕ шизу как чат бот высираешь даже не задумываясь.
Это общепринятое определение абстракции, N петух. А вот у тебя реально ШУЕ.
>>3325
Похоже на начало пути нового петушка. Напомнило времена раннего конструктивного петуха когда он еще мог что то кроме шитпостинга чмориджами, благоговейно цитировал писания швятых Браузера и пророка его Мартина-Лефа.
>Не знаю, что такое "палочки". Если ты имеешь в виду терминальный объект в топосе
Похоже на начало пути нового петушка. Напомнило времена раннего конструктивного петуха когда он еще мог что то кроме шитпостинга чмориджами, благоговейно цитировал писания швятых Браузера и пророка его Мартина-Лефа.
>>3330
Я по сути просто пересказываю позицию всех великих математиков второй половины двадцатого и двадцать первого веков, от Гротендика и Квиллена до Шольце и Лури.
Я по сути просто пересказываю позицию всех великих математиков второй половины двадцатого и двадцать первого веков, от Гротендика и Квиллена до Шольце и Лури.
>>3324
N-петух - ты ультрафинитист или що? Просто если так, то очень бы хотелось увидеть какую-нибудь валидную ультрафинитную программу оснований математики
N-петух - ты ультрафинитист или що? Просто если так, то очень бы хотелось увидеть какую-нибудь валидную ультрафинитную программу оснований математики
Какое мнение было у Гротендика по поводу теории типов и HoTT?
>>3329
Ну да, у Сохацкого есть ссылки. Вообще под гамалогии у него запилен так называемый "стек де Рама - Черубини - Шрайбера", где-то к нему и ссылки на нормальные источники чтобы обпучкаться.
> А можно с нормального Западного источника?
Ну да, у Сохацкого есть ссылки. Вообще под гамалогии у него запилен так называемый "стек де Рама - Черубини - Шрайбера", где-то к нему и ссылки на нормальные источники чтобы обпучкаться.
>>3330
Брауэра цитировать местным ебланам типа тебя бессмысленно, вы в Википедию-то не можете, все ваше ШУЕ и просто весь набор слов контрится первой же ссылкой оттуда. Вот ты же обосрался с универсальной машиной Тьюринга, а мог бы не обсираться а просто прочитать определение в Википедии. Как и N петух, к слову. Успенский ещё ладно, дедушка старый, ему все равно. Рано вам ещё Брауэра и Мартин-Лефа, дети тиктака.
Брауэра цитировать местным ебланам типа тебя бессмысленно, вы в Википедию-то не можете, все ваше ШУЕ и просто весь набор слов контрится первой же ссылкой оттуда. Вот ты же обосрался с универсальной машиной Тьюринга, а мог бы не обсираться а просто прочитать определение в Википедии. Как и N петух, к слову. Успенский ещё ладно, дедушка старый, ему все равно. Рано вам ещё Брауэра и Мартин-Лефа, дети тиктака.
>>3339
Кек. Ты обосрался даже с зелеными машинками.
>Вот ты же обосрался с универсальной машиной Тьюринга
Кек. Ты обосрался даже с зелеными машинками.
>>3340
Я ответил на весь класс подобных вопросов, но ты этого ожидаемо не увидел, дединсайд. То есть, обосрался и в этом.
Я ответил на весь класс подобных вопросов, но ты этого ожидаемо не увидел, дединсайд. То есть, обосрался и в этом.
>>3341
Твои любимые мемасы с чмориджами это универсальный ответ на все только в твоем деградировавшем мозгу.
Твои любимые мемасы с чмориджами это универсальный ответ на все только в твоем деградировавшем мозгу.
>>3342
Ты как-то слишком отстраненно пишешь про чмориджей, хотя сам - ярчайший представитель вида, судя по дегенеративности твоих постов.
Ты как-то слишком отстраненно пишешь про чмориджей, хотя сам - ярчайший представитель вида, судя по дегенеративности твоих постов.
>>3338
(Ко)гомологии в 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).
(Ко)гомологии в 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).
>>3352
Имхо это плохая аналогия, и вопрос "какое понятие более общее" не очень хорошо определен для мат объектов. Попробуй лучше с абстрактной группой и подгруппой группы симметрий.
мимо
Имхо это плохая аналогия, и вопрос "какое понятие более общее" не очень хорошо определен для мат объектов. Попробуй лучше с абстрактной группой и подгруппой группы симметрий.
мимо
>>3354
Чем аналогия плоха? Предельно ясная аналогия доступная даже детсадовцам чтобы навести петуха на правильный ответ.
не в данном случае
Чем аналогия плоха? Предельно ясная аналогия доступная даже детсадовцам чтобы навести петуха на правильный ответ.
> не очень хорошо определен для мат объектов
не в данном случае
>>3344
Так, а это уже реально база. Там можно сделать алгеом? Кинь пожалуйста еще такое. Завтра скачаю Agda если есть алгеом. Помню в 2017 пробовал, но там даже не было когомологий.
Это же она?
>>3357
Я просто пошутил, извини. Пытаюсь троллингом вытянуть истину. Мне реально нужен теоретико-типовой пучок.
Так, а это уже реально база. Там можно сделать алгеом? Кинь пожалуйста еще такое. Завтра скачаю Agda если есть алгеом. Помню в 2017 пробовал, но там даже не было когомологий.
Это же она?
>>3357
Я просто пошутил, извини. Пытаюсь троллингом вытянуть истину. Мне реально нужен теоретико-типовой пучок.
>>3356
Какое "понятие" более общее, абстрактной группы или подгруппы группы симметрий? Для меня этот вопрос не имеет смысла, потому что абстрактная группа (т.е. по сути синтаксическая теория) и конкретные группы (т.е. по сути ее модели) живут в разных категориях. То же с машинами Тьюринга.
Вообще, по-моему здесь происходит путаница между отношением абстрактное-конкретное и отношением общее-частное.
Я не уверен, в каком смысле зеленая машина (эта конкретная зелена машина? понятие зеленой машины?) моделирует любую машину (любую конкретную машину? понятие машины?).
>не в данном случае
Какое "понятие" более общее, абстрактной группы или подгруппы группы симметрий? Для меня этот вопрос не имеет смысла, потому что абстрактная группа (т.е. по сути синтаксическая теория) и конкретные группы (т.е. по сути ее модели) живут в разных категориях. То же с машинами Тьюринга.
Вообще, по-моему здесь происходит путаница между отношением абстрактное-конкретное и отношением общее-частное.
>Чем аналогия плоха?
Я не уверен, в каком смысле зеленая машина (эта конкретная зелена машина? понятие зеленой машины?) моделирует любую машину (любую конкретную машину? понятие машины?).
>>3360
Ну я сразу понял ты предлагаешь сравнить два несравнимых понятия и доказать таким образом что любые два понятия невозможно сравнить. Это какая то форма конструктивизма головного мозга?
очень на то похоже...
>Какое "понятие" более общее, абстрактной группы или подгруппы группы симметрий?
Ну я сразу понял ты предлагаешь сравнить два несравнимых понятия и доказать таким образом что любые два понятия невозможно сравнить. Это какая то форма конструктивизма головного мозга?
>Я не уверен, в каком смысле зеленая машина
очень на то похоже...
>>3358
Определяется пучок в HoTT так же, как везде: как предпучок на сайте, удовлетворяющий ряду свойств. Чтобы увидеть, как это определение выглядит в агде, достаточно загуглить "sheaf agda" и посмотреть, например, сюда https://github.com/jonsterling/constructive-sheaf-semantics
>>3362
Я не знаю, что такое "понятие" в математике. Объекты двух разных категорий действительно нельзя сравнить, поэтому вопрос о том, что более "общее", машина Тьюринга, моделирующая любую конкретную машину Тьюринга, или абстрактная синтаксическая теория машины Тьюринга, для меня не имеет смысла.
Я не конструктивист.
>Мне реально нужен теоретико-типовой пучок
Определяется пучок в HoTT так же, как везде: как предпучок на сайте, удовлетворяющий ряду свойств. Чтобы увидеть, как это определение выглядит в агде, достаточно загуглить "sheaf agda" и посмотреть, например, сюда https://github.com/jonsterling/constructive-sheaf-semantics
>>3362
>что любые два понятия невозможно сравнить
Я не знаю, что такое "понятие" в математике. Объекты двух разных категорий действительно нельзя сравнить, поэтому вопрос о том, что более "общее", машина Тьюринга, моделирующая любую конкретную машину Тьюринга, или абстрактная синтаксическая теория машины Тьюринга, для меня не имеет смысла.
>Это какая то форма конструктивизма головного мозга?
Я не конструктивист.
>>3363
О! так ты новый категориальный петушок. Милости просим.
>Объекты двух разных категорий действительно нельзя сравнить
О! так ты новый категориальный петушок. Милости просим.
453 Кб, mp4,426x240, 0:07
Перепишем петухов: монвый петух (самый гнилой пидор here), конструктивный петух, категорный петух, петух пучкист, ...
>>3364
Давай так -- дай мне множество понятий и определи на нем отношение порядка, которое моделировало бы отношение "x есть более общее понятие, чем y". Потом расскажи, где во всей этой структуре относительно друг друга будут находиться понятия "универсальная машина Тьюринга", "машина Тьюринга", "группа", "подгруппа группы симметрий", "машина" и "зеленая машина" и почему. Или предложи альтернативную модель. Тогда может получиться какой-то разговор.
Ну или загугли хотя бы "aristotle ontological square" и помедитируй над разницей между exemplify, instantiate и inhere.
>>3365
Возьми два множества с определенными на них предпорядками (можешь рассматривать их как категории). Как "сравнить" (каким (би)функтором?) элемент первого предпорядка с элементом второго? inb4: (ко)произведение не это делает.
Давай так -- дай мне множество понятий и определи на нем отношение порядка, которое моделировало бы отношение "x есть более общее понятие, чем y". Потом расскажи, где во всей этой структуре относительно друг друга будут находиться понятия "универсальная машина Тьюринга", "машина Тьюринга", "группа", "подгруппа группы симметрий", "машина" и "зеленая машина" и почему. Или предложи альтернативную модель. Тогда может получиться какой-то разговор.
Ну или загугли хотя бы "aristotle ontological square" и помедитируй над разницей между exemplify, instantiate и inhere.
>>3365
Возьми два множества с определенными на них предпорядками (можешь рассматривать их как категории). Как "сравнить" (каким (би)функтором?) элемент первого предпорядка с элементом второго? inb4: (ко)произведение не это делает.
>>3369
На что это ответ?
На что это ответ?
>>3368
Раньше конструшок такой же напористый был, только предлагал перечитывать все писания швятого Браузера и пророка его Мартина-Лефа. Если тебе все это нужно чтобы ответить на вопрос на который легко ответит даже ребенок пяти лет, то куда то ты не туда свернул.
Раньше конструшок такой же напористый был, только предлагал перечитывать все писания швятого Браузера и пророка его Мартина-Лефа. Если тебе все это нужно чтобы ответить на вопрос на который легко ответит даже ребенок пяти лет, то куда то ты не туда свернул.
>>3371
Сомневаюсь, что типичный ребенок пяти лет хорошо понимает, что такое "более общее понятие". Еще сомневаюсь, что типичный ребенок пяти лет хорошо понимает разницу между синтаксической теорией и ее моделью. Еще сомневаюсь, что мы в строгости должны ориентироваться на детей. Еще прошу заметить, что я никого читать не предлагаю, а прошу описать отношение предпорядка, с чем у умного ребенка пяти лет проблем действительно возникнуть не должно.
Сомневаюсь, что типичный ребенок пяти лет хорошо понимает, что такое "более общее понятие". Еще сомневаюсь, что типичный ребенок пяти лет хорошо понимает разницу между синтаксической теорией и ее моделью. Еще сомневаюсь, что мы в строгости должны ориентироваться на детей. Еще прошу заметить, что я никого читать не предлагаю, а прошу описать отношение предпорядка, с чем у умного ребенка пяти лет проблем действительно возникнуть не должно.
936 Кб, mp4,352x640, 0:14
>>3358
Вопрос не совсем верно задан. Как верно выше замечали, 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.
>Там можно сделать алгеом?
Вопрос не совсем верно задан. Как верно выше замечали, 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.
>>3375
Такое-то окормление говном модульного деда. Годами квакал, что нематематика потому что гамалогий нет, а оказалось что давно уже есть.
Такое-то окормление говном модульного деда. Годами квакал, что нематематика потому что гамалогий нет, а оказалось что давно уже есть.
>>3358
Это кал, качай Anders там всё есть, в том числе и абстракции созданные на основе примеров (но и в коем случае не наоборот!).
Это кал, качай Anders там всё есть, в том числе и абстракции созданные на основе примеров (но и в коем случае не наоборот!).
>>3383
Тут тема несколько сложнее, чем обычно в Википедии пишут. Но против твоих кукареканий и Википедии более чем достаточно. Ты просто знай своё место (оно у параши) и смирись с этим.
Тут тема несколько сложнее, чем обычно в Википедии пишут. Но против твоих кукареканий и Википедии более чем достаточно. Ты просто знай своё место (оно у параши) и смирись с этим.
>>3384
Я знаю, мой дом здесь, я все треды перекатываю.
Я знаю, мой дом здесь, я все треды перекатываю.
>>3375
База уровня выше 9000.
Спасибо, анон. Загрузил плейлист по Агде и буду постепенно вкатываться опять.
База уровня выше 9000.
Спасибо, анон. Загрузил плейлист по Агде и буду постепенно вкатываться опять.
>>3388
Что это? Я вроде видел его мельком если не ошибаюсь, но синтаксис Агды пока топ для математика. Чистый, без всяких проггерских штук.
Что это? Я вроде видел его мельком если не ошибаюсь, но синтаксис Агды пока топ для математика. Чистый, без всяких проггерских штук.
>>3394
Это тебя жирно троллят. Чуть более продвинутая чем cubicaltt (но всё ещё экспериментальная) имплементация кубической теории типов.
В сравнении, в кубической агде библиотека значительно больше и много готовой автоматизации.
В агде нельзя использовать «=» для равенства…
>Что это?
Это тебя жирно троллят. Чуть более продвинутая чем cubicaltt (но всё ещё экспериментальная) имплементация кубической теории типов.
В сравнении, в кубической агде библиотека значительно больше и много готовой автоматизации.
>синтаксис Агды пока топ для математика
В агде нельзя использовать «=» для равенства…
>>3374
Скибиди-петух, а тебе что интересно не позволяет ответить на вопрос? Тебе же не нужно как категориальному петуху выписать категорию всего на свете чтобы было вообще о чем говорить. Подозреваю дело в том что МЛ не завез сабтайпинг и другим отношения на типах строить не велел и теперь для петуха это не доступная концепция так что от одного вопроса у него разрывает пердак. Сейчас порватыш еще чмориджей подкинет.
Скибиди-петух, а тебе что интересно не позволяет ответить на вопрос? Тебе же не нужно как категориальному петуху выписать категорию всего на свете чтобы было вообще о чем говорить. Подозреваю дело в том что МЛ не завез сабтайпинг и другим отношения на типах строить не велел и теперь для петуха это не доступная концепция так что от одного вопроса у него разрывает пердак. Сейчас порватыш еще чмориджей подкинет.
1017 Кб, mp4,460x380, 0:17
Такой смешной тред получается, прямо как никогда.
- доломали N петуха, не осилившего пару определений из Википедии
- совершенно случайно доломали модульного деда, оказалось что гамалогии давно реализованы в агде
- попутно опетушили то ли какого-то подсиралу N петуха, то ли самого N петуха, мимикрирующего под собственного подсиралу, так же не осилившего определение машины Тьюринга из Википедии.
- доломали N петуха, не осилившего пару определений из Википедии
- совершенно случайно доломали модульного деда, оказалось что гамалогии давно реализованы в агде
- попутно опетушили то ли какого-то подсиралу N петуха, то ли самого N петуха, мимикрирующего под собственного подсиралу, так же не осилившего определение машины Тьюринга из Википедии.
>>3399
И только конструктивный петух щебечет все так же резво как и раньше. Уникальный случай в истории когда петух совсем без мозга живет уже больше десятка лет.
И только конструктивный петух щебечет все так же резво как и раньше. Уникальный случай в истории когда петух совсем без мозга живет уже больше десятка лет.
>>3423
Рад, что ты сам себя из вменяемых выписал только что. Можешь и сам отсюда танцевать нахуй. Только одно замечание - опровержение N петушества по существу (конкретными ссылками), это не шиза, как бы неприятно тебе от этого не было.
Рад, что ты сам себя из вменяемых выписал только что. Можешь и сам отсюда танцевать нахуй. Только одно замечание - опровержение N петушества по существу (конкретными ссылками), это не шиза, как бы неприятно тебе от этого не было.
767 Кб, webm,1280x720, 0:02
>>3429
Уважаемый (на самом деле нет), ты в своих анальных половых партнёрах уже запутался. Кто там тебя в анус сношал мне фиолетово ;)
Уважаемый (на самом деле нет), ты в своих анальных половых партнёрах уже запутался. Кто там тебя в анус сношал мне фиолетово ;)
Похоже наш конструктивный петушок наелся таблеток и спит :)
>>3436
По существу ты шизик, это медицинский факт, но что ты от меня хочешь, петушарий? Я не из этих, ваших, если что.
По существу ты шизик, это медицинский факт, но что ты от меня хочешь, петушарий? Я не из этих, ваших, если что.
>>3437
Это кукареканье долбаеба, а не факт, тем более "медицинский".
?
> По существу ты шизик, это медицинский факт,
Это кукареканье долбаеба, а не факт, тем более "медицинский".
> что ты от меня хочешь,
> сам мне безостановочно написывает одну хуйню за другой
?
>>3440
Поциэнт, это ваш диагноз а не хуйня. Не занимайтесь самолечением, обратитесь к специалистам.
Поциэнт, это ваш диагноз а не хуйня. Не занимайтесь самолечением, обратитесь к специалистам.
255 Кб, 400x400Поясните, плиз, логики отдельно от математиков обучаются, вместе с философами или как? Попалось мне как-то видео Андрея Родина, может он вам знаком. Вроде он не математик, но обсуждает постоянно теорию категорий, алгебраическую геометрию, труды Воеводского. Но непонятно, как можно о современной математике говорить, если ты ей не занимаешься. Насколько это все котируется в научном сообществе. Хотя он вроде не балабол, доктор философских наук, тусуется в ВШЭ, у него на защите докторской Вавилов был и хорошо о нем отзывался. Поясните, какой тут положняк?
255 Кб, 400x400Поясните, плиз, логики отдельно от математиков обучаются, вместе с философами или как? Попалось мне как-то видео Андрея Родина, может он вам знаком. Вроде он не математик, но обсуждает постоянно теорию категорий, алгебраическую геометрию, труды Воеводского. Но непонятно, как можно о современной математике говорить, если ты ей не занимаешься. Насколько это все котируется в научном сообществе. Хотя он вроде не балабол, доктор философских наук, тусуется в ВШЭ, у него на защите докторской Вавилов был и хорошо о нем отзывался. Поясните, какой тут положняк?
https://youtu.be/lXTuJL_VaSI?si=hSXsgV4UAF52bfR7
https://youtu.be/lXTuJL_VaSI?si=hSXsgV4UAF52bfR7
>>3542
Есть специальность "логика" у философов (ака 5.7.5 в номенклатуре ВАК) и есть специальность "математическая логика" у математиков (ака 1.1.5).
Соответственно, часто есть кафедра (лаборатория, институт, группа...) логики (и, обычно, чего-то еще) на математическом факультете, и кафедра (лаборатория, институт, группа...) логики на философском. Учатся математики-логики и философы-логики раздельно, если не считать возможные межфакультетские и междисциплинарные курсы/семинары.
Очевидно, он в математике, о которой он говорит, разобрался достаточно, чтобы заниматься философией математики. Разобрался он, вероятно, так же, как разбираются все остальные люди - читая книжки и разговаривая с людьми, работающими в области (вот https://philomatica.org/wp-content/uploads/2013/02/colin.pdf пример такого разговора). В принципе, самоучки, которые освоили какой-то материал в достаточной степени, чтобы понимать, что пишут другие, - это не какое-то редкое явление. Собственно производством новой математики он не занимается и, вроде как, не претендует.
Философия математики это существующая область, и вопросы, которые он обсуждает, в ней обсуждает не только он. Он где-то преподает и пишет статьи. В этом смысле, то, что он делает, вполне себе "котируется".
>Поясните, плиз, логики отдельно от математиков обучаются, вместе с философами или как?
Есть специальность "логика" у философов (ака 5.7.5 в номенклатуре ВАК) и есть специальность "математическая логика" у математиков (ака 1.1.5).
Соответственно, часто есть кафедра (лаборатория, институт, группа...) логики (и, обычно, чего-то еще) на математическом факультете, и кафедра (лаборатория, институт, группа...) логики на философском. Учатся математики-логики и философы-логики раздельно, если не считать возможные межфакультетские и междисциплинарные курсы/семинары.
>Но непонятно, как можно о современной математике говорить, если ты ей не занимаешься
Очевидно, он в математике, о которой он говорит, разобрался достаточно, чтобы заниматься философией математики. Разобрался он, вероятно, так же, как разбираются все остальные люди - читая книжки и разговаривая с людьми, работающими в области (вот https://philomatica.org/wp-content/uploads/2013/02/colin.pdf пример такого разговора). В принципе, самоучки, которые освоили какой-то материал в достаточной степени, чтобы понимать, что пишут другие, - это не какое-то редкое явление. Собственно производством новой математики он не занимается и, вроде как, не претендует.
>Насколько это все котируется в научном сообществе
Философия математики это существующая область, и вопросы, которые он обсуждает, в ней обсуждает не только он. Он где-то преподает и пишет статьи. В этом смысле, то, что он делает, вполне себе "котируется".
>>3054
Нашел кстати где-то у МЛ тезис о том что действительно мы не знаем что такое доказательство, если бы мы знали что такое доказательство, но мы не знаем что это такое...
Но при этом утверждается что единственный способ доказать конъюнкцию это предъявить пару доказательств. Почему нельзя это сделать еще каким то окольным путем? Или почему не учитываются возможные проблемы, например если имеются ресурсные ограничения - та самая "чернильная дыра", у человека заканчивается бумага чтобы выписать оба доказательства вместе, в формальной системе не хватает свободных переменных.
Еще интереснее тезис о применении функций к доказательствам при построении импликации. Т.е. мы не знаем что такое доказательство но мы будем применять к нему функции. Приехали.
Нашел кстати где-то у МЛ тезис о том что действительно мы не знаем что такое доказательство, если бы мы знали что такое доказательство, но мы не знаем что это такое...
Но при этом утверждается что единственный способ доказать конъюнкцию это предъявить пару доказательств. Почему нельзя это сделать еще каким то окольным путем? Или почему не учитываются возможные проблемы, например если имеются ресурсные ограничения - та самая "чернильная дыра", у человека заканчивается бумага чтобы выписать оба доказательства вместе, в формальной системе не хватает свободных переменных.
Еще интереснее тезис о применении функций к доказательствам при построении импликации. Т.е. мы не знаем что такое доказательство но мы будем применять к нему функции. Приехали.
>>3554
Цитату неси.
> Нашел кстати где-то у МЛ тезис о том что действительно мы не знаем что такое доказательство,
Цитату неси.
>>3556
https://archive-pml.github.io/martin-lof/pdfs/Truth-of-a-Proposition-Evidence-of-a-Judgment-1987.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
в конце какая то хуйня-малофья идет про хлеб и ненастоящий сладкий хлеб и про то что можно считать доказательством то что кажется достаточно убедительным лично тебе (или не считать, тут я не понял мнение лично МЛ на этот счет)
>>3559
Петух, ты разобрался какое понятие более общее "зеленые автомобили" или "автомобили" или для тебе это все еще неподъемная задача, кек?
Петух, ты разобрался какое понятие более общее "зеленые автомобили" или "автомобили" или для тебе это все еще неподъемная задача, кек?
>>3562
Хуй там, это ебанько даже определение абстракции не осилило, теперь вот бегает как опущенный со своей википедией. Такая вот абсиракция, лол.
Хуй там, это ебанько даже определение абстракции не осилило, теперь вот бегает как опущенный со своей википедией. Такая вот абсиракция, лол.
>>3563
N петух, общепринятое определение абстракции я цитировал. Но ты его не осилил, зато уверовал в рандомной ШУЕ.
N петух, общепринятое определение абстракции я цитировал. Но ты его не осилил, зато уверовал в рандомной ШУЕ.
>>3564
Ты копипастил нерелевантуню хуйню которую даже нормально прочитать и понять не смог. Ты даже отрицал что абстракция это понитие, т.е. у тебя мозги отшиблены на прочь от слова совсем, тебе с школьной программы нужно начинать а потом уже в основания лезть. О чём с тобой после этого говорить? Эта болезнь головного мозга (асемасия) описана у Манина в "доказумом и не доказуемом", он там приводил примеры как больные с частиным поражением мозга могли копипастить относительно сложные фразы (как например делаешь ты, хотя ни Мартин Лёфа ни Маркова ты не читал) при этом путались в элементарных понятиях. Если будет второе издание книги, тебя нужно в пример поставить, с цитатами, как канонического ебанька.
Ты копипастил нерелевантуню хуйню которую даже нормально прочитать и понять не смог. Ты даже отрицал что абстракция это понитие, т.е. у тебя мозги отшиблены на прочь от слова совсем, тебе с школьной программы нужно начинать а потом уже в основания лезть. О чём с тобой после этого говорить? Эта болезнь головного мозга (асемасия) описана у Манина в "доказумом и не доказуемом", он там приводил примеры как больные с частиным поражением мозга могли копипастить относительно сложные фразы (как например делаешь ты, хотя ни Мартин Лёфа ни Маркова ты не читал) при этом путались в элементарных понятиях. Если будет второе издание книги, тебя нужно в пример поставить, с цитатами, как канонического ебанька.
386 Кб, mp4,764x720, 0:03
>>3565
Энпе Тух, ты просто клоун. Все твои кукареканья - это всего лишь защитная реакция. А все твои маняаргументы контрятся первой же ссылкой из Википедии. Ты пытаешься приплести какую-то нерелевантную хуйню, какую-то "сасимасию Манина" (чего?), какие-то выдуманные "диагнозы", которые с готовностью приписываешь несогласным с твоим ШУЕ итд. Все это просто чтобы не признавать своего обсера в простейшем вопросе - определении абстракции. А это определение есть на каждом углу начиная с Википедии. Ты это прекрасно понимаешь. И тебе от этого никуда не деться, терпи Энпе Тух, терпи.
Энпе Тух, ты просто клоун. Все твои кукареканья - это всего лишь защитная реакция. А все твои маняаргументы контрятся первой же ссылкой из Википедии. Ты пытаешься приплести какую-то нерелевантную хуйню, какую-то "сасимасию Манина" (чего?), какие-то выдуманные "диагнозы", которые с готовностью приписываешь несогласным с твоим ШУЕ итд. Все это просто чтобы не признавать своего обсера в простейшем вопросе - определении абстракции. А это определение есть на каждом углу начиная с Википедии. Ты это прекрасно понимаешь. И тебе от этого никуда не деться, терпи Энпе Тух, терпи.
>>3567
Ничего, стадия отрицания у тебя скоро закончится и придёт сирение, мовный петух. Как говорили в одном фильме "...и тебя вылечат".
Твоя уровень это детские книжки с соовтествующими "определениями" для детей, что бы не травмировать психику раньше времени. Только непонятно, если ты дебил, зачем во взрослые треды лезешь со своим свиным рылом, ась? Отвечай, мовная петушара.
Ничего, стадия отрицания у тебя скоро закончится и придёт сирение, мовный петух. Как говорили в одном фильме "...и тебя вылечат".
Твоя уровень это детские книжки с соовтествующими "определениями" для детей, что бы не травмировать психику раньше времени. Только непонятно, если ты дебил, зачем во взрослые треды лезешь со своим свиным рылом, ась? Отвечай, мовная петушара.
>>3567
Ты бы лучше вместо ШУЕ уёбка сохацкого что нибудь путное почитал, того же Манина например.
Ведь один в один твой случай, как будто с тебя писали:
«Мл. лейтенант Засецкий, 23 лет, получил 2 марта 1943 года пулевое проникающее ранение черепа левой теменно-затылочной области. Ранение... осложнилось воспалительным процессом, вызвавшим слипчивый процесс в оболочках мозга и выраженные изменения в окружающих тканях мозгового вещества».
Нарушения психики Засецкого поначалу ужасны. Над всем доминирует асемасия — разрывы связей между знаком и его значением.
Первая встреча Засецкого с врачом: «Попробуйте прочитать эту страничку! «—»... Нет, что это? ... не знаю ... я не понимаю, что это ... Нет ... какое это? ... — «Ну, попробуйте посчитать что-нибудь простое, например сложите семь и шесть! ...»— «Семь ... шесть .. .как же это ... семь... нет, я не могу ... нет,-я совсем не знаю ...».
Утрачено понимание простейших предикатов:
«Что бывает перед зимой?» — «Перед зимой... или после зимы .. . лето ... или что-нибудь ... нет. Это у меня не выходит ...» — «А перед весной?» — «Перед весной ... сейчас весна ... а вот до ... или после ... я уже теряюсь ... нет ... у меня не выходит . . .»
Нарушается интерпретация смыслоорганизующих кодов синтаксиса:
«В школу, где училась Дуня, с фабрики пришла работница, чтобы сделать доклад». Что это? Кто же сделал доклад? Дуня? Работница? А где училась Дуня? И кто пришел с фабрики? И куда?»
Это трудный пример (текст А. Р. Лурия), но вот что пишет сам Засецкий: «А еще: «слон больше мухи» и «муха больше слона» ... Я понимал только, что «муха» маленькая, а «слон» большой, но разобраться в этих словах и ответить на вопрос, муха меньше слона или больше, я почему-то не мог. Главная же беда была в том, что я не мог понять, к чему относится слово «меньше» (или «больше») — к мухе или слону . . .».
Обращает на себя внимание сложность метаязыкового текста, описывающего языковые нарушения. Точность анализа нарушений кажется несовместимой с грубостью нарушений, которые анализируются. Это можно было бы объяснить тем, что анализ ретроспективен, но вот описание в настоящем времени, еще более глубокое: «... Я снова припоминаю про понятия «муха меньше слона» или «муха больше слона». Берусь думать над ними, как они должны правильно пониматься и как неправильно. От перестановки слов в этих понятиях изменяется смысл понятия. Мне же они кажутся на первый взгляд одинаковыми, словно ничего не изменяется от перестановки этих слов. А подольше подумаешь, заме-
чаешь, что or перестановки слов изменяется смысл указанных четырех слов (слон, муха, меньше, больше). Но мой мозг, моя память после ранения и до сих пор не в силах сразу охватить, к кому отнести слово меньше (или больше) — к слону или к мухе? Перестановок даже в этих четырех словах очень много».
Это сохранение сложных психических способностей при утрате «простых» видно и на образцах творческого воображения Засец-кого, близких к литературно-психологическим этюдам: «Вот-я врач. Я осматриваю больного, сердечно обеспокоен его состоянием, болею за него всей душой, ну как же, ведь это же человек, такой же, как и все, но только он сильно болен, ему надо помочь. Ведь я тоже могу болеть, и мне тоже кто-то должен помочь, а теперь вот надо помочь этому больному. Иначе нельзя. А вот я другой врач. Ох, и надоели мне эти больные со своими жалобами. Я не знаю, зачем я связался с этой медициной. Мне не хочется ничего делать, не хочется никому помогать. Правда, я. помогаю больше тем, кто и мне оказывает какую-нибудь помощь. И не беда, если умрет какой-нибудь больной, не в первый раз они умирали и умирают».
Все это показывает полную неосновательность мнения Дж. Россера [6]: «Когда доказательство открыто и записано на языке символической логики, его может проверить любой слабоумный (moron)».
> Ты пытаешься приплести какую-то нерелевантную хуйню, какую-то "сасимасию Манина" (чего?)
Ты бы лучше вместо ШУЕ уёбка сохацкого что нибудь путное почитал, того же Манина например.
Ведь один в один твой случай, как будто с тебя писали:
«Мл. лейтенант Засецкий, 23 лет, получил 2 марта 1943 года пулевое проникающее ранение черепа левой теменно-затылочной области. Ранение... осложнилось воспалительным процессом, вызвавшим слипчивый процесс в оболочках мозга и выраженные изменения в окружающих тканях мозгового вещества».
Нарушения психики Засецкого поначалу ужасны. Над всем доминирует асемасия — разрывы связей между знаком и его значением.
Первая встреча Засецкого с врачом: «Попробуйте прочитать эту страничку! «—»... Нет, что это? ... не знаю ... я не понимаю, что это ... Нет ... какое это? ... — «Ну, попробуйте посчитать что-нибудь простое, например сложите семь и шесть! ...»— «Семь ... шесть .. .как же это ... семь... нет, я не могу ... нет,-я совсем не знаю ...».
Утрачено понимание простейших предикатов:
«Что бывает перед зимой?» — «Перед зимой... или после зимы .. . лето ... или что-нибудь ... нет. Это у меня не выходит ...» — «А перед весной?» — «Перед весной ... сейчас весна ... а вот до ... или после ... я уже теряюсь ... нет ... у меня не выходит . . .»
Нарушается интерпретация смыслоорганизующих кодов синтаксиса:
«В школу, где училась Дуня, с фабрики пришла работница, чтобы сделать доклад». Что это? Кто же сделал доклад? Дуня? Работница? А где училась Дуня? И кто пришел с фабрики? И куда?»
Это трудный пример (текст А. Р. Лурия), но вот что пишет сам Засецкий: «А еще: «слон больше мухи» и «муха больше слона» ... Я понимал только, что «муха» маленькая, а «слон» большой, но разобраться в этих словах и ответить на вопрос, муха меньше слона или больше, я почему-то не мог. Главная же беда была в том, что я не мог понять, к чему относится слово «меньше» (или «больше») — к мухе или слону . . .».
Обращает на себя внимание сложность метаязыкового текста, описывающего языковые нарушения. Точность анализа нарушений кажется несовместимой с грубостью нарушений, которые анализируются. Это можно было бы объяснить тем, что анализ ретроспективен, но вот описание в настоящем времени, еще более глубокое: «... Я снова припоминаю про понятия «муха меньше слона» или «муха больше слона». Берусь думать над ними, как они должны правильно пониматься и как неправильно. От перестановки слов в этих понятиях изменяется смысл понятия. Мне же они кажутся на первый взгляд одинаковыми, словно ничего не изменяется от перестановки этих слов. А подольше подумаешь, заме-
чаешь, что or перестановки слов изменяется смысл указанных четырех слов (слон, муха, меньше, больше). Но мой мозг, моя память после ранения и до сих пор не в силах сразу охватить, к кому отнести слово меньше (или больше) — к слону или к мухе? Перестановок даже в этих четырех словах очень много».
Это сохранение сложных психических способностей при утрате «простых» видно и на образцах творческого воображения Засец-кого, близких к литературно-психологическим этюдам: «Вот-я врач. Я осматриваю больного, сердечно обеспокоен его состоянием, болею за него всей душой, ну как же, ведь это же человек, такой же, как и все, но только он сильно болен, ему надо помочь. Ведь я тоже могу болеть, и мне тоже кто-то должен помочь, а теперь вот надо помочь этому больному. Иначе нельзя. А вот я другой врач. Ох, и надоели мне эти больные со своими жалобами. Я не знаю, зачем я связался с этой медициной. Мне не хочется ничего делать, не хочется никому помогать. Правда, я. помогаю больше тем, кто и мне оказывает какую-нибудь помощь. И не беда, если умрет какой-нибудь больной, не в первый раз они умирали и умирают».
Все это показывает полную неосновательность мнения Дж. Россера [6]: «Когда доказательство открыто и записано на языке символической логики, его может проверить любой слабоумный (moron)».
>>3567
Ты бы лучше вместо ШУЕ уёбка сохацкого что нибудь путное почитал, того же Манина например.
Ведь один в один твой случай, как будто с тебя писали:
«Мл. лейтенант Засецкий, 23 лет, получил 2 марта 1943 года пулевое проникающее ранение черепа левой теменно-затылочной области. Ранение... осложнилось воспалительным процессом, вызвавшим слипчивый процесс в оболочках мозга и выраженные изменения в окружающих тканях мозгового вещества».
Нарушения психики Засецкого поначалу ужасны. Над всем доминирует асемасия — разрывы связей между знаком и его значением.
Первая встреча Засецкого с врачом: «Попробуйте прочитать эту страничку! «—»... Нет, что это? ... не знаю ... я не понимаю, что это ... Нет ... какое это? ... — «Ну, попробуйте посчитать что-нибудь простое, например сложите семь и шесть! ...»— «Семь ... шесть .. .как же это ... семь... нет, я не могу ... нет,-я совсем не знаю ...».
Утрачено понимание простейших предикатов:
«Что бывает перед зимой?» — «Перед зимой... или после зимы .. . лето ... или что-нибудь ... нет. Это у меня не выходит ...» — «А перед весной?» — «Перед весной ... сейчас весна ... а вот до ... или после ... я уже теряюсь ... нет ... у меня не выходит . . .»
Нарушается интерпретация смыслоорганизующих кодов синтаксиса:
«В школу, где училась Дуня, с фабрики пришла работница, чтобы сделать доклад». Что это? Кто же сделал доклад? Дуня? Работница? А где училась Дуня? И кто пришел с фабрики? И куда?»
Это трудный пример (текст А. Р. Лурия), но вот что пишет сам Засецкий: «А еще: «слон больше мухи» и «муха больше слона» ... Я понимал только, что «муха» маленькая, а «слон» большой, но разобраться в этих словах и ответить на вопрос, муха меньше слона или больше, я почему-то не мог. Главная же беда была в том, что я не мог понять, к чему относится слово «меньше» (или «больше») — к мухе или слону . . .».
Обращает на себя внимание сложность метаязыкового текста, описывающего языковые нарушения. Точность анализа нарушений кажется несовместимой с грубостью нарушений, которые анализируются. Это можно было бы объяснить тем, что анализ ретроспективен, но вот описание в настоящем времени, еще более глубокое: «... Я снова припоминаю про понятия «муха меньше слона» или «муха больше слона». Берусь думать над ними, как они должны правильно пониматься и как неправильно. От перестановки слов в этих понятиях изменяется смысл понятия. Мне же они кажутся на первый взгляд одинаковыми, словно ничего не изменяется от перестановки этих слов. А подольше подумаешь, заме-
чаешь, что or перестановки слов изменяется смысл указанных четырех слов (слон, муха, меньше, больше). Но мой мозг, моя память после ранения и до сих пор не в силах сразу охватить, к кому отнести слово меньше (или больше) — к слону или к мухе? Перестановок даже в этих четырех словах очень много».
Это сохранение сложных психических способностей при утрате «простых» видно и на образцах творческого воображения Засец-кого, близких к литературно-психологическим этюдам: «Вот-я врач. Я осматриваю больного, сердечно обеспокоен его состоянием, болею за него всей душой, ну как же, ведь это же человек, такой же, как и все, но только он сильно болен, ему надо помочь. Ведь я тоже могу болеть, и мне тоже кто-то должен помочь, а теперь вот надо помочь этому больному. Иначе нельзя. А вот я другой врач. Ох, и надоели мне эти больные со своими жалобами. Я не знаю, зачем я связался с этой медициной. Мне не хочется ничего делать, не хочется никому помогать. Правда, я. помогаю больше тем, кто и мне оказывает какую-нибудь помощь. И не беда, если умрет какой-нибудь больной, не в первый раз они умирали и умирают».
Все это показывает полную неосновательность мнения Дж. Россера [6]: «Когда доказательство открыто и записано на языке символической логики, его может проверить любой слабоумный (moron)».
> Ты пытаешься приплести какую-то нерелевантную хуйню, какую-то "сасимасию Манина" (чего?)
Ты бы лучше вместо ШУЕ уёбка сохацкого что нибудь путное почитал, того же Манина например.
Ведь один в один твой случай, как будто с тебя писали:
«Мл. лейтенант Засецкий, 23 лет, получил 2 марта 1943 года пулевое проникающее ранение черепа левой теменно-затылочной области. Ранение... осложнилось воспалительным процессом, вызвавшим слипчивый процесс в оболочках мозга и выраженные изменения в окружающих тканях мозгового вещества».
Нарушения психики Засецкого поначалу ужасны. Над всем доминирует асемасия — разрывы связей между знаком и его значением.
Первая встреча Засецкого с врачом: «Попробуйте прочитать эту страничку! «—»... Нет, что это? ... не знаю ... я не понимаю, что это ... Нет ... какое это? ... — «Ну, попробуйте посчитать что-нибудь простое, например сложите семь и шесть! ...»— «Семь ... шесть .. .как же это ... семь... нет, я не могу ... нет,-я совсем не знаю ...».
Утрачено понимание простейших предикатов:
«Что бывает перед зимой?» — «Перед зимой... или после зимы .. . лето ... или что-нибудь ... нет. Это у меня не выходит ...» — «А перед весной?» — «Перед весной ... сейчас весна ... а вот до ... или после ... я уже теряюсь ... нет ... у меня не выходит . . .»
Нарушается интерпретация смыслоорганизующих кодов синтаксиса:
«В школу, где училась Дуня, с фабрики пришла работница, чтобы сделать доклад». Что это? Кто же сделал доклад? Дуня? Работница? А где училась Дуня? И кто пришел с фабрики? И куда?»
Это трудный пример (текст А. Р. Лурия), но вот что пишет сам Засецкий: «А еще: «слон больше мухи» и «муха больше слона» ... Я понимал только, что «муха» маленькая, а «слон» большой, но разобраться в этих словах и ответить на вопрос, муха меньше слона или больше, я почему-то не мог. Главная же беда была в том, что я не мог понять, к чему относится слово «меньше» (или «больше») — к мухе или слону . . .».
Обращает на себя внимание сложность метаязыкового текста, описывающего языковые нарушения. Точность анализа нарушений кажется несовместимой с грубостью нарушений, которые анализируются. Это можно было бы объяснить тем, что анализ ретроспективен, но вот описание в настоящем времени, еще более глубокое: «... Я снова припоминаю про понятия «муха меньше слона» или «муха больше слона». Берусь думать над ними, как они должны правильно пониматься и как неправильно. От перестановки слов в этих понятиях изменяется смысл понятия. Мне же они кажутся на первый взгляд одинаковыми, словно ничего не изменяется от перестановки этих слов. А подольше подумаешь, заме-
чаешь, что or перестановки слов изменяется смысл указанных четырех слов (слон, муха, меньше, больше). Но мой мозг, моя память после ранения и до сих пор не в силах сразу охватить, к кому отнести слово меньше (или больше) — к слону или к мухе? Перестановок даже в этих четырех словах очень много».
Это сохранение сложных психических способностей при утрате «простых» видно и на образцах творческого воображения Засец-кого, близких к литературно-психологическим этюдам: «Вот-я врач. Я осматриваю больного, сердечно обеспокоен его состоянием, болею за него всей душой, ну как же, ведь это же человек, такой же, как и все, но только он сильно болен, ему надо помочь. Ведь я тоже могу болеть, и мне тоже кто-то должен помочь, а теперь вот надо помочь этому больному. Иначе нельзя. А вот я другой врач. Ох, и надоели мне эти больные со своими жалобами. Я не знаю, зачем я связался с этой медициной. Мне не хочется ничего делать, не хочется никому помогать. Правда, я. помогаю больше тем, кто и мне оказывает какую-нибудь помощь. И не беда, если умрет какой-нибудь больной, не в первый раз они умирали и умирают».
Все это показывает полную неосновательность мнения Дж. Россера [6]: «Когда доказательство открыто и записано на языке символической логики, его может проверить любой слабоумный (moron)».
>>3568
Энпе Тух, приведи свое петушиное определение абстракции, противоречащее общепринятому. Со ссылками, разумеется.
Энпе Тух, приведи свое петушиное определение абстракции, противоречащее общепринятому. Со ссылками, разумеется.
>>3570
Тебе и из википедии сойдёт, ты только его читать нучись без своей ШУЕ примеси.
А главное, это ты поясни почему оно не является понятием и кто тебе разрешал испльзовать в математике понятия без определения и одновременно не считать их исходными неопределямыми.
Тебе и из википедии сойдёт, ты только его читать нучись без своей ШУЕ примеси.
А главное, это ты поясни почему оно не является понятием и кто тебе разрешал испльзовать в математике понятия без определения и одновременно не считать их исходными неопределямыми.
>>3572
Меня оно устраивает если без твоих ШУЕ-интерпретаций, на остальную часть поста отвечай.
Меня оно устраивает если без твоих ШУЕ-интерпретаций, на остальную часть поста отвечай.
50 Кб, 720x405>>3576
Асисяй? Так какие претензии к определению абстракции в Википедии? Это приказ Израиля, чи шо?
>>3568
А у тебя какое-то тайноведение, закрытые оккультные писания не для всех, где абстракция определяется как-то иначе чем в общепринятом её понимании?
> асемасией
Асисяй? Так какие претензии к определению абстракции в Википедии? Это приказ Израиля, чи шо?
>>3568
> детские книжки с соовтествующими "определениями" для детей, что бы не травмировать психику раньше времени
А у тебя какое-то тайноведение, закрытые оккультные писания не для всех, где абстракция определяется как-то иначе чем в общепринятом её понимании?
>>3546
Местные основатели тоже терминов из книжек и разговоров нахватались и тоже получается философией математики занимаются тут.
Местные основатели тоже терминов из книжек и разговоров нахватались и тоже получается философией математики занимаются тут.
>>3580
То что ты привёл из википедии никакого отношения к нашему дискурсу не имеет, более того нисколько не противоречит тому что я писал. Просто ты как и подобает болезному умом простейший текст осилить не можешь, только бегаешь как опущенный с копипастами.
Это у тебя тупого ГСМ-ебанька абстракция магически сама себя определяет, в математике напротив, есть либо исходные понятия (аксиомы или доказательства/редукция к более простым понятиям). Касательно N ты ни первый способ ни второй не продемонстрировал, а значит можно в очередной раз сделать вывод что ты пиздливое хуйло.
То что ты привёл из википедии никакого отношения к нашему дискурсу не имеет, более того нисколько не противоречит тому что я писал. Просто ты как и подобает болезному умом простейший текст осилить не можешь, только бегаешь как опущенный с копипастами.
Это у тебя тупого ГСМ-ебанька абстракция магически сама себя определяет, в математике напротив, есть либо исходные понятия (аксиомы или доказательства/редукция к более простым понятиям). Касательно N ты ни первый способ ни второй не продемонстрировал, а значит можно в очередной раз сделать вывод что ты пиздливое хуйло.
>>3712
10 дней обтекал? Лови тогда ещё струю мочи в ебало.
Абстракция это свойство примеров, собственно, содержащих её. В случае N, абстракция потенциальной осуществимости является свойством аксиом Пеано.
10 дней обтекал? Лови тогда ещё струю мочи в ебало.
> абстракция магически сама себя определяет,
Абстракция это свойство примеров, собственно, содержащих её. В случае N, абстракция потенциальной осуществимости является свойством аксиом Пеано.
>>3712
N определяется аксиомами Пеано, абстракция потенциальной осуществимости это свойство аксиом Пеано. Следовательно, N определено. Свободен, клоун.
> Касательно N ты ни первый способ ни второй не продемонстрировал
N определяется аксиомами Пеано, абстракция потенциальной осуществимости это свойство аксиом Пеано. Следовательно, N определено. Свободен, клоун.
(Почти) $2$-категорные основания теоретико-множественной математики подъехали: https://arxiv.org/abs/2403.03647v1
75 Кб, 446x334>>3732
"А что, так можно было?!" Прикинь, можно. Достаточно писать что-то по теме треда, а не только выгуливать тут шизу, пытаясь "ниспровергать" общепризнанные давно доказанные вещи писаниями ноунейм ШУЕшников.
> О, в треде есть реально полезный контент, чаю
"А что, так можно было?!" Прикинь, можно. Достаточно писать что-то по теме треда, а не только выгуливать тут шизу, пытаясь "ниспровергать" общепризнанные давно доказанные вещи писаниями ноунейм ШУЕшников.
>>3749
Стандартно. Вот если бы через преобразование Фурье, вот это была бы настоящая чмондель-техника.
Стандартно. Вот если бы через преобразование Фурье, вот это была бы настоящая чмондель-техника.
>>3838
А с сохацким есть?
А с сохацким есть?
>>3838
Как же так? Ведь эллиптическая кривая и есть пучок. Но так уж и быть, можно ссылку?
Как же так? Ведь эллиптическая кривая и есть пучок. Но так уж и быть, можно ссылку?
>>3841
Ты загуглить не осилил, буквально. Кто тебе сказал, что ты криптографию в агде осилишь?
Ты загуглить не осилил, буквально. Кто тебе сказал, что ты криптографию в агде осилишь?
Пучкаю с последних постов в штаны.
>>3846
Я хочу создать криптографический пучок, чтобы только я знал, как ему дать формальное определение в теории типов Мартина-Лефа.
Я хочу создать криптографический пучок, чтобы только я знал, как ему дать формальное определение в теории типов Мартина-Лефа.
>>3849
Но пучок - понятие первичное.
Но пучок - понятие первичное.
>>3864
Пук Бернедектта на свiдомых мовах.
Пук Бернедектта на свiдомых мовах.
>>3889
Бернадектт одобряет.
Бернадектт одобряет.
>>3902
Читать научиться для начала. Стек де Рама - Черубини - Шрайбера тут неоднократно упоминали.
> А если серьезно, без шуток?
Читать научиться для начала. Стек де Рама - Черубини - Шрайбера тут неоднократно упоминали.
>>3906
так это для алгтопа
так это для алгтопа
>>4069
Может лучше сжечь книгу? Есть же теория категорий, ну или теория типов на крайний случай.
>теория множеств
Может лучше сжечь книгу? Есть же теория категорий, ну или теория типов на крайний случай.
>>4073
Не дает интуиции, просто язык для описания некоторых свойств. Чтобы понять почему эти свойства верны нужно заглядывать внутрь структуры или строить ее модели.
Удобно как если на беговую дорожку прийти в латексном костюме. Может можно будет о чем то говорить когда компуктер-саентисты разберутся с десятками взаимоисключающих способов определить равенства, структуры, высказывания.
Теория множеств - оптимальная золотая середина на данный момент.
>теория категорий
Не дает интуиции, просто язык для описания некоторых свойств. Чтобы понять почему эти свойства верны нужно заглядывать внутрь структуры или строить ее модели.
>теория типов
Удобно как если на беговую дорожку прийти в латексном костюме. Может можно будет о чем то говорить когда компуктер-саентисты разберутся с десятками взаимоисключающих способов определить равенства, структуры, высказывания.
Теория множеств - оптимальная золотая середина на данный момент.
>>4074
А теория множеств какую интуицию даёт?
Ты аксиоматическую теорию множеств видел? Как там удобно функции строить, например, знаешь?А когда с десятками взаимоисключающих способов определить категорию Set разберутся?
Для математика, который не занимается вознёй в основаниях, в целом, не очень важно, в какой системе работать, а те, кто возятся, в любом случае окажутся по уши в сотне технических проблем.
>Не дает интуиции, просто язык для описания некоторых свойств.
А теория множеств какую интуицию даёт?
>Удобно как если на беговую дорожку прийти в латексном костюме.
Ты аксиоматическую теорию множеств видел? Как там удобно функции строить, например, знаешь?А когда с десятками взаимоисключающих способов определить категорию Set разберутся?
Для математика, который не занимается вознёй в основаниях, в целом, не очень важно, в какой системе работать, а те, кто возятся, в любом случае окажутся по уши в сотне технических проблем.
>>4074
Они-то давно разобрались, это ты разберись.
Заодно разберись, что такое теория категорий. Судя по вышенаписанному, у тебя вообще нет понимания, что это и зачем.
> когда компуктер-саентисты разберутся с десятками взаимоисключающих способов определить равенства, структуры, высказывания.
Они-то давно разобрались, это ты разберись.
> Не дает интуиции, просто язык для описания некоторых свойств. Чтобы понять почему эти свойства верны нужно заглядывать внутрь структуры или строить ее модели.
Заодно разберись, что такое теория категорий. Судя по вышенаписанному, у тебя вообще нет понимания, что это и зачем.
>>4079
Функция определяется тем как действует на элементы. Определи мне возведение в квадрат в терминах теории категорий, а я над тобой поржу. Что такое топос определяется через аналогии с SET; вот если бы было наоборот тогда бы к мокрым мечтам категорщиков не было никаких вопросов.
Пока что потуги перевести основания на альтернативный формализм категорий или типов напоминают мне лисперов которым синтаксис ненужон.
>>4081
Иди терм отредуцируй, клоунесса конструктивная.
Функция определяется тем как действует на элементы. Определи мне возведение в квадрат в терминах теории категорий, а я над тобой поржу. Что такое топос определяется через аналогии с SET; вот если бы было наоборот тогда бы к мокрым мечтам категорщиков не было никаких вопросов.
Пока что потуги перевести основания на альтернативный формализм категорий или типов напоминают мне лисперов которым синтаксис ненужон.
>>4081
Иди терм отредуцируй, клоунесса конструктивная.
>>4083
Ты же в курсе, что функция из A в B в теории множеств стандартно определяется как подмножество A × B с рядом условий, да?
Возведение в квадрат чего? Натурального числа? Вещественного числа? Множества? Группы?
Причём тут топос? Какие аналогии? Ты же в курсе, что для категории Set нужны классы или там, например, универсум Гротендика, да?
>Функция определяется тем как действует на элементы.
Ты же в курсе, что функция из A в B в теории множеств стандартно определяется как подмножество A × B с рядом условий, да?
>Определи мне возведение в квадрат в терминах теории категорий, а я над тобой поржу.
Возведение в квадрат чего? Натурального числа? Вещественного числа? Множества? Группы?
>Что такое топос определяется через аналогии с SET
Причём тут топос? Какие аналогии? Ты же в курсе, что для категории Set нужны классы или там, например, универсум Гротендика, да?
>>4084
А ты в курсе как функция определяется в ТК? Никак
Допустим я хочу понять что из себя представялет возведение в квадрат и я смотрю:
1 - 1
2 - 4
3 - 9
...
поэлементно
Твои действия в аналогичной ситуации в рамках категориального подхода?
А ты в курсе как функция определяется в ТК? Никак
Допустим я хочу понять что из себя представялет возведение в квадрат и я смотрю:
1 - 1
2 - 4
3 - 9
...
поэлементно
Твои действия в аналогичной ситуации в рамках категориального подхода?
>>4086
Ты про какое-нибудь 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, да? А как тогда множество определяется в теории множеств? А отношение принадлежности там же? А как тип определяется в теории типов? А как определяется число в арифметике Пеано? А отношение «лежать между» в 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, например, значением и будет.
>поэлементно
В детский сад.
>>4089
Ясн. Ни для чего не пригодный формализм. Разве что только чтобы "переоткрывать" то что уже давно доказано через множества.т
Да нет, крайне ожидаемо - категорщики пытаются одевать штаны через голову - смешно смотреть.
>>поэлементно
>В детский сад.
Ясн. Ни для чего не пригодный формализм. Разве что только чтобы "переоткрывать" то что уже давно доказано через множества.т
> тоже крайне неожиданно
Да нет, крайне ожидаемо - категорщики пытаются одевать штаны через голову - смешно смотреть.
>>4090
Ты, долбоёбина, функцию Аккермана тоже поэлементно исследовать будешь? А функции из ℝ в ℝ, особенно разрывные?
У тебя, блядь, формализмами являются и теории множеств, и ETCS, дегенерат ебучий.
Ты, долбоёбина, функцию Аккермана тоже поэлементно исследовать будешь? А функции из ℝ в ℝ, особенно разрывные?
>Ни для чего не пригодный формализм.
У тебя, блядь, формализмами являются и теории множеств, и ETCS, дегенерат ебучий.
>>4091
Это противоречит чему именно? Только тому что ты не тупая ебанашка, не пиши мне больше.
>У тебя, блядь, формализмами являются и теории множеств, и ETCS, дегенерат ебучий.
Это противоречит чему именно? Только тому что ты не тупая ебанашка, не пиши мне больше.
>>4092
Сука, уёбок, у тебя в двух формализмах квадрат примерно одинаково определяется, но ты продолжаешь верещать, что один формализм априори лучше, а другой вообще не нужен, не разбираясь, блядь, ни в каком из них. Иди просто нахуй отсюда.
Сука, уёбок, у тебя в двух формализмах квадрат примерно одинаково определяется, но ты продолжаешь верещать, что один формализм априори лучше, а другой вообще не нужен, не разбираясь, блядь, ни в каком из них. Иди просто нахуй отсюда.
>>4074
Вся моя интуиция строится как раз на ней и теории типов, а не на теории множеств.
>Не дает интуиции,
Вся моя интуиция строится как раз на ней и теории типов, а не на теории множеств.
>>4084
NBG равнонепротиворечива с ZFC, а люди всё ещё ссут кровавой мочой от классов..
>Ты же в курсе, что для категории Set нужны классы или там, например, универсум Гротендика, да?
NBG равнонепротиворечива с ZFC, а люди всё ещё ссут кровавой мочой от классов..
>>4079
Гоша?
Гоша?
Почему по поводу аксиомы выбора возникают такие споры? Что это вообще с точки зрения Гротендика и теории категорий? Знаю, что Гротендик был недоволен состоянием топологии и её привязки к анализу.
>>4103
Всегда удивляло тоже, ведь самое проблемное место теории множеств - это схема выделения..
Что у тебя эпи в Set расщепимы, т.е. почти тоже самое, что любой модуль над F_1 проективен..
У меня скорее ощущение, что общей топологии быть не должно..
Просто так совпало, что мы изобрели настолько слабый концепт, что он работает в случаях, где мы используем совершенно разные методы
>Почему по поводу аксиомы выбора возникают такие споры?
Всегда удивляло тоже, ведь самое проблемное место теории множеств - это схема выделения..
>Что это вообще с точки зрения Гротендика и теории категорий?
Что у тебя эпи в Set расщепимы, т.е. почти тоже самое, что любой модуль над F_1 проективен..
>Знаю, что Гротендик был недоволен состоянием топологии и её привязки к анализу.
У меня скорее ощущение, что общей топологии быть не должно..
Просто так совпало, что мы изобрели настолько слабый концепт, что он работает в случаях, где мы используем совершенно разные методы
>>4108
над F2
над F2
>>4111
Ты хочешь своровать категорные интуиции?
Ты хочешь своровать категорные интуиции?
Категория - первичное понятие во всей математике.
>>4121
Не колхозная, а природная. Пучки отражают естественную красоту мира и связь локального с глобальным.
Не колхозная, а природная. Пучки отражают естественную красоту мира и связь локального с глобальным.
>>4125
Подозреваю, что какой-то не математик?
Подозреваю, что какой-то не математик?
>>4127
ПУЧК ПУЧК ПУЧК ПУЧК ПУЧК
ПУЧК ПУЧК ПУЧК ПУЧК ПУЧК
>>4103
Потому что из неё следует что движением можно клонировать шарики.
Потому что из неё следует что движением можно клонировать шарики.
>>4084
Ну это так себе определение, по сути эквивалентно самой упорядоченной паре т.к. если ты определил пару ты уже фиксировал соответствие. Тут как множество это совокупность, а совокупность это множество. Один хер с разных сторон.
>Ты же в курсе, что функция из A в B в теории множеств стандартно определяется как подмножество A × B с рядом условий, да?
Ну это так себе определение, по сути эквивалентно самой упорядоченной паре т.к. если ты определил пару ты уже фиксировал соответствие. Тут как множество это совокупность, а совокупность это множество. Один хер с разных сторон.
>>4083
Подпесалсо. Проблема в том что все альтернативы теории множеств контринтуитивны и при этом не дают ничего нового в в том плане что все равно по сути повторяют конструкции в теории множеств только на более сложном языке.
Подпесалсо. Проблема в том что все альтернативы теории множеств контринтуитивны и при этом не дают ничего нового в в том плане что все равно по сути повторяют конструкции в теории множеств только на более сложном языке.
>>4134
А почему не?
А почему не?
![17121476380070[1].mp4](https://2ch.life/math/thumb/112865/17121487781660s.jpg)
>>4143
Спектральный пук.
Спектральный пук.
196 Кб, 1354x1514>>4069
Да, это тот самый Успенский.
>>4073
Бурбаки с того света продолжают писать книги. В 2016 начала выходить Алгебраическая топология, там есть зайчатки теорката "по Бурбаки".
>>4083
На самом деле связи топосов с SET довольно спорны. По моему скромному мнению, гораздо более правильным является установление связей топосов с геометрией эйлеровых кругов на плоскости.
Да, это тот самый Успенский.
>>4073
Бурбаки с того света продолжают писать книги. В 2016 начала выходить Алгебраическая топология, там есть зайчатки теорката "по Бурбаки".
>>4083
На самом деле связи топосов с SET довольно спорны. По моему скромному мнению, гораздо более правильным является установление связей топосов с геометрией эйлеровых кругов на плоскости.
94 Кб, 1200x675У вас бывало такое, что вы пытались интерпретировать просмотренное аниме или прочитанную визуальную новеллу с помощью категорий? У меня не получается понять, какие должны быть морфизмы и объекты в категории по выбранному аниме 𝔸.
Сначала хотел сделать персонажей объектами, а их отношения морфизмами, но потом понял, что какая-то тривиальная категория получается. Мне кажется, нужно брать отдельную категорию для каждого аспекта произведения, например - категория Сюжет(𝔸), Темы(𝔸) и т.д. Что думаете, братья категористы?
Сначала хотел сделать персонажей объектами, а их отношения морфизмами, но потом понял, что какая-то тривиальная категория получается. Мне кажется, нужно брать отдельную категорию для каждого аспекта произведения, например - категория Сюжет(𝔸), Темы(𝔸) и т.д. Что думаете, братья категористы?
>>4290
я тоже
я тоже
>>4254
Можно сделать морфизмы "тропами" а ля tvtropes, а любой объект это простр "болванка", полностью определённая морфизмами из и в, т.е. всеми применимыми "тропами".
Можно сделать морфизмы "тропами" а ля tvtropes, а любой объект это простр "болванка", полностью определённая морфизмами из и в, т.е. всеми применимыми "тропами".
>>4341
namdak trompa spoq
namdak trompa spoq
111 Кб, 700x611>>4341
В принципе идея неплохая, гораздо лучше моей, но вижу проблему. Думаю тоже будет тривиальная категория или некий скелет высшей категории. Некоторые персонажи в аниме/визуальных новеллах обладают глубиной, которая выше тропов заложенных в них, т.е. тут есть некая высшая структура которая описуема только условными 2-морфизмами в этой категории.
Она не захватывает всей структуры.
Или может нужно использовать интуицию теории пучков и алгема? Локально персонаж определен полностью тропами, но глобально может быть что-то нетривиальное.
В принципе идея неплохая, гораздо лучше моей, но вижу проблему. Думаю тоже будет тривиальная категория или некий скелет высшей категории. Некоторые персонажи в аниме/визуальных новеллах обладают глубиной, которая выше тропов заложенных в них, т.е. тут есть некая высшая структура которая описуема только условными 2-морфизмами в этой категории.
Она не захватывает всей структуры.
Или может нужно использовать интуицию теории пучков и алгема? Локально персонаж определен полностью тропами, но глобально может быть что-то нетривиальное.
Вот есть логика, теория множеств, теория категорий и теория типов, как писали выше. В каком порядке это изучать, чтобы сохранить рассудок?
>>4491
Ну у меня получилось немного нестандартно.
Самое нормальное:
Главное не останавливаться только на одном теоркате или теории типов, там точно с ума можно сойти. И множества вообще не трогай, можно навсегда стать инвалидом в математическом плане. И разбавляй нормальную первокультурную математику теоркатом и теорией типов, чтобы понимать глубинные смыслы.
Ну у меня получилось немного нестандартно.
>программирование - теория типов - гомотопическая теория типов - теоркат - алгтоп - алгем и ПУЧКИ
Самое нормальное:
>база логики - теоркат и теория типов одновременно - алгем, алгтоп, высший теоркат и т.д.
Главное не останавливаться только на одном теоркате или теории типов, там точно с ума можно сойти. И множества вообще не трогай, можно навсегда стать инвалидом в математическом плане. И разбавляй нормальную первокультурную математику теоркатом и теорией типов, чтобы понимать глубинные смыслы.
Перекатываю вопрос из другого треда:
>>114625 →
>>114625 →
>>4638
Лучше сначала объясни, какие «противоречия, найдённые Гёделем» и как именно решила «типология Рассела»?
Лучше сначала объясни, какие «противоречия, найдённые Гёделем» и как именно решила «типология Рассела»?
>>4638
Нет, нельзя. И дело не в Гёделе. Формализация всей математики упирается в проблему разрешимости Гильберта, которая неразрешима, что доказал Тьюринг.
Нет, нельзя. И дело не в Гёделе. Формализация всей математики упирается в проблему разрешимости Гильберта, которая неразрешима, что доказал Тьюринг.
>>4642
Неразрешимость означает, что в общем случае нельзя алгоритмически доказательства искать; возможность загнать всё в одну большую систему и доказать её непротиворечивость она не исключает (исключает теорема Гёделя в известных случаях).
Неразрешимость означает, что в общем случае нельзя алгоритмически доказательства искать; возможность загнать всё в одну большую систему и доказать её непротиворечивость она не исключает (исключает теорема Гёделя в известных случаях).
>>4638
Всё, сам нашёл. ZFC/NBG.
Всё, сам нашёл. ZFC/NBG.
>>4643
Это конструктивный петух, он у нас особенный. Так что лучше приготовься к потоку шитпостов если хочешь ему чего то доказать.
Это конструктивный петух, он у нас особенный. Так что лучше приготовься к потоку шитпостов если хочешь ему чего то доказать.
>>4716
Думаю уёбок сохацкий за последние пару лет на своей жопе почувствовал её существование, лол.
Думаю уёбок сохацкий за последние пару лет на своей жопе почувствовал её существование, лол.
>>4716
Проиграл.
Проиграл.
>>4733
ультрафинитисты насрали
ультрафинитисты насрали
Почему теория типов вызывает такие негативные эмоции у разного круга лиц?
Раньше любил троллить с помощью неё на других бордах финитистов, математиков, алгемщиков пучкистов, и много кого.
Раньше любил троллить с помощью неё на других бордах финитистов, математиков, алгемщиков пучкистов, и много кого.
>>5666
Какой тип у 1?
Алсо достаточно глянуть на конструктивного петуха чтобы отпало желание заниматься теорией типов и вообще основаниями.
Какой тип у 1?
Алсо достаточно глянуть на конструктивного петуха чтобы отпало желание заниматься теорией типов и вообще основаниями.
>>5667
"X имеет тип Y" это же не предикат в теории типов, а утверждение мета уровня. В твоём случае вопрос не имеет смысла, потому что не существует абстрактного объекта в вакууме без типа. Дай определение 1, и сразу поймешь какой у него тип.
За счёт этого и хорошо получается троллить притворяясь ярым сторонником теории типов. Приверженцы других теорий оснований и математики сильно горят от неё, хотя по сути о ней знают очень мало.
"X имеет тип Y" это же не предикат в теории типов, а утверждение мета уровня. В твоём случае вопрос не имеет смысла, потому что не существует абстрактного объекта в вакууме без типа. Дай определение 1, и сразу поймешь какой у него тип.
За счёт этого и хорошо получается троллить притворяясь ярым сторонником теории типов. Приверженцы других теорий оснований и математики сильно горят от неё, хотя по сути о ней знают очень мало.
Почему ещё нет оснований, где именно пучок является первичным и неопределимым понятием? Почему первая культура так остаёт в основаниях? После Гротендика всё скатилось.
>>5669
Бла-бла-бла, бред. Не более "мета" чем существование пустого множества в теории множеств. От того что дурачки повторяют заученные швятые писание они не становятся правдой.
Ты сказал?
На самом деле подвох был в том что 1 это натуральное число. А так же это целое число. И нечетное число. Это очевидно любому здравомыслящему человеку как и то что теория типов ущербна.
Когда будешь тролить в следующий раз расскажи еще про пятьдесят оттенков равенства в теории типов. Тогда ты точно будешь у мамки главным тралом.
>утверждение мета уровня
Бла-бла-бла, бред. Не более "мета" чем существование пустого множества в теории множеств. От того что дурачки повторяют заученные швятые писание они не становятся правдой.
>не существует абстрактного объекта в вакууме без типа
Ты сказал?
На самом деле подвох был в том что 1 это натуральное число. А так же это целое число. И нечетное число. Это очевидно любому здравомыслящему человеку как и то что теория типов ущербна.
Когда будешь тролить в следующий раз расскажи еще про пятьдесят оттенков равенства в теории типов. Тогда ты точно будешь у мамки главным тралом.
239 Кб, 1920x1080>>5671
Существование пустого множества выразимо в самой теории типов. x : A это не предикат, как предикат существования или принадлежности множеству. В теории типов любая точка принадлежит какому-то пространству, без этого невозможно даже говорить об этой точке.
Но это сказал не я, а Мартин Лёв. Если хочешь доказать его неправоту, покажи хоть один объект без типа в теории типов. 1 не имеет смысла в контексте оснований без более глубокого объяснения того, о чём мы говорим. 1 натуральное число, если мы говорим о типе натуральных чисел определенных индуктивно, также это и целое число, если мы говорим о Дедекиновых сечениях.
Понимаешь, запись концепта не равна концепту, который она описывает. 1 может быть даже терминальным объектом в категории.
Про разные равенства кстати математики хорошо понимают интуитивно, но вот именно то, о чём мы сейчас говорим вызывает у них диссонанс. Норм почва для троллинга и финитистов, и теоретико-множественников. Прочитал HoTT и можно троллить почти весь математический контингент, да даже программистов.
Существование пустого множества выразимо в самой теории типов. x : A это не предикат, как предикат существования или принадлежности множеству. В теории типов любая точка принадлежит какому-то пространству, без этого невозможно даже говорить об этой точке.
Но это сказал не я, а Мартин Лёв. Если хочешь доказать его неправоту, покажи хоть один объект без типа в теории типов. 1 не имеет смысла в контексте оснований без более глубокого объяснения того, о чём мы говорим. 1 натуральное число, если мы говорим о типе натуральных чисел определенных индуктивно, также это и целое число, если мы говорим о Дедекиновых сечениях.
Понимаешь, запись концепта не равна концепту, который она описывает. 1 может быть даже терминальным объектом в категории.
Про разные равенства кстати математики хорошо понимают интуитивно, но вот именно то, о чём мы сейчас говорим вызывает у них диссонанс. Норм почва для троллинга и финитистов, и теоретико-множественников. Прочитал HoTT и можно троллить почти весь математический контингент, да даже программистов.
>>5672
Почему мне должно быть не похуй?
Всех затралил лалок, переиграл и уничтожил.
>Но это сказал не я, а Мартин Лёв.
Почему мне должно быть не похуй?
>покажи хоть один объект без типа в теории типов
>В Писании написано что Бог есть - шах и мат аметисты
Всех затралил лалок, переиграл и уничтожил.
>>5675
Вообще смешно как МЛ придумал концепцию "джаджментов" - это как аксиомы, но только аксиому другую можно выкинуть нахуй (как это провернул пришвятой Браузер например) а вот "джаджмент" это нечто "совершенно фундаментальное и само-собой разумеющееся" и если будешь в этом сомневаться то незримый дух конструктивизма тебя покарает. При этой разумеющности МЛ несколько раз менял фундаментальные "джаджменты" своей теории типов, обсираясь в процессе с парадоксами. Но дурачки хавают. just sayin.
(И это еще петух похоже еще где то гуляет на каникулах, а то уже весь тред в его перьях бы был)
Вообще смешно как МЛ придумал концепцию "джаджментов" - это как аксиомы, но только аксиому другую можно выкинуть нахуй (как это провернул пришвятой Браузер например) а вот "джаджмент" это нечто "совершенно фундаментальное и само-собой разумеющееся" и если будешь в этом сомневаться то незримый дух конструктивизма тебя покарает. При этой разумеющности МЛ несколько раз менял фундаментальные "джаджменты" своей теории типов, обсираясь в процессе с парадоксами. Но дурачки хавают. just sayin.
(И это еще петух похоже еще где то гуляет на каникулах, а то уже весь тред в его перьях бы был)
Еще одна очень интересная штука это тайп-классы. Очень смешно это как будто такая теория типов которую теортипизаторы придумали как бы "для себя". У каждого объекта должен быть только один тип и задается он при определении? Вы че ебанутые? Нет, "для себя" мы сделаем все ровно наоборот, мы же не ебнутые.
>>5676
Я слушал только одну его лекцию и не читал книги, он говорит эти джаджменты отражают объективную реальность или они работают только в пределах его теории типов? Если второе, то думаю они могут меняться.
>>5677
Тайп классы это ведь что-то из проггерства? Там вообще непонятно что происходит, у них там и вымышленная категория типов хаскеля есть.
>При этой разумеющности МЛ несколько раз менял фундаментальные "джаджменты" своей теории типов
Я слушал только одну его лекцию и не читал книги, он говорит эти джаджменты отражают объективную реальность или они работают только в пределах его теории типов? Если второе, то думаю они могут меняться.
>>5677
Тайп классы это ведь что-то из проггерства? Там вообще непонятно что происходит, у них там и вымышленная категория типов хаскеля есть.
>>5672
Ты наверно и аксиому унивалетности выпишешь с закрытыми глазами? Только не перепутай equivalence, equality и isomorphism.
>Про разные равенства кстати математики хорошо понимают интуитивно
Ты наверно и аксиому унивалетности выпишешь с закрытыми глазами? Только не перепутай equivalence, equality и isomorphism.
>>5680
Я да, недавно даже думал про неё в обычной жизни. Нормальные математики (то есть алгебраисты, пучкисты и прочие первокультурщики) интуитивно понимают различие изоморфизма и равенства. Им только нужно объяснить judgemental equality.
Я да, недавно даже думал про неё в обычной жизни. Нормальные математики (то есть алгебраисты, пучкисты и прочие первокультурщики) интуитивно понимают различие изоморфизма и равенства. Им только нужно объяснить judgemental equality.
14 Кб, 720x78>>5679
Добавили новую аксиому Брауэра-Вайлдбергера о неконструктивности множества целых чисел и уникальности единицы.
Добавили новую аксиому Брауэра-Вайлдбергера о неконструктивности множества целых чисел и уникальности единицы.
>>5690
В унылых доёбах до технических деталей каких-то теорий.
Точно так же можно визжать про то, почему в теории множеств зачастую 1 ∈ 3 и иногда (0, 0) = 2. Здравомыслящим людям там как, нормально вообще?
Можно повизжать про малые и большие множества, а заодно про классы, про необходимость городить универсум (Гротендика) ради теории категорий. А без теоремы о дедукции много доказать сможешь в Hilbert-style системе? Как, удобно?
>В чем состоит "говнотроллинг"?
В унылых доёбах до технических деталей каких-то теорий.
Точно так же можно визжать про то, почему в теории множеств зачастую 1 ∈ 3 и иногда (0, 0) = 2. Здравомыслящим людям там как, нормально вообще?
Можно повизжать про малые и большие множества, а заодно про классы, про необходимость городить универсум (Гротендика) ради теории категорий. А без теоремы о дедукции много доказать сможешь в Hilbert-style системе? Как, удобно?
>>5690
Не знаю что это, я читал только HoTT. Интересный концепт? Пригоден для троллинга?
>observational equality
Не знаю что это, я читал только HoTT. Интересный концепт? Пригоден для троллинга?
>>5691
Я говорю что то что тейк про то что у чего угодно должон быть один само-собой разумеющийся тип хуйня и это не очевидно только промытым адептам теории типов. Каким хуем это техническая деталь ТТ когда это ее самая основа, ты совсем чтоли ебанько тупое?
>>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.
>В унылых доёбах до технических деталей каких-то теорий.
Я говорю что то что тейк про то что у чего угодно должон быть один само-собой разумеющийся тип хуйня и это не очевидно только промытым адептам теории типов. Каким хуем это техническая деталь ТТ когда это ее самая основа, ты совсем чтоли ебанько тупое?
>>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.
>>5694
Как же у меня печет с ебанашки. HoTT это и есть скучная проггерская тема. А "математики" используют ZFC и вообще про основания не парятся.
>скучная проггерская тема
Как же у меня печет с ебанашки. HoTT это и есть скучная проггерская тема. А "математики" используют ZFC и вообще про основания не парятся.
>>5695
А я говорю тебе, что ты хуесос и пидорас, благодаря единственности типа проще добиться завершимости алгоритма проверки типов, а в теориях, где у терма может быть много типов (ничего себе, а так не один такой умник, да?), за этим надо отдельно следить (Coq).
>Я говорю что то что тейк про то что у чего угодно должон быть один само-собой разумеющийся тип хуйня и это не очевидно только промытым адептам теории типов. Каким хуем это техническая деталь ТТ когда это ее самая основа, ты совсем чтоли ебанько тупое?
А я говорю тебе, что ты хуесос и пидорас, благодаря единственности типа проще добиться завершимости алгоритма проверки типов, а в теориях, где у терма может быть много типов (ничего себе, а так не один такой умник, да?), за этим надо отдельно следить (Coq).
>>5697
Пффф проблемы типоманек, страдайте - добивайтесь, проще должно быть нормальным людям.
А кто тебе сказал что он должон завершатся? (ты ведь о разрешимости тайпчекинга) Опять транслируешь догматы швятых отцов или можешь привести какие то аргументы?
Разве там есть такое? Не припомню.
>проще добиться
Пффф проблемы типоманек, страдайте - добивайтесь, проще должно быть нормальным людям.
>завершимости алгоритма проверки типов
А кто тебе сказал что он должон завершатся? (ты ведь о разрешимости тайпчекинга) Опять транслируешь догматы швятых отцов или можешь привести какие то аргументы?
>у терма может быть много типов
>Coq
Разве там есть такое? Не припомню.
>>5697
Кстати, обрати внимани я использовал оборот "я говорю" т.к. ссылался на раннее написанное в треде. Но ты этого не понял, но решил повторить этот оборот за мной, т.к. ты и есть тупой хуесос и пидорас у которого разорвало сраку.
Кстати, обрати внимани я использовал оборот "я говорю" т.к. ссылался на раннее написанное в треде. Но ты этого не понял, но решил повторить этот оборот за мной, т.к. ты и есть тупой хуесос и пидорас у которого разорвало сраку.
37 Кб, 749x247>>5698
Добейтесь тогда, чтобы в теории множеств не было хуйни вроде «1 ∈ 2». (Ты долбоёб?)
Очевидно, при реализации завершающегося алгоритма можно опираться на пруф завершимости. Поэтому если такой алгоритм зацикливается, то проблема не в теории, а в реализации. Значит уровень доверия к такому чекеру выше.
Доброе утро.
>>5699
Какой же ты дегенерат ебанутый.
>Пффф проблемы типоманек, страдайте - добивайтесь, проще должно быть нормальным людям.
Добейтесь тогда, чтобы в теории множеств не было хуйни вроде «1 ∈ 2». (Ты долбоёб?)
>А кто тебе сказал что он должон завершатся? (ты ведь о разрешимости тайпчекинга) Опять транслируешь догматы швятых отцов или можешь привести какие то аргументы?
Очевидно, при реализации завершающегося алгоритма можно опираться на пруф завершимости. Поэтому если такой алгоритм зацикливается, то проблема не в теории, а в реализации. Значит уровень доверия к такому чекеру выше.
>Разве там есть такое? Не припомню.
Доброе утро.
>>5699
Какой же ты дегенерат ебанутый.
>>5700
Нахуя?
Пичот?
Напиши по-человечески что там тебе очевидно.
Т.е. ты представляешь себе такую гипотетическую ситуацию что - ты скармливаешь чекеру свою теорему. Он начинает чего то там бздеть-пердеть. И тут у тебя есть только два варианта - либо чекер говно, либо ты написал хуйню. Так? И вообще никаких способов выбрать одно или другое у тебя нет. Но вот если чекер исправно тебе выдает да/нет, то
(при том что на практике чекер может точно так же сколько угодно бздеть-пердеть потому что "за конечное время" еще не значит что ты его сможешь дождаться за свою жизнь)
У тебя кашка в голове.
Ну это мы уже реально дошли
Твоей мамке норм, вчера орала как последняя сучка.
>Добейтесь тогда, чтобы в теории множеств не было хуйни вроде «1 ∈ 2».
Нахуя?
>(Ты долбоёб?)
Пичот?
>Очевидно, при реализации завершающегося алгоритма можно опираться на пруф завершимости.
Напиши по-человечески что там тебе очевидно.
>Поэтому если такой алгоритм зацикливается, то проблема не в теории, а в реализации. Значит уровень доверия к такому чекеру выше.
Т.е. ты представляешь себе такую гипотетическую ситуацию что - ты скармливаешь чекеру свою теорему. Он начинает чего то там бздеть-пердеть. И тут у тебя есть только два варианта - либо чекер говно, либо ты написал хуйню. Так? И вообще никаких способов выбрать одно или другое у тебя нет. Но вот если чекер исправно тебе выдает да/нет, то
> Значит уровень доверия к такому чекеру выше.
(при том что на практике чекер может точно так же сколько угодно бздеть-пердеть потому что "за конечное время" еще не значит что ты его сможешь дождаться за свою жизнь)
У тебя кашка в голове.
>Доброе утро.
Ну это мы уже реально дошли
>до технических деталей каких-то теорий
>Though Set and Type are different in Coq, this is mostly due to historical reasons
>Какой же ты дегенерат ебанутый.
Твоей мамке норм, вчера орала как последняя сучка.
43 Кб, 755x258>>5701
А ради твоих хотелок кто чего добиваться должен, петушок?
Тупой хуесос не может понять, что ситуация «скормили терм чекеру, он зациклился, но мы не знаем, проблема в реализации или терме» предпочтительнее ситуации «скормили терм чекеру, он зациклился, но мы не знаем, проблемы в реализации, теории или терме».
Правда что ли? Вот это да! Никогда такого не было!
Причём тут отличия Set и Type, хуесосина тупая? Ты видишь, что там красным подчёркнуто, потому что слева и справа от равенства стоят термы разных типов?
>Нахуя?
А ради твоих хотелок кто чего добиваться должен, петушок?
>Т.е. ты представляешь себе такую гипотетическую ситуацию что - ты скармливаешь чекеру свою теорему. Он начинает чего то там бздеть-пердеть. И тут у тебя есть только два варианта - либо чекер говно, либо ты написал хуйню. Так? И вообще никаких способов выбрать одно или другое у тебя нет. Но вот если чекер исправно тебе выдает да/нет, то
Тупой хуесос не может понять, что ситуация «скормили терм чекеру, он зациклился, но мы не знаем, проблема в реализации или терме» предпочтительнее ситуации «скормили терм чекеру, он зациклился, но мы не знаем, проблемы в реализации, теории или терме».
>при том что на практике чекер может точно так же сколько угодно бздеть-пердеть потому что "за конечное время" еще не значит что ты его сможешь дождаться за свою жизнь
Правда что ли? Вот это да! Никогда такого не было!
>Ну это мы уже реально дошли
>>Though Set and Type are different in Coq, this is mostly due to historical reasons
Причём тут отличия Set и Type, хуесосина тупая? Ты видишь, что там красным подчёркнуто, потому что слева и справа от равенства стоят термы разных типов?
>>5702
Такая смешная тупая обиженка. А ты - А ты - А ты. Аргументов нет т.к. всякая мыслительная деятельность заменена на цитирование швятых отцов.
Должен потому что типизаторы хотят чтобы их построениями пользовались мейнстримные математики, а те в свою очередь в своей работе не различают 1:N и 1:Z и им типы только мешают. Все то надо дауненку разжевывать.
(И чтоб дауненок не квакал еще - нет 1 ∈ 2 математики не доказывают и ровно поэтому им это не мешает ничем, стрелочка не поворачивается)
Ты скормил терм тайпчекеру, он бздит уже второй день. Твои действия?
У долбоебушки ничего сложнее a+b=b+a не доказывавшего безусловно. Out of memory это тоже народные придания.
Напомню мы говорим про
Т.е. ты продолжаешь настаивать что ты больше веруешь в тайпчекер потому что можно доказать что он обязательно рано или поздно остановится на любом входе. Потому что?... Даже если бы он представлял из себя миллион строк говнокода. Ну долбоебушка.
Конечно я же слетал на машине времени чтобы глянут в картинку которую ты запостишь в будущем. Значит ты все таки говоришь про Universe polymorphism, который кстати тоже меняли в coq разок-другой. Чем он вообще релевантен дискуссии? Ты просто решил притащить какого то невнятного говна чтобы все думали какой ты умный. Ты случайно не конструктивный клоун? Нужно срочно проверить.
Ответь пожалуйста на простой вопрос: какое понятие более общее - Машина Тьюринга или Универсальная Машина Тьюринга.
>А ради твоих хотелок кто чего добиваться должен, петушок?
Такая смешная тупая обиженка. А ты - А ты - А ты. Аргументов нет т.к. всякая мыслительная деятельность заменена на цитирование швятых отцов.
Должен потому что типизаторы хотят чтобы их построениями пользовались мейнстримные математики, а те в свою очередь в своей работе не различают 1:N и 1:Z и им типы только мешают. Все то надо дауненку разжевывать.
(И чтоб дауненок не квакал еще - нет 1 ∈ 2 математики не доказывают и ровно поэтому им это не мешает ничем, стрелочка не поворачивается)
>ситуация
Ты скормил терм тайпчекеру, он бздит уже второй день. Твои действия?
>Правда что ли? Вот это да! Никогда такого не было!
У долбоебушки ничего сложнее a+b=b+a не доказывавшего безусловно. Out of memory это тоже народные придания.
Напомню мы говорим про
>Значит уровень доверия к такому чекеру выше.
Т.е. ты продолжаешь настаивать что ты больше веруешь в тайпчекер потому что можно доказать что он обязательно рано или поздно остановится на любом входе. Потому что?... Даже если бы он представлял из себя миллион строк говнокода. Ну долбоебушка.
>Причём тут отличия Set и Type, хуесосина тупая? Ты видишь, что там красным подчёркнуто
Конечно я же слетал на машине времени чтобы глянут в картинку которую ты запостишь в будущем. Значит ты все таки говоришь про Universe polymorphism, который кстати тоже меняли в coq разок-другой. Чем он вообще релевантен дискуссии? Ты просто решил притащить какого то невнятного говна чтобы все думали какой ты умный. Ты случайно не конструктивный клоун? Нужно срочно проверить.
Ответь пожалуйста на простой вопрос: какое понятие более общее - Машина Тьюринга или Универсальная Машина Тьюринга.
>>5704
Мейнстримные математики ими пользуются, несмотря на твоё кудахтанье.
В отличие от тебя, диванного тупого хуесоса, я OOM в разных чекерах видел не раз.
Понимаешь, петушок, веруешь тут только ты, у тебя есть мантры (типов у терма должно быть много), ересь (тип должен быть один), святые отцы (настоящие™ мейнстримные математики) и отступники (проклятые программисты). В реальном же мире бывает и так (MLTT), и сяк (теории типов с subtyping), и даже в Coq’е иногда доказывают False, а в Lean так вообще фундаментальные проблемы с разрешимостью, но мейнстримные математики, о ужас, им всё равно пользуются.
И да, это не означает, что разрешимость нинужна.
Значит ты тупой пидорас-хуесос, который не может разглядеть, блядь, кумулятивность, которая в коке была до модного полиморфизма.
Тупая опущенная пидорасина, если ты пролистаешь чуть вверх, то увидишь, что я писал тебе, как в Coq’е у терма два разных типа бывает, пример чего я тебе и привёл.
Машина Тьюринга.
>Должен потому что типизаторы хотят чтобы их построениями пользовались мейнстримные математики
Мейнстримные математики ими пользуются, несмотря на твоё кудахтанье.
>У долбоебушки ничего сложнее a+b=b+a не доказывавшего безусловно. Out of memory это тоже народные придания.
В отличие от тебя, диванного тупого хуесоса, я OOM в разных чекерах видел не раз.
>Т.е. ты продолжаешь настаивать что ты больше веруешь
Понимаешь, петушок, веруешь тут только ты, у тебя есть мантры (типов у терма должно быть много), ересь (тип должен быть один), святые отцы (настоящие™ мейнстримные математики) и отступники (проклятые программисты). В реальном же мире бывает и так (MLTT), и сяк (теории типов с subtyping), и даже в Coq’е иногда доказывают False, а в Lean так вообще фундаментальные проблемы с разрешимостью, но мейнстримные математики, о ужас, им всё равно пользуются.
И да, это не означает, что разрешимость нинужна.
>Значит ты все таки говоришь про Universe polymorphism
Значит ты тупой пидорас-хуесос, который не может разглядеть, блядь, кумулятивность, которая в коке была до модного полиморфизма.
>Чем он вообще релевантен дискуссии?
Тупая опущенная пидорасина, если ты пролистаешь чуть вверх, то увидишь, что я писал тебе, как в Coq’е у терма два разных типа бывает, пример чего я тебе и привёл.
>Ответь пожалуйста на простой вопрос: какое понятие более общее - Машина Тьюринга или Универсальная Машина Тьюринга.
Машина Тьюринга.
>Дежурное напоминание - абстракция не может быть первичнее примеров, содержащих абстрагируемое свойство, а метаязык строится только над объектным языком, и так же не может быть первичнее него.
Получается, так и не было дано определение порядка, на котором здесь даётся определение первичности. Понятное дело, что для метаязыка как прессуппозиция подразумевается язык-объект подобно тому как пресуппозицией для вопроса "перестали ли вы пить коньяк по утрам?" является утверждение "вы пили коньяк" или для "является ли король Франции лысым?" утверждение "Франция не является республикой". Но я здесь не ставлю задачей себе логический анализ языка, а ставлю задачей выставить автора тупым долбоёбом и хохлом. Поэтому я добавлю, что для целых чисел отношение "больше" абсолютно изморфно отношению "меньше", и лишь если мы добавим аксиому, что "0<1", то мы сможешь сказать, что единица меньше минус-едницы, а не наоборот. Чисто экстенционально, без учёта смысла слов "больше" и "меньше", эти отношения одинаковые. Поэтому понять, какой смысл автор-хохол вкладывает в свои слова представляется затруднительным, а сам он его сформулировать не в состоянии в силу врождённой тупости и регидности мышления.
>>5707
Опа, дежурный петух опять вылез. Санитарам объявляется выговор.
Опа, дежурный петух опять вылез. Санитарам объявляется выговор.
>>5706
Я бы вообще этот вопрос ставил таким образом, что это не бог-из-машины, а вот как лично я могу написать программу, например, на питоне чтобы считать свои формулы, например, на латексе. Что я должен знать? Какими принципами руководствоваться? И банально какие аксиомы как правила преобразования строк мне нужны?
То есть это банальное требование воспроизводимости эксперимента, а не i+1 i-1
Я бы вообще этот вопрос ставил таким образом, что это не бог-из-машины, а вот как лично я могу написать программу, например, на питоне чтобы считать свои формулы, например, на латексе. Что я должен знать? Какими принципами руководствоваться? И банально какие аксиомы как правила преобразования строк мне нужны?
То есть это банальное требование воспроизводимости эксперимента, а не i+1 i-1
>>5709
Ты для начало понятие строки попробуй определить строго, многие вопросы отпадут.
Ты для начало понятие строки попробуй определить строго, многие вопросы отпадут.
>>5710
Понятия не имею, что ты подразумеваешь под строкой. Вот у меня текстовый редактор видит \n - значит дальше новая строка. У каждого свой взгляд.
Понятия не имею, что ты подразумеваешь под строкой. Вот у меня текстовый редактор видит \n - значит дальше новая строка. У каждого свой взгляд.
>>5710
А вот давай погорим, что такое вообще ЗНАК. Вот в отношении SRC - MSG - DST. Вот в этих рамках. И посмотрим, что ты ск4ажешь.
А вот давай погорим, что такое вообще ЗНАК. Вот в отношении SRC - MSG - DST. Вот в этих рамках. И посмотрим, что ты ск4ажешь.
>>5706
А про 1 ∈ 2 нечего не спизданешь еще? Ну пользуются конечно поплевываясь, куда деваться.
Только совершенно ебанутый будет утверждать что нет никаких трудностей при переносе неформальной математики в формальную когда надо дохуя всего переиначить чтобы просто запихнуть в прувер то что тебе надо. Будешь отрицать?
А к чему тогда были твои восклицания. Анивей, как к такому повороту отнеслись в твоей церкви Швятой Разрешимости?
Но сначала один анон спизданул что 1 это только если 1:N а по другому никак и быть не может в сам целый Мартин Леф так сказал. А потом ты закукарекал про разрешимость и... без нее тоже наверное никак?
Но если бывает и так и сяк, то у меня больше вопросов нет.
расшифруй только еще
Как это поможет мне определять существенно разные типы для одного терма - 1:N, 1:Z. Давай по-новой, чего ты там хотел доказать принеся какую то обскурную
фичу из coq. То что чем больше фичей в теории типов тем она сложнее? Ну охуеть ты мне глаза открыл.
Ну хотя бы не конструктивный петух, так что диалог в принципе возможен.
>Мейнстримные математики ими пользуются
А про 1 ∈ 2 нечего не спизданешь еще? Ну пользуются конечно поплевываясь, куда деваться.
Только совершенно ебанутый будет утверждать что нет никаких трудностей при переносе неформальной математики в формальную когда надо дохуя всего переиначить чтобы просто запихнуть в прувер то что тебе надо. Будешь отрицать?
>OOM в разных чекерах видел не раз.
А к чему тогда были твои восклицания. Анивей, как к такому повороту отнеслись в твоей церкви Швятой Разрешимости?
>В реальном же мире бывает и так (MLTT), и сяк
Но сначала один анон спизданул что 1 это только если 1:N а по другому никак и быть не может в сам целый Мартин Леф так сказал. А потом ты закукарекал про разрешимость и... без нее тоже наверное никак?
Но если бывает и так и сяк, то у меня больше вопросов нет.
расшифруй только еще
>Очевидно, при реализации завершающегося алгоритма можно опираться на пруф завершимости.
>Coq’е у терма два разных типа бывает
Как это поможет мне определять существенно разные типы для одного терма - 1:N, 1:Z. Давай по-новой, чего ты там хотел доказать принеся какую то обскурную
>The status of Universe Polymorphism is experimental.
фичу из coq. То что чем больше фичей в теории типов тем она сложнее? Ну охуеть ты мне глаза открыл.
Ну хотя бы не конструктивный петух, так что диалог в принципе возможен.
>>5712
Знак это клеймо на жопе мовно-конструктивной петушары.
Знак это клеймо на жопе мовно-конструктивной петушары.
>>5713
Заставляют, надо понимать, жрать теорию типов?
А я такое утверждал что ли?
Ты, наверное, охуеешь, но если запихивать пруф в прувер с теорией множеств, то тоже придётся переиначивать.
Я же не ебанутый.
Это проблемы одного анона.
Как никак, если я тебе сам же привёл в пример Lean, у которого с ней проблемы. Разрешимость тайпчекинга — одно из хороших свойств, как непрерывность — хорошее свойство функции. Зачем вообще нужна непрерывность, без непрерывности нельзя что ли? Иногда можно, иногда нужно, точно так же как и с разрешимостью тайпчекинга (да и разрешимостью предикатов вообще). Или зачем группе коммутативность?
Я же уже писал. Точно так же Lean, ядро которого хорошо отделено от фронтенда (в виде парсера, elaborator’а и прочего), вызывает больше доверия, чем ядро Coq, которое перемешано с языком (языками) тактик.
Как выше верно писали, такое ещё позволяет проще «воспроизвести эксперимент». У Lean, например, есть экспортный формат, то есть ты можешь написать свой независимый чекер термов в этом формате и проверить, действительно ли пруфы из Mathlib (https://github.com/leanprover-community/mathlib4) пруфы, а не наёбка, не занимаясь восстановлением алгоритма вывода типов и сотен тактик, как это было бы в Coq’е.
Что, собственно, уже не раз делали, одна из последних попыток, например: https://github.com/digama0/lean4lean
А разные юниверсы — это несущественно разные типы что ли, ёбаный в рот? Где проходит граница существенности?
Впрочем, то, чего именно ты хочешь, называется subtyping; хотя эти проблемы реально неплохо решаются продвинутым парсером вместе с тайпклассами (и нет, обычно их частью синтаксиса теории не делают, предвосхищая вскукареки про две разные теории на бумаге и в реализации).
Сука, блядь, какой 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.
>>5713
Заставляют, надо понимать, жрать теорию типов?
А я такое утверждал что ли?
Ты, наверное, охуеешь, но если запихивать пруф в прувер с теорией множеств, то тоже придётся переиначивать.
Я же не ебанутый.
Это проблемы одного анона.
Как никак, если я тебе сам же привёл в пример Lean, у которого с ней проблемы. Разрешимость тайпчекинга — одно из хороших свойств, как непрерывность — хорошее свойство функции. Зачем вообще нужна непрерывность, без непрерывности нельзя что ли? Иногда можно, иногда нужно, точно так же как и с разрешимостью тайпчекинга (да и разрешимостью предикатов вообще). Или зачем группе коммутативность?
Я же уже писал. Точно так же Lean, ядро которого хорошо отделено от фронтенда (в виде парсера, elaborator’а и прочего), вызывает больше доверия, чем ядро Coq, которое перемешано с языком (языками) тактик.
Как выше верно писали, такое ещё позволяет проще «воспроизвести эксперимент». У Lean, например, есть экспортный формат, то есть ты можешь написать свой независимый чекер термов в этом формате и проверить, действительно ли пруфы из Mathlib (https://github.com/leanprover-community/mathlib4) пруфы, а не наёбка, не занимаясь восстановлением алгоритма вывода типов и сотен тактик, как это было бы в Coq’е.
Что, собственно, уже не раз делали, одна из последних попыток, например: https://github.com/digama0/lean4lean
А разные юниверсы — это несущественно разные типы что ли, ёбаный в рот? Где проходит граница существенности?
Впрочем, то, чего именно ты хочешь, называется subtyping; хотя эти проблемы реально неплохо решаются продвинутым парсером вместе с тайпклассами (и нет, обычно их частью синтаксиса теории не делают, предвосхищая вскукареки про две разные теории на бумаге и в реализации).
Сука, блядь, какой 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.
>>5715
Да, можно и так сказать. Когда математику надоедает марать бумагу он лезет посмотреть какие там пруверы самые модные и молодежные. И видит там - coq, agda, lean... Приходится жрать что дают.
Видел тезис что если бы в безтиповые пруферы вливали бы столько же средств то и они бы были тоже вполне конкурентны.
Пример у тебя абсолютно ебанутый. Даже не знаю что еще сказать.
Да какое блядь это имеет отношение к разрешимости. Ты совсем дурачек и не понимаешь что никакого или просто пишешь хуйню лишь бы написать побольше хуйни?
Тебе часто в детстве говорили что ты какой то тупенький?
Но ведь ты прекрасно понял о чем я, зачем тогда опять включаешь дурачка? Или это дефолтный режим.
Кек знал что у тебя опять подорвет. Я мог бы написать как одно отменяет другое, ну да похуй. Я еще раз повторяю - нахуя ты его притащил, чудик? Чего хотел этим доказать?
>Заставляют, надо понимать, жрать теорию типов?
Да, можно и так сказать. Когда математику надоедает марать бумагу он лезет посмотреть какие там пруверы самые модные и молодежные. И видит там - coq, agda, lean... Приходится жрать что дают.
Видел тезис что если бы в безтиповые пруферы вливали бы столько же средств то и они бы были тоже вполне конкурентны.
>Разрешимость тайпчекинга — одно из хороших свойств, как непрерывность — хорошее свойство функции.
Пример у тебя абсолютно ебанутый. Даже не знаю что еще сказать.
>Точно так же Lean, ядро которого хорошо отделено от фронтенда
Да какое блядь это имеет отношение к разрешимости. Ты совсем дурачек и не понимаешь что никакого или просто пишешь хуйню лишь бы написать побольше хуйни?
Тебе часто в детстве говорили что ты какой то тупенький?
>А разные юниверсы — это несущественно разные типы что ли, ёбаный в рот?
Но ведь ты прекрасно понял о чем я, зачем тогда опять включаешь дурачка? Или это дефолтный режим.
>Сука, блядь, какой polymorphism?
Кек знал что у тебя опять подорвет. Я мог бы написать как одно отменяет другое, ну да похуй. Я еще раз повторяю - нахуя ты его притащил, чудик? Чего хотел этим доказать?
>>5716
Тут спорить не буду, вполне возможно, да.
Ну и в чём разница? У теорий типов точно так же есть синтаксис, как у, например, групп, и точно так же есть модели. Если ты воспринимаешь теорию типов как заповеди, спущенные святым (ну или наоборот, как тебе там надо?) Мартином-Лёфом, то это исключительно твои проблемы.
Сука, ну такая же мотивация, блядь, что ядро маленьким делать, что разрешимости добиваться. Ты реально не понимаешь?
У тебя комплексы какие-то?
Что кого? Без (universe) полиморфизма не бывает кумулятивности? Без кумулятивности не бывает полиморфизма? Так ты же дегенерат.
Так это не ты верещал, что всем директивно спустили необходимость иметь каждому терму ровно один тип?
Я пишу тебе, блядь, бывает у терма много типов, даже в, казалось бы, Coq’е (но не только там), хоть и не в той форме, какой тебе надо, но у тебя почему-то от этого истошный визг.
>Видел тезис что если бы в безтиповые пруферы вливали бы столько же средств то и они бы были тоже вполне конкурентны.
Тут спорить не буду, вполне возможно, да.
>Пример у тебя абсолютно ебанутый. Даже не знаю что еще сказать.
Ну и в чём разница? У теорий типов точно так же есть синтаксис, как у, например, групп, и точно так же есть модели. Если ты воспринимаешь теорию типов как заповеди, спущенные святым (ну или наоборот, как тебе там надо?) Мартином-Лёфом, то это исключительно твои проблемы.
>Да какое блядь это имеет отношение к разрешимости. Ты совсем дурачек и не понимаешь что никакого или просто пишешь хуйню лишь бы написать побольше хуйни?
Сука, ну такая же мотивация, блядь, что ядро маленьким делать, что разрешимости добиваться. Ты реально не понимаешь?
>Тебе часто в детстве говорили что ты какой то тупенький?
У тебя комплексы какие-то?
>Я мог бы написать как одно отменяет другое, ну да похуй.
Что кого? Без (universe) полиморфизма не бывает кумулятивности? Без кумулятивности не бывает полиморфизма? Так ты же дегенерат.
>Но ведь ты прекрасно понял о чем я, зачем тогда опять включаешь дурачка?
Так это не ты верещал, что всем директивно спустили необходимость иметь каждому терму ровно один тип?
>Чего хотел этим доказать?
>>в Coq’е у терма может быть много типов
>>привожу пример
>аррряяя ПОЛИМОРФИЗМ аррряяяя
Я пишу тебе, блядь, бывает у терма много типов, даже в, казалось бы, Coq’е (но не только там), хоть и не в той форме, какой тебе надо, но у тебя почему-то от этого истошный визг.
>>5717
А у кошки четыре ноги и позади длинный хвост. Какой же ты ебанутый. Я хотел обсудить должна ли теория типов быть разрешимой или не обязательно и какие плюсы и минусы. Вроде удалось донести мысль что не должна. Напомню мы начали с тезиса
Теперь при более детальном рассмотрении я вижу что в нем столько нонсеквитуров что даже лениво их все разбирать.
Тяжело понять бред от безмозглого дебила. Маленькое ядро может реализовывать неразрешимую систему типов. Это вообще ортогональные консерны, можешь ты это уже понять ебаклак?
Сам себе напридумывал. Сам же себе и подибил. Главное по плечу себя не забудь похлопать какой ты у мамки молодец.
Ору с даунича. Может потому что
Не? Может попробуешь в какой надо форме принести чтобы не было никаких визгов? Но я понял твой модус-операнди это спиздануть какую то слайтли-релейтед хуету и пытаться делать умный вид.
>>Пример у тебя абсолютно ебанутый. Даже не знаю что еще сказать.
>Ну и в чём разница? У теорий типов точно так же есть синтаксис, как у, например, групп, и точно так же есть модели.
А у кошки четыре ноги и позади длинный хвост. Какой же ты ебанутый. Я хотел обсудить должна ли теория типов быть разрешимой или не обязательно и какие плюсы и минусы. Вроде удалось донести мысль что не должна. Напомню мы начали с тезиса
>А я говорю тебе, что ты хуесос и пидорас, благодаря единственности типа проще добиться завершимости алгоритма проверки типов, а в теориях, где у терма может быть много типов (ничего себе, а так не один такой умник, да?), за этим надо отдельно следить (Coq).
Теперь при более детальном рассмотрении я вижу что в нем столько нонсеквитуров что даже лениво их все разбирать.
>Сука, ну такая же мотивация, блядь, что ядро маленьким делать, что разрешимости добиваться. Ты реально не понимаешь?
Тяжело понять бред от безмозглого дебила. Маленькое ядро может реализовывать неразрешимую систему типов. Это вообще ортогональные консерны, можешь ты это уже понять ебаклак?
>>Я мог бы написать как одно отменяет другое, ну да похуй.
>Что кого? Без (universe) полиморфизма не бывает кумулятивности? Без кумулятивности не бывает полиморфизма? Так ты же дегенерат.
Сам себе напридумывал. Сам же себе и подибил. Главное по плечу себя не забудь похлопать какой ты у мамки молодец.
>хоть и не в той форме, какой тебе надо
>но у тебя почему-то от этого истошный визг.
Ору с даунича. Может потому что
>не в той форме, какой тебе надо
Не? Может попробуешь в какой надо форме принести чтобы не было никаких визгов? Но я понял твой модус-операнди это спиздануть какую то слайтли-релейтед хуету и пытаться делать умный вид.
>>5718
Какой же ты непрошибаемо тупой хуесос.
Я уже написал, что необязательно, ты это прочитал, но уже, видимо, забыл.
А, так это ты, хуесосина полуграмотная? Иди нахуй отсюда, уёбок тупой.
А где я писал обратное, дебилушка? Покажешь?
Опять ты жопой прочитал, но сделал далеко идущие выводы.
Так ты напишешь, кто кого отменяет? Зачем-то начал верещать про полиморфизм, а теперь загадочно умалчиваешь, зачем, делая вид дохуя специалиста.
Верещал нагло придуманную хуйню про
А теперь оправдывается, что он, видите ли, на самом деле, про subtyping говорил. Просто говна поешь.
Какой же ты непрошибаемо тупой хуесос.
>Я хотел обсудить должна ли теория типов быть разрешимой или не обязательно и какие плюсы и минусы.
Я уже написал, что необязательно, ты это прочитал, но уже, видимо, забыл.
>Теперь при более детальном рассмотрении я вижу что в нем столько нонсеквитуров что даже лениво их все разбирать.
А, так это ты, хуесосина полуграмотная? Иди нахуй отсюда, уёбок тупой.
>Маленькое ядро может реализовывать неразрешимую систему типов.
А где я писал обратное, дебилушка? Покажешь?
>Это вообще ортогональные консерны, можешь ты это уже понять ебаклак?
Опять ты жопой прочитал, но сделал далеко идущие выводы.
>Сам себе напридумывал.
Так ты напишешь, кто кого отменяет? Зачем-то начал верещать про полиморфизм, а теперь загадочно умалчиваешь, зачем, делая вид дохуя специалиста.
>Может попробуешь в какой надо форме принести чтобы не было никаких визгов?
Верещал нагло придуманную хуйню про
>У каждого объекта должен быть только один тип и задается он при определении? Вы че ебанутые?
А теперь оправдывается, что он, видите ли, на самом деле, про subtyping говорил. Просто говна поешь.
>>5719
Кто? У тебя делирий?
Нахуй ты вообще притащил свое маленькое ядро, клоунесса ебаная.
Очевидно чтобы сральню тебе разворотить. Как видишь план удался.
Чего блядь? Энивей, я же тебе говорю показывай теорию типов в которой рутинно объявляют один объект с разными типами вроде
А свой исторический флюк с coq'овским Set-Prop-Type-MProp(?)-сабтайпами для них и чего они там еще нахуевертели засунь себе в разорванную сральню откуда ты их вынул.
>А, так это ты
Кто? У тебя делирий?
>>Маленькое ядро может реализовывать неразрешимую систему типов.
>А где я писал обратное, дебилушка? Покажешь?
Нахуй ты вообще притащил свое маленькое ядро, клоунесса ебаная.
>Зачем-то начал верещать про полиморфизм, а теперь загадочно умалчиваешь, зачем, делая вид дохуя специалиста.
Очевидно чтобы сральню тебе разворотить. Как видишь план удался.
>>У каждого объекта должен быть только один тип и задается он при определении? Вы че ебанутые?
>А теперь оправдывается, что он, видите ли, на самом деле, про subtyping говорил.
> на самом деле, про subtyping говорил.
Чего блядь? Энивей, я же тебе говорю показывай теорию типов в которой рутинно объявляют один объект с разными типами вроде
>1 это натуральное число. А так же это целое число. И нечетное число.
А свой исторический флюк с coq'овским Set-Prop-Type-MProp(?)-сабтайпами для них и чего они там еще нахуевертели засунь себе в разорванную сральню откуда ты их вынул.
>>5721
Можешь не продолжать, я уже узнал тебя по твоим неуместным латинизмами, долбоёб.
Хули тебе показывать, если ты всё равно нихуя не понимаешь.
Что вот это предложение ярко и демонстрирует. Исторический флюк у него, блядь, во дегенерат.
Можешь не продолжать, я уже узнал тебя по твоим неуместным латинизмами, долбоёб.
>Энивей, я же тебе говорю показывай теорию типов в которой рутинно объявляют один объект с разными типами вроде
Хули тебе показывать, если ты всё равно нихуя не понимаешь.
>А свой исторический флюк с coq'овским Set-Prop-Type-MProp(?)-сабтайпами для них и чего они там еще нахуевертели засунь себе в разорванную сральню откуда ты их вынул.
Что вот это предложение ярко и демонстрирует. Исторический флюк у него, блядь, во дегенерат.
>>5722
Реально заинтриговал. Но думаю ты снова обосрался по причине - обсерытышь по жизни. Вообще 21 век идет, привыкай дедуль.
На самом интересном месте слился, жаль.
Контр-аргументы? Будешь утверждать что в coq не нахуевертели говна? Ты похоже еще на десяток ийсикю пунктов отупел от бессильной злобы.
>Можешь не продолжать, я уже узнал тебя по твоим неуместным латинизмами, долбоёб.
Реально заинтриговал. Но думаю ты снова обосрался по причине - обсерытышь по жизни. Вообще 21 век идет, привыкай дедуль.
>Хули тебе показывать, если ты всё равно нихуя не понимаешь.
На самом интересном месте слился, жаль.
>Что вот это предложение ярко и демонстрирует. Исторический флюк у него, блядь, во дегенерат.
Контр-аргументы? Будешь утверждать что в coq не нахуевертели говна? Ты похоже еще на десяток ийсикю пунктов отупел от бессильной злобы.
>>5723
Продолжай мриять, что не насрал хуйни, а филигранно затроллил.
Хули ты на ходу придумываешь тезисы, пидорас-хуесос-говноед? Вот где про это речь шла?
Продолжай мриять, что не насрал хуйни, а филигранно затроллил.
>Будешь утверждать что в coq не нахуевертели говна?
Хули ты на ходу придумываешь тезисы, пидорас-хуесос-говноед? Вот где про это речь шла?
>>5724
Чет маня совсем слилась. Думал манька будет получше. Но очень плохая манька попалась, некачественная к сожалению.
Чет маня совсем слилась. Думал манька будет получше. Но очень плохая манька попалась, некачественная к сожалению.
Линейный морфизм пучков.
>>5727
Чего не скажешь о Сохацком подцепившем сифилис в ТЦК.
Чего не скажешь о Сохацком подцепившем сифилис в ТЦК.
Перекат! https://2ch.hk/math/res/116183.html (М)
М)Двач.hk не отвечает.
Вы видите копию треда, сохраненную 17 сентября в 13:36.
Скачать тред: только с превью, с превью и прикрепленными файлами.
Второй вариант может долго скачиваться. Файлы будут только в живых или недавно утонувших тредах. Подробнее
Если вам полезен архив М.Двача, пожертвуйте на оплату сервера.
Вы видите копию треда, сохраненную 17 сентября в 13:36.
Скачать тред: только с превью, с превью и прикрепленными файлами.
Второй вариант может долго скачиваться. Файлы будут только в живых или недавно утонувших тредах. Подробнее
Если вам полезен архив М.Двача, пожертвуйте на оплату сервера.