Вся математика за пределами Спектральной категории формальных мов https://github.com/groupoid/formal.uno https://formal.uno/ - художественная литература, философский словарь гарантирует это: Философия: Энциклопедический словарь. — М.: Гардарики. Под редакцией А.А. Ивина. 2004. статья "гипостазирование" применительно к закону исключенного третьего.
Предыдущий - https://2ch.hk/math/res/105562.html
Сохацкий с бородкой на четвёртой?
Определили только пару петухов на парашу рядом с сохацким но не N.
Спрашиваю тебя-долбоёба в двадцатый раз: чем тебя не устраивает такое определение "минимальное по включению индуктивное множество" ?
Тебе уже объясняли сто раз. Попробуй доказать его существование без ссылок к интуитивному представлению индукции или рекурсии. Ты завуалировал вторичными понятиями суть дела, как только начнёшь его распутывать (а это неизбежно при доказательстве существования или практического использования натуральнрых чисел) опять скатишься к интуитивным представлениями.
ЗЫ ИМХО тебе подобные просто не владеют культурой математического мышления раз в упор не видят эти логичепские противоречия. Надеюсь тебя не допустят к обучению детей когда закончишь матфак своего педвузика, лол.
> к интуитивному представлению индукции или рекурсии
При чём тут интуитивное представление, если индукция и рексурсия - это схемы теорем в zfc? Ты глупенький что ли?
> Попробуй доказать его существование
Зачем ты заставляешь людей проделывать упражнения для школьников средних классов?
Ну если очень хочешь, то вот:
1) Cвойство "индуктивности" выражается в языке zfc следуюим образом: phi(x) = (\emptyset \in x) \land (\forall y \in x (y \cap {y} \in x))
2) Аксиома бесконечности из zfc дословно гласит следующее: \exists x phi(x)
3) Воспользуемся аксиомой степени и рассмотрим множество P(x) - всех подмножеств x.
4) Пользуясь инстансом схемы аксиом выделения для предиката phi выделим из P(x) все индуктивные элементы и обозначим получившееся множество за A. A не пусто, так как x \in P(x) и phi(x).
5) Пользуясь аксиомой пересечения рассмотрим множество N = \cap A.. Множество N индуктивно как пересечение множества индуктивных множеств. В частности, N \in A.
6) Пусть теперь z - проивзольное индуктивное множество. N \cap z индуктивно как пересечение индуктивных. Более того, N \cap z \subseteq N \subseteq x, а значит N \cap z \in A. Но значит N \subseteq N \cap z, а следовательно N = N \cap z. Откуда N \subseteq z.
Итак получили, что N - это индуктивное множество, вложенное в любое другое индуктивное множество.
Вроде бы тривиальное доказательство. Зачем ты тупишь, чел?
phi(x) = (\emptyset \in x) \land (\forall y \in x (y \cup {y} \in x))
Должно быть так.
>>107407
А ZFC у тебя где висит? Часом не в формальной системе которая внезапно формулируется как минимум в счетных алфавитах и вообще из нидукции и рекурсии не вылазит (иди перечитывай определение ФС)? Ты ж как попка фразы заучил а что за ними стоит не понимаешь. Открою тебе секрет, это называется не определением в классическом смысле (когда одно понятие сводится к другому) а КОДИРОВАНИЕ. Т.е. ты просто закодировал понятие натурального числа в ZFC используя при этом на метаязыке те же самые абстрации (индукцию, потенциальную осуществимость, рекурсию). По уровню доказательности это всё равно что множество определять как совокупность предметов.
То есть ты решил продолжить прикидываться дурачком?)
Хорошо. Тогда расскажи, в каких терминах ты хочешь, чтоб тебе определили натуральные числа?
> где висит
А какая разница где оно "висит", если это метаязык?) Я тебя наверно удивлю, но что бы ты не начал "определять" всё равно будет зиждиться на каких-то неопределимых понятиях. Мне эти трюизмы даже обсуждать смешно, этим обычно в детском саду переболеть успевают.
В любых что бы не было замкнутого круга. Если что метаязык замкнутый круг не рвёт по очевидным причинам.
>>107410
Так ты пиздел якобы можешь определит, а теперь скулишь что это неопределяемый труизм.
> В любых что бы не было замкнутого круга.
У тебя в любом случае будет либо бесконечная цепочка понятий, которые ты определяешь последовательно. Либо будет какой-то набор неопределимых понятий. Ты тупой что ли или да?
> Часом не в формальной системе которая внезапно формулируется как минимум в счетных алфавитах и вообще из нидукции и рекурсии не вылазит
А какая разница как формулируется определение формальной системы?
Ну так принеси мне этот минимальный набор исходных понятий и не пизди. Кто тебе мешал это сделать? Ты сам полез определять N через самого себя.
>>107414
Охуенная разница. Давай я сформулирую определение ФС и скажу что у неё алфавит это множество всех множеств?
> скажу что у неё алфавит это множество всех множеств?
Вообще похуй. В любом предложении, которое ты напишешь всё равно будет только конечное число символов. Чел, уровень твоего понимания проблематики - это реально уровень ясельной группы детсада. Мне чёт даже реально смешно стало)
Ну рассмотри урезанную логику первого порядка с конечным числом переменных и определи в ней всё то же самое. В чём проблема?)
> Математика наука о бесконечном
Которая представляет из себя преобразования конечных последовательностей символов. Пиздец ты сливаешься) Мог бы какие-то более свежие и интересные тейки подготовить, конечно.
Долбоящер, ты N не определил а опять кукарекаешь о конечном (т.е. натуральном числе). Ты совсем ебанько или да?
Тебе не надо определять, что такое N, чтобы написать на бумажке {a, b, c}.
Скучно...
Ты в глаза долбишься? тебе двумя сообщениями выше предложили конечный алфавит вместо счётного взять. Ебать ты конченый.
Крым - это территория государства Российская Федерация. Вот так адекватный, психически здоровый человек должен отвечать на вопрос "Чей Крым?". Ты ссылаешься на наличие какой-то собственности в Крыму, но у рядового хохла там тоже не было никакой собственности ни до майдана, ни тем более после. Так что по твоей логике хохлам вообще стоит забыть про Крым и заняться более насущными вопросами.
Зато на Украине тем временем вот что происходит:
>Украинская армия изменила правила призыва. Помимо отмены отсрочки от призыва для получающих второе высшее образование, внесены изменения в список "непризывных" болезней. Включая:
>2-в – клинически излеченный туберкулез;
>4-в – вирусные гепатиты с незначительным нарушением функций;
>5-в – бессимптомный ВИЧ;
>13-в – болезни эндокринной системы с незначительными нарушениями функций;
>14-в – легкие кратковременные болезненные проявления расстройств психики;
>17-в — невротические, связанные со стрессом и соматоформные расстройства при умеренно выраженных, краткосрочных проявлениях;
>21-в – медленно прогрессирующие болезни центральной нервной системы;
>22-в – эпизодические и пароксизмальные расстройства.
>Те, кого признали негодными ранее по этим болезням, теперь будут проходить обследование повторно.
>Комментировать не зачем. Можно просто сказать, что по каким-то неизвестным обстоятельствам украинская армия теперь нуждается и в людях с психическими заболеваниями, и в больных ВИЧ. При том, обращаю внимание, доказать наличие или отсутствие той или иной болезни, например ВИЧ или диабета, проще, чем доказать её "выраженность" или "не выраженность".
Получается что, хохлы заканчиваются?
>>107353 →
Я не понимаю, какой месседж ты пытаешься донести фотографиями сросшихся фруктов. По-моему, это трикстерство в самом строгом смысле слова.
>>107373 →
Я думаю, что ты попросту тупой, раз ты не смог осилить учебник по логике дальше нескольких абзацев. Ничего там хитрого нет, но у тебя почему-то закипели мозги, и ты изошёлся на говно в духе "не читал, но осуждаю". Если ты не вывозишь, то так и скажи. А пока что всё это выглядит как жалкий ресентимент.
Прочитай главу "Пра-логическое мышление в отношении к счислению" книги "Первобытное мышление" автора Люсьен Леви-Брюль, там описываются самые примитивные формы мысли, и это чисто один-в-один как ты мыслишь, в особенности в понимании счисления как процесса. Сейчас люди люди так не мыслят, поэтому, в частности, геометрия и алгебра как что-то различное не рассматривается, это всё вместе в одну дисциплину входит.
Могу ли я проголосовать за присоединение своей квартиры к территории США?
Вел ли Скиннер эксперименты над петухами?
* Сколько букв достаточно чтобы описать формальную теорию?
>Сколько букв достаточно чтобы описать формальную теорию?
Читай спектральные мовы там всё есть и больше!
>Вел ли Скиннер эксперименты над петухами?
Да, на этом и основанна вся моя любимая конструктошизовская теория!
>Могу ли я проголосовать за присоединение своей квартиры к территории США?
У Скиннера об этом ничего нет...
> Прочитай главу "Пра-логическое мышление в отношении к счислению" книги "Первобытное мышление" автора Люсьен Леви-Брюль, там описываются самые примитивные формы мысли,
Там описывается хуйня из головы. Я тебе уже сто раз написал, почему без четкого определения понятия мысли все остальные пуки на эту тему не стоят внимания.
> понимании счисления как процесса.
Вычисление и вообще существование потенциально-бесконечных типов и множеств как процесса вытекает из правил их построения. Это не чье-то понимание или мнение, это прямо прописанные правила формальной системы. Просто посмотри, как это прописано в какой-нибудь агде и все, ничего додумывать не нужно. Это соответствует потенциальной бесконечности. А вера в бесконечные объекты именно как в законченные вещи, соответствует актуальной бесконечности, и естественно является хуйней из головы, так как подобные объекты невозможны из самих их определений. В тех же аксиомах Пеано нет аксиомы, задающей последний элемент множества натуральных чисел, поэтому такое множество как законченный объект невозможно. Максимум возможно свойство "натуральности" числа, которое можно назвать "множеством", потому что чисел с таким свойством много.
>Просто посмотри, как это прописано в какой-нибудь агде и все
Куда смотреть?
> Куда смотреть?
https://agda.github.io/agda-stdlib/Agda.Builtin.Nat.html#186 N-петух ты или нет, в любом случае должен понимать, что любое определение чего угодно возможно только в контексте (в виде части операнта, элемента анализа в том числе вербального поведения), никаких "абсолютных", "высших" итд определений элементов вербального поведения (морфем, токенов, знаков, символов,...) вне контекста (остальных элементов операнта) невозможно. Именно это является в том числе причиной всех логических парадоксов. Вера в возможность определения вербального поведения вне контекста это как раз уровень зарядки банок от телевизора. Только в данном случае лучше заряжать банки с мочой от монитора с этим тредом и хлебать потом до просветления.
>Там описывается хуйня из головы
С точки зрения долбоёба - безусловно.
>без четкого определения понятия мысли все остальные пуки на эту тему не стоят внимания.
С точки зрения долбоёба - безусловно.
>так как подобные объекты невозможны из самих их определений
Дело в том, что ты ебанько и занимаешься гипостазированием.
У тебя совершенно примитивное, дологическое мышление. Древний человек поклоняется тотему вороны какой-нибудь вороны, и он видел в ней ворону как таковую. Также и ты в какой-нибудь конкретной тройке, например, яблок, видишь тройку вообще. Или путаешь имена и вещи, например, слово "хуй" и сам хуй как орган тела. Неудивительно, что с таким типом мышления ты не осилил учебник логики дальше двух обзацев. Ты попросту глуп. Впрочем, чего ещё ожидать от хохла?
> С точки зрения долбоёба - безусловно.
> С точки зрения долбоёба - безусловно.
Что-то тебя заклинило.
> Дело в том, что ты ебанько и занимаешься гипостазированием.
> У тебя совершенно примитивное, дологическое мышление. Древний человек поклоняется тотему вороны какой-нибудь вороны, и он видел в ней ворону как таковую
Ага, а ты сейчас поклоняешься тотему исключённого третьего, потому что видишь в нем исключенное третье как таковое, а не как правило, применимое в одних случаях и не применимое в других.
> Древний человек поклоняется тотему вороны какой-нибудь вороны, и он видел в ней ворону как таковую.
Вот этот момент тоже вопросы вызывает. С чего ты взял, что древний человек воспринимал тотем именно так, как написано в твоём дурачковом справошнике для долбаебов? Ты не допускаешь, что там могли быть абсолютно неочевидные для современного человека контексты? Или для тебя твой справошник - непререкаемая истина в последней инстанции?
>Что-то тебя заклинило.
Потому что иначе как долбоёбом я тебя назвать не могу.
>Ага, а ты сейчас поклоняешься тотему исключённого третьего, потому что видишь в нем исключенное третье как таковое, а не как правило, применимое в одних случаях и не применимое в других.
Я тебе сразу сказал, что данное правило является частью языка, а не внеязыковой реальности. А ты пытаешься опровернуть его ссылками на эмпирические факты.
Уловка 22. Я тебе говорю, что пруфы содержатся в книге, читай книгу. А ты не хочешь читать и требуешь пруфы. Но пруфы находятся в книге. И всё, хохол засофтлочился.
>>107467
Майдан в отдельно взятой квартире - это чудесно! Только вот тебя не возьмут в США, а отправят сжигать коран и потом получать пиздюлей от Кадырова.
> Я тебе сразу сказал, что данное правило является частью языка, а не внеязыковой реальности.
Так в твоём дурачковом справошнике нет определения языка, апеллируюшего к чему-либо доказуемому иначе чем ссылками на другую такую же хуйню из головы. Как и определения "неязыковой реальности", кстати. Поэтому все твои кукареканья особого значения не имеют.
> Я тебе говорю, что пруфы содержатся в книге, читай книгу.
Я тебе на примере мысли уже цитировал, что там за "пруфы". Это рандомная хуйня из головы. Если для тебя твой дурачковый справошник - священное писание, это не значит, что для всех остальных тоже.
Ты предложил хуйню с замкнутым кругом и опять нихуя не заметил потому что дебил. Шары разуй от стекломоя и внимательно посмотри на слово КОНЕЧНЫЙ. Если бы ты не был совсем конченым, ты бы заметил что это и езть натуральное число. И как я уже писал выше вся теория ФС, почти вся её теория основана на индукции и рекурсии, т.е. cуть N.
> Ты предложил хуйню с замкнутым кругом
Вот конкретный код определения N на агде, https://agda.github.io/agda-stdlib/Agda.Builtin.Nat.html#186 либо ты показываешь, где там замкнутый круг в определении множества натуральных чисел, либо официально признаешь себя клоуном.
Т.е. у тебя типичная ошибка когда на метаязыке ты используешь понятие которое якобы определяешь внутри этой системы. Но это тогда не определение а кодирование так же как ты вводишь в ZFC N в виде {0}, {{0}} и т.д.
> Агда на чем работает, ась? Это же имплементация ФС.
>>107498
> у тебя типичная ошибка когда на метаязыке ты используешь понятие которое якобы определяешь внутри этой системы.
Это не так. MLTT разрешима в MLTT (anders Сохацкого), агда - в агде https://www2.tcs.ifi.lmu.de/~abel/master/agda-scope-checker.html все понятия, определимых в агде, не требуют ничего кроме агды, никаких "метаязыков", все работает без этого. Собственно, на этом твои смешные "аргументы" про несуществующий замкнутый круг закончены?
Ебанько, у тебя совсем что ли вместо мозга насрано? Причём тут разрешимось, тебя бы даже дурачок сохацкий опустил бы.
> Причём тут разрешимось,
При том, что никакого метаязыка не требуется для определения N в MLTT, все необходимое для этого существует в самой MLTT, в том числе проверка корректности такого определения.
Major League Table Tennis в данном случае и есть метаязык для формулирования определения N. Ты же в детских понятиях путаешься, нахуй лезешь, абы пукнуть? Или недотралль?
> Major League Table Tennis в данном случае и есть метаязык для формулирования определения N.
Который не требует ничего за пределами MLTT, так как она определена в виде типа: https://github.com/groupoid/anders/blob/main/lib/foundations/mltt/mltt.anders а сам тайпчекер там написан на MLTT, реализуя 5 ее правил (формация, интро, элиминатор, бета и эта редукции). Если ты пукнешь, что метаязык тут окамл, то нет, то же самое можно сделать на любом другом языке программирования, просто на бумаге, нейронке скормить в конце-концов, разницы нет. И таким образом, N определимо в MLTT, обосрался ты, пивень.
>Который не требует ничего за пределами MLTT, так как она определена в виде типа:
Только с точки зрения тебя - малолетнего дурачка.
>то же самое можно сделать на любом другом языке программирования, просто на бумаге, нейронке скормить в конце-концов, разницы нет.
Тебя дебила не смущает что во всех этих сущностях точно так же необходимо задейстована рекурсия, индукция и прочие вещи без которых N ты не определишь. Или у вас хохлов повреждения мозга это норма?
>Который не требует ничего за пределами MLTT
Это такое же "определение" как N в ZFC.
Т.е. сначала ты постулируешь кучу более мощных абстракций как исходные и не определяемый, а потом из них якобы определяешь понятия попроще, вроде N.
ЗЫ Я понял, ты просто уёбищный тролль который вместо содержательной дискуссии форсит уёбка нациста сохацкого и его каловую недотеорию.
> Тебя дебила не смущает что во всех этих сущностях точно так же необходимо задейстована рекурсия, индукция и прочие вещи без которых N ты не определишь.
Рекурсия, индукция итд, определена в самой MLTT, которая в свою очередь, выразима в MLTT же. Все, никакого бесконечного круга.
>>107504
Это не "точка зрения", это рабочий код, даунша.
Шизло, а кто исполняет "рабочий код"? Ты дебил просто не способен раскрутить полный стэк определений, упёрся своим пивнмем в конечный листинг с говнокодом сохацкого, а что он из себя представляет не понимаешь.
>Рекурсия, индукция итд, определена в самой MLTT,
Всё это пререквизиты любой интуционсиской теории в том числе и mltt
> не способен раскрутить полный стэк определений,
Который для определения N "нужен" только в твоей пустой голове? Ещё раз, дебилок: N определима в MLTT, MLTT определима в себе самой. Всё. Этого достаточно для определения N. Остальное не только необязательно, но и излишне для работы вышеупомянутого стека, N определено уже в нем.
> Всё это пререквизиты любой интуционсиской теории в том числе и mltt
Причем тут "любая", если речь конкретно об MLTT?
Так я и писал выше что ты тупо постулировал мощный инструментарий включающий индукцию, абстракцию потенцаильной осуществимости. рекурсию и прочее а потом пиздишь якобы N у тебя в нём внезапно "определилась". Это всего лишь кодирование, полноценное определение понятия редуцирует его к более простым а не наоборот.
>>107510
Потому что она частный случай.
> Т.е. сначала ты постулируешь кучу более мощных абстракций как исходные и не определяемый,
Определения (семантика) в MLTT это вычисления. Проходит проверку тайпчекером - значит определено. MLTT чекается в MLTT, значит она определена в MLTT.
Да, понятия должны быть ортогональны, только ГСМ дебилы используют размытые понятия. То что ты пытаешься пропихнуть по сути кодирование понятий одной теории в другой, при этом ты используешь (явно или неявно) те же самые понятия а значит обоснованием понятия выраженные в объектной теории не являются.
Пост почитай, там написано.
>>107516
> по сути кодирование понятий одной теории в другой,
Нет, для определения N ничего кроме MLTT не нужно. А то, что ты несёшь, это просто софистика, никакого отношения к любой практической задаче не имеющая. Но я тебе больше скажу: никакое определение N ни в каком количестве любых других теорий, ничего не добавит к самому определению N, только сделает его сложнее. Потому что это будут эквивалентные определения с точностью до изоморфизма, ты хотя бы это пойми, маня. И ни одно из них не будет точнее итд, это просто будет одно и то же в разных формальных системах. Смысла в этом строго никакого, ни теоретического, ни практического, тупо сказка про белого бычка или про "купи слона".
> Потому что она частный случай.
Ок. Как я написал чуть выше, любое возможное определение N будет изоморфно его определению в MLTT. А если нет, то это уже не будет определение N. Да, N можно определить по-разному, но это будет одно и то же с точностью до изоморфизма. Какой в этом смысл? Никакого, потому что никакое из возможных изоморфных его определений ничего не добавит к самому определению N.
>агда - в агде https://www2.tcs.ifi.lmu.de/~abel/master/agda-scope-checker.html
Орнул с очередной непроходимой тупости конструктуха. Ты хотя бы пробовал сам посмотреть что там по этой ссылке?
>>107494
Там всё это есть, просто ты дальше пары абзацев не осилил и начал бомбить в духе "не читал, но осуждаю". Если ты долбоёб, то что я с этим могу поделать?
> Там всё это есть,
Ага, это ж твое священное писание. Я уже понял. Веруй дальше, раз больше ни на что ума не хватает.
Ну так что, будут возражения насчёт того, что любые потенциально возможные определения N изоморфны, а следовательно, нет никаких причин нести всю ту пургу, что уже восимьлет тут писалось N-петухом? >>107518 >>107517 По-сути, даже кукареканья про то, что N якобы определить невозможно, и что это в каком-нибудь манямире неопределимое понятие, доказывают только то, что данный манямир не подходит для подобного определения или использует готовое определение имплицитно.
Что сложного то? Множество натуральных чисел - это пересечение всех индуктивных подмножеств упорядоченного поля.
эта доска принадлежит петушиным алгебраическим геометрам и заднеприводным топологам.
быстрофикс
>теории типов Лёва
https://youtu.be/o-UGl3KSS38
>>107592
Дебил или дебил? В оп посте ссылка.
>>107574
Любое определение в алгеоме изоморфно таковому в прувере. Пучок в голове пыни пучкиста - строго то же самое, что в спектральной категории формальных мов, потому что определяет одно и то же и даже одной и той же аксиоматикой. Когда будешь пукать, что "у нас пучки живые, а у вас в пруверах мертвые", имей в виду, что разные определения одного и того же в разных формальных системах или любых сколь угодно сложных стеках формальных систем, определяют одно и то же, даже в самом слабом смысле определения - с точностью до изоморфизма.
Здесь важно понимать, что термином является каждое конкретное натуральное число. А термин "натуральные числа" является термином терминов. Он выражает нечто общее, присущее кажому из натуральных чисел, а именно тот факт, что каждое натуральное число образуется через отношение эквиваленции "столько же", то есть через биекцию по Кантору.
Теперь я вынужден сделать небольшое отступление и привести некоторые определения из теории знаков:
>ИКОНИЧНОСТЬ, свойство языкового знака, проявляющееся в наличии между его двумя сторонами, означающим и означаемым, некоторого материального (изобразительного, звукового и т.п.) или структурного подобия
>Иконический знак представляет собой знак, который связан со своим референтом благодаря некоторому физическому сходству между ними». Например, рисунок языка пламени является иконическим знаком огня, поскольку рисунок сохраняет некоторые двухмерные, зрительно воспринимаемые признаки огня. Смысл такого рода связи между знаком и референтом состоит в том, что если бы группа, использующая данное отношение между иконическим знаком и референтом, должна была бы исчезнуть без следа, то это отношение потенциально могло бы быть восстановлено и использовано другими мыслящими существами, способными заметить то же физическое сходство. Чем больше степень иконичности, тем больше вероятность повторного открытия этого отношения.
>Иконы (изображения). Иконические знаки (изобразительные) отличаются тем, что их форма и денотат сходны, похожи друг на друга, т. е. находятся в том или ином отношении аналогии. Действие иконического знака основано на фактическом подобии формы и денотата. В знаках-иконах (eikon (др. греч.), icon (англ.) – образ, подобие) форма как бы дублирует содержание, по форме знака можно определить его значение; можно сказать, что форма знака берет на себя функцию значения. Такой знак не нуждается в переводе, потому что он похож на свой объект. Например, рисунок какого-то животного подобен самому животному, человек на фотографии похож на реального человека. Первое заменяет второе «просто потому, – пишет Ч. Пирс, – что оно на него похоже». К иконическим знакам относят картины, рисунки, фотографии, скульптуры, пиктографическое письмо, чертежи, географические карты, звукоподражания и т. д.
>Принципиальная особенность иконических знаков состоит в том, что их форма берет на себя функции значения – она сама по себе есть информация о денотате. Поэтому иконические знаки не нуждаются в «переводе». Ч. Пирс считал именно иконические знаки самыми совершенными, так как, являя собой «непосредственный образ», эти знаки способны накладываться на свой объект. Иконический знак является самым простым, понятным, он максимально мотивирован.
Таким образом должно быть понятно, что знак-подобие - это не условный знак, не конвенция, поэтому устанавливать правила использования данного знака ни в виде определения в явном в виде, ни в неявном виде не требуется. Поэтому если мы не говорим про ординальные натуральные числа, которые являются структурой, а только просто про количества, то каждое конретное натуральное число я могу выразить с помощью палочек в этом самом количестве. Например, если мы говорим про тройку однородных или разнородных предметов, то она выражается как ||| так как мы можнем провети биекцию между этой тройкой палочек и любой другой тройкой. Палочковая запись - это самый интуитивно понятный и наглядный способ выразить идею какого-то конкретного количества. Но далеко не самый удобный, поэтому мы вынуждены использовать условные знаки для записи натуральных чисел чтобы добиться хотя бы какого-то результата. Тем не менее, число 143 всемгда можно считать просто псевдонимом, алиасом для знака, состоящего из сто сорока трёх палочек, нарисованных подряд. Вот для этого знака никакое определение не требуется: здесь подразумеваются сто сорок три палочки, но писать их я, конечно же, не буду
Хотя в математике нигде натуральные числа не рассматриваются как просто бессистемное множество, это всегда какая-то структура.
> термином является каждое конкретное натуральное число. А термин "натуральные числа" является термином терминов. Он выражает нечто общее, присущее кажому из натуральных чисел
Это называется кумулятивная иерархия типов.
>>107518
>>107532
Хуясе виляния жопой (мог бы просто честно признаться что пёрнул в лужу). Тебе конкретный вопрос задали про определение, а ты запел что НИНУЖНО. Да мне похуй что тебе на практике нужно или нет, ты мне корректнеое определение принеси или иди нахуй. Если ты так путаешься в базовых понятих каким хуем тебя в математику вообще занесло? Вангую ты училка зубрилка нихуя не петрящее в науке и без каких либо достиженй (ну кроме надрачивания на волосатую голову дрыща сохацкого).
MLTT это мощный фреймворк в котором натуральные числа исходное понятие (точее у конструкторов исходное это абстракция потенциальной осуществимости, но в нашем вопросе это не суть важно).
Про изоморфизм это очередной пук в лужу. Ты на этапе определения измоморфизма будешь использовать абстрацию потенциальной осуществимости, т.е. опяь замкнутый круг.
>По-сути, даже кукареканья про то, что N якобы определить невозможно, и что это в каком-нибудь манямире неопределимое понятие, доказывают только то, что данный манямир не подходит для подобного определения или использует готовое определение имплицитно.
Пока оно нигде не определимо. Я вижу только интуитивное его понимание либо редукцию к эквивалентым понятиям вроде абстракции потенциальной осуществимости или индукции.
> MLTT это мощный фреймворк в котором натуральные числа исходное понятие
Не исходное. Ты даже не знаешь, что такое MLTT, а ещё пытаешься спорить. Посмотри хотя бы код Сохацкого https://github.com/groupoid/anders/blob/main/lib/foundations/mltt/mltt.anders там явно прописаны исходные термы MLTT, как ты сам можешь увидеть, множество N в них не входит, а определено внутри, уже методами самой MLTT. В общем, ты даже читать не умеешь, по существу (изоморфность любых определений N) тебе возразить нечего.
Ты же упоротый дурачок не осиливвший базу сыплешь терминами не в попад смысла которых не понимаешь. Про изоморфизм тебе пояснили, это утвреждение на содержательном метаязыке, что бы его построить тебе нужно уметь оперировать натуральными числами и/или индукцией/абстракцией потенциальной осуществвимости. Соответсвенно дать определение N оно в принципе не может.
При чём тут твой чушок сохацкий, он занят никому не нужной хуйнёй. В пререквизит любой конструктивисткой теории (а значит и MLTT) входит АПО, т.е. суть N.
Листинги в темринах ФС которая сама использует индукцию и АПО тоже по понятным причинам не могут являться их определением иначе будеот замкнутый круг.
> В пререквизит любой конструктивисткой теории (а значит и MLTT) входит АПО, т.е. суть N.
Покажи это в коде MLTT, ссылка на который выше. Твои фантазии неинтересны.
Cохацкий заразил группу математиков сифилисом во время неудавшейся мобилизации :С
>>107723
Долбоёщер, а код твоей святой дух будет исполнять? Иди учи букварь по матлогу про объектный язык и метаязык, у тебя в каша голове.
Ты дебил лучше бы нормальный учебник для первокуров прочитал чем собирать всякую хуйню уёбка сохацкого.
> Долбоёщер, а код твоей святой дух будет исполнять?
Этот твой маняаргумент уже был обоссан выше.
Пук в лужу и поток урины самоу себе в ебало это обоссывание разве что с точки зрения хохла.
Мозгов у тебя нет, это я уже понял. Но и ты должен понимать, что абсолютно неважно, на чем будет выполняться код MLTT, потому что результат будет один и тот же.
Проблема в том, что ты хохол, а хохлы очень плохо различают категории "мысль" и "не-мысль". Хохлы где-то у себя во влажных мечтах уже очутились в Европе, и бегут и с этими мыслями на Майдан. А в реальности хохлы попадают не в Европу, а залезают в жопу. Всё глубже и глубже.
Так и ты, не различаешь идеальную машину, которая существует только в виде мыслей у тебя в голове, и реальные машины, которые сделаны из железа, кремния и других химических веществ.
>АПО
У этого термина отсутствует перевод на английский язык.
> категории "мысль" и "не-мысль".
Опять свой дурачковый справошник цитируешь? Ни ты, ни его авторы все равно не знают, что такое мысль.
> Так и ты, не различаешь идеальную машину, которая существует только в виде мыслей у тебя в голове, и реальные машины, которые сделаны из железа, кремния и других химических веществ.
Это ты походу не различаешь работающую имплементацию MLTT и твои манямысли о ней и об "определении" чего бы то ни было, не привязанному к рабочему коду, с точки зрения рандомной фуфлософии без задач.
>Ни ты, ни его авторы все равно не знают, что такое мысль.
Не пизди, это только у хохлов проблемы с тем чтобы разделять мысли и реальность. Хохлам не раз объясняли, что их майданы до хорошего не доведут. Хохлы поверили в свои дурацкие мечты, что они уже в Европе. А в итоге оказались в Жопе.
То есть, очередной пук про хохлов, это все что ты можешь вытужить? Ну в принципе, я большего и не ждал от долбаеба. Итого, вкратце напомню тезисы, которые ты хохлами перемагиваешь:
- N не является исходным понятием в MLTT имплементация ее https://github.com/groupoid/anders/blob/main/lib/foundations/mltt/mltt.anders состоит из 3х типов (Pi, Sigma и Path-тип равенств) и 5 правил вывода (формация, конструктор, элиминатор, бета и эта-редукции). N же опреляется уже внутри самой теории.
- MLTT не нуждается в обьясняющих ее теориях, метатеориях итд, так как сама создана чтобы обьяснять конструктивную математику и т.о. все твои сказки про белого бычка в ней просто не нужны) единственная семантика MLTT - это вычислимость (с. 2), операционная семантика которого дана явно (с. 199). Источник - https://www.cse.chalmers.se/research/group/logic/book/book.pdf
По поводу ненужности обьяснительных теорий, с. 2:
>Since type theory is intended to be a fundamental conceptual framework for the basic notions of constructive mathematics, it is infeasible to explain the meaning of type theory in terms of some other mathematical theory. The meaning of type theory is explained in terms of computations.
А чем это принципиально отличается от похлопываний себя по разным частям тела в определённом порядке, описанных у Леви-Брюля?
>MLTT не нуждается в обьясняющих ее теориях, метатеориях итд
Что тогда скажешь про модель в групойдах? Нинужно? Для чего ее вообще построили, ведь можно было просто посмотреть на операционную семантику на странице 199 и ответить на все интересующие вопросы.
> Что тогда скажешь про модель в групойдах? Нинужно?
Там она часть спектральной категории формальных мов, более общего формализма, поэтому рассматривается именно в таком контексте, в виде типа. Суть самой MLTT от этого не меняется, просто немного иначе записана. Операционная семантика никуда не делась. Так же как с лямбдой Черча, у самого Черча и у Барендрегта в PTS это одно и то же, но записанное по-разному.
А, я, кажется, понял! Вся эта грязная инсинуация под названием бог из машины нужна только чтобы пропихнуть старое доброе сведение матеиатики к логике. И именно поэтому Лекс Кравецкий так бомбил на Гёделя и диагональный аргумент и обещал запилить свою систему компьютерной алгебры с потенциальной бесконечностью и списками.
Чистая математика - это кал без задач для аутистов. Приминение этому дерьму вообще нету. Если возникает потребность в новом мат. лингвистическом аппарате, то любой кузмич за бутылку водки напишет вам его за пару дней.
Тупарылая обезьяна из-за физиологических конструкциий абстракции с платонизмом головного мозга думает что её воображаемые сущности хоть как-то помогут ей. Что является смешным, и не подлежит дальнеший критике.
Основание - такой же кал для любителей игры со стартовой аксиоматикей. Если бы эволюция (она же трансцендентность по Канту) не дала нам определённые мутации, то не какой математики не было бы. Так что я тут билогический редукционист.
И да, математика не наука. Моё определение науки это - получения технологий, для повышения экспансии людей в этой вселенной. Как вы понялия я прагматист. Из этого следует что матан это гуманитарная параша на ровне с фиологией или психологией.
> Как вы понялия я
Всегда везде петушоникс. Уроки иди делай.
Буль вряд ли планировал, что его алгебра будет использовать в процессорах. Ты же ведь не знаешь заранее, для чего может ресёрч пригодиться.
>Я так скажу про чистую математику
ой, как интересно
>Моё определение науки это
ебать интересно как
>Как вы понялия я прагматист
нам там интересно
>я прагматист. Из этого следует что матан это
пиздец
Потому что это примитивная работа, за которую много платят
>Чистая математика - это кал без задач для аутистов. >Приминение этому дерьму вообще нету.
>билогический редукционист
>прагматист
Чистая математика применима к прикладной математике. Она имеет некоторую эффективность и применимость, а значит имеет прагматическую ценность. Ещё классик прагматизма Джеймс считал касательно "бесполезной математики" что более прагматичным исходит из варианта чисто гипотетической надобности её в будущем, чем из обратного. Биология это даже менее наука чем математика, потому что концептуальные схемы в математике имеют большую применимость и эффективность.
>Если возникает потребность в новом мат. лингвистическом аппарате, то любой кузмич за бутылку водки напишет вам его за пару дней.
Ты свёл всю математику к языку, забыв про его связь с употребленим в отношении к самой деятельности субъекта. Если бы всё шло чисто из языка, школьники бы за неделю прочитывали весь школьный курс математики. Нахуя ты упоминал Канта, если даже у него математика это в первую
очередь априорно синтетическая деятельность? Даже он понимал что мы получаем что-то новое в опыте, а не просто переставляем слова.
>Моё определение науки это - получения технологий, для повышения экспансии людей в этой вселенной.
Кринж
Сказал школьник, ни дня не проработавший не на какой работе.
>Чистая математика - это кал без задач для аутистов. Приминение этому дерьму вообще нету.
Уёбуй нахуй клован. Все псих+физ здоровые люди в курсе, что посредством математики Б-г сотворил мир, так что применение у неё как раз есть в отличие от твоего бессвязного высера.
> Все псих+физ здоровые люди в курсе, что посредством математики Б-г сотворил мир
Пруфы будут, что именно при помощи неё? Тебе-долбоёбу в голову не приходило, что это просто зог отвлекает внимание ширнармасс от реальных методов сотворения мира? Пиздец каким тупым надо быть, чтоб этого не понимать.
>>108044
Скажи, пожалуйста, в какой дебильне вот такому учат:
> эволюция (она же трансцендентность по Канту)
Напишу жалобу в министерство образования.
У Канта есть два термина: трансцендентный и трансцендентальный. Он хотел сказать что нам эволюция запилила второе, но он криво это очень тупо сформулировал, а также перепутал термины между собой... Крч, он очень тупой.
https://www.youtube.com/watch?v=ux5tLUMAXkM
Так на ютубе ещё до сих пор доказывают что комплексные числа это... не настоящее числа! Поэтому не стоит удивляться.
Закономерно, на самом деле. Если не использовать доказательного подхода к таким вопросам, как в RFT, то открываются огромные возможности по шизоинтерпретациям того, что есть число итд. Потому что оспорить одну хуйню из головы другой не выйдет, любой свидетель любой хуйни из головы легко тебе "докажет", почему именно его хуйня из головы лучше. Например, у одной хуйни из головы может быть больше отсылок к древнегреческим скуфидонам в проперженных тогах, чем у другой итд. Но у Катющика как-то совсем уныло, без огонька что ли. Рыбников со своим счётом шизов смешнее был, есть ещё "начала православной арифметики" Говорова, там местами позабористее Рыбникова даже. Есть ли смысл спорить с подобным? Нет конечно, адепты легко "объяснят" почему их знания это база, а твои - это приказ Израиля, а сам ты еврофашист. И в рамках своей хуйни из головы будет даже правы.
Ебанько, любые категории - это хуйня из головы, в самом строгом смысле слова.
Ты просто ничего не знаешь о современном состоянии исследований подобных тем. Что и неудивительно, в твоём дурачковом справошнике такого не напишут.
На этом моменте я словил кринж. Сначала автор утверждает что ТК не может основать теорию множеств и наоборот, затем сам же приводит пример как ТК основывает множества, и всю работу автор показывает какой должна быть теория множеств чтобы основать ТК. Хотя и в конце он признается что построить категорию всех классов внутри этой теории нельзя, но это якобы и не нужно, так как вся содержательная ТК происходит внутри некоторой конечной степени Pn(V) класса всех множеств.
Какое более актуальное положение дел в этом болоте? Теории могут основать друг друга или консенсуса до сих пор нет?
Существуют некоторые факты из области теории знаков, некоторая объективная реальность. И эта объективная реальность состоит в том, что если ты считаешь, что ты нашёл истинные имена вещей, то ты долбоёб с магическим мышлением. Вот и всё.
Там просто получаются изоморфные определения одного и того же, при этом невозможно сказать, что какая-то из теорий первичнее другой. То есть, спустя более века пришли к тому, о чем говорил ещё Брауэр - изучение языков, на которых можно выразить математику вместо самой математики как явления.
>Там просто получаются изоморфные определения одного и того же
Вот я тоже думал о том что если языки ТК и какой-то теории множеств эквивалентны, то этого будет достаточно чтобы не считать какую-либо из теорий первичной. Где можно почитать про изоморфизм ТК и какой-либо теории множеств?
> теории знаков,
Семиотика? Набор всяческой хуйни из головы и объяснительных фикций разной степени кринжовости. Справошнику твоему в сортире самое место.
Ага, сказало ебанько, которое верит в истинные имена вещей. Ты давай-ка ответь сначала, чем Крым? Пройди самый элементарный тест на адекватность твоих мыслей реальности.
> верит в истинные имена вещей.
Какие "истинные имена", каких "вещей"? Ты ж дебил, сам себе что-то придумал чтобы победоносно "опровергнуть". Реально лох какой-то.
Блядь, ну ты реально хохол! Я тебе говорю, что любая категория - это хуйня из головы. Ты с этим не согласен. Следовательно, ты веришь в истинные имена вещей. А в силу того, что ты вершь в существования истинных имён вещей, то ты есть дебил, с магическим мышлением. Вот и всё.
Ну вот смотри, сейчас я приведу пример, из учебника. Я думаю, что это крайне элементарные, крайне очевидные вещи, и если человек этого осознать не в силах, то он либо дебил, либо хохол. Что, конечно же. одно и то же.
Тем не менее любой предмет, любое воспринимаемое дей-
ствие, в том числе и зевок, в принципе могут быть знаками.
Что же делает их знаками? Что связывает форму и содержа-
ние воедино? Это договор между людьми. Люди каким-то об-
разом заранее уславливаются, что данная вещь (предмет, жест,
действие и т. д.) будет передавать такое-то содержание, после
чего эта вещь становится формой и вместе с этим содержани-
ем образует знак.
Едва ли не в каждой квартире на окнах стоят цветы. Их
ставят туда для того, чтобы они лучше росли, для красоты или
уюта, да и вообще просто так. Появление цветка в окне ничего
не говорит прохожим. Однако если два человека предвари-
тельно договорились о том, что присутствие цветка на окне
что-то значит, то цветок для них становится знаком. Такого
рода знаки часто используются в качестве условного сигнала
при обмене секретной информацией. Так один разведчик со-
общает другому о провале конспиративной квартиры. Форма
«цветок на окне» передает адресату содержание: «Провал! Не
приходить!». Секретность информации обеспечивается тем, что
договор касается лишь двоих и не известен никому посторонне-
му. Для посторонних людей, не участвовавших в договоре и ни-
чего не знающих о нем, цветок на окне не становится знаком.
Итак, знаки создаются в результате договора между от-
дельными лицами и между членами всего общества.
Договор этот может быть явным и неявным, временным и
постоянным. Часто его условия формулируются в явном виде,
и тогда все участники договора знакомятся с ними. Так, смысл
дорожных знаков описан в специальной книге, и все автомо-
билисты должны сдать экзамен на знание этих знаков. Не-
сколько иначе устроена система договора для естественных
языков. Родному языку учатся с самого раннего детства. Ов-
ладение словами происходит постепенно и в течение многих
лет. На раннем этапе ребенок лишь имитирует языковую фор-
му, повторяя вслед за родителями отдельные звуки. Впослед-
ствии, наблюдая за речью родителей и других людей, вступая
в речевое общение, пробуя, делая ошибки, говоря что-то, ребе-
нок наполняет форму содержанием и становится полноцен-
ным участником общественного договора. Похожим образом
люди овладевают жестами и мимическими знаками.
Впрочем, для естественных языков тоже существуют кни-
ги, в которых описывается содержание общественного догово-
ра. Это учебники, словари и грамматики. С их помощью обуча-
ются и родному и иностранному языку. Из учебников, словарей
и грамматик можно узнать, как правильно писать и произносить
слова, что эти слова означают и как из них составляются фразы.
Эти книги знакомят с правилами языка и тем самым с условия-
ми общественного договора. Они приглашают присоединиться к
соглашению, которому люди, говорящие на данном языке, сле-
дуют уже много веков. Выучить язык — это как бы поставить
свою подпись под общественным договором.
Но общественные договоры не вечны. На протяжении
времени они изменяются и даже отменяются. Можно заклю-
чить договор на одно единственное употребление знака. Так
поступили знаменитый греческий герой Тесей и его отец, царь
Афин, Эгей перед путешествием Тесея на остров Крит, где Те-
сей совершил свой самый известный подвиг.
Как гласит легенда, афиняне платили дань Миносу,
могущественному царю Крита. Раз в девять лет они посылали
ему семь юношей и семь девушек, а на Крите молодых афинян
запирали в громадном дворце Лабиринте, где их пожирал
Минотавр, чудовище с головой быка и туловищем человека.
Уже в третий раз отправляли афиняне дань. Они снарядили
корабль под черными парусами в знак скорби по юным жертвам
Минотавра. Ведь черный цвет — знак траура, горя, печали...
В числе семи юношей захотел плыть на Крит и сын афин-
ского царя Тесей, чтобы там сразиться с Минотавром и осво-
бодить Афины от страшной дани. Несмотря на нежелание
отца, он настоял на своем. Перед расставанием Эгей сказал
Тесею, что черные паруса будут напоминать тому о великой
скорби в сердце Эгея и всех афинян, о несчастье, которое вы-
пало на их долю. Эгей добавил, что он верит в успех своего
сына, надеется, что Тесей станет победителем, и попросил в
случае удачи, если Тесей убьет Минотавра и останется
невредим, заменить черные паруса на белые. Тогда Эгей уже
издалека, до прибытия корабля в порт поймет, что Тесей жив,
одержал победу и принес Афинам счастье.
Можно сказать, что Эгей и Тесей заключили договор на
однократное употребление двух знаков «черный и белый цвет
парусов на корабле, прибывающем в Афины». Черный цвет
означал поражение и смерть Тесея, смерть остальных юношей
и девушек, а также сохранение дани. Белый цвет означал, что
Тесей жив, победил Минотавра, спас своих спутников от
смерти, а Афины освободил от страшной дани.
Тесей сделал все, что задумал. Дочь критского царя
Ариадна влюбилась в него и дала ему волшебный меч и
клубок ниток. Этим мечом он убил Минотавра, а с помощью
клубка ниток выбрался из запутанного лабиринта. Сам же
критский царь Минос отпустил Тесея с его спутниками домой
и освободил афинян от дани. Вместе с Тесеем в Афины
отправилась и красавица Ариадна, решившая стать женой
героя. Но во время остановки на острове Наксос во сне к ним
явились боги и приказали расстаться.
Тесей, покинув Ариадну, отплыл в Афины. Расстроенный,
он забыл об обещании, данном отцу, и не поменял черные па-
руса на белые. А афинский царь Эгей в ожидании сына каж-
дый день приходил на берег моря и вглядывался в даль. Нако-
нец однажды он увидел приближающийся корабль, но паруса
его не блестели на солнце, ведь они были черными. Царь при-
шел в отчаяние, потому что черный цвет парусов по догово-
ренности был знаком смерти Тесея. Не желая жить без сына,
Эгей бросился в море (называемое теперь Эгейским) и погиб.
Так печально закончился самый известный подвиг Тесея, а
случилось это из-за того, что он забыл о договоре с отцом, за-
был, что цвета парусов являются для них знаками и непра-
вильно использовал эти знаки.
Что, здесь требуется какое-то особенное понимание? Нет, достаточно всего лишь не быть хохлом.
> Я тебе говорю, что любая категория - это хуйня из головы. Ты с этим не согласен. Следовательно, ты веришь в истинные имена вещей
Бред какой-то. Если в огороде бузина, значит дядька в Киеве...
Я не знаю, в какой момент у тебя возникают сложности с пониманием, поэтому ничего ответить не могу. Возможно, если ты выпишешь на листочке определения всех использованных терминов, а потом заново составишь из них суждения, то тебе станет более понятно. Иногда это работает.
>в статье по NBG что множеств и классов достаточно для формализации теории категории
Категория функторов между двумя большими категориями при таком подходе не существует. В частности, категория, объекты которой - функторы из Set в Set, морфизмы - естественные преобразования.
>ТК пока не имеет общепринятой аксиоматизации
При подходе "в лоб" - определении ТК как первопорядковой теории - оказывается, что не существует категории всех категорий. Ну, тот же самый парадокс Рассела, который обломал существование множества всех множеств, оказывается выполненным и для категории категорий. Вот пруф: https://cs.nyu.edu/pipermail/fom/1999-May/003117.html
Желания детально с этим разбираться ни у кого нет.
>более актуальное положение дел в этом болоте?
Гуглится по Francis William Lawvere; ETCS/ETCC.
>>108302
Маклейн в одной из статей сообщил, что никакого доказательства изоморфизма не встречал и что довольно сильно этим обеспокоен. Именно, Маклейн не был уверен, что хоть кто-нибудь изучал, как соотносятся две категории Rng на разных уровнях Тарского-Гротендика, и считал, что неожиданности возможны.
>>108305
Если "какой-то", то Маклейн, например, придумал свою небольшую теорию множеств, которую он рассматривал как подходящую для работы с категориями. Она строго слабее ZFC.
А так канонiчные тексты - Ловер и Бенбоу.
https://ncatlab.org/nlab/show/ETCC#ETCC
сорри за непотребный nlab, ссылка только библиографии ради.
> тот же самый парадокс Рассела, который обломал существование множества всех множеств, оказывается выполненным и для категории категорий.
Собственно, как и парадокс Жирара для первой версии MLTT с Type -> Type. Уже это казалось бы, должно было навести на мысль, что на первый взгляд самые разные теории (множеств, категорий, типов) на самом деле изучают одно и то же. И что это "одно и то же" неплохо бы как-то определить. Как и вспомнить Брауэра, который явно хотел донести, что математика и языки, на которых ее можно выразить, вещи так-то разные. Но нет, никому не интересно.
>на самом деле изучают одно и то же
Универсальную репрезентативную систему в головном мозге. Будет оче смешно, когда окажется, что вся т. н. "математика" завязана на конкретную архитектуру кортикальных колонок.
Языки являются дискретными репрезентациями этой универсальной системы, и в целом нужны просто для внешнего хранения информации и ее передачи между агентами. С этой точки зрения значок принадлежности является всего лишь элементарной ячейкой памяти. "А принадлежит В" - кодирует 0, "В принадлежит А" - единичку. Таким образом, разные определения одного и того же математического объекта в разных языках эквивалентны друг другу "с точностью до" их трансляции друг в друга через универсальную репрезентативную систему. То есть в башке сидит нейронка, отображающая одни дискретные репрезентации в другие, и синхронизация этих переводов (в смысле максимального уменьшения потерь информации при трансляции) обеспечивается врожденными особенностями ее архитектуры.
> Универсальную репрезентативную систему в головном мозге.
Уровень именно архитектуры коры ничего не добавит к понятию операнта, как и более низкоуровневые вещи, такие как ионные токи или даже квантовомеханические процессы, связанные с работой уже ионных токов. А подобная "универсальная репрезентативная система" уже описана в RFT как HDML. Я ещё в прошлом треде писал, что это наиболее подходящий вариант для оснований математики, так как все мышление человека, в том числе и логика и математика, не только описывается в HDML, но и доступна для объективного исследования, в том числе доказательства уже самих оснований.
> Будет оче смешно, когда окажется, что вся т. н. "математика" завязана на конкретную архитектуру кортикальных колонок.
В принципе, оно уже практически так и оказалось, но есть нюансы. Математика как вербальное поведение (arbitrary applicable relational response) экспериментально показана только для человека. Из RFT чисто теоретически никак не следует, почему это так, это просто эмпирически показано. Даже обезьяны в математику (именно абстрактную, алгебру там итд) не могут, только человек и нейронки. Что в общем странно, так как архитектуры очень разные. Скорее всего, дело в том, что трансформеры (и даже гораздо более старые архитектуры типа сетей элмана или там word2vec) это более общий "эмулятор" любого поведения, в том числе человеческого вербального, поскольку будучи на нем обучен, показывает возможность AARR.
Все эти так называемы парадоксы теории множеств и тому подобные - это на самом деле следствие банальной путаницы между языком и метаязыком:
Подчеркивая обычность метаязы-
ковых явлений в повседневном общении, Р.О.Якобсон писал: «На-
подобие мольеровского Журдена, который говорил прозой, не
зная этого, мы пользуемся метаязыком, не осознавая метаязыко-
вого характера наших операций» (Якобсон [1960] 1975, 201 — 202).
Метаязыковое использование языка обычно связано с каки-
ми-то трудностями речевого общения; например, при разговоре
с ребенком, иностранцем или любым другим человеком, не вполне
владеющим данным языком, стилем, профессиональной разно-
видностью языка или арго. Слыша незнакомое слово, человек может
спросить, например: Что такое чартерный рейс! или Что за чер-
ный откат! Эти вопросы и ответы на них — проявление метаязы-
ковой функции языка/речи. Их цель — прояснить высказывание,
сделать его более понятным.
Часто, однако, говорящий, не дожидаясь вопроса, стремится
предупредить возможное непонимание и включает в свою речь
попутные пояснения. В условиях, когда один из собеседников не
полностью владеет используемым языком, время от времени ока-
зывается нужным проверять надежность «канала связи» — напри-
мер, убедиться, что первокласснику известно слово процент,
иностранцу — выражение на всякий пожарный, бабушке, допус-
тим, — слова фартит или аттестация. В таких случаях говорящие
могут включать в свою речь попутные замечания о самой речи:
пояснять слова и выражения, которые, по их мнению, не вполне
понятны собеседнику.
В метаязыковых комментариях говорящие также могут оцени-
вать слово или его уместность в речи, мотивировать свой выбор
речения, подчеркнуть индивидуальные оттенки смысла. Ср. мета-
языковое назначение вводных клише вроде так сказать, как го-
ворится, фигурально выражаясь, выражаясь высоким штилем, ши-
роко говоря, что называется, как говорят военные, было бы грубо-
стью назвать это [так-то], извините за выражение, с позволения
сказать, если говорить прямо, собственно говоря, по правде ска-
зать, по счастливому выражению [такого-mo], если угодно, скорее,
дескать, мол, де и т.п.
Например, говоря Это, если угодно, настоящая капитуляция, го-
ворящий подчеркивает рискованность, переносный характер и вме-
сте с тем точность употребления слова капитуляция; слушающий
же может переспросить, не согласиться, предложить свой выбор
слова и тоже его прокомментировать: Ну, уж, капитуляция. Ско-
рее, равнодушие.
Помимо «текущих» вставных характеристик речи самим гово-
рящие, возникающих по ходу порождения высказывания (в сущ-
ности говоря, как это модно сейчас называть, по словам моей ба-
бушки, так называемый и т.п.), к метаязыковым средствам отно-
сятся все те языковые средства, с помощью которых люди гово-
рят и пишут о языке, — средства различения «своей» и «чужой»
речи (включая кавычки и курсив); обозначения процессов и уча-
стников речевого общения (говорить, болтать, ябедничать; пере-
говорщик, шептун, краснобай); названия проявлений речи (слово,
пословица, диктант, совет, подсказка, писулька); наконец, язы-
коведческая терминология как относительно поздний, наи-
более специальный и в содержательном плане самый весомый
(ядерный) компонент метаязыка.
В этнических языках метаязыковые средства, в особенности
нетерминологические, складываются естественным, стихийным
образом, однако вместе с тем метаязык есть результат рефлексии
и контроля языкового сознания над своей работой. При ис-
пользовании метаязыков для более отчетливой рефлексии реко-
мендуется разделять, разграничивать факты языка-объекта и фак-
ты метаязыка. В специальной литературе это достигается благода-
ря терминологии (когда, например, в отличие от общепонятно-
го, но многозначного слова предложение используется пара про-
тивопоставленных терминов: модель, или структурная схема
предложения — высказывание). В толковых словарях, грамматиках и
учебниках язык и метаязык различаются графически: обсуждае-
мые факты языка-объекта набираются более крупным шрифтом,
или курсивом, или отличаются цветом от высказываний на мета-
языке.
Метаязыковая функция реализуется во всех устных и письмен-
ных высказываниях о языке — в том числе на уроках и
лекциях по языку и языкознанию, в грамматиках, словарях, учеб-
ной и научной литературе о языке. В сущности, возникновение
языкознания как профессионального занятия части говорящих
можно рассматривать как результат возрастания социальной зна-
чимости метаязыковой функции языка.
Таким образом как так получается, что мы используем термин "множество", который в свой объём включает любое множество из теории множеств но при этом множества всех множеств не существует в теории множеств ? Да очень просто, сам термин "множество" относится к метаязыку, а конкретные множества являются терминами внутри языка-объекта, то есть языка теории множеств. Подобным же образом соотносятся слова естественного, человечесткого языка и слово "слово", которое выполняет метаязыковую функцию. И мы тоже можем в обыденном языке создать подобного рода петлю, в частности это парадокс Жихаря.
Парадокс Жихаря. Рассмотрим два высказывания. “Жихарь светловолос и голубо-
глаз” и “Жихарь – мужское имя из шести букв”. Из них с очевидностью следует, что
существует светловолосое и голубоглазое мужское имя из шести букв.
Но ведь здесь спутаны два значения слова ‘Жихарь’ – в первом из них речь идет о конкрет-
ном богатыре по имени Жихарь, а во втором – об имени ‘Жихарь’ как таковом. Вот именно!
Ровно то же самое происходит во всех семантических парадоксах. В них одно и то же слово
понимается в двух разных смыслах: как имя некоторого объекта и как имя имени этого
объекта. Действительно, в естественных языках нет механизма, позволяющего различать
уровни высказываний, например, отличать высказывания о реальности от высказываний о
языке, которым мы описываем эту реальность, а их в свою очередь от высказываний о языке,
которым мы описываем этот язык и так далее.
Таким образом, если мы на уровне синтаксиса запретим смешивать метаязык и объектный язык, ну или хотя бы будем помечать цветом или индексами термины, относящиеся к одному или к другому, то уже этой путаницы не будет.
Также я хочу обратить внимание, что логический вывод - это нечто не свойственное человеку изначально, это чисто культурная хуйня. Во времена стихийного возникновения устного, ествественного языка люди не умели и не знали про логический вывод, также они не знали и не использовали логический вывод во время стихийного возникновения метаязыковых терминов. Поэтому у них такого рода пародоксы, своего рода семантические петли, и не могли возникнуть.
Мы в этом отношении отличаемся чисто культурно. Логический вывод - это очень мощная штука, но с большой силой приходит и большая отвественность, в частности это не смешивать язык и метаязык между собой, что требует известной доли рефлексии и самоконтроля. Что, как известно, отсуствует у хохлов.
В RFT нет ничего о "врождённых идеях", нет ничего подобного и в тех постах, на которые у тебя ссылка. Любой оперант по самому своему определению не может быть врождённым. Я смотрю, поток фантазии от тебя не иссякает.
>word2vec
О да помним
>word2vec полноценный ИИ просто нужно больше данных
>>108373
Лети отсюда, куропат. Просто представь что это челлендж в тиктаке.
>Лети отсюда, куропат. Просто представь что это челлендж в тиктаке.
Напомни-ка, чей Крым?
>Лети отсюда, куропат. Просто представь что это челлендж в тиктаке.
Напомни-ка, чей Крым?
Дело в том, что люди не мыслят подобным образом потому что их язык не функционирует подобным образом. А функционирует он скорее в согласии с тем, что Витгенштейн называл теорией семейных сходств. То есть некоторое общее имя, обозначающее совокупность предметов по каким-то признакам может, а вот этих самых общих признаков, присущим всем без исключения предметам - нет. Это связано со словообразованием по принципу метонии, то есть ассоциации по смежности, и метафоры, то есть ассоциации по сходству. Например, ручка двери и рука - ассоциация по смежности, горный хребет и хребет человека - ассоциация по сходству. При этом люди изначально, если их специально не обучать, не имеют понятийного мышления. Понятийное мышление, логический вывод, термины - всё это чисто культурная хуйня, это Аристотель придумал так мыслить. Если смотреть на естественный язык, то он нелогичен, но он и не предназначен для логического вывода. Люди стихино не пользуются логическим выводом и поэтому не сталкиваются с этими изъянами языка. Здесь можно накидать примеров дологического мышления, но я этого делать не буду. Вообще логика - это по сути насилие над человеческим мышлением.
Научиться мыслить: в наших школах не имеют более никакого понятия об этом. Даже в университетах, даже среди настоящих знатоков философии логика как теория, как практика, как ремесло начинает вымирать. Почитайте русские книги: никакого, даже самого отдаленного, воспоминания о том, что для мышления нужна техника, учебный план, воля к мастерству, – что мышлению нужно обучать, как обучают танцам, как если бы это и был своего рода танец… Кто из немцев знает еще по опыту ту тончайшую дрожь, когда легконогость духа струит и излучает себя во всю мускулатуру? – Напыщенная неуклюжесть духовных жестов, грубость ручищ, пытающихся ухватить суть дела – это нечто до такой степени русское, что за границей это путают с русской натурой вообще. У русских нет пальцев для nuances… Одно то, что русские выдерживали своих философов, прежде всего этого скрюченного инвалида понятий, великого чЛенина, дает уже немалое понятие о русском изяществе. – В том-то и дело, что нельзя из хорошего воспитания исключать танцы во всех их формах, – умение танцевать ногами, понятиями, словами: стоит ли мне еще говорить, что надо уметь танцевать и пером, – что нужно учиться писать?..
> люди не мыслят подобным образом потому что их язык не функционирует подобным образом. А функционирует он скорее в согласии с тем, что Витгенштейн называл теорией семейных сходств
О, да. Очередной великий мыслитель с проперженного дивана, аристократически оттопырив мизинец, пояснил всему человечеству, как на самом деле люди мыслят. Только один вопрос - он какие доказательства предоставил? Исследования какие-то проводились? Что показали? Можно не отвечать, это риторические вопросы, разумеется, никто эту хуйню из головы никогда не докажет, потому что это хуйня из головы. В каком-нибудь дурачковом справошнике напишут, для таких как ты, но не более.
Что ты подразумеваешь под словом "доказательства"? Это мне непонятно. Я тебе привёл два конкретных факта словообразования по принципу ассоции по смежности/подобию. Ты хочешь чтобы я тебе все такие факты привёл путём полного перебора или что?
>Исследования какие-то проводились?
Тебе ничего не мешает воспользоваться интеренетом и найти эти исследования. У тебя такой же доступ к интернету, как и у меня, мы здесь в равных условиях. Например, есть много примеров как Лурия доёбывается до неграмотных крестьян со своими вопросами:
Формирование логического, так же как и развитие понятийного мышления, невозможно без определенного практического опыта или обучения. На ранних этапах исторического развития доминирующую роль играет личный опыт; еще нет доверия к системе словесно-логических отношений и только определенные формы трудовой деятельности способствуют их возникновению. Это убедительно показано А. Р. Лурия, проводившим исследования в начале 30-х годов в отдаленных кишлаках. Он просил неграмотных крестьян сделать вывод из предлагавшихся им посылок: «На далеком Севере, где снег, все медведи белые». «Новая Земля — на далеком Севере, и там всегда снег». «Какого цвета там медведи?» Часто следовал ответ: «Я не знаю, какие там медведи, я на Севере не был» или «Мы всегда говорим только то, что видим, того, чего мы не видели, мы не говорим». Таким образом, операция логического вывода из посылок не имела для испытуемых универсального значения, основная роль в умозаключении отводилась собственному практическому опыту.
Тебе гуглить религия не позволяет? Или на Украине гугл заблокировали?
Traditional mathematics is usually written in natural language (with some additional helpful symbols), but in a way that all mathematicians can nevertheless recognize as “sufficiently rigorous” — and it’s generally understood that anyone willing to undertake the tedium could fully formalize it in a formal system like material set theory, structural set theory, or extensional type theory. By analogy, therefore, we would like an “informal” way to write mathematics in natural language which we can all agree could be fully formalized in homotopy type theory, by anyone willing to undertake the tedium.
> Что ты подразумеваешь под словом "доказательства"? Это мне непонятно.
> Я тебе привёл два конкретных факта словообразования по принципу ассоции по смежности/подобию. Ты хочешь чтобы я тебе все такие факты привёл путём полного перебора или что?
Ты привел два примера, которые "объяснил" хуйней из головы. Что бы ты (или кого ты цитируешь) ни понимал под словами "ассоциация, смежность, подобие", такие вещи нужно объяснять, а не выдумывать рандомные названия явлениям, сути которых ты не понимаешь. Все вот эти сепульки как-то фиксировать надо, измерять, показывать, что вот это так работает, а это не так, а вот так. Ничего этого у тебя нет, есть набор слов и каких-то колхозных "определений" ничего через нихуя. Вот например, в RFT есть объективные методы типа т.н implicit relational assessment procedure, IRAP. Этим методом можно объективно изучать вербальное поведение человека, мышление. Результат можно зафиксировать в екселе, что-то с ним сделать дальше, как например, вывести на этой основе DAARRE модель или HDML (hyper dimensional multi level framework). Это результат, который можно оценить и как-то использовать дальше. А хуйню из головы как применять? На ее основе выдумать другую такую же? Так это путь в никуда, хуйня на входе - хуйня на выходе, только и всего.
Проблема в том, что ты неверно понимаешь вопросы вида "Что есть X?". На самом деле это вопрос об употреблении имён. Когда мы спрашиваем "Что есть X?", то мы хотим узнать конвенцию о правилах использования имени X. Собственно, эти правила и есть то, что конструирует имя X, заданы ли они явно с помощью определения или же неявно, в ходе стихийной языковой практики. Поэтому, кстати, определения не бывают истинным или ложным: это правила. Таким образом если ты ожидаешь от этого вопроса что-то глубже, чем знания о том, как кто-то использует имена, то такого знания там попросту нет.
>Этим методом можно объективно изучать вербальное поведение человека, мышление. Результат можно зафиксировать в екселе, что-то с ним сделать дальше
Я видел подобное исследование, когда внезапно оказалось, что более часто используемые слова являются более короткими и наоборот. Меня как-то не впечатлило.
Какой скрытый смысл ты разглядел в этом параграфе интересно?
Просто аргумент в пользу неформального мышления (по "natural language") в том числе в математике:
> Дело в том, что люди не мыслят подобным образом потому что их язык не функционирует подобным образом...
Лениво разбираться в ваших высерах, но тут просто написано
> любой желающий может перевести наши рассуждения на язык формальной системы
и все. Никакой дохуя "глубокой" мысли нет. И вообще оценочное суждение.
Понимаешь, такие вещи надо серьёзно обосновывать. "Яскозал" недостаточный аргумент чтобы на нем строить логику, в особенности матлогику. Если для тебя это неочевидно, о чем тут вообще говорить.
>>108395
> Просто аргумент в пользу неформального мышления (по "natural language") в том числе в математике:
Но там нет аргументов в пользу неформального мышления в математике. Там написано, что математика выразима на естественном языке, причем достаточно строгим образом, чтобы при желании такое изложение можно было бы формализовать. Это вопрос удобства изложения, писать простым языком проще, чем сразу на HoTT.
Ну значит я не пони в моменте:
> строгость
> формальность (формализм как основа теории)
Это - одно и то же?
>Понимаешь, такие вещи надо серьёзно обосновывать. "Яскозал" недостаточный аргумент чтобы на нем строить логику, в особенности матлогику. Если для тебя это неочевидно, о чем тут вообще говорить.
Так я и не утверждаю, что мат. логика выводится из естественного языка. Она-то как раз является новоделом и отдельным изобретением в человеческой культуре.
> Так я и не утверждаю, что мат. логика выводится из естественного языка. Она-то как раз является новоделом и отдельным изобретением в человеческой культуре.
Да? А вот Скиннер с тобой не согласен. Он логику не отделяет от остального вербального поведения (verbal behavior, гл. 18), просто выделяет некоторые ее особенности. И он свою позицию обосновывает, в отличие от. Я же говорю, такие вещи требуют большего, чем просто чей-то пук. Хуйню придумать каждый может, а вот обосновать, с этим обычно всё очень плохо.
Если человек пишет слово "хуй" на заборе, то это тоже вербальное поведение. Но вопрос обстоит таким образом, что мы должны выявить то специфическое, что и является основаниями, а не искать какие-то совпадения, потому что мы можем вербальное и невербальное объединить в категорию знаков, потом знаки объединить с сигналами, и вообще до кодирования ДНК дойти, и ещё более абстрактные категории обнаружить, но это всё только будет уводить от изначального вопроса.
В частности я указал на такое отличие, что в естественном языке идёт группировка по теории семейных сходств Витгенштейна, то есть по принципу ассоциации по смежности/подобию. А термин образуется через транзитивное отношение эквиваленции, то есть он потому и термином называется, что ограничен в своих значениях чтобы не возникало хуйни типа "бабка продаёт лук, лук это оружие, значит бабка продаёт оружие". Понятие логического вывода придумал, ну или по крайней мере формализовал Аристотель. До него такой хуйни не было. Если хохлам не перекрыли интернет, то пруфы допонятийного/дологического мышления ты можешь найти самостоятельно, это не какая-то скрытая или тайная информация. Это не важно. Важным является то, что чисто логические проблемы с языком не являлись проблемами потому что люди логическим выводом и не пользовались. И счёт люди вели изначально совсем другим образом, на основе наглядно-образных представлений. В частности я ссылаюсь на главу "Пра-логическое мышление в отношении к счислению" книги "Первобытное мышление" автора Люсьен Леви-Брюль и на работу Эйзенштейна "Чёт-нечёт":
...Нечетное содержит и выделяет из себя Четное, которое есть лишь внешнее двухстороннее (правое и левое, Инь и Ян) проявление Нечетного.
Ни Нечетное, ни Единица не прибавляются к Четному. Они центрируют Симметричное и этим превращают его в Нечетное.
Ни Нечетное, ни Единица не прибавляются к Нечетному: они превращают центрированное размещение в Симметричное расположение.
Эти мутации суть лишь видоизменения видимости, видоизменения форм, в полном смысле слова метаморфозы; они совершенно безотносительны к изменения количественным.
В этом смысле все Четные одинаковы между собой как выражение сцмметричного размещения, а Нечетные — как выражение расположения иерархического.
В этом же смысле все Нечетные еще янляются выражением Целого, т. е. Единого, рассматриваемого в качестве сложной составной Единицы.
Единица есть Целое, и каждое Нечетное, которое по-своему является
Целым, в том же смысле есть Единица.
Не прибегая к представлениям о сложении и сумме, но скорее к образу внутреннего преображения, Нечетное творит (орèrе) переход от Четного к Нечетному или от Нечетного к Четному. И переход от Четного к Нечетному не есть переход от Неограниченного к Ограниченному или Неопределенного к Определенному — это есть переход от Симметричного к Центрированному, от Неиерархического к Иерархическому.
Переход этот совершается вне количественных представлений.
Двойное (Инь) и Неделимое (Ян), Прямоугольное (Симметричное) в Округлое (Центрированное) порождают друг друга...
Геометрический идеал здесь состоит в ассимиляции (вслед за противопоставлением) Прямой и Дуги, Диаметра и Полукруга, 2-х и 3-х, направленной к тому, чтобы не придавать Единице количественного осмысления»
Единение (ассимиляция) и противопоставление Четного и Нечетного, Симметричного и Центрированного показывают с полной отчетливостью, что учение о Числах не отличается от учения геометрического..
Ты похоже, слабо (если вообще) понимаешь, зачем нужен научный метод, что он даёт по сравнению с хуйней из головы, и почему им в принципе пользуются, когда можно просто не обращать внимания на такие вещи.
Всё вышеозвученное - это научная информация, вот прямо научнее некуда.
Наверное, даже ещё проще, ты не знаешь, чем научный метод отличается от хуйни из головы.
> религиозная вера в подвид бихевиоризма у которого до конца не проработана матмодель так, чтобы быть "железобетонной" как хотя бы физика макромира (классическая)
Ты серьезно сейчас апеллируешь к психометрии? Типа у неё безупречная объективная метрология и теория репрезентации? Это же курам на смех.
Ничем не отличается от того, что ты критикуешь, даже больше, - что ты критикуешь не претендует на столь божественно-ньютоновскую истинность.
>Категория функторов между двумя большими категориями при таком подходе не существует. В частности, категория, объекты которой - функторы из Set в Set, морфизмы - естественные преобразования.
Твой пример это частный случай пикрелейтед из указанной работы, в которой Obj(Set) = V. Не особо шарю за кардинальную арифметику, но если |V V| = |P(V)|, то данная категория это допустимый объект в ARC.
Какая вера, ты о чем? Матмодель операнта? IRAP + HDML же, это в RFT, модели оперантов по Скиннеру тоже есть, благо сам метод в виде кумулятивной записи делает это возможным без всяких костылей. Насчёт истинности, в функциональном контекстуализме прямо определено, что и в каком смысле можно считать истиной, никаких абсолютных истин там не постулируется. В общем, я тебя понял, ты не видишь разницы между научным методом и хуйней из головы.
Коня можно подвести к воде, но нельзя заставить её пить. У тебя такой же доступ к интернету, как и у меня. Ты точно также можешь найти все необходимые сведения и ознакомится с методологией исследований.
> ты не видишь разницы между научным методом и хуйней из головы.
Пока что я вижу только то, что ты долбоёб.
Ты наверное хотел сказать, что ты видишь, что ты долбаеб? Давай-ка, покажи матмодель а так же безупречную обьективную метрологию и теорию репрезентации той хуйни из головы, на которую ты ссылаешься (Витгенштейн, например).
Таблетки, долбоящер. Ты хотя бы один фреймворк на котором твой MLTT выполнится определи а потом пизди.
ЗЫ Я хуею с тупости хохла. Его просят дать определение хотя бы одной метасистемы, а это ебанько отвечает что НА ВСЕХ будет выполняться.
На английском надо полностью писать, это я тут сократил что бы сто раз не писать, общепринятого сокращения нет.
> MLTT не нуждается в обьясняющих ее теориях, метатеориях итд, так как сама создана чтобы обьяснять конструктивную математику и т.о. все твои сказки про белого бычка в ней просто не нужны) единственная семантика MLTT - это вычислимость (с. 2), операционная семантика которого дана явно (с. 199). Источник - Since type theory is intended to be a fundamental conceptual framework for the basic notions of constructive mathematics, it is infeasible to explain the meaning of type theory in terms of some other mathematical theory. The meaning of type theory is explained in terms of computations.
Так тут очередная хуйня написана, давай тогда определи что такое вычисление. Тебе выше писали что там как минимум включена абстракция потенциальной осуществимости. Это всё равно что в качестве основы взять теорию множеств и через конечные мощности определять N.
Я начал с того что на скриншоте >>108377 показал формализацию. Вот, можешь ещё статью на википедии почитать https://en.m.wikipedia.org/wiki/Family_resemblance
MLTT может выполняться в MLTT.
>>108429
> давай тогда определи что такое вычисление
Долбаебша, там прямо написано, что это такое, и даже со ссылками. Все, шах и мат, N петух. Можешь дальше кукарекать, конечно, но это уже неинтересно.
> It argues that things which could be thought to be connected by one essential common feature may in fact be connected by a series of overlapping similarities, where no one feature is common to all of the things.
Define: thing, connection, overlapping, similarity, feature. Ты же и сам должен понимать, что без четкого определения как минимум вышеперечисленного, серьёзно воспринимать это не получится, не говоря уже о каком-то изучении или тем более, использовании.
>MLTT может выполняться в MLTT.
А множество это совокупность. да?
>Долбаебша, там прямо написано, что это такое, и даже со ссылками. Все, шах и мат, N петух. Можешь дальше кукарекать, конечно, но это уже неинтересно.
Там написана хуета или ты опять ничего не понял ибо дебил. Давай тащи сюда пруфы или пиздабол. Я не собираюсь делать за тебя работу, тем более очевидно ты тупой недотралль и тупо сольёшься когда тебя как щенка натычут мордой в твое же говно.
Но это же очевидные требования к любой теории, не являющейся хуйней из головы.
>>108433
> А множество это совокупность. да?
Там прямо написано, что такое множество, N петух.
Осилить статью на википедии - это тоже очевидные требования.
Статья на википедии внезапно написана словами. Эти слова определены.... где и как?
> В общем, я тебя понял, ты не видишь разницы между научным методом и хуйней из головы.
И этот замечательный научный метод показывает мне 20 пылесосов после того как я куплю один раз ковёр (и больше покупать его не буду). Просто замечательный метод функционального анализа и влияния на моё поведение.
Просто превосходный.
Если что - ты не прошёл проверочьку. Психометрия и behavior analysis это отдельные вещи. Если ты не всекаешь о чём речь (в чём тут разница и как это связано с психолингвистикой) - то грош цена твоим рассуждениям - то есть ты не видишь разницы между научным методом и хуйней из головы - и тупо употребляешь слова IRAP, HDML, RFT примерно так же как люди поминают Бога как универсальный аргумент.
У тебя в паспорте написано сын шлюхи, и что с того?
Ты ебанько которое смотрит в кникгу видит фигу, даже свой букварь для петушар-интуиционистов осилить не можешь а лезешь спорить.
ЗЫ Судя по тому как ты засунул язык в жопу и отмалчиваешься мжоно официально засчитать тебе слив. И напоминать что бы будущие посетители треда знакли с кем имеют дело.
>Но это же очевидные требования к любой теории, не являющейся хуйней из головы.
Чисто академический интерес, что ещё тебе очевидно? Аксиома выбора? Континуум гипотеза?
Да не трясись ты уже. Обосрался - обтекай, обтекешь - ещё придёшь. Если нечего сказать, ничего писать и не нужно.
>>108447
Раз какой-то клоун так на подтираче написал, наверное мне нужно признать, что так оно и есть? Или как ты это видишь? Ты действительно считаешь, что можешь мне что-то новое сказать про бихевиоризм и его методы? Или в чем твоя цель писать всю ту хуйню, что ты пишешь? Что ты долбаеб, ты вполне доказал. Что ещё докажешь?
Да не трясись ты уже. Обосрался - обтекай, обтекешь - ещё придёшь. Если нечего сказать, ничего писать и не нужно.
В NBG совокупность объектов и совокупность морфизмов для категории эндофункторов Set не являются классами - иными словами, не могут быть определены. Причина в том, что у собственных классов, таких как V, нет операции P, которая бы давала класс всех подклассов.
В NBG можно говорить лишь о классе подмножеств собственного класса (т.е. подсовокупностей, которые являются множествами), а этого недостаточно для определения категории функторов между большими категориями (теми, у которых класс объектов - собственный класс).
Можно даже доказать, что категории эндофункторов Set в NBG не существует.
Я говорю не про NBG, а про ARC, собственно в работе о NBG ни слова, ссылка на эту работу была в статье по NBG в контексте возможности определения категорий через классы, но как понятно из работы но не статьи в вики в ARC и NBG понятие классов отличаются. В частности, в ARC определены степени Pn(V) для любого натурального n. Не совсем очевидно насколько большие категории можно построить в рамках таких классов, сразу возникает вопрос о возможности представления ∞-категорий.
-
>степени Pn(V)
Имеются в виду булеаны булеанов, а не декартовая степень.
Нк, довольно очевидно, что категория всех категорий в этих основаниях тоже не существует.
Её там не существует потому что термин категория относится к метаязыку, а в языке теории его попросту нет.
Дебила кусок, категория всех категорий, множество всех множеств итп невозможны из-за ограничения самой бинарной логики на промежуточные варианты функции принадлежности. В метаязыке будет точно такой же парадокс Рассела, Жирара итд как и без метаязыка. Прочитал псевдоумное слово и теперь лепишь его куда попало.
Потому что для метаязыка будет свой метаязык и так далее. Приведу простой пример:
Его речь была чёткой и громкой: пошёл нахуй.
Есть какие-то сомнения в том, почему "его речь была чёткой и громкой" относится к метаязыку?
>Да не трясись ты уже. Обосрался - обтекай, обтекешь - ещё придёшь. Если нечего сказать, ничего писать и не нужно.
Обтекает твоя мамаша бимбоунитаз когда на ней сидит очередной клиент.
Ответ по существу будет или очередной пук? Отвечай, МРАЗЬ!
N петух, все ответы были даны ещё в прошлом треде, а если серьезно, то ещё в первом треде в 2016. То, что у тебя мозгов нет, проблема твоя, а не моя.
>>108497
В примере с множеством всех множеств метаязыки не при чем.
Ответ на бочку или хуйло пиздливое, хватит вилять жопой, я не знаю и знать не хочу в каких ещё тредах ты обосрался со своим бредом про МЛТТ.
>В примере с множеством всех множеств метаязыки не при чем.
Казалось бы, причём здесь Лужков? А он как всегда причём! С одной стороны, у нас есть термин "множество", обозначающий любое множество, в том числе и множество всех множеств, которого не существует. С другой стороны, мы можем строго доказать, что в языке теории такого термина нет. Таким образом этот термин оказывается в метаязыке, на котором мы и формулируем язык теории множеств. Ну куда же ему ещё, евонное место только тута.
> С одной стороны, у нас есть термин "множество", обозначающий любое множество, в том числе и множество всех множеств, которого не существует.
Гипостазирование.
Понятия не имею, что ты имеешь в виду. Рискну предположить, что ты попросту не понимаешь значения данного термина и применяешь его наугад.
>>108503
Хуетому.
Видно же, что тут нет comprehension через метаязык. Для теоремы достаточно наличия предиката "быть категорией", который, разумеется, должен быть в любых основаниях теории категорий. Вопрос, коллективизирующий этот предикат или нет, тут не ставится, и свёртывание по этому предикату не производится.
Да я просто над справошником твоим смеюсь, понятно что это хуйня из головы, и причина парадокса Рассела и ему подобных не в этом.
>>108507
Я тебе говорю очевидные вещи, но ты не в состоянии их понять. Это говорит о том, что ты хохол.
> очевидные вещи,
Очевидные кому? Какому-то двачному долбаебу, который всерьёз считает дурачковый справошник чем-то большим недели художкой?
Написал хохол, который не смог осилить статью на википедии.
Просто осознай степень своего долбаебства. Несешь хуйню про метаязык, когда тебе минимум двое указывают на то, что дело не в этом, начинаешь кукарекать про "хохлов"...
Это ты тупой хохел не осиливший метаязык и путающий его с объектный ибо дебил. У тебя ебанька и N определяется в петушином МЛЛТП
Да, это понятно, как и категории всех классов, о чем автор сам признается. Но дефает это тем что для конкретной не в смысле конкретных категорий как с функторами в Set, а просто неформально конкретными как возникающими в математической практикеработы с категориями такой категории и не нужно.
> метаязык
Так как ты не понимаешь, что это такое, и в каких случаях вообще уместно говорить о метаязыке, то ты официально назначаешься метапетухом. Если ты не тот же даун, что уже официально N петух, конечно.
Только с точки зрения тебя - обосанного хохло-петуха у которого вместо мозга насрано.
>Так как ты не понимаешь, что это такое, и в каких случаях вообще уместно говорить о метаязыке
Поржал, ты тупица в упор не видишь где сам этот метаязык используешь (взять зотя бы твой бред про "вычисления") и при этом смеешь кого-то назыать петухом. Ты же упоротый газнюх и просто невменяем.
Вот здесь >>108359 я достаточно чётко пояснил, что я подразумеваю под термином "метаязык". Впрочем, для человека, не осилившего статью на википедии, вполне может быть и недостаточно.
Так в твоём дурачковом справошнике тоже хуйня написана. Возможно, из-за этого и ты нихуя про метаязык не понял, но скорее всего дело в том, что ты дебил.
Ты про какой справочник - МЛТТ или писанину уёбка сохацкого на старославянском нахрюке?
Так ты даун с магическим мышлением, верующий, что "вычисление" как понятие или сущность (в виде гномика?) может как-то существовать отдельно от самих правил вычисления типа операционной семантики. Как в дурачковом справошнике пишут, гипостазирование.
Проблема в том, что дебил как раз таки ты. К тому же ещё и хохол. Если ты элементарные понятия вроде метаязык или теория семейных сходств не можешь усвоить, то о чём вообще с тобой разговаривать? Иди лучше ещё раз на майдане поскочи, тогда точно Крым вернётся.
> метаязык
Ты не понимаешь, что это,а тем более, зачем и когда используется.
> или теория семейных сходств
Это хуйня из головы. Объективно ты это никак не докажешь, можно только в справошниках для дебилов писать, читатели подобного и так поверят. Витгенштейн что-то там примерно почувствовал, пук, и вот уже готовая "теория".
>Объективно ты это никак не докажешь
Ебанько, достаточно одного примера.
>Ты не понимаешь, что это,а тем более, зачем и когда используется.
С точки зрения долбоёба - безусловно. Я привёл определение термина, дальше ты либо в состоянии его усвоить, либо ты хохол. А ты и есть хохол, потому что ни у кого кроме хохлов нет такой степени необучаемости. По каналу 1+1, который принадлежит жиду Коломойскому, показывают рекламу, как трупами хохлов будут удобрять поля. Но это же полный пиздец! А хохлу всё похуй, ему ссы в глаза - всё божья роса.
Откуда такая фиксация на хохлах? Живешь в приграничной зоне куда стала прилетать демократия?
> Ебанько, достаточно одного примера.
Какого примера, дура? Даже к абсолютно научным аналогам подобного (семантический дифференциал Осгуда, implicit association test Гринвальда) есть много вопросов. А ты принес какую-то херню, которую даже измерить и зафиксировать невозможно. То, что ты даже вот такой элементарщины не понимаешь, хорошо показывает, что ты дебил. Насчёт твоего "понимания" понятия метаязыка, ты хорошо это показал своим кукареканьем про его якобы роль в парадоксах типа Расселовского. Больше вопросов не имею, ты доказал свою дэбильность. Про "хохлов" и так очевидно, что подобное с маниакальной уверенностью, что все вокруг хохлы, будет писать только умственно неполноценный. В общем, все с тобой ясно, поди подмойса, маня.
Анус себе измерь, пёс. Здесь есть только одна проблема - что ты долбоёб. А ещё говоришь, что ты не хохол. Хохол на все 100%. На 146%.
Ебанько, это ты как опущенный бегаешь с неведомой хуетой под названием "вычисление" которое у тебя неопределяемое понятие. У тебя полный раздрай в башке, ты даже понятийное мышление не усвоил, тут даже о минимальной математической культуре мышления не приходится. ТЬюфу на тебя ебанька из жмеринки.
Спроси у ебанашки которая тут форсит сохацкого и вего высеры.
> Откуда такая фиксация на хохлах?
Дебилу почти 10 лет серят в наплечную парашу про хохлов. Потом дебил видит упоминание хохла Сохацкого, срабатывает условный рефлекс, и дебил начинает транслировать все, что ему в наплечную парашу поместили всякие инфлюэнсеры.
>>108586
Я уже даже не помню, сколько раз написал, что вычисление как семантика MLTT сформулирована в терминах операционной семантики в самой MLTT. Приносил ссылки и на книгу, и на рабочий код. Но дегенерату вроде тебя все равно ничего не понятно.
Ага, а почему тогда половина прошлого треда - это нахрюк и перемога после вопроса про Крым? После такой бурной реакции тебе уже не съехать с темы.
Так ты же дебил, тебе сто раз на это отвечали что опредление не может содержать замкнутый круг.
>перемога после вопроса про Крым?
Потому что база, что не ясно?
> После такой бурной реакции тебе уже не съехать с темы.
Какой бурной реакции, ты о чем? О твоём кукареканьи про хохлов уже второй тред подряд? Причем тут я тогда?
>>108592
Это определение не содержит замкнутого круга. Как не содержит его и определение N в аксиомах Пеано. Но, ты слишком тупой, чтобы это понять.
>Это определение не содержит замкнутого круга. Как не содержит его и определение N в аксиомах Пеано. Но, ты слишком тупой, чтобы это понять.
Только с точки зрения тебя, малограмотного ебанька. Или это тебе твой протык уёбок сохацкий напиздел? Ну тогда два дебила это сила, да.
Про аксимы Пеано (то что они не являются определением) ещё Пуанкаре писал, из современных Успенский, и это очевидно любому у кого не насрано вместо мозга.
Ты хуйло пиздливое или пруфы неси (которых естественно нет по очевидным причинам) или иди подмойся и не пизди. От того что ты свою шизу сто раз повторяешь как опущенный, истиной она не станет.
Ты пишешь как малолетний дегенерат пикрелейтед, коим скорее всего и являешься. Если нет, это ещё хуже, не школотрон с мозгами школотрона это уж вообще дно полное. Про пруфы уже отвечал, повторять сто раз не вижу смысла. Ни про какого Успенского я не слышал, потому что это ноунейм. Насчёт Пуанкаре, это не твой уровень, ты кроме ЛГБТ зумерков из тиктака вряд ли кого-то поймёшь.
>Ты пишешь как малолетний дегенерат пикрелейтед, коим скорее всего и являешься. Если нет, это ещё хуже, не школотрон с мозгами школотрона это уж вообще дно полное. Про пруфы уже отвечал, повторять сто раз не вижу смысла. Ни про какого Успенского я не слышал, потому что это ноунейм. Насчёт Пуанкаре, это не твой уровень, ты кроме ЛГБТ зумерков из тиктака вряд ли кого-то поймёшь.
Карабах чей?
В аксиоматике, которую я считаю более совершенной, существует Арцах, а несуществование Карабаха всех Карабахов - несложная теорема.
Такие вы внушаемые детишки, пздц. Как вы живёте вообще, не стыдно на каждый пук из тиливизера, или что вы там смотрите, вестись как собачки Павлова? Этим барабахом мозги парафинили ещё при Горбачеве в 80х, такая это новая и необычная повесточка, охуеть как интересно...
А если чичи снова отделяться захотят или снова дома начнут взрываться, то тоже скажешь - ну это я все в нулевых уже по телеку видел. Кекнул с прожженного гео-политика.
Не пизди, про пруфы у тебя был только жидкий пердёж в лужу в котоую тебя как нагадившего щенка тычут мордой уже по дестяому кругу а ты всё не умимаешься.
Конечно не слышал, ты вообще ничего не слышал кроме мусороной хуеты которой серет в интернетах уёбок сохацкий т.к. ты суть малограмотное ебанько. А про Пуанкаре то хоть слышал, дебил? Или вам какелам про такое тоже не рассказывают?
>Ни про какого Успенского я не слышал
Погуглил бы тогда. Он хотя бы дохтур профессор математики МГУ, а ты вообще рандомное шизло из интернета.
>>108633
N-пердеж, все ссылки были представлены. Это во-первых. Во-вторых, ты как раз ничем не обосновал свое кукареканье о том что парадокс Рассела связан с метаязыком. Так что, либо обоснуй свои кукареки, либо лизни-ка ты балду, да нахуй путешествуй.
> профессор МГУ
Там ещё один профессор был, рассказывал на Ютубчике, что так-то человек может летать, просто соевички на Логосе Кибелы и лично Ньютон всем в штаны насрали, да и вообще кали-юга, а без бороды человек это и не человек в принципе.
Кстати, 100% признак шизла - "ниспровергательство" Ньютона и Дарвина (этот тут не в тему). Любой шиз всегда что-то против Ньютона имеет, причем, чем более запущенный и инкурабильный случай, тем больше претензий к Ньютону. Я раньше не понимал, почему именно эти персонажи, других же полно, часто даже более релевантных, а потом понял - в школе только про них рассказывают, поэтому во-первых, больше вероятности что именно они станут причиной детских травм дебилоида, а во-вторых, крайне маловероятно что дебил про кого-нибудь более подходящего узнает из учебных заведений уровнем выше школы.
Тогда отсылки к уёбку сохацкому который даже по меркам инет-форумов ебанько тем более смешны. К тому же в книжке Успенского не пиздеж авториитетом (как по "ссылкам" хохлякого петуха а цепочка рассуждений. Ну и про Пуанкаре что спиздаенёшь, тоже ноу нейм?
>>108641
Выпердышь сифозной пробляди, все твои ссылки нерелевантная хуета и пиздёж не просто ноунеймов а самых натуральных фриков. Давай точную ссылку или цитату (а не отсыл к шизофазии на 1000 страниц где якобы оно закопано) или никогда не отмоешься от звания пиздабола и гнилого педераста. Неси обоснование почему редукция к метаязыку рвёт замкнутый круг, а не виляй жопой про парадокс Рассела про который лично я вообще ничего не писал (ты дебил так и не понял что тебя весь тред уже обоссал, а не только я, лол).
> в книжке Успенского не пиздеж авториитетом (как по "ссылкам" хохлякого петуха а цепочка рассуждений. Ну и про Пуанкаре что спиздаенёшь, тоже ноу нейм?
> Давай точную ссылку или цитату (а не отсыл к шизофазии на 1000 страниц где якобы оно закопано
Давай ссылки, я жду. Надеюсь, это доказательства, а не оценочные суждения. Тебе были даны ссылки на код и на точную страницу в конкретной книге. С твоей стороны одни кукареканья смелого только в интернете зумерка.
>Давай ссылки, я жду.
Погуглил за тебя дебила:
https://forallxyz.net/a-52#t2
...Довольно скоро мы убеждаемся, что такие попытки бесплодны. Натуральное число следует признать первичным, неопределяемым понятием, одной из категорий математики.
>Надеюсь, это доказательства, а не оценочные суждения.
Даже по вопросам видно что ты - дебил не имеющий представления о математике. На таком низком уровне базовых понятий доказательство не к чему редуцировать, тут работает обратный реквест, или ты приносишь корректное определение N и тогда можешь на него ссылаться или не пользуешься неопределенным понятием т.к. это незаконно.
>ебе были даны ссылки на код и на точную страницу в конкретной книге.
Здесь тебе не галера что бы своим говнокодом разбрасываться. Долбоёб, тебе сто раз уже писали что код это лишь текст в объектом языке который имплементируется на метаязыке который уже должен содержать как минимум абстракцию потенциалльной осуществимости, а значит и N. Твоя конструктивисткая параша тут вообще не нужна (я даже не буду говорить что любой конструктивизм начинается с признаня исходным понятием АПБ, а значит и N через рисование палочек), в аксиомах Пеано точно такая же проблема. Так что или ты приносишь обоснование почему на метаязыке можно пользоваться неопределяемым понятием а в объектном нет, или идёшь нахуй со своим пиздежом.
>все ссылки были представлены
Ебанько, я тебе тоже могу ссылку предоставить: Вавилов Не совсем наивная теория множеств Раздел 1 параграфы 7, 8. Только у тебя мозгов не хватит осилить.
> ...Довольно скоро мы убеждаемся, что такие попытки бесплодны. Натуральное число следует признать первичным, неопределяемым понятием, одной из категорий математики.
И что это? Кто убеждается, почему, что за "мы", они все в одной комнате? В общем, как я и предполагал, очередной пук.
>>108660
> Вавилов Не совсем наивная теория множеств
Ещё худлит? Спасибо, не интересно. В общем, я тебя услышал, очередной нитакусик, начитавшийся хуйни. Рыбникова ещё почитай.
> Конечно, можно сказать, что натуральное число — это количество предметов в конечной совокупности. Эта формулировка, по-видимому, будет отвечать как значению (точнее, одному из значений) слова «определить», предложенному «Толковым словарем русского языка» под редакцией Д. Н. Ушакова [5] («дать научную, логическую характеристику, формулировку какого-либо понятия, раскрыть его содержание (научн.)»), так и формулировке Философской энциклопедии [11]
Еее, дурачковый справошник, наканецта! Ещё и толковый словарь русского языка бонусом. Даже не буду спрашивать, какое отношение все это имеет к доказательствам в математике.
>И что это? Кто убеждается, почему, что за "мы", они все в одной комнате? В общем, как я и предполагал, очередной пук.
"мы" это сообщество математиков, не путать с отрядом чурбанов в комнате с твоей пролапсовой мамашей пердящей от каждой фрикции чёрного члена.
Ебанько, это интуити>>108663
>Еее, дурачковый справошник, наканецта! Ещё и толковый словарь русского языка бонусом.
Долбоящер, тебе на твоей хохляцкой мове чтоли надо? Ебать дебил.
> "мы" это сообщество математиков,
С тобой сейчас, в одной комнате? Ты свои справошники к математике не приплетай, это худлит.
>>108665
Неосиоятор чего? Рандомной хуйни из головы? Ты же сам понимаешь, что доказать это невозможно, это чисто чье-то мнение. В отличие от нотации операционной семантики MLTT, и даже рабочего кода, реализующего ее. И все это прекрасно работает без твоих справошников. И N там определено.
> Палочки - это не числа, это имена чисел.
Ещё один со справошником? Откуда вы лезете?
>С тобой сейчас, в одной комнате? Ты свои справошники к математике не приплетай, это худлит.
Я сейчас сижу на твоей мамаше бимбоунитазе и больше в комнате никого нет.
Какие справочники, долбоёб, ты опять таблетки не принял с утра?
>И N там определено.
Чушок, это кодирование или моделирование, но не полноценное определение т.е. требует аналогичных средств на метаязыке. И твой говнокод тут ничего не решает.
>
> это кодирование или моделирование, но не полноценное определение
Это полноценное определение, более того, работающее. А что ты называешь "полноценным определением"? Что-то оторванное от нотации или рабочего кода? И где оно? В мире идей Платона? Или что то же самое, в виде хуйни в голове верующих во дурачковый справошник?
>>108682
Что-то мне подсказывает ты позоришь старика Мартина, он поди совсем другое имел вввиду а ты нихуя не понял и клевещешь на него выставляя дебилом. Хотя дебил это только ты.
>Это полноценное определение, более того, работающее.
Только у тебя в башке если не принять таблетки. Как оно работает, если требует имплементацию которая сама требвет эти же понятия которые она якобы определяет? У тебя поди и вечный двигатель работает и ты сам себя за волосы из лужи говна каждый день вытягиваешь, лул.
> полноценным определением"? Что-то оторванное от нотации или рабочего кода?
Определение в обычном поинмании, которое полностью редуциорует одно понятие к существенно другому и более простому, а не к тому же самому но завуалированное другими терминами.
> В мире идей Платона?
Интерпретация тут вообще не причем, вопрос о формальных зависимостях.
>Или что то же самое, в виде хуйни в голове верующих во дурачковый справошник?
Ты про справочник уёбка сохацкого? Я шизофазию не читаю, чел, тем более на свиноязыке.
Ебанько, ты хоть осознаёшь, что у тебя волшебное мышление?
Так почитай, что он имел в виду, я же прямую ссылку принес. Почитай и найди там хоть одно упоминание своего дурачкового справошника или любой другой хуйни, которую ты тут лепишь.
> Определение в обычном поинмании, которое полностью редуциорует одно понятие к существенно другому и более простому,
И где оно, это "более простое"? В рабочем коде его нет, в нотации тоже. Где оно есть, покажи. В твоём дурачковом справошнике?
Нахуй мне его читать, я знаю базу конструктивистов и интуиционистов, у всех у них это исходное понятие, т.е. определить они его не могут и тупо верят.
>И где оно, это "более простое"? В рабочем коде его нет, в нотации тоже. Где оно есть, покажи. В твоём дурачковом справошнике?
Пизданись, мудило, здесь тебе не борда быдлокодеров, заебал со своим кодом. Тем более тебе петушари уже тыщщу раз пояснили что код тут ни при чем, он тупо нерабочий без исполнителя которому самому нужна абстракция потенциальной осуществимости т.е. N.
> Нахуй мне его читать, я знаю базу конструктивистов и интуиционистов, у всех у них это исходное понятие, т.е. определить они его не могут и тупо верят.
Веришь ты во свои дурачковые справошники. Ни у кого из интуиционистов и конструктивистов нет ни слова о том, что N это "исходное, неопределяемое понятие". Это хуйня из головы, никакого отношения к математике не имеющая. Ты написал, что все знаешь, так покажи, где у Мартин-Лефа или ещё кого-нибудь из конструктивистов написано, что в N они просто верят, а определить не могут. А все на самом деле просто - никто из них такого никогда не писал, это хуйня из твоего дурачкового справошника.
Ты не кукарекай, ты покажи, где. Нечего ответить, чучело? Тогда я за тебя отвечу - это хуйня из головы.
>дурачковом справошнике
Блядь, какой же ты ёбаный дегенерат, просто пиздец! Настолько непробиваемо, непроходимо тупым и необучаемым может быть только хохол. Ты постоянно используешь это словосочетание в качестве своего основного и ульмитативного аргумента, что, блядь, за ёбанный пиздец? Это так интуционистская логика работает или что это хуита?
Ты на вопрос отвечай. Ок, пусть будет умничковый справошник. Что это меняет по факту? Вот есть MLTT, есть определение N в ней. А вот той хуйни, что ты цитируешь, нет нигде кроме того худлита, который ты тут тщетно пытаешься приплести к математике. И вот такие дегроды что-то там против Сохацкого пукают. Да он умнее вас тут всех вместе взятых раз в 10. Тебе самому не стыдно таким быть, дебил?
>Вот есть MLTT
Дурачковый справочник.
>есть определение N в ней
Хуита из головы.
Быстро ты в манямир съехал. Хотя, чего ожидать от дебила. Значимость MLTT огромна, от теории - конструктивных оснований до языков с зависимыми типами, позволяющих писать сертифицированный код, предотвращающий даже техногенные катастрофы, у Сохацкого в книге есть примеры, чего стоили ошибки в программном обеспечении, аварии ракет ещё не самый пиздец из того, что уже произошло. А твой справошник, какая от него польза кроме того что им можно жопу подтирать и играть в игру про белого бычка и купи слона на двачах? Никакого.
Сохацкий даже не может правильно ответить на вопрос "чей Крым?", не говоря о большем. А к какому количеству жертв привёл Украину неверный ответ на этот вопрос? Трупы хохлов уже настолько девать некуда, что ими поля удобряют!
https://math-cs.spbu.ru/pamyati-nikolaya-aleksandrovicha-vavilova-1952-2023/
Наверняка он так и не понял, что его "аргумент" про "чернильную дыру" - это не против конструктивизма, а за ультрафинитизм. Не будьте такими.
>тот самый Вавилов, на которого постоянно ссылается N-петух, помер буквально неделю назад?
Бля, жаль этого добряка.
> его "аргумент" про "чернильную дыру"
Можно подробнее?
Почему рабзиянин не понимает что независимо от ответа на этот вопрос всё было бы так же как и сейчас?
> "Когда конструктивист говорит, что натуральное число выражается в алфавите, состоящем из одного символа |, ||, |||, и заявляет, что этот процесс можно неограниченно продолжать, мне кажется, он не учитывает чего-то весьма существенного. А именно, того, что в процессе написания таким образом уже крошечных чисел, ну хотя бы 10^10000000000мы собъемся со счета, кончатся чернила, кончится бумага, кончится время, но главное все-таки, состоит в том, что еслимы будем писать все дальше и дальше, то под действием гравитации чернилаи бумага превратятся в чер[ниль]ную дыру. Словом, требуемого количествачерточек ему написать не удастся."
(С)
Проблема в том, что конструктивисты не считаю, что палочковая нотация - нотация, способ записи. Коеструктивисты считаю, что эти палочки - это и есть числа сами по себе, числа как таковые.
Если бы спор вёлся о том, какая нотация удобнее, палочковая или арабская, то ясен хуй, что арабская.
Это примерно как с золотом и бумажными деньгами. Если мы посмотрим на купюру в 500 рублей, то у нас не будет никаких сомнений в том, что это просто знак, символ. А в случае с золотом у людей почему-то сохраняется магическое мышление, и они не отдают себе отчёта в том, что золото - это такой же точно символ, они считают золото ценным само себе.
Я считаю, что надо пиздить, иначе никак этот вопрос не решить.
>Веришь ты во свои дурачковые справошники. Ни у кого из интуиционистов и конструктивистов нет ни слова о том, что N это "исходное, неопределяемое понятие".
Ясен пень, ты ж дебил не умеющий сложить два плюс два. У них база это абстракция потенциальной осуществимости на которой целиком и полностью суть N (рисованием палочек например). Во всех книжках (которые ты дебил конечно же не читал) по интуиционизму и конструктивизму об этом говорится в первых главах. Если ты настолько дурачок, в википедии хотя бы почитай.
>Это хуйня из головы, никакого отношения к математике не имеющая.
Это ты, выблядок сифозной пробляди, не имеешь никакого отношения к математики ибо клинический дегенерат.
> Ты написал, что все знаешь, так покажи, где у Мартин-Лефа или ещё кого-нибудь из конструктивистов написано, что в N они просто верят, а определить не могут.
См. выше ебанько. Мне похуй что твой дядя Мартина высрал, если он этого явно не написал, его проблемы, тем хуже для него. Мне теория типов не интересна настолько что бы читать от корки до корки все подряд т.к. она слишком уныла и не естественна в отличии от теории множеств и ни одной математической проблемы которая бы не решалась в ТМ не решает, так что по сути говно без задач.
>>108695
Так тебе дебилу ответили что объектный язык не может опираться на понятия метаязыка если он должен их обосновывать иначе будет замкнутый круг.
Хуйня - это то что у тебя вместо мозга насрано и весь тот малограмотный бред которым ты тут серешь, порчелло хохляцкое. Ты даже простейший текст осилить не в состоянии, долбоящер, гоняешь по кругу одни и те же простейшие вопросы, а лезешь со своим пиздежом как опущенный.
Ещё раз дебил, поясни кто дал тебе козлу право обосновывать понятия объектного языка такими же из метаязыка которые нихуя не определены? Отвечай, МРАЗЬ!
>есть MLTT, есть определение N в ней
Это не определение, ебанько, а модель или кодирование.
>Сохацкого пукают. Да он умнее вас тут всех вместе взятых раз в 10. Тебе самому не стыдно таким быть, дебил?
Уёбок сохацкий это натурально шизло (в плохом смысле), он тупой кодерок а не математик т.к. математических результатов у него ровно 0. Этот дурачек даже матфак не осилил, и всю жизнь провалялся на какой-то прикладной математике - ублюдочной кафедре для кодерков.
Чмоша, разговор был про основания математики, а не обсуждение инструментов что бы пасти быдлокодеров что бы они лишнего не наговнокодили. Впрочем в связи с успехами нейронок, даже тут твоему ЛТП ловить нечего.
>у Сохацкого в книге есть примеры, чего стоили ошибки в программном обеспечении, аварии ракет ещё не самый пиздец из того, что уже произошло.
Типа если бы был МЛТТ то в Крыму всё сложилось бы иначе? Или протохохлы закопали бы черное море обратно?
> Коеструктивисты считаю, что эти палочки - это и есть числа сами по себе, числа как таковые.
Это тоже из твоего справошника? Конструктивно нумералы Черча (а именно так называются эти "палочки") https://en.m.wikipedia.org/wiki/Church_encoding это один из способов записи натуральных чисел:
> The Church numeral 3 represents the action of applying any given function three times to a value.
Т.е (s(s(s 0))) это то же самое что и 3 и наоборот в нотации нумералов Черча. Эта нотация записывается по-разному, считать можно палочки, лямбды, функции succ итд, но суть у нее одна - кодирование по Черчу. Я специально принес ссылку, попробуй найти там ту хуйню, что ты приписываешь каким-то конструктивистам, видимо, из своей головы, а именно про "числа сами по себе", "как таковые" итд. Где там (или в любом источнике по конструктивизму) хотя бы упоминание того, что число может существовать отдельно от нотации, его записи итп. Ты бы не путал конструктивизм как таковой, и как твои фантазии о том, что это такое. С вопроса о том, где у Мартин-Лефа хоть как-то упоминается неопределимость N ты слился, так хотя бы про нумералы ответь. Ну или признай что хуйню пишешь.
> У них база это абстракция потенциальной осуществимости на которой целиком и полностью суть N
Эта абстракция конструктивно существует только в виде правил построения, никакой отдельной сущности под названием "абстракция потенциальной осуществимости", которая существует где-то там, в отрыве от правил построения, нет. Ты вот этого никак не понимаешь, потому что ты дебил со справошником.
>Это тоже из твоего справошника?
Нет, это хуйня из твоего головы. Ты постоянно возбуждаешься, когда я пишу, что "|||" - это не число три, это имя числа. Я ещё в пример приводил идеографическую (иероглифическую) запись со свинками. У тебя с этого вообще бомбануло.
Опять виляешь жопой, дебил. Хуйло пиздливое, покажи где я противопостовлял "сущность" и "правило"?
>>108727
Долбоёбина, там ключевое это неограниченное применение прехода к следующему числу (палочками или любым другим способом).
Про палочки на первой странице книжки Маркова можешь прочитать, тебе ебаньку уже давали ссылку.
>У тебя с этого вообще бомбануло.
Ну ещё бы, он же хохол, узнал себя и припекло.
>>108730
> покажи где я противопостовлял "сущность" и "правило"?
То есть, ты признаешь, что кроме самих правил построения, записанных явно, больше ничего не требуется?
Да.
Т.е. ты сейчас на "правилах" хочешь съеъать или к чему ты клонишь? Принцип (потенциальной осуществимости) он по определению правило.
Если ничего, кроме явно прописанных правил построения не требуется, тогда какие вообще могут быть претензии к коду MLTT? Ты сам согласен, что кроме того, что там явно прописано, больше не нужны никакие сущности, оторванные от кода. То есть, сам себе противоречишь.
Достаточно для чего? Я тебе говорю, что это имена чисел, а не сами числа. Это способ кодировки/декодировки, записи/интерпретации символов. Это способ построения имён, но не способ построения самих чисел. Точно также и арабская нотация есть ничто иное как правила построения: из исходного алфавита, (то есть цифр 1, 2, 3, 4, 5, 6, 7, 8, 9, 0) имён чисел. И римская нотация - это тоже способ кодировки чисел, причём полученные имена являются синонимами для палочковой и арабской нотации. Что мы напишем "три", что напишем "|||", что напишем "3" - всё это однохуйственно.
> Это способ построения имён, но не способ построения самих чисел
Каких "самих чисел"? Что по-твоему есть "само число" в отрыве от его записи? Зачем оно нужно, что с ним можно сделать такого, чего нельзя с нотацией числа? Это магическое мышление, веровать что вот есть нотация, запись числа, а где-то там ещё есть "само число". При этом ты же пишешь, что якобы какие-то конструктивисты якобы считают, что запись числа это и есть "сами числа как таковые" >>108719 Чё ты несёшь вообще?
Чем "имя числа" не конкретный представитель класса эквивалентности "самого числа"? В этом смысле имя числа ничем не отличается от конкретного представления множества мощности k. Как конкретное множество изоморфно любому другому той же мощности, так и имена изоморфны друг другу, но при этом формально не равны. Но это не мешает рассматривать в теории множеств множество мощности k, не рассматривая его конкретное представление.
мимокрок
> Чем "имя числа" не конкретный представитель класса эквивалентности "самого числа"? В этом смысле имя числа ничем не отличается от конкретного представления множества мощности k.
Я это и пытаюсь выяснить. Что именно предыдущий оратор имеет в виду под "самим по себе числом как таковым". N-петух явно разделяет нотацию, запись числа и какое-то "число само по себе, как таковое", причем в его представлении это абсолютно разные понятия или что там.
Блядь, а что по твоему можно кодировать/декодировать? Сообщение, данные, информацию, суждение и так далее. Например, у нас в РФ за всю историю было три уникальных президента. То есть у нас есть некоторвя совокупность уникальных президентов РФ и я хочу каким-то образом в виде знаков языка записать такой атрибут этой совокупности как количество. И я могу записать это следующим образом: у нас в РФ было столько же уникальных президентов, сколько здесь палочек: |||. Всё. Таким образом понятие тройки экстенционально соотвествует совокупности всех совокупностей, количество которых равно трём.
А если я напишу, что я ебал твою мать, то это будет то же самое, что если бы я выебал твою мать?
Очередной подрыв жопы + ложная аналогия, очень умно... Так что такое "число как таковое, само по себе"? Физический референт, или что? Ещё раз, что ты несешь вообще?
Неприятно, пориньш, произошло задымление ниже спины? А ты про хохлов что-нибудь напиши, N-петуху помогает, и ты так делай. Даунятник тут такой, слов нет...
Нет, это как охуенная аналогия, которая демонстрирует суть волшебного мышления. Например, в более ранние периоды времени люди с волшебным мышлением не различали имя человека и самого человека и верили, что через истинное имя человека можно сделать что-то плохое с самим человеком. Колдунство вуду с прокалываем кукол - из этой же оперы. Поэтому истинное имя следовало скрывать.
Ты же осознаёшь, что имя Владимир Путин и сам Владимир Путин - это не одно и то же? Точно также и имя числа три, записываемое как "3" или "|||", это именно имя, которое всего лишь обозначает тройку, но её не является. Даже то что я называю именем числа три - это тоже не имя как таковое, а конкретный экземпляр класса.
> Ты же осознаёшь, что имя Владимир Путин и сам Владимир Путин - это не одно и то же?
Конечно. То есть ты говоришь о физическом референте. Ок, я тебя услышал. Применительно к математике это ровно то, что нес Рыбников. Счёт шизов, это все на что ты способен умно_жить тут пытаешься, клоун? Что насчёт модуля над кольцом как такового, самого по себе? Какому Путину это соответствует?
> Точно также и имя числа три, записываемое как "3" или "|||", это именно имя, которое всего лишь обозначает тройку, но её не является.
Что является тройкой как таковой, самой по себе?
>Что является тройкой как таковой, самой по себе?
Её не существует. Когда мы задаём в математике переменную типа натуральное число, то это не значит, что есть какое-то натуральное число само по себе, как таковое. Есть конкретные натуральные числа: 1, 2, 3, 4 и так далее.
Но и конкретные натуральные числа тоже являются своего рода переменной в естественном языке. Референтом будет совокупность всех совокупностей, у которых атрибут количество столько же сколько тут палочек: |||.
Могут быть числа, у которых вообще нет референта, они обозначают пустой класс, это нормально. Мы знаем, что класс "вечный двигатель" - это пустой класс, но это не мешает выражению "вечный двигатель" быть осмысленным и фигурировать в осмысленных высказываниях.
>Могут быть числа, у которых вообще нет референта, они обозначают пустой класс
> Её не существует. Когда мы задаём в математике переменную типа натуральное число, то это не значит, что есть какое-то натуральное число само по себе, как таковое. Есть конкретные натуральные числа: 1, 2, 3, 4 и так далее.
Ок. С чего тогда ты решил, что:
>>108719
> Проблема в том, что конструктивисты не считаю, что палочковая нотация - нотация, способ записи. Коеструктивисты считаю, что эти палочки - это и есть числа сами по себе, числа как таковые.
Вот это ты где взял вообще? Вот есть некая нотация числа, нумералы Черча например. С чего ты взял, что помимо нотации нужны или кем-то подразумеваются итд какие-то "числа сами по себе как таковые", про которые ты сам пишешь, что они не существуют? С тобой там все в порядке, хохлы не сильно беспокоят?
Какие-то совокупности предметов встречаются чаще, например, двойки (пара ботинок, пара друзей) и тройки (три листка клевера, тройка лошадей). Какие-то реже, например, 198758 предметов. А какие-то не встречаются вообще. То, что для каждого числа должна быть непременно своя конкретная совокупность предметов, хотя бы одна, - я не понимаю за счёт чего должно такое правило выполняться.
> В прошлом треде.
Ссылку на мое сообщение. Я никогда не писал, что существуют некие "числа сами по себе как таковые", в отрыве от их нотации. Ни в прошлом треде, ни в каком другом. Ты совсем уже запизделся, клоун.
А, ты о совокупности физических объектов. То есть для тебя важно чтобы каждой записи числа n соответствовала совокупность физических объектов мощности n?
> для тебя важно чтобы каждой записи числа n соответствовала совокупность физических объектов мощности n?
Ну да. Ноль, целковый, полушка, четвертушка, осьмушка, пудовичок, медячок, серебрячок, золотничок, девятичок, десятичок, ..., N на воротничок.
Да нет, пока не предоставишь пруфы >>108757 ты официально пиздливое хуйло.
>>108762
> настоящей математики.
Гамалогии? Чем ты лучше N-петуха, такое же шизло, только вместо дурачкового справошника у тебя условно EGA. С одной стороны, хоть и не первая культура, как основания, но хотя бы не художка, уже что-то. А с другой, шизы там не меньше, начиная с Манина.
Да это хуцпа самая настоящая! Сначала ты полтора треда спорил. Потом понял, что обосрался как Украина с контрнаступлением, и заявил, что вообще никогда такого не говорил.
Так покажи где я такое говорил. Не можешь, потому что такого не было никогда, а ты пиздабол. Все просто на самом деле.
У меня сразу флешбеки с универа, где химики-преподы то не знали как решить квадратное уравнение, то не знали что касательная строится в точке. Поделить одно число на другое - средний уровень математических навыков химика.
Странно. Вроде бы в химии, когда там скорости протекания каких-то реакций считаются, то вроде бы даже иногда диффуры возникают. Или там всегда один и тот же диффур возникает, который уже решили и остаётся только числа в формулу подставить?
>Или там всегда один и тот же диффур возникает, который уже решили и остаётся только числа в формулу подставить?
Да, на практике ты просто подставляешь уже все в готовую формулу, так что откуда она взялась большинство химиков в душе не знает.
Очень грустно. Получается, свои книжки он так никогда и не допишет. А я ждала.
Вообще говоря пидорах тоже никто ни о чем не спрашивал, а так же тупо поставили перед фактом.
>Вообще говоря пидорах тоже никто ни о чем не спрашивал, а так же тупо поставили перед фактом.
Так на пикче хохла и не спросили же.
>>108825
>>108791
> рее хахли
Чё, расслабился, пиздабол? На вопросы отвечай, хуйло тупое:
>>108732
>>108733
>>108734
Конструктивный-петух, ты теперь будешь в каждом обидчике N-петуха видеть?
Ах да, вы ж тут все хохлозависимые дегенераты, извиняюсь, забыл.
Это как в СССР иметь фамилию "Баринов" или "Кулаков". Так и "Москаль" или "Белов" для украинцев.
>У хохлочурок шизофренический ресентемент на Москву
Да уж, с чего бы.
>Мне противно иметь частично кровь с этими подстилками жидов.
Гордись частично финно-угорскими корнями, или кто ты там, в чем проблема?
>>108946
руззким не обидно, украм весело, профит.
>так этот плебс и несёт такие ценности.
Почему русских так интересуют чужие ценности?
>Лучше вы дети интернационала на свои ебальники посмотрели бы
Опять, схуяли тебя волнует чужой ебальник? Речь изначально была о твоей гордости за твою кровь.
Содержание оккупированных территорий - задача оккупационных властей.
Я тут мимопроходил, но оснований тред причем тут КРЫЛОВ нахуй? Он же программист-философ по образованию, литератор по призванию и вроде математикой не сильно интересовался...
Damage control N-петуха, который обосравшись, старается перевести внимание со своего обсера на хохлосрач.
>Я тут мимопроходил, но оснований тред причем тут КРЫЛОВ нахуй
>оснований тред
Тут просто срут. Например, конструктивный петух всех несогласных пориджами называет и спамит картинками с зумерами.
Именно поэтому ты притащил хохла Сохацкого в прошлый тред?
> Именно поэтому ты притащил хохла Сохацкого в прошлый тред?
Во-первых, там написано, почему. Ты читать не умеешь, или просто умствено отсталый? Скорее последнее, конечно. Упоминание Мартин-Лефа не вызывает шведосрач, а Брауэра - голландосрач только потому, что долбаебов вроде тебя в эту сторону не особо прогревают пока. Во-вторых, вся твоя трансляция повесточки из тиливизера никак не перекрывает твой обсер, подробнее тут: >>108841
1. h-level 0 (contractible types):
1.1. Point: A single point is a contractible space, as it can be continuously deformed into itself.
2. h-level 1 (propositions):
2.1. Cohomology: Cohomology theories usually involve abelian groups or modules, which are sets, but the actual cohomology groups can be seen as propositions when considering them up to isomorphism.
2.2. Equivalence relations: An equivalence relation on a set partitions the set into disjoint subsets, and can be seen as a proposition about the elements of the set.
2.3. Equations: Mathematical statements that assert the equality of two expressions can be seen as propositions.
2.4. вся теория порядков - предпорядки, решетки, соответствия Галуа и т.п.
3. h-level 2 (sets, и тут вычислимость, так как объекты стали различимы и можно вычислять их свойства):
3.1. Chu spaces: A Chu space is a set-theoretic structure consisting of a set of states, a set of events, and a satisfaction relation between them.
3.2. Categories: A category consists of a set of objects and a set of morphisms, along with composition and identity operations satisfying certain axioms.
3.3. Simplicial sets: A simplicial set is a functor from the simplex category to the category of sets. The category of sets is an h-level 2 object, so simplicial sets can be considered at this level.
3.4. Topological spaces: A topological space is a set of points, along with a collection of open sets satisfying certain axioms.
3.5. Groups: A group is a set with a binary operation satisfying certain axioms, such as associativity, identity, and inverses.
3.6. Functions: A function is a relation between a set of inputs and a set of possible outputs with the property that each input is related to exactly one output.
3.7. Matrices: A matrix is a rectangular array of numbers, symbols, or expressions, arranged in rows and columns.
3.8. Vectors: A vector is an element of a vector space, which is a set of objects that can be added together and multiplied by scalars.
3.9. Sequences and Series: A sequence is an ordered list of elements, while a series is the sum of the terms of a sequence.
3.10. Graphs: A graph is a mathematical structure consisting of a set of vertices and a set of edges connecting pairs of vertices.
3.11. Probability Distributions: A probability distribution is a function that describes the likelihood of obtaining the possible values of a random variable.
4. h-level 3 (groupoids):
4.1. Sheaves: A sheaf is a functor from a category (usually a topological space or a site) to the category of sets or groupoids, satisfying certain axioms. Since groupoids are at h-level 3, sheaves taking values in groupoids can be considered at this level.
4.2. Lie groups: A Lie group is a group that is also a smooth manifold, with the group operations being smooth maps. Since groups are h-level 2 objects and manifolds are h-level 3 objects, Lie groups can be considered at this level.
4.3. Fractals: A fractal is a complex geometric shape that exhibits selfsimilarity and has a non-integer dimension. Fractals can be considered at h-level 3 as they often involve groupoid structures.
А твой Спасокукоцкий не хочет извиниться за оккупвцию Крыма хохлами в течении более чем двух десятилетий?
Спектральная категория формальных мов интереснее. По-сути, унификация нотации всех конструктивных логик, от простой типизированной лямбды до кубической теории типов в одном фреймворке, и все это в виде рабочего кода, ещё и с экстракцией в бэкенд (эрланг).
>Спектральная категория формальных мов интереснее. По-сути, унификация нотации всех конструктивных логик, от простой типизированной лямбды до кубической теории типов в одном фреймворке, и все это в виде рабочего кода, ещё и с экстракцией в бэкенд (эрланг).
>Тут просто срут. Например, конструктивный петух всех несогласных пориджами называет и спамит картинками с зумерами.
Проходил мимо, посрал на конструктивного петуха. Хорошая идея, предлагаю флешмоб.
>Спектральная категория формальных мов интереснее. По-сути, унификация нотации всех конструктивных логик, от простой типизированной лямбды до кубической теории типов в одном фреймворке, и все это в виде рабочего кода, ещё и с экстракцией в бэкенд (эрланг).
>Спектральная категория формальных мов
Хуйня из головы.
>По-сути, унификация нотации всех конструктивных логик
Дурачковый справошник.
>Т.е. сначала ты постулируешь кучу более мощных абстракций как исходные и не определяемый, а потом из них якобы определяешь понятия попроще, вроде N
А как померить сложность понятия?
Дорисовал тут немного из треда. Что-то ещё добавить?
И почему большинство любителей оснований это кодерки?
>И почему большинство любителей оснований это кодерки?
это же как раз и хорошо
голубая мечта человечества - научиться выводить математические факты автоматически. когда это получится, наступит благоденствие
>научиться выводить математические факты автоматически
А что это даст? Представь такая машина была бы у Ферма, и она бы пёрнула доказательством его знаменитой теоремы. Много ли пользы бы было?
Не представляю, каким надо быть додиком-аутистом, чтобы интересоваться не, там, тачками, ни футбиком, ни телками, а блядь площадями, алгебраическими уравнениями и поворотами пространства.
>футбиком
Все быдло-интересы могу понять, но с этой хуйни особо ору. Как можно трястись надо игрульками для малолетних даунят, не явялясь малолетним дауненком? Как цивилизация дошла до этой хуйни?
>А что это даст? Представь такая машина была бы у Ферма, и она бы пёрнула доказательством его знаменитой теоремы. Много ли пользы бы было?
даст возможность сильно упростить математику как науку, в то же время значительно усилив её как инструмент для физиков и прочих
в перспективе это будет значительный скачок в технологическом прогрессе
> какие вообще могут быть претензии к коду MLTT?
Претензия к МЛТТ только одна - он бесполезное и кривое говно для ебаньков. Но он тут вообще ни при чем, это тольлко твоя шиза с неуместными попытками воткнуть его в каждую дырку (ты лучше бы на своей мамаше тренировался болезный).
>Ты сам согласен, что кроме того, что там явно прописано, больше не нужны никакие сущности, оторванные от кода. То есть, сам себе противоречишь.
Только с точки зрения тебя - малограмотного дебила. Ты когда принесёшь корректное определение без порочных кругов и перестанешь пердеть в лужу? Отвечай МРАЗЬ!
К математике не имеешь отношение только ты шепелявый говнокодерок со своим уёбком сохацким, ты ебанько даже корректное определение N дать не можешь а только носишься как опущенный со своими листингами на петушином недоязычке. Твой код может только определить долбёжку твоей сифозной мамаши в пукан с отрядом чурбанов в бесконечном цикле, ничего более. Это убожество неспособно дать опредление натуарального чилса в принципе и твоё циклический обсёр это только подтверждает.
У местного дебила-конструктивного-петуха это исходное понятие, ему сойдёт.
>>107716
>а сам тайпчекер там написан на MLTT
Чекер написан наOCaml, OCaml неMLTT.
>https://github.com/groupoid/anders/blob/main/lib/foundations/mltt/mltt.anders
Если не быть долбоёбом, а вглядеться в терм, то видно, что в таком «определении» MLTT нет, например, юниверса (и вообще там полтора типа). Ну, то есть, на определение MLTT не тянет, на модель MLTT — тоже.
мимо автор этого самого anders
ёбаная макаба блядь, жрёт неразрывные пробелы, вообще охуеть
Ну и вообще говоря, хули в «Π-ctor₁ : Π (B : A → U), Pi A B → Pi A B» и ниже нет «Π-form : Π (B : A → U), U», Π-form вообще сам по себе почему-то. Что за хуйня, м-м?
У меня нет желания ковыряться в той куче щитпостинга, что ты навалил. Но это не мешает мне повторить свои тезисы. Я напомню, что изначальный вопрос был об онтологическом статусе математических объектов, что они вообще такое есть. Итак, каждое конкретное число, например, тройка, является термином. Экстенсионально, в объём понятия тройки входит каждая совокупность вещей в количестве трёх. Таким образом тройка - это класс или совокупностей по три штуки каких-либо вещей, не обязательно однородных, кстати. А термин "натуральное число" обозначает уже не вещи и их совокупности, а другие термины, такие как тройка или пятёрка. Таким образом натуральные числа - это совокупность совокупностей совокупностей, термин терминов. Но также существует термин-омоним "натуральные числа", который обозначает не количества, а порядковые номера, про него я не говорю пока что ничего. Затем из этого всего следует вывод, что математическое знание, например, 2+2=4, это знание не о вещах, а об именах вещей, именно в этом природа его дедуктивности и априорности. Мы условились называть вещи таким образом, что 2+2=4, и только в силу этого 2+2 оказывается каждый раз равно четырём. Запишите это с помощью палочковой записи, а не арабских цифр, и станет понятно почему: ||+ || = ||||. Это примерно как у Канта, только без всей той мистики, что он нагнал. Утверждение 2+2=4 выражает свойство (языковой) модели, с помощью которой мы структурируем реальность в своём восприятии. Это грамматика языка. Далее пару слов про интесионал термина тройка, который лучше записать теперь в палочковой нотации как ||| для чистоты понимания. Этот термин строится по принципу пересчёта с помощью отношения биекции как в диагональном методе кантора. То есть палочек "столько же", сколько их в любой другой тройке предметов, а между любыми тройками предметов существует отношение биекции. То есть мы записываем количество просто в лоб воспроизводя его количеством палочек. Это тот общий смысл, который мы вкладываем в термин "три" и который фиксируем в палочковой записи тройки |||. А общим смыслом для всех натуральных чисел является то, что все они образованы с помощью отношения биекции, без указания конкретного количества.
Теперь почему палочковой записи не требуется определение. Палочковая запись - это именно запись, нотация, правила кодировки/декодировки каких-то знаков. У этой нотации есть отличие от арабских цифр, а именно что палочки являются знаками-подобиями. Если мы запишем число три в арабской нотации: 3, то у нет никаких иных причин интерпретировать значок "3" как тройку кроме как конвенции, общественного договора, это целиком условное обозначение. В противоположность этому я приведу в пример картину пикрелейтед "Это не трубка", на которой изображениа трубка. Это действительно не трубка, это образ трубки, который можно использовать как знак трубки, в силу его структурного сходства с оригиналом. Такие знаки в принципе не требуют опредления так как мы можем из их сходства установить связь с оригиналом. Например, вместо слова "свинья" мы можем использовать пинктограммы из юникода 🐷, 🐖 или 🐽. Если человек не знает заранее русского языка, то он не сможет дешифровать слово "свинья", понять, что оно означает. А вот что изображено на пиктограммах 🐷, 🐖 или 🐽, сможет если он встречал свинью в оригинале, разумеется. Всё это имеет важное логическое значение так как у любого человека с мало-мальски развитой рефлексией должен был появиться вопрос, что если мы даём определения словам с помощью других слов, а их ограниченное количество, то мы должны либо впасть в порочный круг, либо оставить какие-то слова без определений.
Таковы мои тезисы, они представляются мне максимально очевидными и интуитивно понятными, то есть спорить здесь не с чем.
Петушара конструктивная, твоя манятеория ещё более не математика.
>Попробуй /re/ или /izd/.
Весь тред туда перекатить что ли?
Тебе путин платит чтобы ты сюда эту херню постил? Мразь рашистская.
>рашистская
Это что типо конструктивизма? Я нагуглить не могу что это.
>Тебе путин платит чтобы ты сюда эту херню постил? Мразь рашистская.
Лол. Сохацкий теперь хуйня?
>лучше
Лучше бы ты научился различать язык-объект и метаязык.
> Если не быть долбоёбом, а вглядеться в терм, то видно, что в таком «определении» MLTT нет, например, юниверса (и вообще там полтора типа). Ну, то есть, на определение MLTT не тянет, на модель MLTT — тоже.
> мимо автор этого самого anders
Ты ж сам писал, что там только основные типы, из которых можно вывести недостающие, например wellordering. Поэтому у тебя в модели MLTT полтора типа - пи, сигма и path равенство.
> мимо автор этого самого anders
И ещё вопрос, по спектральной категории формальных мов. Если программа написана на MLTT-80 или там HoTT например, как ее можно трансформировать в программу на PTS, там же нет таких типов, как в более сложных, той же HoTT. А исходя из свойств спектральной категории, как я понял, такая трансформация должна быть возможна, так как морфизмы в этой категории обратимы. Или я чего-то не понимаю?
>Ты ж сам писал, что там только основные типы, из которых можно вывести недостающие, например wellordering. Поэтому у тебя в модели MLTT полтора типа - пи, сигма и path равенство.
Во-первых, я не Сохацкий, и прувер писал не он (он, в основном, занимался и занимается лендингом, изредка пытаясь написать какие-то термы, и почти никогда не пытаясь собственно написать какой-нибудь терм-доказательство).
Во-вторых, мало ли что там Сохацкий писал про основные типы. На деле же, действительно, из Π и Σ можно вытащить импредикативные кодировки, с которыми постоянно носится сам Сохацкий, но для этих кодировок не будет принципов индукции; так что такое определение годится только для вычислений, но не для доказательств. (Ну то есть банально коммутативность сложения для натуральных чисел не докажешь, но в оригинальном MLTT она, внезапно, доказывается.) Но с тем кодом (https://github.com/groupoid/anders/blob/main/lib/foundations/mltt/mltt.anders) проблем ещё больше: а) там нет юниверса, его импредикативной кодировкой не заменишь; а для импредикативных кодировок нужен юниверс, б) у всех Π- и Σ-типов и путей там одинаковый домен (лол!), как и у всех путей одинаковое пространство, в) собственно Π-form/Σ-form/=-form просто висят в воздухе (о чём я и писал выше), а остальные элементы сигмы никакие их свойства не задают.
То есть это совсем не определение модели MLTT; «internalizing» ниже — вообще не модель MLTT, а какая-то очень странная структура вокруг одного произвольного (который A : U) типа. Если ещё нагляднее: можешь в «MLTT A» в поле Π-form вписать «λ (B : A → U), A», проверку типов оно пройдёт, хоть это и семантически — херня.
>wellordering
Well-order чего?
>И ещё вопрос, по спектральной категории формальных мов.
На самом деле там не категория, а какие-то мутные диаграммы со стрелками: можешь попробовать найти в его «диссере» определение формального языка. А чтобы определить категорию нужно ещё нормально определить стрелки, композицию между ними, доказать ассоциативность и прочее.
>Если программа написана на MLTT-80 или там HoTT например, как ее можно трансформировать в программу на PTS, там же нет таких типов, как в более сложных, той же HoTT.
Очевидно, не всякую программу можно хорошим образом транслировать в более слабую систему, но есть всякие трюки вроде стирания типов (type erasure) или тех же импредикативных кодировок.
> На самом деле там не категория, а какие-то мутные диаграммы со стрелками: можешь попробовать найти в его «диссере» определение формального языка. А чтобы определить категорию нужно ещё нормально определить стрелки, композицию между ними, доказать ассоциативность и прочее.
То есть, это больше некий набросок, общая схема. А почему никто не занимается деталями этой темы, идея-то очень мощная - унификация всех возможных теорий типов в одном фреймворке. Я не думаю, что там будут проблемы с тем, чтобы вычислительно определить стрелки в этой категории.
>унификация всех возможных теорий типов в одном фреймворке
А ты погугли: https://arxiv.org/abs/2009.05539
для малолетнего долбоеба характерно вырывать фразы из контекста ради тупого троллинга
мимо
С точки зрения малолетнего долбоёба - безусловно.
ЗЫ Контекст так и не поменялся, ты - ебанько зафейлившее опредление N в своей петушиной манятеории.
мимо крок не терпящий неопределённости
Посмотрел, это же не категорная модель. Вот это https://arxiv.org/abs/1904.04097 поинтереснее выглядит. Спектральную категорию Сохацкого примерно так же стоило бы допилить.
Тебе дебилу уже разложили что кал сохацкого неоперабелен и недопиливаем впринципе.
Не категорная, да, но, во-первых, не весь мир вокруг категорий вращается; во-вторых, никто не мешает переписать такой концепт в категорном сеттинге и/или собрать всё это в ещё одну большую категорию (вперёд, ёпт, пиши статью); в-третьих, в том, что я скинул, в related work же куча ссылок, например, на Исаева (https://arxiv.org/pdf/1602.08504.pdf), который как раз «we also define the category TT of algebraic dependent type theories»; а про «Uemura’s general type theories» вообще целый небольшой параграф.
Но, конечно, Сохацкий, который записал Исаева (и вообще почти всех, кто так или иначе интересуется теорией типов) в фашисты, рашисты и долбоёбы, лучше знает.
Я все равно считаю, что у Сохацкого самый интересный вариант унификации систем типов, что-то уровня куба Барендрегта или даже лучше. А насчет экстракции кода из теорий типов в бэкенды есть что-нибудь интересное почитать? Мне кроме диссера Брэди со ссылками и его же заметок о реализации этого в идрисах, почти ничего умного не попадалось. У Сохацкого ("перша формальна система") этот вопрос тоже как-то вскользь упомянут, ну или просто я в украинском не настолько силен.
>Я все равно считаю, что у Сохацкого самый интересный вариант унификации систем типов, что-то уровня куба Барендрегта или даже лучше.
Да нет у Сохацкого нихуя, это — набросок наброска, а не «диссер» (не удивлюсь, если и эта идея — категории формальных языков — откуда-то спизжена и криво переписана, поскольку на эту тему нормальные статьи, как мы видим, гуглятся). Сохацкий — шарлатан, которому за деньги пишут проекты; через некоторое время он выгоняет авторов проекта и везде, где может, клеймит их Erlang-долбоёбами/рашистами/другим модным сегодня оскорблением, авторство же присваивает себе.
>А насчет экстракции кода из теорий типов в бэкенды есть что-нибудь интересное почитать? Мне кроме диссера Брэди со ссылками и его же заметок о реализации этого в идрисах, почти ничего умного не попадалось.
Из подобного могу вспомнить только статьи про RC из Lean 4 (https://lean-lang.org/papers/thesis-sebastian.pdf, пункт 6, «An Efficient Reference Counting Scheme for Functional Programming»; ну и вообще в https://lean-lang.org/publications/ полно материалов).
>У Сохацкого ("перша формальна система") этот вопрос тоже как-то вскользь упомянут, ну или просто я в украинском не настолько силен.
На самом деле, это чуть ли не половина всей его «работы», но поскольку он косноязычный графоман, это сложно уловить. Только вот этот самый язык с экстрактом (PTS, он же Henk, он же EXE, он же Om, он же ещё что-то там) Сохацкому тоже другие люди писали.
>Я все равно считаю
Держи в курсе блеать, пипец это каким долбоёбом нужно быть что бы считать что твое мнение доказанного ебанька кого-то ебёт.
>он косноязычный графоман
В точку. Ему походу лавры Луговского покоя не дают, только мозгов для этого нет. И он это понимает, в своё время симулировал нервный срыв что бы подтереть свою шизофазию в жж, компромат мешавший его академической карьере даже по меркам хохляцкой трэш тусовки.
>не удивлюсь, если и эта идея — категории формальных языков — откуда-то спизжена
На самом деле, он подобные идеи еще в середине 10х высказывал, например https://tonpa.guru/stream/2016/2016-05-08%20%D0%9D%D0%B5%D0%BC%D0%BD%D0%BE%D0%B3%D0%BE%20%D0%9C%D0%B0%D0%B4%D1%85%D1%8C%D1%8F%D0%BC%D0%B8%D0%BA%D0%B8%20%D0%B2%20MLTT%20%D1%81%D0%B5%D1%82%D1%82%D0%B8%D0%BD%D0%B3%D0%B5.htm думаю, именно в таком виде это его идея. Ни в одной статье по унифицированным теориям типов нет подобного взгляда на вопрос, даже в тех, на которые сам Сохацкий явно ссылается. Насчет того, что это набросок, ну да, реализовать такое одному нереально наверное.
>На самом деле, он подобные идеи еще в середине 10х высказывал, например https://tonpa.guru/stream/2016/2016-05-08%20%D0%9D%D0%B5%D0%BC%D0%BD%D0%BE%D0%B3%D0%BE%20%D0%9C%D0%B0%D0%B4%D1%85%D1%8C%D1%8F%D0%BC%D0%B8%D0%BA%D0%B8%20%D0%B2%20MLTT%20%D1%81%D0%B5%D1%82%D1%82%D0%B8%D0%BD%D0%B3%D0%B5.htm
Это вот здесь подобная идея?
>Представьте себе пространство всех языков программирования
Выглядит как попытка вычленить в потоке символов, генерируемых им, какие-то собственные идеи, когда там (на самом деле) копипаст уровня ChatGPT.
>думаю, именно в таком виде это его идея.
А я думаю, что он спиздил, потому что он постоянно что-то пиздит.
>Насчет того, что это набросок, ну да, реализовать такое одному нереально наверное.
В случае Сохацкого абсолютно нереально.
>компромат мешавший его академической карьере
это про то, как он жену пиздил?
Я примерно об этом:
> У всех типов есть четкая логика заселения пространства бесконечного топоса, подобно тому как жители самсары заселяют шесть лок. Начинается все с нижнего дна ада — Bottom типа. И потом по кирпичику начиная с Unit (), потом A -> A, потом Nat, потом Stream, потом List, потом ... и так далее вплоть до инфинити-групоида, потом все начинает повторятся и узор начинает меняться. Где у этого узора дырки я пока не вижу, и какая у него структура, но как бы чувствую немного дыхание этой мандалы.
> KLONG CHEN NYING THIG обширное пространство сердечной сущности. Так же как Инфинити Топос — это пространство всех MLTT типов, которое объединяет континуум и дискретное, а также проглатывает всю математику со всеми ее логиками и теориями, так как все математики разговаривают уже давно на этом языке кванторов и бесконеченых вселенных
> Пространство типов безгранично и все типы одновременно живут в этом бесконечномерном пространстве — где каждое его измерение наслаивается друг на друга, а сами типы образуют паттерны, похожие на гомотопические группы.
Это очень характерный взгляд, видение не просто отдельных типов и разных теорий типов, а именно общей структуры, которая за всеми ними стоит, логичная реализация такого видения - спектральная категория формальных мов. Она может быть сколько угодно недопилена, но сама по себе она следствие определенного взгляда, который даже хз где можно спиздить, до такого даже Мартин-Леф с Воеводским не додумались.
Как он срался в комментах, травил какого-то своего одноклассника типа "гыгы, ты дрочишь а я жену ебу" (цитата почти дословная. Весь его жж состоял из этого, особенно в комментах.
> шизифазия шправочника хохляцкого агитатора
Съеби уже шиз.
>потом Nat
Как мы выяснили никакого Nat там отродясь не было. Зачем ты пиздишь, сын шлюхи?
Хорошо, расшифровываю поток сознания.
> У всех типов есть четкая логика заселения пространства бесконечного топоса, подобно тому как жители самсары заселяют шесть лок. Начинается все с нижнего дна ада — Bottom типа. И потом по кирпичику начиная с Unit (), потом A -> A, потом Nat, потом Stream, потом List, потом ... и так далее вплоть до инфинити-групоида, потом все начинает повторятся и узор начинает меняться. Где у этого узора дырки я пока не вижу, и какая у него структура, но как бы чувствую немного дыхание этой мандалы.
Тут он смешал импредикативные кодировки, лестницу n-типов из HoTT и (n, m)-категории в одну ебанутую уже бессмысленную последовательность. Поверх навернул красивых буддийских слов. Про категорию теорий типов речь не идёт.
>KLONG CHEN NYING THIG обширное пространство сердечной сущности. Так же как Инфинити Топос — это пространство всех MLTT типов, которое объединяет континуум и дискретное, а также проглатывает всю математику со всеми ее логиками и теориями, так как все математики разговаривают уже давно на этом языке кванторов и бесконеченых вселенных
Тут он вспомнил, что, оказывается, основания (соответствует словам «проглатывает всю математику») в виде HoTT (соответствует слову «дискретное») не придумались сам собой; а в теории гомотопий существует не только синтетический подход, но и аналитический (соответствует слову «континуум»). Поверх навернул красивых буддийских слов. Про категорию теорий типов речь не идёт.
>Пространство типов безгранично и все типы одновременно живут в этом бесконечномерном пространстве — где каждое его измерение наслаивается друг на друга, а сами типы образуют паттерны, похожие на гомотопические группы.
Тут он вспомнил, что у типов в HoTT есть семантика ∞-групоидов, у которых (сюрприз-сюрприз!) есть гомотопические группы. Поверх навернул хуйню какую-то про паттерны, без буддийских слов. Про категорию теорий типов речь не идёт.
Дальше сможешь сам?
>Это очень характерный взгляд, видение не просто отдельных типов и разных теорий типов, а именно общей структуры, которая за всеми ними стоит, логичная реализация такого видения - спектральная категория формальных мов.
Нет там нихуя, см. выше.
>который даже хз где можно спиздить
Где угодно.
>до такого даже Мартин-Леф с Воеводским не додумались
А Исаев додумался? Или не только он додумался, может, не?
> Про категорию теорий типов речь не идёт.
В этой статье не идёт. Но это ровно то направление мысли, которое его к ней привело. Как я это вижу, во всяком случае.
Ведёт его не мысль, а желание выебнуться, в чём и состоит трагедия.
Вместо того, чтобы искать в его графомании направления мысли, лучше почитать статьи и книги, на которые он сам ссылается: https://tonpa.guru/stream/2023/2023-04-30%20%D0%A7%D0%B8%D1%81%D1%82%D0%B0%20%D0%BC%D0%B0%D1%82%D0%B5%D0%BC%D0%B0%D1%82%D0%B8%D0%BA%D0%B0.htm
Вот например, пикрелейтед. Понятно, что это набросок, но у кого еще есть хоть что-то подобное?
Откуда берётся стрелка (в 2.1) из синтаксиса, содержащего Π-тип, в синтаксис, содержащий Σ-тип? Почему не наоборот? Почему вообще есть стрелка? Какая в этом логика? (Никакая.)
И как эта последовательность генерирует последовательность 2.2? Была стрелка из синтаксиса с Π-типом в синтаксис с Σ-типом, а получилась стрелка из языка, содержащего Π-тип, в язык, содержащий Π-тип и (!) Σ-тип. Функтор древних шизов, не иначе.
>но у кого еще есть хоть что-то подобное?
Ну ёбана, выше что обсуждали-то?
Или посмотрите на эти сигнатуры сразу после 2.2: O_PTS имеет тип O_Π → U, но до этого (в 2.2) Сохацкий пишет O_PTS(O_Π). Получается, O_Π : O_Π? Ну це справжня перемога, прорив у теорії типів.
>Откуда берётся стрелка (в 2.1) из синтаксиса, содержащего Π-тип, в синтаксис, содержащий Σ-тип? Почему не наоборот? Почему вообще есть стрелка? Какая в этом логика? (Никакая.)
На третьей же странице. Система с пи-типом это PTS, а с сигма-типом - это MLTT-72. И то и другое само по себе представлено как "индуктивный тип, або дерево Бема", отсюда стрелки между ними.
>>109575
Там просто нотация кривовата, но совершенно очевидно, что он имеет в виду, схема в самом верху на 31 странице.
>выше что обсуждали-то?
Но там нигде нет именно такого взгляда. Там в основном просто общая нотация для всех систем типов, какой-то структуры типа куба Барендрегта, как из одних систем порождаются другие добавлением новых типов итд, там нет.
>На третьей же странице. Система с пи-типом это PTS, а с сигма-типом - это MLTT-72. И то и другое само по себе представлено как "индуктивный тип, або дерево Бема", отсюда стрелки между ними.
Причём тут система с Π-типом? PTS с Π-типом в 2.2 у него, в 2.1 последовательность синтаксисов, которая никакой логике не подчиняется.
>Там просто нотация кривовата, но совершенно очевидно, что он имеет в виду, схема в самом верху на 31 странице.
Нет, ничего не очевидно; на самом деле, просто у Сохацкого хронические проблемы с юниверсами, вот и пишет хуйню в этой схеме на 31 странице.
>>109578
>Но там нигде нет именно такого взгляда.
Шизофункторов там действительно нет.
>как из одних систем порождаются другие добавлением новых типов итд, там нет.
Открой статью Исаева и найди там примеры 5.7 и 5.8. Не надо иметь IQ 300, чтобы понимать, что если есть общее определение теории типов, то можно из одних теорий типов другие получать, добавляя что-нибудь.
И вообще, Исаев в примерах 5.1—5.6 как раз строит все эти теории с Π-типом, с Σ-типом и далее (кроме O_W), но (неожиданно как) никаких стрелок из одной в другую у него нет.
>Причём тут система с Π-типом? PTS с Π-типом в 2.2 у него, в 2.1 последовательность синтаксисов, которая никакой логике не подчиняется.
Дык этот дурачок (который серет итт в тред) нахватался модных терминов а нихуя в них не шарит, как подросток на понт берёт высыпая на собеседника тонну сохацкой и просто конструктивистской шизы.
>Исаев в примерах 5.1—5.6 как раз строит все эти теории с Π-типом, с Σ-типом и далее (кроме O_W),
Я об это м и писал выше, у Исаева и в других обсуждаемых статьях дается общая нотация для всех систем типов, но там нет общего взгляда на все системы типов как на спектральную последовательность.
>но (неожиданно как) никаких стрелок из одной в другую у него нет.
Потому что у него любая система типов рассматривается как набор собственно типов и правил. А у Сохацкого любая система типов - сама по себе единый тип. Это и есть та разница во взглядах, о которой я говорю. Как у Барендрегта, есть общая нотация PTS, но при этом есть и куб со стрелками из одного лямбда-исчисление в другое, по которым можно проследить их порождение.
>но там нет общего взгляда на все системы типов как на спектральную последовательность.
Ну то есть у Исаева категория систем типов есть, эндофункторы в ней, но какого-то там общего взгляда нет, OK.
>Потому что у него любая система типов рассматривается как набор собственно типов и правил. А у Сохацкого любая система типов - сама по себе единый тип.
Не пиши хуйню: нет никакой логики в том, чтобы система только с Π-типом вкладывалась в системы только с Σ-типом (что у Сохацкого как-то происходит в 2.1), зато даже ежу понятно, что система с Π-типом вкладывается в систему с Π-типом и Σ-типом (что у Сохацкого в 2.2). Именно поэтому в категории у Исаева нет первых стрелок, но есть вторые, о которых он, впрочем, не пишет (потому что, наверное, считает, что и так всё тут понятно).
>нет никакой логики в том, чтобы система только с Π-типом вкладывалась в системы только с Σ-типом (что у Сохацкого как-то происходит в 2.1)
В 2.1 у него последовательности синтаксических деревьев, соответствующих каждому типу и его правилам, а не теориям типов, их содержащих. То, что ты говоришь, это все равно что сказать, что нет никакого смысла в стрелке между Nat -> Bool, например.
Ёбаный насос, блядь, а я о чём в >>109573 писал? Как синтаксическое дерево только с Π-типом вкладывается в синтаксическое дерево только с Σ-типом? Везде формально меняем букву Π на букву Σ или что? Зачем? Для чего? Почему?
Ну, можешь представить функцию, берущую значение из пи типа и возвращающую значение из сигма типа. Я же привел пример с Nat -> Bool.
Какую, нахуй, функцию? У тебя стрелка между синтаксисами.
В конце концов, зачем ты ищешь смысл в этой шизе? Почитай уже нормальную литературу.
> стрелка между синтаксисами.
Между типами же.
> В конце концов, зачем ты ищешь смысл в этой шизе?
Очевидно, потому что не вижу там никакой шизы.
> Почитай уже нормальную литературу.
Например? Про Исаева, Уемуру и Бауера понял, принял, ознакомлюсь.
>Между типами же.
>>109588
>В 2.1 у него последовательности синтаксических деревьев
>последовательности синтаксических деревьев
>синтаксических деревьев
Какими типами?
>Очевидно, потому что не вижу там никакой шизы.
Это означает, что ты мало понимаешь в теме. Читай книги, не читай графоманию Сохацкого.
>Например?
Осиль, например, HoTT book. Или, например, Маклейна (Categories for the Working Mathematician). Что-нибудь, в общем, осиль, что не является потоком сознания.
> Какими типами?
Пи и сигма. Они у него заданы в виде синтаксических деревьев.
> Это означает, что ты мало понимаешь в теме.
В чем это выражается?
Это выражается в твоём тупняке относительно очевидной херни от Сохацкого; который ебанул побольше стрелочек от балды, чтоб поцоны увожали.
В Coq вбей уже синтаксические деревья эти и не пиши хуиту.
Насколько же надо быть опущенным, чтобы в /math/ верещать о практических применениях.
> Именно поэтому в категории у Исаева нет первых стрелок, но есть вторые, о которых он, впрочем, не пишет (потому что, наверное, считает, что и так всё тут понятно).
Где у него это есть, покажи. Для того, чтобы у него были подобные стрелки, нужно, чтобы вся (каждая!) система типов сама была задана как тип. Я этого вообще нигде не видел, кроме как у Сохацкого. Я ещё у него в жежешечке читал про подобное, у него мог быть тип, начинающийся с data MLTT, или функция с типом MLTT -> MLTT. Понятно, что смысл такой нотации - структура над системами типов. В случае с Сохацким, это разумеется, спектральная категория. В anders у него точно такая же типизация, кстати.
Этот кал даже в математике бесполезен.
>>109599
>Я этого вообще нигде не видел
Потому что это бесполезная шиза.
> это разумеется, спектральная категория.
Дуращковый справощник уёбка сохацкого.
>Где у него это есть, покажи.
Статью осиль.
>Для того, чтобы у него были подобные стрелки, нужно, чтобы вся (каждая!) система типов сама была задана как тип.
Набор слов.
>у него мог быть тип, начинающийся с data MLTT
Да, синтаксис MLTT можно закодировать в MLTT, это даже пучковому пыньке понятно.
>Понятно, что смысл такой нотации - структура над системами типов. В случае с Сохацким, это разумеется, спектральная категория.
Набор слов.
>В anders у него точно такая же типизация, кстати.
Какая «такая» типизация? Система типов Anders — вариация системы из кубической Agda + модальность с парой написанных на коленке вычислительных правил.
Сначала:
> Статью осиль.
А потом:
> Набор слов.
Стрелки между теориями типов возможны только в случае если эти теории типов сами записаны как тип. Иначе между чем и чем собственно стрелка например, в случае PTS -> MLTT?
>Стрелки между теориями типов возможны только в случае если эти теории типов сами записаны как тип.
Нет, не только.
Или что, у Исаева в статье, на самом деле, нет категории? Или у него категория дискретная? Ты статью-то его хоть пролистал? На примеры посмотрел?
>Иначе между чем и чем собственно стрелка например, в случае PTS -> MLTT?
Сука, ты долбоёб что ли? Между PTS и MLTT эта стрелка, блядь, ты сам это пишешь, нахуй.
Ясно, ещё один N-петух. Я уж думал, что тут хоть кто-то с мозгами есть. Увы.
То есть ты статью даже не открывал, а просто спизданул умно звучащее словосочетание?
Какая кумулятивная иерархия? Которая https://ncatlab.org/nlab/show/cumulative+hierarchy? Не, какая-то хуйня, не то.
Наверное, ты что-то хотел спиздануть про кумулятивные юниверсы (https://ncatlab.org/nlab/show/type+universe)? Причём тут они?
На скриншоте T — algebraic dependent type theory из его категории, U — эндофунктор в этой категории, на диаграмме стрелки между T и U(T), которых, оказывается, быть не должно, теории же не в теории типов записаны, ебать.
Ок, ты прав, я не прав. Т - это любая система типов? Если да, что будет с программой, написанной в HoTT, если ее транслировать в PTS? Это вообще возможно? Как вообще может выглядеть экстракция кода из такой системы в какой-нибудь бэкенд?
>Т - это любая система типов?
Любая в том смысле, в каком определил Исаев; любой элемент определённой в статье категории.
>Если да, что будет с программой, написанной в HoTT, если ее транслировать в PTS? Это вообще возможно?
С одной стороны, в самой PTS (https://ncatlab.org/nlab/show/pure+type+system) очень мало всего. Понятно, что (чисто синтаксически) Π-тип из HoTT нужно транслировать в Π-тип из PTS.
Но в HoTT у нас есть ещё, как минимум, Σ-типы, равенство, унивалентность и высшие индуктивные типы.
При желании для Σ-типа можно придумать импредикативную кодировку (в PTS, правда, в таком случае, нужен импредикативный юниверс), но одной кодировки мало — нужно определить проекции. Первая проекция (Σ (x : A), B x → A) определяется нормально, вторая же (Π (w : Σ x, B x), B w.1) не определяется никак, и это неудивительно, поскольку у импредикативных кодировок наблюдается общее правило: принцип рекурсии определяется, принцип индукции — нет; а для сигма-типов принцип индукции получается как раз из этих двух проекций и η-правила. Если нам нужно весь HoTT транслировать, нам нужно транслировать и эту проекцию, но с ней ничего не выйдет.
С высшими индуктивными типами примерно такая же история: импредикативная кодировка есть, принципа индукции — нет.
Вообще, есть хитрожопые кодировки (https://arxiv.org/pdf/1802.02820.pdf), но а) в их определении участвует равенство, которого в голом PTS нет, б) там появляются другие проблемы, которые в конце этой статьи оговорены.
С равенством такие же проблемы, поэтому до унивалентности дело не дойдёт.
В итоге получается, что в лоб можно транслировать лишь некоторое подмножество HoTT в PTS, но не весь HoTT сразу.
С другой стороны, трансляцией в лоб такие трансляции не исчерпываются. Например, понятно, что синтаксис HoTT легко представить как дерево (для переменных можно использовать https://ncatlab.org/nlab/show/de+Bruijn+indices, а для натуральных чисел взять импредикативную кодировку, то есть нумералы Чёрча), а дерево легко записать как импредикативную кодировку (получится что-то вроде пика, только конструкторов больше). И вот уже в таком смысле получится полная трансляция, можно будет писать функции, которые преобразовывают синтаксис в синтаксис (или синтаксис в число, например, считают глубину терма).
А, ну и правила вывода теории, конечно, тоже записываются как деревья и представляются импредикативной кодировкой.
Другой вопрос в том, что принципа индукции не будет, а потому доказать внутри PTS нечто серьёзное относительно свойств этих кодировок не получится (в метатеории можно подоказывать, но это другой разговор).
Опёздыш сифозной пробляди, ты сначала на определении N жидко обдристался, теперь тебя твой протык по конструктивной параше как нагадившего щенка мордой по говну возит. Ты хохол или просто долбоёб? Неиначе мазохист.
Что это за код у тебя на картинке, откуда это?
А напрямую из HoTT или кубической системы можно экстрактить в бэкенд? Или только из более простых систем типов? Вот у Сохацкого для этого есть проект Henk (om, exe,...), а из anders так же можно?
Этот проект мертворождённый точно так же как проект украина.
>Что это за код у тебя на картинке
Это Anders.
>откуда это?
Сам написал.
>А напрямую из HoTT или кубической системы можно экстрактить в бэкенд?
Какой именно бекенд и как именно напрямую? Если бекенд — PTS, а напрямую как первый вариант в >>109610, то, я написал, увы. Если с кодировками, то вот оно и есть.
>Вот у Сохацкого для этого есть проект Henk (om, exe,...), а из anders так же можно?
У Сохацкого из PTS в Erlang прямая трансляция, потому что там как раз никаких Σ-типов и прочего нет (аналогично можно из PTS в питон, руби, любую другую парашу с лямбдами); если из Anders в Erlang, то, опять же, либо см. пик (хотя в Erlang уже можно нормальные таплы использовать), либо получится частичная трансляция.
Правда, заметь, что в Henk не все термы транслируются в Erlang: https://github.com/groupoid/henk/blob/main/src/om_extract.erl#L35-L36
[тугая струя блевотины с жидким бульканьем ударила в переполненный таз]
Какой же там говнокод. Буээээ.
>У Сохацкого из PTS в Erlang прямая трансляция, потому что там как раз никаких Σ-типов и прочего нет (аналогично можно из PTS в питон, руби, любую другую парашу с лямбдами); если из Anders в Erlang, то, опять же, либо см. пик (хотя в Erlang уже можно нормальные таплы использовать), либо получится частичная трансляция.
Я под бэкендами имел в виду что-то общеупотребительное, питон там, жабаскрипт. Из идриса вон даже в С экстракт есть. Если в языке бэкенда нет лямбд, то для экстракта нужно FFI?
Cеъебите уже на /pr'ашу со своим говнокодом, а. Хватит тред засирать.
>Я под бэкендами имел в виду что-то общеупотребительное, питон там, жабаскрипт. Из идриса вон даже в С экстракт есть.
Ну вот вычислительный кусок (лямбды, применение лямбды, конструкторы типов, принципы рекурсии и прочее) как-нибудь можно, правда, с кубами придётся попердолиться.
>Если в языке бэкенда нет лямбд, то для экстракта нужно FFI?
Тогда лямбду некуда транслировать, придётся строить AST (как на пике, опять же). Причём тут FFI, я не знаю.
> Это Anders.
> Сам написал.
Если ты считаешь Сохацкого долбаебом, зачем тогда вообще Андерс пишешь? Написал бы имплементацию описанного Исаевым, как я понял, у него там стрелки не для прикола, а реально работают? Вообще, как считаешь, профильные нейронки уже могут хотя бы помочь с написанием кода теорий типов?
https://2ch.hk/math/res/109635.html
https://2ch.hk/math/res/109635.html
https://2ch.hk/math/res/109635.html
Кста, в NFU есть множество всех множеств и оно может быть конечным (sic!)
Отличный алфавит выйдет