Двач.hk не отвечает.
Вы видите копию треда, сохраненную 12 сентября в 23:59.
Скачать тред: только с превью, с превью и прикрепленными файлами.
Второй вариант может долго скачиваться. Файлы будут только в живых или недавно утонувших тредах. Подробнее
Если вам полезен архив М.Двача, пожертвуйте на оплату сервера.
Вы видите копию треда, сохраненную 12 сентября в 23:59.
Скачать тред: только с превью, с превью и прикрепленными файлами.
Второй вариант может долго скачиваться. Файлы будут только в живых или недавно утонувших тредах. Подробнее
Если вам полезен архив М.Двача, пожертвуйте на оплату сервера.
1,3 Мб, 2560x1920Поясните за математику. Что она описывает? Понятно, что окружающий нас мир, но где находятся такие вещи как множество мандельброта, например? И ведь не всякое можно описать, а только то, что существует. Но можно ли сказать, что Что-то описанное языком математики существует, если это что-то описано только ей, а в физическом мире не встречается? И если можно сказать, что существует, значит ли это то, что существуют другие миры?
>>65355 (OP)
/pr/
/re/
/sci/
>где находятся такие вещи как множество мандельброта, например?
/pr/
>Но можно ли сказать, что Что-то описанное языком математики существует, если это что-то описано только ей
/re/
>И если можно сказать, что существует, значит ли это то, что существуют другие миры?
/sci/
>>65355 (OP)
http://caute.ru/ilyenkov/texts/vf/prideala.html
>Понятно, что окружающий нас мир, но где находятся такие вещи как множество мандельброта, например?
http://caute.ru/ilyenkov/texts/vf/prideala.html
>>65366
Благодарю
Благодарю
>>65355 (OP)
Множество мандельброта - это просто множество компллексных чисел, удовлетворяющих некоему условию. Где оно существует в реальности? А где в реальности существует множество четных или простых чисел?
Множество мандельброта - это просто множество компллексных чисел, удовлетворяющих некоему условию. Где оно существует в реальности? А где в реальности существует множество четных или простых чисел?
Всё-таки эта подмывальня скатилась. Ещё года 4 назад основания обсуждали, философию математики, а сейчас хуета какая-то типа этого треда. Если бы сейчас N-петух вылез и начал тралить, местные зумера просто не поняли бы о чем речь вообще.
>>65376
Возьми судьбу в свои руки и сделай перекат треда оснований.
Возьми судьбу в свои руки и сделай перекат треда оснований.
>>65375
Ну вот же он, на оп-пике. Очевидно, это его проекция, но насколько реальна проекция, настолько же реально и само множества
Ну вот же он, на оп-пике. Очевидно, это его проекция, но насколько реальна проекция, настолько же реально и само множества
20 Кб, 300x300>>65383
Но на самом деле абсолютно похуй что рассматривать. Не нравятся мемные фракталь? Давайте посмотрим на числа. Я не могу просто крикнуть в окно, что поверх комплексных чисел есть хуемплексные. Это просто невозможно, потому что они нереальны, а все что на пике - реально. Так вот откуда это все появилось?
Но на самом деле абсолютно похуй что рассматривать. Не нравятся мемные фракталь? Давайте посмотрим на числа. Я не могу просто крикнуть в окно, что поверх комплексных чисел есть хуемплексные. Это просто невозможно, потому что они нереальны, а все что на пике - реально. Так вот откуда это все появилось?
363 Кб, 1650x1050>>65385
Но ведь вещественные числа, также известные как числа Аллаха существуют не более чем хуемплексные...
Но ведь вещественные числа, также известные как числа Аллаха существуют не более чем хуемплексные...
>>65388
Как видим, чуть более, все же
Как видим, чуть более, все же
>>65385
Есть же история математики. Там описано, какие причины послужили для придумывания новых типов чисел.
Есть же история математики. Там описано, какие причины послужили для придумывания новых типов чисел.
>>65392
Не придумывания, а скорее открытий? Это как говорить, что число pi придумали и продолжают придумывать уже дохуя знаков после запятой
Не придумывания, а скорее открытий? Это как говорить, что число pi придумали и продолжают придумывать уже дохуя знаков после запятой
>>65394
А почему ему не существовать? Комплесное число - это пара. Паре чисел можно поставить в соответствие точку на листке бумаги. Значит множество может быть нарисовано с какой-то точностью.
А почему ему не существовать? Комплесное число - это пара. Паре чисел можно поставить в соответствие точку на листке бумаги. Значит множество может быть нарисовано с какой-то точностью.
>>65385
Можешь. Можешь даже придумать для них опрделение и вывести теорию. Только никто не будет ими пользоваться, потому что нинужно.
Можешь. Можешь даже придумать для них опрделение и вывести теорию. Только никто не будет ими пользоваться, потому что нинужно.
>>65375
В определенном смысле, число пи придумали. Придумали обозначать "пи" отношение длины окружности к диаметру.
В определенном смысле, число пи придумали. Придумали обозначать "пи" отношение длины окружности к диаметру.
>>65438
Я не о его названии, братан, а вот об этом:
Число, которое люди для себя открыли существовало задолго до того как появились люди и наука изучающая его
Я не о его названии, братан, а вот об этом:
>отношение длины окружности к диаметру
Число, которое люди для себя открыли существовало задолго до того как появились люди и наука изучающая его
>>65437
Не потому что ненужно, а потому что связи с реальностью никакой у моих хуилионов не будет. Это совершенно разные вещи. Если бы они просто никому ненужны билы, но их можно было бы использовать, это одно, и совершенно другое, когда за названием ничего не стоит
>Только никто не будет ими пользоваться, потому что нинужно.
Не потому что ненужно, а потому что связи с реальностью никакой у моих хуилионов не будет. Это совершенно разные вещи. Если бы они просто никому ненужны билы, но их можно было бы использовать, это одно, и совершенно другое, когда за названием ничего не стоит
>>65437
>>65438
А вообще, ребята, вы меня поправьте, если я ошибаюсь, но ведь это тематическая доска и о математике здесь должны понимать побольше меня, мимокрокодила.
Кто-то умный сказал: математика - наука об отношениях между объектами, о которых ничего не известно, кроме описывающих их некоторых свойств, — именно тех, которые в качестве аксиом положены в основание той или иной математической теории.
Вот о чем тред! Математика изучает объекты изначально существующие, а не выдумывает их. Да, даёт названия, но как без этого?
Почему у анонов дающих здесь ответы настолько плоское восприятие математики?
>>65438
А вообще, ребята, вы меня поправьте, если я ошибаюсь, но ведь это тематическая доска и о математике здесь должны понимать побольше меня, мимокрокодила.
Кто-то умный сказал: математика - наука об отношениях между объектами, о которых ничего не известно, кроме описывающих их некоторых свойств, — именно тех, которые в качестве аксиом положены в основание той или иной математической теории.
Вот о чем тред! Математика изучает объекты изначально существующие, а не выдумывает их. Да, даёт названия, но как без этого?
Почему у анонов дающих здесь ответы настолько плоское восприятие математики?
>>65452
Основыные понятия (неопределяемые и определяемые) и аксиомы математики выдуманы. Разумеется, не на пустом месте, но тем не менее (необъяснимая эффеквтивность математики и бла-бла-бла). Пример с числом пи: окружности выдуманы, длины выдуманы и т.д.
>Математика изучает объекты изначально существующие, а не выдумывает их.
Основыные понятия (неопределяемые и определяемые) и аксиомы математики выдуманы. Разумеется, не на пустом месте, но тем не менее (необъяснимая эффеквтивность математики и бла-бла-бла). Пример с числом пи: окружности выдуманы, длины выдуманы и т.д.
>>65449
Это платонизм - всего лишь один из вариантов восприятия математики.
>Математика изучает объекты изначально существующие, а не выдумывает их.
Это платонизм - всего лишь один из вариантов восприятия математики.
>>65452
Если интересуешься философией математики, можешь начать с Википедии, там over 9000 названий и ссылок. Но это именно что философия - никаких определенных ответов там нет и никогда не будет.
Если интересуешься философией математики, можешь начать с Википедии, там over 9000 названий и ссылок. Но это именно что философия - никаких определенных ответов там нет и никогда не будет.
17 Кб, 512x342>>65460
Ну не траль. Выдуманы были определения этих явлений, а не они сами. Неужели ты хочешь сказать, что до того как люди произнесли эти слова, не было ни окружностей, ни длин?
>окружности выдуманы, длины выдуманы и т.д.
Ну не траль. Выдуманы были определения этих явлений, а не они сами. Неужели ты хочешь сказать, что до того как люди произнесли эти слова, не было ни окружностей, ни длин?
>>65461
Один из, но не менее справедливый чем все остальные. Поэтому я создал этот тред
Один из, но не менее справедливый чем все остальные. Поэтому я создал этот тред
>>65468
Ну, на мой взгляд да. Потому что это все абстракции свойств материальных предметов, а не сами предметы. Но я ж говорю, это философия, тут правды нет.
Ну, на мой взгляд да. Потому что это все абстракции свойств материальных предметов, а не сами предметы. Но я ж говорю, это философия, тут правды нет.
>>65355 (OP)
Самый разумный тред на доске.
Самый разумный тред на доске.
>>66009
Nlab вреден, это давно установлено. Читай
http://stacks.math.columbia.edu
а если так уж хочется философию, то лучше сразу
https://plato.stanford.edu
Nlab вреден, это давно установлено. Читай
http://stacks.math.columbia.edu
а если так уж хочется философию, то лучше сразу
https://plato.stanford.edu
Не испорченный шизой оригинал карты, если кому надо
http://srln.se/mapthematics.pdf
http://srln.se/mapthematics.pdf
>>66016
Нарисуй свой вариант
Нарисуй свой вариант
>>66094
уж лучше чем герыч
уж лучше чем герыч
![48ba242372782ef876b8e41a76f3e9db[1].jpg](https://2ch.life//math/src/65355/15901707169520.jpg)
48 Кб, 500x334>>65355 (OP)
Так и не могу понять как оно строится. Понял только, что комплексное число прогоняют через какую-то рекурсию. В чем ее суть?
>>65375
Под ЛСД, если глаза закрываю, то вижу эти фракталы.
Так и не могу понять как оно строится. Понял только, что комплексное число прогоняют через какую-то рекурсию. В чем ее суть?
>>65375
Под ЛСД, если глаза закрываю, то вижу эти фракталы.
>>69242
Берем комплексное число C, строим из него последовательность.
Z[1]=C
Z[2]=Z[1]^2 + C
...
Z[n]=Z[n-1]^2 + C
Если последовательность ограничена, то C принадлежит множеству (черный цвет).
Берем комплексное число C, строим из него последовательность.
Z[1]=C
Z[2]=Z[1]^2 + C
...
Z[n]=Z[n-1]^2 + C
Если последовательность ограничена, то C принадлежит множеству (черный цвет).
1 Мб, 1468x1129>>65355 (OP)
Ментальные построения, удовлетворяющие определенным свойствам.
> Поясните за математику. Что она описывает?
Ментальные построения, удовлетворяющие определенным свойствам.
>>69361
Модульный дед сам что-то подобное затирает. Типа пруверы это бездушное говно, в математику может только человек, а математическая запись на бумаге не более чем отражение математического мышления. Но без дальнейшего развития мысли в этом направлении ("математика подвешена в воздухе"), такой интуиционизм на минималках.
Модульный дед сам что-то подобное затирает. Типа пруверы это бездушное говно, в математику может только человек, а математическая запись на бумаге не более чем отражение математического мышления. Но без дальнейшего развития мысли в этом направлении ("математика подвешена в воздухе"), такой интуиционизм на минималках.
>>69376
Не нужно вдаваться в такие крайности, чтобы понять (и показать), что пруверы - говно без задач. Тут уже просили показать, как пруверы справляются с любой из реально важных теорем ХХ века, но местные питонисты слились. И дело тут ни в каких-то эфемерных сущностях, "душе", что-то там про "человека" - критерий исключительно прагматический.
Не нужно вдаваться в такие крайности, чтобы понять (и показать), что пруверы - говно без задач. Тут уже просили показать, как пруверы справляются с любой из реально важных теорем ХХ века, но местные питонисты слились. И дело тут ни в каких-то эфемерных сущностях, "душе", что-то там про "человека" - критерий исключительно прагматический.
>>69378
Ты же сам пынимаешь, что твой аргумент - такое себе "доказательство". Если всем создателям пруверов по какой-то причине похуй на то, что лично ты или там условный Вербицкий считаете важными теоремами а скорее всего похуй потому, что на самом деле, а не в сектантстком манямире, важными они не являются, это никак не доказывает твоей правоты. Ты путаешь отсутствие доказательства с доказательством отсутствия. Алсо, я ж давал ссылку на UniMath, там частично как раз пытаются обпучкаться. И опять же, я давал ссылку на работу, где доказывалось, что в общем случае гамалогии доказуемы только в изначально противоречивой системе со специально прописанным парадоксом Жирара. Что само по себе говорит о гамалогиях лучше чем о них сказано всей вашей сектой. С немалой вероятностью эта ваша хуета вообще ошибочна. Отсюда и ваше сектантство с отношением к математике уровня "тут играем, тут не играем, тут вообще рыбу заворачивали".
Ты же сам пынимаешь, что твой аргумент - такое себе "доказательство". Если всем создателям пруверов по какой-то причине похуй на то, что лично ты или там условный Вербицкий считаете важными теоремами а скорее всего похуй потому, что на самом деле, а не в сектантстком манямире, важными они не являются, это никак не доказывает твоей правоты. Ты путаешь отсутствие доказательства с доказательством отсутствия. Алсо, я ж давал ссылку на UniMath, там частично как раз пытаются обпучкаться. И опять же, я давал ссылку на работу, где доказывалось, что в общем случае гамалогии доказуемы только в изначально противоречивой системе со специально прописанным парадоксом Жирара. Что само по себе говорит о гамалогиях лучше чем о них сказано всей вашей сектой. С немалой вероятностью эта ваша хуета вообще ошибочна. Отсюда и ваше сектантство с отношением к математике уровня "тут играем, тут не играем, тут вообще рыбу заворачивали".
>>69417
Чекаются только если специально прописать правило типизации Type -> Type без использования кумулятивной иерархии типов. Жирар ещё в 1972 году доказал, что MLTT с таким правилом противоречива, т.к в ней можно прописать парадокс Рассела. В противном случае чекаются только очень некоторые гамалогии. Но свидетелям гамалогий проще заявить, что теория типов не математика, и вообще нет никаких оснований, а математика это гамалогии онли и они "подвешены в воздухе" и не нуждаются в основаниях.
> что значит "гамалогии ошибочны"?
Чекаются только если специально прописать правило типизации Type -> Type без использования кумулятивной иерархии типов. Жирар ещё в 1972 году доказал, что MLTT с таким правилом противоречива, т.к в ней можно прописать парадокс Рассела. В противном случае чекаются только очень некоторые гамалогии. Но свидетелям гамалогий проще заявить, что теория типов не математика, и вообще нет никаких оснований, а математика это гамалогии онли и они "подвешены в воздухе" и не нуждаются в основаниях.
>>69421
Это неправда, не обязятельно U -> U, можно U_n -> U_{n+1} :-) и тогда фиксается Жирар и открывается инфинити иерархия вселенных. К тому же модальные пруверы прекрасно работают с бесконечностями.
Это неправда, не обязятельно U -> U, можно U_n -> U_{n+1} :-) и тогда фиксается Жирар и открывается инфинити иерархия вселенных. К тому же модальные пруверы прекрасно работают с бесконечностями.
>>69422
На пруверах даже вселенную Махло можно построить, если кто-то тут знает, что это такое.
На пруверах даже вселенную Махло можно построить, если кто-то тут знает, что это такое.
>>69423
Гомологий это не касается, бесконечности нужны для когомологий.
Гомологий это не касается, бесконечности нужны для когомологий.
>Где в реальном мире находятся такие вещи как множество мандельброта?
Нигде. Описание окружающего мира заканчивается на аксиоматической системе, которая, вообще говоря, даже не обязана описывать мир, просто изначально придуманная для математики классическая АС не противоречила тому что было известно об окружающем мире, когда ее придумали, да и до сих пор не, поэтому мы считаем, что математика достоверно описывает действительность. Причем, некоторые части АС репрезентованы в окружающем мире очень условно, например мнимая единица. Вообще-то, есть математики построенные на АС, которые противоречат нашему восприятию мира. Наверное. Я, кроме неевклидовых геометрий, примеров привести не могу, но, я думаю, есть и какие-нибудь неклассические алгебры. Вся остальная математика - это следствия из АС. Множество мандельброта, в частности - это дополнительно введенное определение, которое можно свести к описанным в АС фундаментальным понятиям, нужное для того, чтобы проще описать некоторые следствия из АС. Оно само по себе ничего не репрезентует, помимо фундаментальных понятий на которые раскладывается.
В общем, анон >>69340 описал все то же самое существенно более кратко.
>>69422
Я знаю, что такое кумулятивная иерархия типов. И знаю что парадокс Жирара ими фиксится. Но, в такой непротиворечивой теории типов не чекаются гамалогии, я об этом писал.
Я знаю, что такое кумулятивная иерархия типов. И знаю что парадокс Жирара ими фиксится. Но, в такой непротиворечивой теории типов не чекаются гамалогии, я об этом писал.
>>69421
Проблемы млтт, а не гамалогий.
>Жирар ещё в 1972 году доказал, что MLTT с таким правилом противоречива,
Проблемы млтт, а не гамалогий.
>>69431
Отнюдь. Это ж чистое сектантство - основывать гамалогии на самих гамалогиях, утверждая что они висят в воздухе, а если противоречат основаниям, так это проблема оснований. Нет, ребятки, это так не работает. Можно конечно окуклиться в некоем манямире и игнорировать все остальное, только это уже уровень Рыбникова с его счётом шизов, семитами и электроатомами русов.
> Проблемы млтт, а не гамалогий.
Отнюдь. Это ж чистое сектантство - основывать гамалогии на самих гамалогиях, утверждая что они висят в воздухе, а если противоречат основаниям, так это проблема оснований. Нет, ребятки, это так не работает. Можно конечно окуклиться в некоем манямире и игнорировать все остальное, только это уже уровень Рыбникова с его счётом шизов, семитами и электроатомами русов.
>>69432
Понятное дело, что если добавить противоречивое правило, то из противоречия можно вывести что угодно, это не значит, что гамалогии противоречивы, это значит, что интуиционисты слишком тупые, чтобы вывести их без добавления противоречивого правила.
Понятное дело, что если добавить противоречивое правило, то из противоречия можно вывести что угодно, это не значит, что гамалогии противоречивы, это значит, что интуиционисты слишком тупые, чтобы вывести их без добавления противоречивого правила.
>>69433
Гамалогии в общем случае неконструктивны, без парадокса Жирара их никак не типизировать. Можно только дальше в них веровать, но как я написал выше, это ничем не лучше счета шизов.
Гамалогии в общем случае неконструктивны, без парадокса Жирара их никак не типизировать. Можно только дальше в них веровать, но как я написал выше, это ничем не лучше счета шизов.
294 Кб, 1197x593>>69435
А не швятых ли гамалогий? Или они априори истинны, ибо так завещал пыня пучкист?
> Проблемы МЛТТ.
А не швятых ли гамалогий? Или они априори истинны, ибо так завещал пыня пучкист?
>>69421
>>69426
>>69436
Я не понимаю.
"гамалогии" -- это не утверждения (это инварианты)
Как они могут быть "истинны", "чекаться", "противоречить"?
>>69426
>>69436
>Чекаются только если специально прописать правило
>не чекаются гамалогии
>основывать гамалогии на самих гамалогиях
>противоречат основаниям
> они априори истинны
Я не понимаю.
"гамалогии" -- это не утверждения (это инварианты)
Как они могут быть "истинны", "чекаться", "противоречить"?
>>69461
Как говорится: от модульного деда до N-петуха рукой подать.
Как говорится: от модульного деда до N-петуха рукой подать.
>>69435
На MLTT действительно хуй шо напишешь, это же ядро вокруг которого строится HoTT, ее флейворы кубические, точно N-петух.
На MLTT действительно хуй шо напишешь, это же ядро вокруг которого строится HoTT, ее флейворы кубические, точно N-петух.
>>69463
Вообще-то в той статье речь как раз об унивалентных основаниях, а не чистой MLTT. Но дело не в этом, а в том, что гамалогии в общем случае не имеют вычислительного содержания, с точки зрения свидетелей гамалогий, они истинны потому что что? Правильно, потому что истинны. Это принципиально нефальсифицируемая религия.
Вообще-то в той статье речь как раз об унивалентных основаниях, а не чистой MLTT. Но дело не в этом, а в том, что гамалогии в общем случае не имеют вычислительного содержания, с точки зрения свидетелей гамалогий, они истинны потому что что? Правильно, потому что истинны. Это принципиально нефальсифицируемая религия.
>>69471
Ответ на который прямо следует из того, на что я ответил. Если б ты понимал что вообще такое основания, то понимал бы и следствия из этого, а именно, что гамалогии представимы в виде термов HoTT, и как и все термы имеют в том числе свойства чекаться или не чекаться в различных системах типов. Так вот, чекаются гамалогии только в противоречивых системах с прописанным парадоксом Жирара.
> это были не аргументы, это был вопрос
Ответ на который прямо следует из того, на что я ответил. Если б ты понимал что вообще такое основания, то понимал бы и следствия из этого, а именно, что гамалогии представимы в виде термов HoTT, и как и все термы имеют в том числе свойства чекаться или не чекаться в различных системах типов. Так вот, чекаются гамалогии только в противоречивых системах с прописанным парадоксом Жирара.
> поясни, что значат выделенные зелёным фразы
Какой вообще смысл этих тредов, если местные фанатики пруверов и хотт не знают чистой математики в принципе? Это аналог волны CS андерградов, читающих теоркат и делающих вид, что им всё понятно, потому что в хаскеле якобы категории?
>>69480
Двачую, причём именно читающих, не царское это дело упражнения выполнять.
Двачую, причём именно читающих, не царское это дело упражнения выполнять.
>>69476
пиздец, а по-человечески никак нельзя?
но последующее объяснение, кажется, понял: "гамалогии можно описать в моём манямирке, но там это описание становится днищем; следовательно, гамалогии днище"
комментировать от себя это не буду, просто выделил главное
>прямо следует из того, на что я ответил.
>Если б ты понимал
пиздец, а по-человечески никак нельзя?
но последующее объяснение, кажется, понял: "гамалогии можно описать в моём манямирке, но там это описание становится днищем; следовательно, гамалогии днище"
комментировать от себя это не буду, просто выделил главное
>>69488
Это не я льщу себе, а ты не можешь ничего внятно сформулировать. Я простой вопрос спросил, но ты сумел только про мою тупость
Это не я льщу себе, а ты не можешь ничего внятно сформулировать. Я простой вопрос спросил, но ты сумел только про мою тупость
>>69522
Да нет, правда. Иначе они бы нормально чекались в любой теории типов, не требуя прописывания парадокса Жирара. Т.е были бы конструктивными объектами.
Да нет, правда. Иначе они бы нормально чекались в любой теории типов, не требуя прописывания парадокса Жирара. Т.е были бы конструктивными объектами.
>>69477
Гомологии начали формализировать еще на PRL системах, эта ебанутая идиотина N-петух наводить тень на конструктивною математику своей гадкой блевотиной. Они есть на Coq, Agda, и вообще на любой хуйне их можно написать --- это просто фактор группы спектральных комплексов, на бейсике можно, это комбинаторика.
Гомологии начали формализировать еще на PRL системах, эта ебанутая идиотина N-петух наводить тень на конструктивною математику своей гадкой блевотиной. Они есть на Coq, Agda, и вообще на любой хуйне их можно написать --- это просто фактор группы спектральных комплексов, на бейсике можно, это комбинаторика.
>>69532
Я так и думал.
Я так и думал.
>>69536
А еще CAS системы для счета интегралов и решения диффуров. Наверное, анализ и теория ду на этом исчерпаны.
>Ты понимаешь что уже десятилетия существуют CAS системы для счета гомологий?
А еще CAS системы для счета интегралов и решения диффуров. Наверное, анализ и теория ду на этом исчерпаны.
>>69537
Но ты же не говоришь что численное интегрирование неконструктивно. Что в эпсилон-окресностях больше конструктивизма, чем в перечислении дыр?
Но ты же не говоришь что численное интегрирование неконструктивно. Что в эпсилон-окресностях больше конструктивизма, чем в перечислении дыр?
50 Кб, 512x512>>69539
Самый неконструктивный тред в истории конструктивной математики :-)
Самый неконструктивный тред в истории конструктивной математики :-)
>>69537
А причем тут "исчерпаны" вообще? Вот есть автотранспорт, ты же надеюсь не считаешь, что ноги исчерпаны и "ногоблядь не человек"? Это просто инструмент. Ногами ты 200-300км в день не пройдешь, а на машине запросто. С чего вообще вся эта швитая война с пруверами итд, не очень понятно.
> А еще CAS системы для счета интегралов и решения диффуров. Наверное, анализ и теория ду на этом исчерпаны.
А причем тут "исчерпаны" вообще? Вот есть автотранспорт, ты же надеюсь не считаешь, что ноги исчерпаны и "ногоблядь не человек"? Это просто инструмент. Ногами ты 200-300км в день не пройдешь, а на машине запросто. С чего вообще вся эта швитая война с пруверами итд, не очень понятно.
>>69543
Это ты уже говорил. И да, это так. Про аналогию как явление вам в школке еще не рассказывали?
> я нихуя не понимаю
Это ты уже говорил. И да, это так. Про аналогию как явление вам в школке еще не рассказывали?
>>69544
если ты доказательства строишь так же как аналогии, то у меня для тебя плохие новости
если ты доказательства строишь так же как аналогии, то у меня для тебя плохие новости
>>69546
Доказательства это доказательства, аналогии это аналогии, что сказать-то хотел?
Доказательства это доказательства, аналогии это аналогии, что сказать-то хотел?
525 Кб, 948x1250Ну а если серьезно? Я смотрю, мнения обпучканных разделились. Модульный дед говорит, что гамалогии неконструктивны, какой-то хуй >>69532 утверждает обратное, грит хоть на бейсике можно сделать. Я лично сюда приносил ссылку на статью от создателей кока, там черным по белому написано что гамалогии в общем случае не чекаются в системе, в которой не прописан парадокс Жирара, а все что таки чекается, более-менее есть в UniMath. Ну так, что в итоге?
>>69536
.. для счёта гомологий простейших комплексов, да. Математика у вас тут дальше Пуанкаре не двигается?
Тут вообще кто-нибудь в треде современную чистую математику в глаза видел? Тред уровня IQ тредов на форче, только актёры из хотт палаты.
>Ты понимаешь что уже десятилетия существуют CAS системы для счета гомологий?
.. для счёта гомологий простейших комплексов, да. Математика у вас тут дальше Пуанкаре не двигается?
Тут вообще кто-нибудь в треде современную чистую математику в глаза видел? Тред уровня IQ тредов на форче, только актёры из хотт палаты.
>>69548
Проблема в том, что тот, кто сильно шарит в гамалогиях не шарит в пруферах, коках и всём таком и наоборот. Нужно астрально с Воеводским связаться, чтобы он пояснил за всё.
Проблема в том, что тот, кто сильно шарит в гамалогиях не шарит в пруферах, коках и всём таком и наоборот. Нужно астрально с Воеводским связаться, чтобы он пояснил за всё.
>>69554
Это да.
А это нет. Я ж приводил в пример UniMath. Воеводский в этой тусовочке не единственный в гамалогиях шарил.
> Проблема в том, что тот, кто сильно шарит в гамалогиях не шарит в пруферах, коках и всём таком
Это да.
> и наоборот.
А это нет. Я ж приводил в пример UniMath. Воеводский в этой тусовочке не единственный в гамалогиях шарил.
>>69556
лол
лол
>>69588
У одного гомологии неконструктивные, у второго UniMath оказывается еще актуален. Йобаные пидаро-черви.
У одного гомологии неконструктивные, у второго UniMath оказывается еще актуален. Йобаные пидаро-черви.
>>69589
На дваче нема с кем общаться. Все долбоебы.
На дваче нема с кем общаться. Все долбоебы.
>>69596
То есть, в твоём дырявом манямире факт недоказуемости аксиомы унивалентности в HoTT делает ее неактуальной?
То есть, в твоём дырявом манямире факт недоказуемости аксиомы унивалентности в HoTT делает ее неактуальной?
>>69619
тебе хотят объяснить что UniMath настолько аутдейтнутое говно, что в ней даже аксиома унивалентности недоказума.
тебе хотят объяснить что UniMath настолько аутдейтнутое говно, что в ней даже аксиома унивалентности недоказума.
>>69619
манямирок тут у тебя один, двач
манямирок тут у тебя один, двач
>>69660
ну дебил тут один ты, пушо UniMath написана на Coq, а Coq не является конструктивным прувером с аксиомой унивалентности, этим свойством обладают только кубические системы и HoTT пруверы на них построенные. Поэтому собирай остатки своего математического достоинства и упиздывай нахуй отседова, долбоебина второкультурная.
ну дебил тут один ты, пушо UniMath написана на Coq, а Coq не является конструктивным прувером с аксиомой унивалентности, этим свойством обладают только кубические системы и HoTT пруверы на них построенные. Поэтому собирай остатки своего математического достоинства и упиздывай нахуй отседова, долбоебина второкультурная.
>>69660
посцал тебе в рот
посцал тебе в рот
>>69680
Хуйни не неси.
Мань, в кубической теории типов аксиома унивалентности доказуема конструктивно, и является теоремой, а не аксиомой. Я не зря говорю что ты дебил, смирись с медицинским фактом.
> Coq не является конструктивным прувером
Хуйни не неси.
> с аксиомой унивалентности, этим свойством обладают только кубические системы и HoTT пруверы на них построенные
Мань, в кубической теории типов аксиома унивалентности доказуема конструктивно, и является теоремой, а не аксиомой. Я не зря говорю что ты дебил, смирись с медицинским фактом.
>>69691
очевидный шизик, распарсать текст не может
очевидный шизик, распарсать текст не может
>>69691
Так в кубической теории, ебанашка, а не в Coq, Coq это не кубическая теория, а значит в UniMath унивалентность недоказуема.
>Мань, в кубической теории типов аксиома унивалентности доказуема конструктивно, и является теоремой, а не аксиомой. Я не зря говорю что ты дебил, смирись с медицинским фактом.
Так в кубической теории, ебанашка, а не в Coq, Coq это не кубическая теория, а значит в UniMath унивалентность недоказуема.
>>70367
*Топология - это НЕ всякие узелки, да красивые бутылочки Клейна.
НЕ, СУКА, НЕ, БЛЯДЬ!!!
НЕ ВСЯКИЕ УЗЕЛКИ
НЕ ВСЯКИЕ БУТЫЛОЧКИ
НЕ НЕ НЕ!!!!
НЕЕЕЕЕЕЕЕЕЕЕЕЕЕЕЕЕЕ!!!!!!
*Топология - это НЕ всякие узелки, да красивые бутылочки Клейна.
НЕ, СУКА, НЕ, БЛЯДЬ!!!
НЕ ВСЯКИЕ УЗЕЛКИ
НЕ ВСЯКИЕ БУТЫЛОЧКИ
НЕ НЕ НЕ!!!!
НЕЕЕЕЕЕЕЕЕЕЕЕЕЕЕЕЕЕ!!!!!!
Начал читать, половина треда ссылается на гомологии и Жерара (Жирара). Не могу нагуглить, где Жирар (Жерар) запрещает гомологиями заниматься. Реквестирую линк.
>>77917
Читай внимательно
Читай внимательно
Весёлый тред. Я поорал! Всем добра и непротиворечивых гамалогий.
>>69421
А в чём проблема с существованием непротиворечивой вселенной? В плане, на стороне теории множеств есть же какие-нибудь новые основания Квайна, а на стороне теории типов не создали чего-то подобного?
А в чём проблема с существованием непротиворечивой вселенной? В плане, на стороне теории множеств есть же какие-нибудь новые основания Квайна, а на стороне теории типов не создали чего-то подобного?
>>82200
Можно доказать, что ZFC погружается в паранепротиворечивую теорию так, что область содержательных утверждений непротиворечива. Более того, аналогичными свойствами обладает цермело-френкель с большими кардиналами (почти всеми).
Можно доказать, что ZFC погружается в паранепротиворечивую теорию так, что область содержательных утверждений непротиворечива. Более того, аналогичными свойствами обладает цермело-френкель с большими кардиналами (почти всеми).
Двач.hk не отвечает.
Вы видите копию треда, сохраненную 12 сентября в 23:59.
Скачать тред: только с превью, с превью и прикрепленными файлами.
Второй вариант может долго скачиваться. Файлы будут только в живых или недавно утонувших тредах. Подробнее
Если вам полезен архив М.Двача, пожертвуйте на оплату сервера.
Вы видите копию треда, сохраненную 12 сентября в 23:59.
Скачать тред: только с превью, с превью и прикрепленными файлами.
Второй вариант может долго скачиваться. Файлы будут только в живых или недавно утонувших тредах. Подробнее
Если вам полезен архив М.Двача, пожертвуйте на оплату сервера.