Математика

Тред закрыт.

Check this out!
Оснований тред №5 Аноним 07/10/17 Суб 20:45:00 256241
AlanTuringAged16.jpg 64Кб, 707x919
707x919
Church.jpeg 16Кб, 256x326
256x326
220px-HenkBaren[...].jpg 26Кб, 220x330
220x330
deBruijn.gif 157Кб, 350x480
350x480
В любой науке ровно столько науки, сколько в ней математики. В любой математике ровно столько математики, сколько в ней вычислимости.
Предыдущий - https://2ch.hk/math/res/21361.html
Аноним 07/10/17 Суб 21:00:20 256262
coding.png 170Кб, 1440x900
1440x900
На самом деле непреодолимой пропасти между конструктивным и неко нструктивным подходом нет. Поскольку и то и другое выразимо в языковых конструкциях, имеем просто еще один работающий пример релятивизма Маннури. Более того, легко показать изоморфизм между математическими формулами и соответствующим им языковыми конструкциями. Однако, проблему невычислимых верований такой подход не снимает. Но тут на самом деле только один возможный выход, и он был предложен еще Брауэром - выкинуть к хуям всю подобную ебулду из математики, или как минимум, перестать называть ее математикой. Тем более, что таких вещей немного и они все равно математике никак не помогают. Затыкать же открытые проблемы невычислимыми верованиями вообще очень плохая практика.
Аноним 07/10/17 Суб 21:12:08 256283
Давайте так.
После Тьюринга математика делится на информатику и собственно математику.
Вычислимость, автоматы, пруверы = информатика.
Все остальные школы (ньютон-пуанкаре-гротендик) = традиционная математика.
Пруф ми ронг.
Аноним 07/10/17 Суб 21:15:43 256294
>>25628
>традиционная математика.
Либо выразима в типизированной лямбде, либо все те же невычислимые Аллахи.
Аноним 08/10/17 Вск 05:33:26 256325
>>25628
>Вычислимость, автоматы, пруверы = информатика.
Так называемая "информатика" это лишь частный случай математики.
Аноним 08/10/17 Вск 05:40:22 256336
>>25632
Кто не каппа-дескриптивен, идёт нахуй.
Аноним 08/10/17 Вск 05:43:45 256347
>>25633
Можно показать простой диагонализацией, что сама каппа-дескриптивность не является каппа-дескриптивной, следовательно она тоже идёт нахуй.
Аноним 08/10/17 Вск 05:48:45 256358
>>25634
Что? Ты бредишь.
Аноним 08/10/17 Вск 05:49:38 256369
>>25628
>Либо выразима в типизированной лямбде
Исключённое третье тоже спокойно выразимо если у тебя есть пустой тип и пи-типы, но это не делает его не невычислимым Аллахом.
Аноним 08/10/17 Вск 05:53:21 2563910
>>25635
Да нет, это ведь очевидно. Каппа-дескриптивность не сохраняет копределы, а это необходимо, чтобы быть каппа-дескриптивным. Это доказал ещё Витгенштейн.
Аноним 08/10/17 Вск 05:57:30 2564411
>>25639
Каппа-дескриптивность - это конечный орграф. Что ты там диагонализировать собрался? Впрочем, я понял. Ты просто говоришь рандомные слова без всякого смысла.
Аноним 08/10/17 Вск 06:00:55 2564612
>>25644
Это без разницы на самом деле. Конечность или "бесконечность" тут не играет никакой роли. По индукции спокойно доказывается, что каппа-дескриптивность не каппа-дескриптивна. Следует из существования NNO в топосе графов.
Аноним 08/10/17 Вск 11:29:39 2566413
Я уже перестаю понимать что тут происходит.
Аноним 08/10/17 Вск 12:39:33 2566514
216-0018.jpg 115Кб, 1240x698
1240x698
>>25646
Двачую этого сударя
Аноним 08/10/17 Вск 12:50:22 2566615
>>25664
Да что тут понимать - основания математики пусты. Можешь мыслить их как контейнер, в который можно положить всё что угодно. Не всем такая свобода по душе, они хотят непременно какой-то объектный фундамент.
Аноним 08/10/17 Вск 12:57:40 2566716
>>25666
Да мне похуй на "пустоту" оснований математики, я на интуитивном уровне верую в теорию категорий, мне этого в принципе достаточно.
Конечно можно формально с помощью индукции показать (причём конструктивно), что она непротиворечива, но меня это особо не волнует.
Аноним 08/10/17 Вск 13:06:09 2566817
Как конструктивно доказывать отрицание исключённого третьего?
Аноним 08/10/17 Вск 13:09:29 2566918
>>25646
Хватит бредить.
Аноним 08/10/17 Вск 13:10:35 2567019
Аноним 08/10/17 Вск 13:12:27 2567120
Аноним 08/10/17 Вск 13:12:52 2567221
>>25671
Услышать то я услышал, но вот смысла не понял. Объяснишь?
Аноним 08/10/17 Вск 13:14:20 2567322
>>25672
Вот это >>25646 - бессмысленная чепуха.
Аноним 08/10/17 Вск 13:14:49 2567423
>>25666
Конкретно что именно из этого бессмысленная чепуха?
Аноним 08/10/17 Вск 13:40:55 2567524
>>25646
Ссылку на книгу или статью с определением каппа-дескриптивности приведи, а то непонятно про что ты говоришь.
Аноним 08/10/17 Вск 13:41:30 2567625
>>25675
Тысячу раз уже приводил.
Аноним 08/10/17 Вск 14:26:48 2567726
>>25675
Каппа-дескриптивность = дескриптивность в некоторой каппа-библиотеке.
Аноним 08/10/17 Вск 15:18:33 2568027
>>25666
>основания математики пусты. Можешь мыслить их как контейнер, в который можно положить всё что угодно.
Коран сойдет? Основания математики - это то, на чем можно основать всю математику. Т.е. нечто даже потенциально противоречивое не подойдет, а это уже не "все, что угодно".
>Не всем такая свобода по душе, они хотят непременно какой-то объектный фундамент.
Математика - это самое точное знание, какое есть у человечества. Нет объективного фундамента - нет точного знания. Смешно считать мир идей Платона или любую другую религию точным знанием.
Аноним 08/10/17 Вск 15:19:25 2568128
>>25675
Sur quelques points d'algèbre homologique
Аноним 08/10/17 Вск 15:31:57 2568229
>>25680
А, ну ладно тогда. Удачи в поисках.
Аноним 08/10/17 Вск 15:39:17 2568330
>>25676
>>25677
>>25681

Неправильно.
Во-первых, нужен текст на русском или английском, во-вторых нужно указывать страницу.
Аноним 08/10/17 Вск 15:50:51 2568431
>>25682
>Удачи в поисках.
Нашли уже, вопрос в том, чтобы реализовать, но и это в процессе. Воеводского вот жалко, то, что он помер, упомянутому процессу не на пользу.
Аноним 08/10/17 Вск 15:58:28 2568532
>>25683
>нужен текст на русском или английском,
Не можешь в языки, учись работать с гугл переводчиком, инвалид.
Аноним 08/10/17 Вск 16:12:32 2568633
>>25683
Да это ебнутый местный, его репортить за шитпостинг надо.
Аноним 08/10/17 Вск 16:20:06 2568734
>>25683
>нужен текст на русском или английском
Если ты ещё французский не выучил, то сразу видно, что на математику тебе похуй по сути.
Аноним 08/10/17 Вск 16:30:31 2568835
>>25687
Двачую.
Le son de langue russe est un bête du son... Jusqu'à un degré d'être ridicule. Je suis tombé par hasard, en cet istant regardais une translation sportive — c'est dérisoire. Elles parlent du cette langue avec tel air et telles intonations comme si tout était normal, comme si ne faisaient pas une bouffonnerie, faisont une voix sérieux. Il y a une espèce du épouvantable dans cette monde, qui ne note pas le comique de russe. Voilà cette speaker regarde moi en camera avec un air serieux — comme si tout était en ordre — prononce les mots russes, "pétaouchnok", "vskrvzénski", "sklijniarfrvrstchnost" et fait encoir ce voix, elles sont tous fous. Zut alors!
J'ai dû dire-vous là et ouvrir les yeux. Vous, probablement, ne comprenes pas mêmes et comptez à la façon des autres qui le russe soit "une langue belle" et non gloussement de la poule, qui les hommes rejetent de soi. Ça cloche dans cette monde.
Аноним 08/10/17 Вск 16:44:38 2568936
>>25683
Здесь такое не принято. Здесь просто называют фамилии. Чем малоизвестнее, тем лучше.
Аноним 08/10/17 Вск 16:46:49 2569037
>>25689
А кто-то виноват, что фамилии типа Мартин-Лёф и Брауэр тебе неизвестны? Это не повод подгорать и срать в треде.
Аноним 08/10/17 Вск 17:02:22 2569138
>>25690
Релятивизм Маннури, ATOM и MT, Бишоп, цифферкомплекс, Уолш, нумероны, изоморфизм Карри-Говарда - всё это входит в общеизвестный багаж знаний теоретика оснований? Ну окей. Если тебе позволено поступать так, то и я буду ссылаться на моих ученых без всяких дополнительных слов. Тебя интересует, что такое каппа-библиотека, - твои проблемы, ебись с гуглом самостоятельно.
Аноним 08/10/17 Вск 17:09:25 2569239
>>25691
Изоморфизм Карри-Говарда точно входит, как и интрерпретация логических констант по Брауэру-Гейтингу-Колмогорову, "это классика, это знать нада". За остальное я вполне доходчиво пояснял, при том по-русски.
Аноним 08/10/17 Вск 17:10:11 2569340
>>25692
Ну вот и я доходчиво пояснил за каппа-дескриптивность, в посте >>25677 .
Аноним 08/10/17 Вск 17:12:22 2569441
>>25693
Разница в том, что я на что-то ссылаюсь по теме, в связи с основаниями, а у тебя просто БАРЕНДРЕХТ.
Аноним 08/10/17 Вск 17:16:53 2569542
>>25694
Отнюдь. Я предельно точен в своих описаниях. Хочешь знать больше - повторяю, гугли самостоятельно. Твой ко-ко-конструктивизм гроша ломаного не стоит, объективно. Смотри, ты говоришь, что число пи построимо. Но ты даже банально не можешь сказать, какова цифра номер гугол после запятой в его десятичном представлении. Всех вычислительных мощностей этой вселенной не хватит, чтобы её найти. Значит, твоя абстракция потенциальной осуществимости ущербна, и от неё нужно отказаться в пользу каппа-библиотек.
Аноним 08/10/17 Вск 17:23:25 2569643
>>25695
>ты говоришь, что число пи построимо.
Я такого нигде и никогда не говорил. Более того, про вещественные числа я вообще говорил только то, что они фактически построимы только до конечного числа цифер после запятой, в каковом качестве и используются в любой математике, в т.ч. и неко нструктивной. Про абстракцию потенциальной осуществимости ты так и не понял, что это и зачем, чему я не удивлен. Итого, в сухом остатке от твоих предъяв одна батрушка.
Аноним 08/10/17 Вск 17:30:38 2569744
>>25696
Ну да, начались оправдания. А ведь до простой мысли, что Брауэр не гений на все времена, ты не додумался. Жемайтис изобрёл каппа-библиотеки, и это открытие уничтожило и конструктивистов, и даже ультра-финитистов. All hail Жемайтис.
Аноним 08/10/17 Вск 17:42:10 2569945
Figure-4-LEJ-Br[...].jpg 294Кб, 490x750
490x750
>>25697
>до простой мысли, что Брауэр не гений на все времена, ты не додумался.
Но он гений на все времена. И до него никто не додумался поставить вопросы об основаниях так, как это сделал он. Хотя математике тысячи лет. А вот ты простой недотролль с мейлру.
Аноним 08/10/17 Вск 17:49:58 2570246
>>25699
Жемайтис решил проблемы, о которых Брауэр даже не думал. А ещё у тебя фиксация на мейлру.
Аноним 08/10/17 Вск 19:12:20 2570747
>>25699
Брауэр конечно великий человек, но гениальность его не в постановке вопроса об основаниях (об этом задумывался еще Кронекер) а в переоткрытии понятия интенциальности, независимо от Маха и Брентано.
Математике, впрочем, никак не тысячи лет, а около двух веков, ибо "алгебра это решение уравнений" и "чертежи без доказательств" к ней очевидно не относятся. Это не значит что ранее до математики никто не додумался, например были же Дезарг и Паскаль, но это не могло прижиться, поскольку общество до-индустриальной эпохи не обладало достаточными ресурсами, чтобы позволить ученым мужам всю жизнь заниматься лишь математикой. Соответственно, никто и не занимался основаниями, потому что дисциплины такой не было. С другой стороны, понятно, что Брауэр на голову выше таких людей как Курт Гёдель или Герман Вейль, последние прочитали Гуссерля, а Брауэр пере-придумал его сам.
Аноним 08/10/17 Вск 19:15:23 2570848
>>25702
Жемайтис это генерал наподобие Бурбаки или персонаж повести Стругацких? В любом случае, он сильно уступает Дедекинду, так что я бы тут не бравировал каппа-фейсом.
Аноним 08/10/17 Вск 19:41:38 2571049
>>25708
Жемайтис - это известный логик, изобретатель каппа- и омикрон-библиотек.
Аноним 09/10/17 Пнд 18:47:01 2573950
>>25710
Я с ним лично знаком, удивительный человек.
Аноним 09/10/17 Пнд 19:30:49 2574051
Аноним 09/10/17 Пнд 20:38:27 2574252
>>25740
Это мне не мешает.
Аноним 10/10/17 Втр 05:28:37 2575053
Java программисты занимаются основаниями математики. Из теории акторов известно что паралельные вычисления нельзя сгрупировать по логическим выводам. Из этого следует что арбитр (который выбирает кому отдать процессорное время из потоков) неразрешимая задача в общем случая. Поэтому арбитров пишут используя теорию вероятности попутно, с умным видом, обсуждая проблемы математики.
Аноним 10/10/17 Втр 16:00:30 2575354
200px-Lemma28Fo[...].jpg 24Кб, 200x284
200x284
Вот в этих тредах часто приводится "аргумент", >>25628 что типа математика это одно, а информатика это другое. В связи с чем вопрос - тута про изоморфизм Карри-Говарда вообще кто-то слышал? Осилить не пробовали было бы там что осиливать? Там же просто как 3 копейки, зато становится понятно, почему математику можно представить с помощью информатики и наоборот. И как и почему невычислимые верования при этом отсеиваются.
Аноним 10/10/17 Втр 16:28:34 2575455
>>25753
С тем же успехом можно утверждать, что любая наука - частный случай генеративной лингвистики, поэтому нет ничего кроме генеративной лингвистики.

Ты слишком сильно абстрагируешься и поэтому упускаешь из виду важные отличия информатики от математики.
Аноним 10/10/17 Втр 16:29:24 2575556
>>25754
>важные отличия информатики от математики
Примеры?
Аноним 10/10/17 Втр 16:46:28 2575657
>>25755
Ну, самое очевидное - разные дискурсивные поля. В математике в принципе нет понятия "стандарт оформления кода" и многих других специфичных для информатики понятий. А в информатике нет доминирующей аксиоматической теории, в которой всё строится, - тогда как в математике в основном играют внутри ZFC-TG-NBG.
Аноним 10/10/17 Втр 16:48:39 2575758
>>25754
>С тем же успехом можно утверждать, что любая наука - частный случай генеративной лингвистики,
Если любую науку можно свести к генеративной лингвистике, почему бы и не утверждать подобное?
>поэтому нет ничего кроме генеративной лингвистики.
Э, нет. Не "нет ничего кроме Х", а "можно свести к Х". Если неважно, от какой именно печки танцевать по причине того, что нечто всегда можно свести к чему-то другому, то мы тут имеем пример работы релятивизма Маннури, но в качестве начала отсчета логичнее брать то, что удобнее и проще в практическом использовании. И я очень сомневаюсь, что любую науку проще всего представлять в генеративной лингвистике и изучать с этой точки зрения, даже если такая возможность реально существует.
>важные отличия информатики от математики.
Их нет, упомянутый изоморфизм как раз об этом. Вся математика, основанием которой может быть исчисление предикатов, представима в лямбда-П исчислении, именно этот факт лежит в основе первого прувера AUTOMATH де Брауна.
>>25756
Некоторая разница в терминологии, не более.
Аноним 10/10/17 Втр 16:49:40 2575859
>>25756
>В математике в принципе нет понятия "стандарт оформления кода"
Ты доказательства абсолютно в любом виде пишешь?
>А в информатике нет доминирующей аксиоматической теории
Это не говорит ничего о математике и информатике как о науках.
Аноним 10/10/17 Втр 16:50:58 2575960
>>25757
>представима в лямбда-П исчислении
Что ты имеешь ввиду под "представима"?
Аноним 10/10/17 Втр 16:51:26 2576061
>>25756
>в информатике нет доминирующей аксиоматической теории, в которой всё строится,
Типизированная лямбда же.
>тогда как в математике в основном играют внутри ZFC-TG-NBG.
Которые представимы в типизированной лямбде.
Аноним 10/10/17 Втр 16:55:11 2576162
>>25759
>Что ты имеешь ввиду под "представима"?
Скажем, "однозначно выразима" с помощью все того же изоморфизма Карри-Говарда. У де Брауна полно годных примеров, но меня опять же тут будут обвинять, что я всех своими евреями пугаю и даю ссылки на сложночитаемые источники.
Аноним 10/10/17 Втр 16:56:16 2576263
5DMueo2NDNQ.jpg 101Кб, 614x995
614x995
>>25757
>>25758
Информатика и математика различаются, и я показал вам отличия. Просто вы сидите на заоблачном уровне абстракции, и на нём эти отличия теряются. Но если вы снизите абстрактность, вы не сможете игнорировать разницу. А держаться на вашем уровне абстрактности и не снижать его вы сможете только в том случае, если так и останетесь сторонними философствующими наблюдателями, далёкими от реалий предметов, про которые чешете языками.

Пикрандом.
Аноним 10/10/17 Втр 16:58:09 2576364
>>25760
Все математики знают про ZFC.
Редкий информатик слышал про какую-то там типизированную лямбду.
Аноним 10/10/17 Втр 17:00:09 2576465
>>25762
>Но если вы снизите абстрактность
Извини, я математикой занимаюсь, а не какой-то хуйнёй.
>>25763
>Редкий информатик
Программисты и информатики это разные люди.
Аноним 10/10/17 Втр 17:06:40 2576566
>>25762
>Просто вы сидите на заоблачном уровне абстракции, и на нём эти отличия теряются.
Изоморфизм Карри-Говарда это не заоблачный уровень абстракции. Но уже с этих позиций вся разница, что ты назвал - это разница в терминологии.
>А держаться на вашем уровне абстрактности и не снижать его вы сможете только в том случае, если так и останетесь сторонними философствующими наблюдателями, далёкими от реалий предметов, про которые чешете языками.
Опять же, сложно найти что-то более практически применимое, чем изоморфизм Карри-Говарда, чему пример пруверы. Это не стороннее наблюдение, а самая что ни на есть практическая математика.
>>25763
>Редкий информатик слышал про какую-то там типизированную лямбду.
Это вообще ничего не меняет.
Аноним 10/10/17 Втр 17:09:30 2576667
>>25764
Выбор уровня абстрактности очень важен. Чем выше уровень, тем больше деталей теряется. На самом высоком уровне абстрактности между любыми двумя вещами нет разницы, любые две вещи - одна и та же вещь.

Подходящим выбором уровня абстрактности можно отождествить любые две вещи. Это очевидно.

Если две вещи оказались отождествлены, то нужно посмотреть, за счет чего это произошло: из-за слишком высоко задранной планки абстрактности или же из-за более содержательных причин. И если оказалось, что из-за абстрактности, - оное отождествление не имеет никакой познавательной ценности.
Аноним 10/10/17 Втр 17:11:52 2576768
>>25766
Вот я и хочу спросить - как эта болтология соотностится с приведенным мной конкретным примером - изоморфизмом Карри-Говарда?
Аноним 10/10/17 Втр 17:15:37 2576869
>>25766
>На самом высоком уровне абстрактности между любыми двумя вещами нет разницы, любые две вещи - одна и та же вещь
Ты несёшь полную хуйню, никто тут не говорит про "самый высокий уровень абстракции".
Это уже никакого отношения не имеет даже к изначальной теме.
Аноним 10/10/17 Втр 17:16:47 2576970
>>25765
Это разница не в терминологии, а в понятийном аппарате. Дискурсивное поле информатиков включает в себя идеи, которые ни в каком виде не содержатся в дискурсивном поле математиков. И обратно.

>>25767
"Информатика", которая оказывается в твоих глазах тем же самым, что "математика", - это вовсе не то же самое, что информатика (без кавычек).

На твоём уровне абстрактности нет разницы между допотопной пекарней с четвертым пентиумом и модным айфоном. С абстрактной точки зрения - они одно и то же. Но реальность такова, что допотопная пекарня и айфон - две разные вещи.
Аноним 10/10/17 Втр 18:18:54 2577071
>>25769
Я тебя услышал. Терминология под разными названиями для тебя "существенное отличие". Видно, что даже примеров использования AUTOMATH ты не видал, не говоря уже о полноценных пруверах. У де Брауна был пример с книгой "Grundlagen" Ландау, полностью переписанную на AUT, т.е. в конечном счете, в лямбде-П. https://www.win.tue.nl/automath/archive/pdf/aut046.pdf тут http://www.cs.ru.nl/F.Wiedijk/aut/index.html есть архив с этой книгой, переписанной под нотацию AUT. Есть пример этой же книги, прочеканной в Коке, что так же естественно, т.к. лямбда-П подмножество "исчисления построений", типизированной лямбде, на которой основан Кок. к слову, я тоже этой же книжкой обмазываюсь для своего недопиленного прувера Мартин-Лёф в своей MLTT показывает, как в типизированной лямбде можно представить основания. А местные полтора философа на мейлру говорят, что вы все врети и математика это не информатика, яскозал! Очень убедительно.
Аноним 10/10/17 Втр 18:27:58 2577172
>>25770
Действительно, ведь это разные уровни абстракции, поэтому и не математика.
Аноним 10/10/17 Втр 18:29:56 2577373
>>25771
Я еще раз попрошу уточнить что есть твое выражение "уровень абстракции" применительно к конкретному обсуждаемому примеру - изоморфизму Карри-Говарда.
Аноним 10/10/17 Втр 18:31:52 2577474
>>25770
Информатика это часть математики, в чём проблема?
Аноним 10/10/17 Втр 18:33:17 2577575
Конструктивные основания противоречивы. Какой в них смысл тогда?
Аноним 10/10/17 Втр 18:34:03 2577676
>>25774
Или математика часть информатики.
>>25775
>Конструктивные основания противоречивы.
Ага, раз так на мейлру написали.
Аноним 10/10/17 Втр 18:34:31 2577777
>>25776
>Ага, раз так на мейлру написали.
В прошлом треде доказательство было ведь.
Аноним 10/10/17 Втр 18:36:40 2577878
>>25777
Не было. Нет и не может быть доказательств противоречивости MLTT, поскольку эта противоречивость непосредственно вычислима и была бы получена лет еще 30 назад.
Аноним 10/10/17 Втр 18:37:33 2577979
>>25778
Зайди в последний тред, там открытым текстом написано доказательство противоречивости HoTT.
Аноним 10/10/17 Втр 18:40:17 2578080
>>25779
>HoTT.
Вычислительная интерпретация НоТТ - открытая проблема. Это во-первых. Во-вторых, конструктивные основания - это MLTT. Ты даже изоморфизм Карри-Говарда понять не можешь, хотя его и школьнику можно объяснить, ну куда ты лезешь в НоТТ? Может быть, хватит уже цирка?..
Аноним 10/10/17 Втр 18:41:13 2578181
>>25770
Я отказываюсь продолжать с тобой разговор; ты сошёл с ума, ты ёбнутый.
Аноним 10/10/17 Втр 18:42:56 2578282
>>25780
>Вычислительная интерпретация НоТТ - открытая проблема.
Но противоречивость HoTT уже закрытая.
>Ты даже изоморфизм Карри-Говарда понять не можешь
Почему ты так уверен?
>ну куда ты лезешь в НоТТ?
А что такого?
Аноним 10/10/17 Втр 18:46:32 2578383
>>25781
>>25782
>А что такого?
Толку-то тебе рассуждать о том, чего не понимаешь даже приблизительно?
Аноним 10/10/17 Втр 18:46:53 2578484
>>25783
Почему я не понимаю этого даже приблизительно?
Аноним 10/10/17 Втр 21:41:44 2578985
канструктивные основания пративоречивы. даже смысла нет, а жаль...
док-во в пред. треде.
Аноним 11/10/17 Срд 22:22:57 2581086
>>25789
Каждый раз, когда ты постишь в таком стиле, нарушается синхронность и один из внетелесных разумов погибает.
Аноним 11/10/17 Срд 23:57:35 2581487
Аноним 13/10/17 Птн 22:33:14 2584688
>>25814
Ты видимо не знаком с той ололомистической бодягой, которую Воеводский толкал в жж на пару с Михайловым.



Аноним 14/10/17 Суб 07:46:30 2584989
>>25846
Зато внетелесные разумы вычислимы.
Шах и мат веруны.
Аноним 14/10/17 Суб 13:23:51 2585190
>>25846
Я с ним лично знаком, так что знаю про это.
Аноним 14/10/17 Суб 13:49:07 2585291
Есть какие-нибудь непротиворечивые основания? Я почти уверен, что любая теория множеств противоречива и противоречивость HoTT уже доказана. Что остаётся тогда?
Аноним 14/10/17 Суб 14:37:27 2585392
Аноним 14/10/17 Суб 14:38:30 2585593
Аноним 17/10/17 Втр 00:23:33 2592394
>>25853
>Он умер.
Ну йобана.
Аноним 17/10/17 Втр 17:37:04 2593995
idris.png 62Кб, 1123x349
1123x349
Противоречивость конструктивных оснований, как и их непротиворечивость вычислима непосредственно. Так вот, ко всем кто хочет покукарековать за противоречивость конструктивных оснований, к своим кукарекам прилагать вычислимое доказательство противоречивости, в противном случае кукареки не принимаются к рассмотрению.
Аноним 17/10/17 Втр 17:39:25 2594096
Аноним 17/10/17 Втр 17:40:00 2594197
>>25940
Противоречивая хуйня, стало очевидно после доказательства независимости аксиомы выбора.
Аноним 17/10/17 Втр 17:40:34 2594298
>>25939
>Противоречивость конструктивных оснований
Что уже доказано в самих конструктивных основаниях.
Аноним 17/10/17 Втр 17:41:12 2594399
>>25940
>>25941
В ZFC верно исключенное третье, о чем вообще тут говорить.
>>25942
Где?
Аноним 17/10/17 Втр 17:43:06 25944100
>>25943
>Где?
В предыдущем треде.
Аноним 17/10/17 Втр 17:44:03 25945101
уходи.webm 1038Кб, 640x360, 00:00:07
640x360
>>25944
А, это ты. Давай, досвиданья.
Аноним 17/10/17 Втр 17:47:35 25946102
>>25945
Что ты хочешь этим сказать? Ты ебанутый, если тебе не очевидно, что из аксиомы Аллаха следует разрешимость типа путей для любого типа. Из чего следует тривиальность всех гомотопических групп любого типа, а можно построить сколько угодно типов с нетривиальными гомотопическими группами.
Аноним 19/10/17 Чтв 23:00:46 26009103
>>25852
Бамп вопросу. Сейчас пытаюсь доказать, что положительное разрешение данного вопроса эквивалентно:
1) существованию непротиворечивой теории типов где исключённое третье отрицается. (тривиально эквивалентно тому, что я пытаюсь доказать)
2) существованию теории типов, где двойное отрицание исключённого третьего недоказуемо. (эквивалентность уже почти доказал, но вот с существованием сложнее)

Что-нибудь уже известно про такие теории? Желательно, чтобы по "мощности" не уступала MLTT, хотя это конечно маловероятно.
Аноним 21/10/17 Суб 11:18:48 26039104
luitzenegbertus[...].jpg 11Кб, 238x363
238x363
>>26009
Непротиворечивые основания изложил еще Брауэр в 1907 году. Сама суть там в том, что их противоречивость принципиально невозможна в той мере, в которой не дропаются основные принципы (пример, что бывает, если их дропнуть - парадокс Жирара). Все, что было сделано на эту тему позднее, в т.ч. самим Брауэром - это адаптация его первоначальных идей к несовершенству людишек, которые не имеют физических возможностей работать со сколько-либо сложными ментальными построениями (или алгоритмическими, что то же самое по тезису Черча). Некий компромисс между самой идеей конструктивности и реальными возможностями в т.ч. вычислительных машин. Любая теория типов, MLTT хотя бы, это просто дальнейшее развитие брауэровской теории species/spreads/choice sequences.
Аноним 21/10/17 Суб 13:09:11 26040105
>>26039
Я не понимаю твой пост. Видимо такой теории типов пока нет, значит сам строить буду. Надеюсь, что мне всё удастся.
Аноним 21/10/17 Суб 15:47:15 26045106
>>26039
Верно ли, что математический объект не называется существующим, если не известен способ его построения из натуральных чисел за конечное число шагов?
Аноним 21/10/17 Суб 16:05:00 26046107
>>26045
>построения из натуральных чисел
Что ты несёшь?
Аноним 21/10/17 Суб 16:09:56 26047108
>>26046
Вообще, любой конструктивный объект представим в виде натуральных чисел, поэтому основаниями конструктивной математики является арифметика, а не логика. Я даже Мартин-Лёфа цитировал на эту тему, даже со скринами страниц. Вопрос предыдущего оратора тоже обсуждали уже, ответ на его вопрос положителен с учетом абстракции потенциальной осуществимости, или lazy evaluation в функциональном программировании.
Аноним 21/10/17 Суб 17:16:59 26050109
>>26047
>с учетом абстракции потенциальной осуществимости
Вопрос как раз про то, как именно учитывать эту абстракцию.
Аноним 21/10/17 Суб 17:26:36 26051110
>>26050
>Вопрос как раз про то, как именно учитывать эту абстракцию.
Да я уж понял, что вопрос про это. Тут больше чем за год никто не понял, как это. Учитывать эту абстракцию очень просто, lazy evaluation называется. Т.е. вычисляется только то, что нужно для конкретного построения. Проще говоря, если мы работаем с множеством N, то нам не требуется веровать в наличие этого множества целиком, как объекта платоновского мира идей. Ах, ох, фофудью отобрали? Но ведь если задуматься, верование в это множество (с точки зрения платонизма) ничего не добавляет к возможностям работы с элементами этого множества.
Аноним 21/10/17 Суб 17:28:55 26052111
>>26051
То есть само множество N не называется при этом слово "существует", правильно?
Аноним 21/10/17 Суб 17:35:20 26053112
>>26052
Не он, но я вообще сомневаюсь в существовании множеств.
Аноним 21/10/17 Суб 17:35:49 26054113
Аноним 21/10/17 Суб 17:44:10 26055114
А рисование значков алеф^n можно назвать математикой?
Аноним 21/10/17 Суб 17:55:33 26056115
>>26054
Хорошо, спасибо.
Аноним 21/10/17 Суб 18:13:26 26058116
>>26055
А ты умеешь их рисовать? Рукописный алеф совсем не похож на печатный алеф, он не как буква N.
Аноним 21/10/17 Суб 18:20:14 26059117
cqmjjn.jpg 45Кб, 763x512
763x512
>>26055
>>26058
Нарисовать-то все можно, вот только это каллиграфия, а не математика.
Аноним 21/10/17 Суб 18:21:49 26061118
CursiveWritingH[...].png 254Кб, 608x977
608x977
>>26059
Внимание на последний столбец. Именно так пишут алефы-беты-гимели спецы по теории множеств.
Аноним 21/10/17 Суб 20:08:05 26066119
Аноним 22/10/17 Вск 18:51:07 26122120
>>26051
Ты из ДС, где учишься? Думаю может тебя пригласить на семинар по этой вот тематике.
Аноним 26/10/17 Чтв 09:12:13 26317121
Сейчас учился рисовать значки алеф, бет и так далее. Это и есть "теория множеств"?
Аноним 26/10/17 Чтв 16:17:47 26324122
8944-Hebrewlett[...].jpg 12Кб, 384x1024
384x1024
>>26317
Нет. В теории множеств используются только некоторые значки и только в особенной форме. Например, алеф от руки рисуют только как на пикрелейтед, обязательно двумя раздельными чертами причем.
Аноним 26/10/17 Чтв 22:21:30 26339123
>>26324
Какие значки можно поучить для лучшего понимания теории множеств?
Аноним 27/10/17 Птн 00:09:16 26352124
>>26317
Это практика множеств.
Аноним 27/10/17 Птн 02:23:27 26361125
ramseydiagram.jpg 387Кб, 2480x3508
2480x3508
>>26339
Алеф, бет, гимель, маленькое с готическое, маленькие греческие омега, эпсилон, эта и дзета. Для дальнейшего исследования - маленькую латинскую эйч, большую греческую тета, еврейскую букву тав, маленькую греческую лямбда, маленькую латинскую k и некоторые другие символы, о которых я сейчас забыл.
Аноним 27/10/17 Птн 13:17:32 26370126
15090958367210.jpg 559Кб, 2216x1868
2216x1868
Аноним 27/10/17 Птн 22:44:53 26390127
>>26324
Нужно учить именно рукописный вариант для хорошего понимания теории множеств?
Аноним 28/10/17 Суб 02:19:45 26398128
Аноним 01/11/17 Срд 07:57:55 26619129
Как начать веровать в исключённое третье?
Аноним 04/11/17 Суб 03:17:20 26950130
Что расскажите про трансфинитные множества в теории вычислимости?
Аноним 04/11/17 Суб 09:25:55 26952131
>>26950
>трансфинитные множества
А такие существуют?
Аноним 04/11/17 Суб 13:49:32 26961132
>>26952
хуйню написал сорян. Не перечислимые множества и теория вычислимости.
Аноним 13/12/17 Срд 06:44:41 31573133
15113893307530.jpg 282Кб, 604x511
604x511
Аноним 13/12/17 Срд 06:50:43 31574134
>>31573
>тезис Чёрча
Помолился.
Аноним 13/12/17 Срд 07:03:19 31575135
>>31574
А Чёрч от него отошёл.
Аноним 13/12/17 Срд 12:23:02 31607136
Что такое «интуитивная ясность»?
Аноним 13/12/17 Срд 13:13:17 31611137
>>31607
Некая внешняя по отношению к математике характеристика. Вопросы о ее природе, возможно, стоит лучше задавать психиатрам и нейробиологам.
Аноним 24/02/18 Суб 18:10:34 37050138
bump
Аноним 26/02/18 Пнд 12:53:41 37068139
>>31611
Я бы доверился в этом вопросе священникам и шизофреникам
Аноним 26/02/18 Пнд 17:33:27 37080140
>>37068
Ну, каждому свое.
Аноним 02/03/18 Птн 15:04:23 37198141
Воеводский в одной из своих последних лекций утверждал, что классическая математика сводится конструктивной.
Аноним 02/03/18 Птн 15:05:22 37199142
Аноним 02/03/18 Птн 15:34:27 37204143
>>37198
Вот поэтому он и умер. Как и конструктивист местный. Мораль: хочешь жить не трогай конструктивную математику.
Аноним 02/03/18 Птн 20:15:37 37221144
>>37204
Он не умер, а в /dr/ перекатился.
Аноним 02/03/18 Птн 23:56:44 37229145
>>37204
И то верно, желание познавать истину и желание жить - цели редко совпадающие.
Аноним 03/03/18 Суб 01:27:22 37232146
>>37204
Это заговор жидомасонов ордена Исключённого Третьего.
Аноним 03/03/18 Суб 08:31:04 37235147
Аноним 03/03/18 Суб 09:35:00 37236148
Аноним 03/03/18 Суб 11:03:09 37237149
>>37236
там автор хвастается, что выписывает какую-то притимтивную категорную хуйню

пару раз выписал

не, это просто школьник
Аноним 03/03/18 Суб 11:57:28 37238150
>>37237
Что ж тебе так припекает от чьей-то личности, да ещё и на анонимной борде? У тебя же все должно быть хорошо, академия ведь во всем права, никаких проблем в основаниях современного понимания науки и математики нет... так ведь?
Аноним 03/03/18 Суб 13:12:51 37240151
>>37237
Он там пару раз упоминал, что пруверы пишет, так что это всё же он.
Аноним 03/03/18 Суб 13:34:28 37241152
>>37236
Тёмные уголки двача, двач наоборот какой-то. брр.
Аноним 03/03/18 Суб 14:13:45 37244153
>>37240
>Это, вероятно, потому, что автор поста сам не понимает того, о чем пишет, - как какой-нибудь постмодернист. Это такой сорт кофейного помешательства: взять кучу баззвордов и пытаться их упорядочить, ничего не понимая сколько-нибудь глубоко.
>>175125
Слушай, ну похоже. И ник Coquus от coq.
Аноним 04/03/18 Вск 15:05:23 37276154
image.png 116Кб, 640x256
640x256
Аноним 04/03/18 Вск 20:15:55 37289155
>>37276
> Владимир Воеводский о своем мистическом опыте и "игре, хозяйкой которой является страх"
Пиздец, это же у него неврология была какая-то, а не мистика. От чего он умер?
Аноним 04/03/18 Вск 20:30:38 37291156
>>37289
ты хоть посмотри что неврология означает, знаток душ
Аноним 04/03/18 Вск 22:56:57 37302157
>>37291
> знаток душ
Груш. Поехавшим он явно не был, а тут такое - нарушения чувствительности, галюны, расстройства сна итд. 100% клиент невролога.
Аноним 04/03/18 Вск 23:31:28 37304158
>>37302
Тут такая забава, невролог с ходу никогда не определяет - его это клиент или нет. Он сначала просит посетить терапевта, как говорится "чтобы исключить другую патологию". Эта такая общая тенденция, когда сталкиваешься с непонятным, то первая, обывательская, реакция - подумать, что существует некий другой человек, который это понимает.
Аноним 05/03/18 Пнд 01:42:10 37308159
>>37289
Википедия говорит, что от аневризмы. До неврологии далековато.
Аноним 08/03/18 Чтв 17:42:19 37399160
>>37304
Все проще: самый простой способ нихуя не делая как бы "вылечить" чувака это закормить его нейролептиками и антидепрессантами, поэтому все специалисты сейчас сталкивающиеся с чем-то сложнее того, решение чего в первой строчке гугла можно найти, сначала отправляют к психотерапевту, чтобы тот с вероятностью 90% после каких-то идиотских тестов сказал "да у вас депрессия" и прописал это самое.
Аноним 30/03/18 Птн 13:23:00 37987161
Аноним 30/03/18 Птн 15:07:22 37988162
>>37987
Как в мат сообществе относятся к Вилдбергеру?
Аноним 30/03/18 Птн 21:10:35 38003163
Аноним 30/03/18 Птн 22:47:51 38008164
Аноним 01/04/18 Вск 15:39:57 38063165
Аноним 10/04/18 Втр 00:45:09 38344166
Принёс вам свет знаний.

Развитие модели акторов имеет интересную связь с математической логикой. Одной из ключевых мотиваций для её развития была необходимость управления аспектами, которые возникли в процессе развития языка программирования Planner. После того как модель акторов была первоначально сформулирована, стало важно определить мощность модели в отношении тезиса Роберта Ковальского о том, что «вычисления могут быть сгруппированы по логическим выводам». Тезис Ковальского оказался ложным для одновременных вычислений в модели акторов. Этот результат всё ещё является спорным и противоречит некоторым предыдущим представлениям, поскольку тезис Ковальского верен для последовательных вычислений и даже для некоторых видов параллельных вычислений, например, для лямбда-исчислений.

Тем не менее были предприняты попытки расширения логического программирования для одновременных вычислений. Однако, Хьюитт и Ага в работе 1999 года утверждают, что результирующая система не является дедуктивной в следующем смысле: вычислительные шаги параллельных систем программирования логики не следуют дедуктивно из предыдущих шагов.
Аноним 19/04/18 Чтв 15:38:12 38588167
image.png 407Кб, 480x726
480x726
Аноним 27/04/18 Птн 14:18:44 38836168
Аноним 07/05/18 Пнд 22:07:01 39176169
Аноним 09/05/18 Срд 01:08:03 39207170
Аноним 10/05/18 Чтв 17:59:52 39246171
Аноним 10/05/18 Чтв 19:43:33 39249172
>>39246
Да, самый лучший.
Аноним 11/05/18 Птн 08:35:59 39254173
>>39249
Он верует в "доказательство" от противного. Мы тут такое не приветствуем.
Аноним 12/05/18 Суб 00:40:47 39277174
Аноним 12/05/18 Суб 18:33:25 39288175
Тут вам вопросы по петушку(coq) можно задавать или есть более специализированный тредик?
Аноним 13/05/18 Вск 19:07:53 39293176
>>39288
Задавай тут, все равно никто нихуя не знает.
Аноним 18/05/18 Птн 19:46:02 39563177
14397438300760.jpg 33Кб, 413x709
413x709
Тут тред конструктивистов, да?
Помогите выбрать - Coq или Agda?
Я недоматематик-недопогромист, хочу просто немного поиграться с пруверами.
Agda привлекает использованием юникода в синтаксисе, Coq - тем что он более популярный, а следовательно (наверн) для него больше гайдов.
Аноним 18/05/18 Птн 20:40:28 39564178
Аноним 19/05/18 Суб 04:59:24 39574179
Помирать не над[...].png 519Кб, 471x606
471x606
>>39564
>последняя правка от 2010 года
С тех пор в этих языках ничего не поменялось?
Аноним 19/05/18 Суб 05:32:17 39575180
Леса.png 438Кб, 570x585
570x585
Алсо, за https://github.com/leanprover/lean можете что сказать?
Похоже на Агду, только проект кажется более живой.
Аноним 19/05/18 Суб 09:01:53 39576181
>>39563
> Помогите выбрать - Coq или Agda?
Однозначно кок. Его больше 30 лет уже пилят, там полно тактик на все случаи жизни. Только ставить его лучше через OPAM, даже на шиндовс. И SSReflect к нему очень желательно доустановить. Lean скатили. Когда там было дополнительное ядро HoTT, то да. А так, обычный второсортный прувер.
Аноним 19/05/18 Суб 11:17:21 39577182
>>39576
ssreflect зачем нужен, в двух словах?
а то что-то взглянул и не понял
Аноним 20/05/18 Вск 13:13:46 39583183
>>39293
Дошел до главы logic(уже и дальше) в software foundations и завис на вроде бы простом доказательстве:

Example and_exercise :
∀ n m : nat, n + m = 0 → n = 0 ∧ m = 0.
Proof.
( FILL IN HERE ) Admitted.

Как это доказать примитивными тактиками вроде destruct, apply, intros, rewrite, unfold, inversion, induction и т.д. не привлекая всякие однострочники типа omega и auto?
Самое интересное что следующее упражнение, где импликация в другую сторону, я доказал сходу, а вот это нихуя.
Аноним 20/05/18 Вск 13:20:48 39584184
>>39583
Доказать, что из ложности "n или m" следует истинность "n и m ложны".
Связка " ИЛИ" или "+", значит, что существует три варианта, когда истина. Когда "ИЛИ", когда "+" или когда " "ИЛИ" и "+" "
Связка "ИЛИ" ложна тогда, когда ЛОЖНО ВСЕ.

Ты должна погрузиться В СУТЬ ИЛИ ИЛИ ИЛИ
Аноним 20/05/18 Вск 19:49:20 39587185
Можно ли считать, что основания математики/философия математики и есть самая важная математика?
Аноним 20/05/18 Вск 20:05:11 39588186
>>39587
Да. Есенин-Вольпин, следовательно, один из важнейших математиков.
Аноним 21/05/18 Пнд 00:17:44 39597187
1325505222864.jpg 49Кб, 704x396
704x396
>>39576
>там полно тактик на все случаи жизни. Только ставить его лучше через OPAM, даже на шиндовс. И SSReflect к нему очень желательно доустановить.
Ты уверен что мне это будет важно, учитывая
>хочу просто немного поиграться с пруверами.
?
Я сейчас выбираю Agda или Lean, просто из-за более приятного синтаксиса.
Аноним 21/05/18 Пнд 02:22:56 39606188
Смешно читать, как гуманитарии обсуждают легитимность математич.доказательства. Я работаю на стыке философии и математики и у меня много мат.статей в престижных англоязычных журналах по математике. Так вот, как все выглядит в математике на самом деле. Есть просто профессиональные статьи по математике -- их проверить легко (я сам регулярно пишу рецензии для западных мат.журналов), а есть статьи по математике, притендующие на серьезный результат. Обычно такие статьи не менее, чем страниц на 50 без всякой воды. Вдумайтесь сколько там шагов в доказательстве! Иногда несколько тысяч! Проверить такие статьи -- архитрудная задача. На это способны математики высочайшего класса! Чтобы проверить такую статью, нужно это доказательство повторить вслед за автором. Чтение такой статьи -- это не чтение Сартра перед сном. Оно забирает уйму времени и уйму сил. Поэтому здесь действительно возникает эффект консенсуса. Статью проверили пару десятков человек и этого достаточно для признания. А вдруг они ошиблись?
Аноним 21/05/18 Пнд 17:44:08 39616189
>>39606
>А вдруг они ошиблись?
Для этого и нужны пруверы и конструктивисты. Чтобы ухмыляться и потирать ручки каждый раз, когда кто-то ошибается.
Аноним 25/05/18 Птн 18:50:13 39780190
>>39616
> конструктивисты
Конструктивизм тут вообще не при чем. Ещё де Браун писал про Automath, что это исчисление не привязано к конкретной аксиоматике, а речь всего лишь о лямбдаР. В коке же гораздо более продвинутое CiC. Никто не запрещает туда что угодно прописать, хоть аксиому исключённого третьего, хоть десять заповедей. Любую ебулду можно доказывать в рамках прописанной аксиоматики. Проблема не в этом, а в том, что конечное доказательство к прописанной ебулде и сведется.
Аноним 26/05/18 Суб 01:18:41 39784191
Хочу перекатиться из математики в основания. Больше всего интересуют кубы Барендрегта и конструктивизм в смысле Маннури. Что почитать?
Аноним 26/05/18 Суб 04:23:29 39786192
>>39784
> конструктивизм в смысле Маннури
Он не был конструктивистом.
Аноним 26/05/18 Суб 04:27:21 39787193
>>39786
Я этого и не говорил.
Аноним 27/05/18 Вск 13:52:12 39857194
Смогу ли я упражнения и всю теорию из книжки Зорича по матанализу прорешать и формализовать в Coq?
Аноним 27/05/18 Вск 15:53:42 39866195
>>39857
Если есть формализация анализа в той полноте, которой требует Зорич, то да. Если нет — то вряд ли. Формализация для компухтерный пруверов это титанический труд, заходи лет через 10.

http://www.ens-lyon.fr/LIP/AriC/MSC2014/clelay.pdf
Посмотри эти слайды, там мелькают названия либ.
Аноним 27/05/18 Вск 17:36:22 39873196
>>39857
Только если сможешь себя клонировать.
Аноним 02/06/18 Суб 14:23:44 40054197
1478554453031.png 296Кб, 500x375
500x375
https://www.youtube.com/watch?v=U75S_ZvnWNk
За Вайлдбергером соскучились? У него новая серия видеороликов всё о том же, о старом выходит. Будет пояснять по хардкору почему современная теория множество - религиозная вера, и на чём нужно строить правильный фундамент для математики на натуральных числах, конечно же.
Спешите видеть.
Аноним 02/06/18 Суб 18:32:01 40065198
>>40054
Он хотя бы раз употребил словосочетание "доказать Аллаха" или слово "Аллах"?

Алсо, пикрелейтед давно пора ставить в шапку раздела вместо того лысого поца.
Аноним 02/06/18 Суб 22:43:42 40080199
>>40065
>вместо того лысого поца
Ты поуважительнее будь, тут тебе не тифаретник.
Аноним 03/06/18 Вск 11:27:07 40090200
>>40054
> Будет пояснять по хардкору почему современная теория множество - религиозная вера
За это Брауэр пояснил чуть более 100 лет назад.
> на чём нужно строить правильный фундамент для математики на натуральных числах, конечно же.
Будто не так.
Аноним 03/06/18 Вск 15:03:53 40099201
>>40080
Извините, Александр Николаич.
Аноним 03/06/18 Вск 23:07:50 40124202
>>40090
>За это Брауэр пояснил чуть более 100 лет назад.
Что меня возмущает в Ваилдбергере так это то, что он откровенно игнорирует всю историю интуиционизма, конструктивизма, ультрафинитизма и т.п. Как будто он первый предложил основывать математику на натуральных числах и алгоритмах.
Аноним 07/06/18 Чтв 08:21:12 40225203
>>40124
А вдруг он не в курсе просто и независимо к этим идеям пришёл?
Аноним 07/06/18 Чтв 08:57:26 40226204
>>40225
Ну положим независимо - вполне можно в это поверить. То что он игнорирует предшествующие исследования в этом направление говорит либо о том, что он практически ничего не знает о развитие мысли в основаниях математики, либо о том, что все-таки он слышал о конструктивизме, но предпочитает о нем не упоминать. Даже если верно первое, это все-равно плохо о нем говорит - значит он уже много лет пропагандирует свои идеи об основаниях математики и не удосужился прочесть хотя бы что-то уровня статьи в википедии о предмете. Хотя я думаю, что верно второе - он производит впечатление более-менее образованного математика - и ему просто приятнее делать вид что он совершенно оригинален.
Аноним 08/06/18 Птн 23:43:40 40273205
Я залетный.
Что-то читаю основания, ну там про ZFC, про модели ZFC, и чувствую, что меня хотят наебать. Ну серьезно, все эти von Neumann universe, inacessible cardinals, каждая модель ZFC имеет модель ZFC; существуют модели ZFC, в которых ZFC is inconsistent.
Понял, что не хочу всего этого, хочу палочки к палочкам приписывать, как дедушка Марков завещал.
Аноним 09/06/18 Суб 00:04:51 40277206
>>40273
Третья проблема Гильберта гарантирует, что приписывания палочек к палочкам не хватит, чтобы заниматься математикой, то есть теория длин и объёмов необходимо должна использовать рассуждения с бесконечностью. Поэтому однажды кому-то всё-таки придётся строить хорошую, рациональную теорию бесконечного. Текущая стандартная теория множеств несовершенна, многие нужные бесконечности в неё не влезают. Но реформа бесконечного будет, по-видимому, нескоро. Сейчас размышления о теории бесконечного - окраинная часть науки, почти маргинальная. Некоторые философы пытаются сделать свою ТМ, но у них ничего не получается и не сможет получиться, ибо заниматься такими вещами может только математик, очень хорошо изучивший современную математику, а не хуй с горы. Сейчас философы и логики просто априорно что-нибудь постулируют, не заботясь о реальном устройстве науки, и поэтому все их кадавры - мертворожденные.
Аноним 09/06/18 Суб 21:22:18 40293207
15197005162890.jpg 20Кб, 351x351
351x351
>>40277
> Третья проблема Гильберта гарантирует, что приписывания палочек к палочкам не хватит, чтобы заниматься математикой, то есть теория длин и объёмов необходимо должна использовать рассуждения с бесконечностью.
Есть бесконечность здорового человека и курильщика. Брауэр за это пояснил в своей вступительной речи по случаю назначения профессором в 1912 году, статья "intuitionism and formalism". Он там на пальцах поясняет, почему алеф-нуль - единственная допустимая бесконечность, а континуум ни к какому алефу сводиться не может. Опять же, и тут сто раз обсуждали отличие актуальной бесконечности от потенциальной, по-моему никто так нихуя и не понял.
Аноним 09/06/18 Суб 22:07:08 40294208
>>40293
>алеф-нуль - единственная допустимая бесконечность
Единственное объяснение этому скандальному заявлению, которое было озвучено итт, - религиозно-мистическое. Если у тебя есть какие-нибудь другие - произноси их. В противном случае ты просто фрик, как Катющег.
Аноним 09/06/18 Суб 22:29:04 40295209
image.png 109Кб, 298x376
298x376
>>40293
О, коконструктивист вернулся. Как жизнь вообще? Как объект? Всё охраняешь?
Аноним 09/06/18 Суб 22:36:04 40296210
>>40293
> 15197005162890.jpg
>Опять же, и тут сто раз обсуждали отличие актуальной бесконечности от потенциальной, по-моему никто так нихуя и не понял.
Внезапно, эта картинка идеально передаёт твои эмоции.
Аноним 10/06/18 Вск 00:32:26 40302211
tumblrinlinentj[...].gif 916Кб, 245x183
245x183
Аноним 10/06/18 Вск 04:37:00 40304212
>>40294
> Единственное объяснение этому скандальному заявлению, которое было озвучено итт, - религиозно-мистическое.
Тыскозал?
> Если у тебя есть какие-нибудь другие - произноси их.
Я и принёс. В виде названия конкретной статьи.
Аноним 10/06/18 Вск 10:31:33 40307213
>>40295
Он пришёл и ты заикаться начал.
Аноним 10/06/18 Вск 13:07:13 40310214
>>40293
> Он там на пальцах поясняет, почему алеф-нуль - единственная допустимая бесконечность
Для начала N определить нужно.
Аноним 10/06/18 Вск 14:05:26 40311215
>>40304
>Я и принёс
Там написано "интуиционистскозал"
Аноним 10/06/18 Вск 17:37:36 40321216
>>40310
> Для начала N определить нужно.
О, N-петух. Так он и определил. Правда, не в этой статье, а раньше.
>>40311
> Там написано "интуиционистскозал"
Тыскозал, что там это написано?
Аноним 10/06/18 Вск 17:47:54 40322217
>>40321
>Тыскозал, что там это написано?
Да, япрочетал.
Аноним 10/06/18 Вск 18:34:16 40326218
>>40293
Причём самому Брауэру на его интуиционизм было строго поебать всюду кроме философских семинаров. В своих работах по топологии он вплоть до середины XX века пользовался ZFC/NBG, на пенсии начал экспериментировать с аксиомой детерминированности.
Аноним 10/06/18 Вск 18:34:39 40327219
15219863638960.jpg 69Кб, 960x878
960x878
>>40322
> Да, япрочетал.
Искать знакомые буквы и понимать прочитанное - слишком разные вещи, на примере Брауэра это особенно хорошо заметно. Я вот не сразу въехал в его аргументацию по поводу того, почему восприятие пространства нельзя считать априорным суждением, и т.о в этом вопросе не прав не только Кант, но и автор т.н metaphor theory, объясняющей нейрофизиологию понятия числа, времени итп метрик. И у Брауэра это не просто "ятакскозал", а конкретное математическое доказательство.
Аноним 10/06/18 Вск 18:37:40 40328220
Давайте придумаем иное слово для бесконечности.
Аноним 10/06/18 Вск 18:40:50 40329221
>>40326
Не совсем так. Топологию к интуиционизму он привязал ещё до своего профессорства, просто задача полной реформы математики неподьемна для одного человека, даже если это Брауэр. Поэтому и приходилось пользоваться устаревшими методами.
Аноним 11/06/18 Пнд 18:17:56 40360222
>>25626
Скинь этот R скрипт пж
Аноним 11/06/18 Пнд 23:38:35 40368223
>>40328
Батхерт древних греков.
Аноним 12/06/18 Втр 00:06:01 40369224
>>40328
Актуальной или потенциальной?
Аноним 12/06/18 Втр 11:25:22 40374225
>>40328
> Давайте придумаем иное слово для бесконечности.
Так давно уже. Брауэр писал, что одно из свойств two-ity, выводимое путём ее рассмотрения, это "and so forth" (и так далее), возможность продолжать построение дальше. Что и есть потенциальная бесконечность. Насчёт актуальной - разницы нет как называть объект религиозной веры.
Аноним 12/06/18 Втр 21:01:55 40381226
>>40374
А, ну раз так Браузер писал, то так оно и есть. Слово Браузера - закон.
Аноним 13/06/18 Срд 03:44:12 40393227
>>40374
В реальности потенциальной бесконечности не бывает. Текст рано или поздно схлопнется в чер(ниль)ну дыру.
Аноним 13/06/18 Срд 12:29:51 40398228
15231018922750.jpg 181Кб, 1920x1080
1920x1080
>>40393
> В реальности потенциальной бесконечности не бывает. Текст рано или поздно схлопнется в чер(ниль)ну дыру.
А это не потенциальная бесконечность. Ты за все это время так и не понял, что это вообще такое, ладно ты, этого не понял и тот кловн, которого ты сейчас цитируешь про чернильную дыру. Не поняли про потенциальную бесконечность, не поняли про существование математического объекта. Вообще нихуяшеньки не поняли, если называть вещи своими именами. И такие вот гейнии мне что-то предъявлять будут и за математику пояснять, пиздец.
Аноним 13/06/18 Срд 12:59:19 40399229
>>40398
Нельзя "и так далее" сделать в реальном мире.
Аноним 13/06/18 Срд 13:17:18 40401230
15200835080770.png 123Кб, 500x339
500x339
>>40399
> Нельзя "и так далее" сделать в реальном мире.
Потому оно и называется потенциальным. Strict evaluation такого выражения и приведёт к дыре. Однако, есть ещё lazy evaluation, которое к дыре не приводит. И тем не менее оно возможно в реальном мире, т.к у нас есть правила построения, та самая потенциальная бесконечность. Впрочем, все это за последнюю пару лет мильен раз обсуждалось, посему нот зис шит егейн.
Аноним 13/06/18 Срд 17:03:52 40421231
>>40401
Значит, это просто верунство. Всё эти лэзи-городки. В то, чего в реальности быть не может.
Аноним 13/06/18 Срд 18:00:31 40423232
15258844733460.png 283Кб, 604x505
604x505
>>40421
> Значит, это просто верунство. Всё эти лэзи-городки. В то, чего в реальности быть не может.
Охуительные истории. Проснись, это не только может быть в реальности, это уже давно есть в любом языке с зависимыми типами. А вот чего в реальности действительно нет и быть не может, так это актуальной бесконечности и платоновского мира идей. Такое только в религии бывает.
Аноним 13/06/18 Срд 18:38:26 40425233
Это забавно. Я периодически появляюсь на этой доске (и математических тредах в /sci/ до её появления) уже весьма давно. И каждый раз, когда речь заходит о том, что очень больших чисел в реальности не существует ровно также как и бесконечных объектов, конструктивист начинает юлить и уходит от содержательного обсуждения.
Аноним 13/06/18 Срд 18:54:40 40427234
>>40401
>оно возможно в реальном мире
Возможно? То есть, мы не можем сказать, что это существует и просто верим?
То есть потенциальная бесконечность может быть, а может и не быть? Чем это отличается от Аллаха?
Аноним 13/06/18 Срд 19:09:10 40428235
14759910428490.jpg 709Кб, 992x1403
992x1403
>>40425
> И каждый раз, когда речь заходит о том, что очень больших чисел в реальности не существует ровно также как и бесконечных объектов,
С этим - к свидетелям алефов. Про отличия фактического построения от правил построения мне нечего добавить к уже сказанному. Мозги купите, что ли.
Аноним 13/06/18 Срд 19:29:52 40430236
>>40401
И в чем тогда преимущество если и там и там ты построить ничего не можешь?

Это вопрос интерпретации. Я могу сказать что правила построения бесконечности - это нарисовать ее символ на листочке и принципиально это ничем не отличается от твоих ленивых манядогм.

В каком-то треде видел ты или не ты еще копротивлялся за биологическую обусловленность математики, т.е. то что там в каком-то участке мозга есть что-то похожее на числа в конструктивном смысле, а значит только такая математика - тру. Это вообще кек.
Аноним 13/06/18 Срд 19:54:42 40431237
>>40430
> Это вопрос интерпретации. Я могу сказать что правила построения бесконечности - это нарисовать ее символ на листочке и принципиально это ничем не отличается от твоих ленивых манядогм.
Думай что хочешь, мне до бороды на самом деле. Если ты не видишь разницы, более того, не понимаешь объяснений, что тут сказать.
> В каком-то треде видел ты или не ты еще копротивлялся за биологическую обусловленность математики, т.е. то что там в каком-то участке мозга есть что-то похожее на числа в конструктивном смысле, а значит только такая математика - тру. Это вообще кек.
С этой темой могу сказать то же самое, что выше. Если тебе не очевидна связь идей Брауэра с современными моделями типа ATOM или MT которая неверна, т.к пространство не может быть априорным суждением, что заметил ещё Сеченов, могу только посочувствовать. Биологически обусловлена не только математика, но и вся вообще деятельность человека. Ну если это тяжеловато понять, остаётся религия.
Аноним 13/06/18 Срд 20:00:55 40432238
>>40431
>Ну если это тяжеловато понять, остаётся религия.
Вижу что ты решил остановиться на религии.

P.S. Если бы тебе было до бороды ты вообще бы не отстаивал свои догмы в этом треде
Аноним 13/06/18 Срд 21:01:05 40433239
>>40428
Ладно, давай разберем не примере.
Утверждение. Для любого натурального n есть простое p большее его.
Доказательство. Число n!+1 взаимно просто со всеми числами <=n, следовательно найдется простое p между n+1 и n!+1.

У меня есть такие вопросы:
1) Конструктивно ли это рассуждение?
2) Можно ли применить его к числу в десятичной системе исчисления n=1000000000000000000000000000000000000000000000000000000000000000000000000?
3) Есть ли принципиальная разница между верой в то, что для этого конкретного n найдется p, основываемая на этом рассуждение (т.е. используя существование числа 1000000000000000000000000000000000000000000000000000000000000000000000000!+1), от веры в то, что нет доказательств противоречия в ZFC длиной <=10000000, обосновываемой на базе существования недостижимого кардинала?
Аноним 13/06/18 Срд 21:12:09 40435240
>>40430
>Это вообще кек.
Разве? Почему?
Аноним 14/06/18 Чтв 00:49:19 40441241
>>40435
Потому что это такое же верунство.
Аноним 14/06/18 Чтв 04:50:39 40444242
>>40441
> Потому что это такое же верунство.
Это физиология, дебилок.
Аноним 14/06/18 Чтв 12:58:43 40446243
>>40444
>Это физиология, дебилок.
И при чем тут математика?
Аноним 14/06/18 Чтв 13:49:15 40447244
14925132359350.jpg 71Кб, 850x400
850x400
>>40446
> И при чем тут математика?
При том, что математика это деятельность человека, никакого мира идей Платона нет. Причём тут математика, написано на пикрелейтед, который сто раз постился.
Аноним 14/06/18 Чтв 16:29:40 40455245
>>40441
Верунство во что? Не понимаю. Ты отрицаешь, что математикой занимаются люди, или что?
Аноним 14/06/18 Чтв 17:56:49 40456246
А что, интуиционист действительно считает, что всю математику вне секты Брауэра нужно выкинуть и забыть?
Аноним 14/06/18 Чтв 18:02:00 40458247
>>40456
Нет, так как он считает, что математики вне секты Браузера не существует.
Аноним 14/06/18 Чтв 19:03:46 40460248
>>40455
Лучше чем ответил анон в одном из предыдущих тредов я мысль не выскажу так что, в привычном для твоей демагогии стиле, отсылаю тебя к нему.

Вообще почитал твои хуй знает может вас несколько посты на три треда назад и как и следовало ожидать никакой конкретики.

Все твои посты сводятся к пустословию в стиле "мне лень в n раз объяснять", "я уже n раз писал", "мне это не интересно", "не конструктивно - не мотематика, Я СКОЗАЛ" и т.д. с периодисческими ссылками на свои же посты, где точно так же нет никакой конкретики или сепеульки, и с ссылками на книжки на многие сотни страниц.
Аноним 14/06/18 Чтв 19:09:25 40461249
brouwercitate.png 48Кб, 419x484
419x484
В чем смысл обсуждать интуиционизм Брауэра с тем, кто не знает, что это. Ещё меньше смысла не читая Брауэра пытаться его "опровергнуть" своим незнанием предмета. Вы хотя бы это понимаете?
Аноним 14/06/18 Чтв 19:13:16 40462250
>>40460
> Я СКОЗАЛ"
Мань, ты не туда воюешь. Это мне нужно писать, а не рандомному собеседнику, охуевающему с уровня твоей аргументации а-ля детский сад штаны на лямках. Я ни разу не использовал аргумент "яскозал", а вот ты только им и пользуешься.
Аноним 14/06/18 Чтв 19:38:06 40463251
>>40462
>Мань, ты не туда воюешь.
Но ты то все равно прочитал, так что не вижу проблемы. Это двач и напротив твоих постов иконку петуха не рисует, для однозначной идентификации

>Я ни разу не использовал аргумент "яскозал"
"я это уже тыщу раз писал" - это как раз уровень я скозал. Еще бы ты начал прямо яскозакать и мамок ебать, было бы совсем потешно.
Аноним 14/06/18 Чтв 20:09:52 40464252
>>40461
В чем смысл обсуждать библию и Христа с тем, кто не знает, что это. Ещё меньше смысла не читая библию пытаться её "опровергнуть" своим незнанием предмета. Вы хотя бы это понимаете?
Аноним 14/06/18 Чтв 20:28:02 40465253
Вот я с начала этого треда успел продвинутую алгебру заботать, научился доказывать клёвые штуки про группы и поля. А что нового узнал ты, интуиционист-кун?
Аноним 14/06/18 Чтв 20:31:18 40466254
>>40465
>А что нового узнал ты, интуиционист-кун?
Его вера в непогрешимость браузера ещё сильнее усилилась.
Аноним 14/06/18 Чтв 20:51:04 40467255
>>40460
>в привычном для твоей демагогии стиле
Что? Это мой второй пост в этом треде. Мне так и хочется предложить тебе принять таблетки, но я воздержусь.

Я, кажется, задал вполне конкретный вопрос, а в ответ получил какую-то не имеющую отношения к теме доски ерунду. Это печально.

>>40447
>>40461
Цитаты вот на этих картинках мне видятся весьма здравыми. Кто-нибудь из несогласных с ними может внятно объяснить, с чем именно он несогласен? Или у вас тут просто какая-то специальная олимпиада? Опять же, извиняюсь, но со стороны вот эти >>40466 >>40464 >>40463 >>40460 посты выглядят нерелейтед бредом шизика, которого непонятно почему еще тут не забанили. Это какой-то троллинг или я чего-то не понимаю?
Аноним 14/06/18 Чтв 21:26:20 40470256
Снимок экрана о[...].png 19Кб, 241x80
241x80
>>40467
> Это мой второй пост в этом треде
Аноним 14/06/18 Чтв 21:31:35 40471257
>>40467
Тебя приняли за человека, который некоторое время назад совершенно упорото, люто, дико, безумно воевал с математикой, подняв на знамена почему-то Брауэра. В адекватный разговор с тем человеком пытались, но понимания с его стороны не нашли. Он так затерроризировал сначала тред в /sci, а потом и всю эту доску, что аноны до сих пор реагируют очень нервно, стоит лишь тени этого безумца промелькнуть где-нибудь в уголке.
Аноним 14/06/18 Чтв 21:34:31 40472258
>>40471
Да это он же, ты что, не видишь? Он уже второй раз на моей памяти "пропадает", ждёт, чтобы на доску пришли ньюфаги, а потом возвращается за свежей едой.
Аноним 14/06/18 Чтв 21:35:43 40473259
>>40472
Ну или это мятежная душа Брауэра кочует из тела в тело. Как вариант.
Аноним 14/06/18 Чтв 21:37:14 40474260
>>40472
Есть некоторый шанс, что всё-таки не он. Впрочем, не пофиг ли.
Аноним 14/06/18 Чтв 22:42:30 40475261
>>40472
Проиграл
Потому что очень похоже на правду
Аноним 15/06/18 Птн 05:58:32 40479262
15224620502200.jpg 47Кб, 512x680
512x680
>>40465
> Вот я с начала этого треда успел продвинутую алгебру заботать, научился доказывать клёвые штуки про группы и поля.
Немалая часть практически полезной алгебры формализована в коковской либе ssreflect. Проще было кок поразбирать.
> А что нового узнал ты, интуиционист-кун?
А я таки нашёл общий подход к реализации изначальной программы Брауэра, чего он сделать не смог. Без всякой теории типов, машин Тьюринга и тезисов Чёрча, сам Брауэр бы не доебался. Алсо я говорил, что пилю прувер по мере возможности, так вот, почти готово :3
>>40471
> В адекватный разговор с тем человеком пытались, но понимания с его стороны не нашли.
Не было адекватного разговора. С самого 2016 года весь разговор с вашей стороны был точно такой же как сейчас, с маняаргументацией, от невменяемости которой хуеют даже мимокрокодилы.
> совершенно упорото, люто, дико, безумно воевал с математикой, подняв на знамена почему-то Брауэра.
Я никогда с математикой не воевал. С моей стороны на этот счёт было только утверждение о религиозном характере некоторых верований, которые натащили в математику ещё древние греки, а именно исключенное третье, актуальные бесконечности и платоновский мир идей. Ну и некоторые производные от этих верований, вроде догмы Гильберта.
Аноним 15/06/18 Птн 07:29:56 40482263
>>40479
>практически полезной
Практически полезной для чего/кого?
Аноним 15/06/18 Птн 08:04:32 40484264
pierre.jpg 93Кб, 850x400
850x400
we are from chop.png 278Кб, 503x335
503x335
>>40447>>40461
>>40479
В твоём понимании "математикой" называются теоретические основы функционального программирования, центральным результатом которых является "изоморфизм" Бойля-Кавендиша, устанавливающий связь между написанной на Clojure праграммой и канструктивным доказательством в смысле некоего Лёфа. Ничего из математики в общепринятом смысле ты при этом не знаешь.
Аноним 15/06/18 Птн 08:41:58 40487265
>>40484
> В твоём понимании "математикой" называются теоретические основы функционального программирования,
Нет, конечно же. Ты даже этого не понял, о чем тут говорить вообще.
>>40482
> Практически полезной для чего/кого?
Для чего/кого вообще полезна алгебра.
Аноним 15/06/18 Птн 08:56:39 40488266
15134215990580.png 200Кб, 851x400
851x400
grot.jpg 106Кб, 850x400
850x400
>>40487
Лямбда-калькулюс Барендрегта в математике не используется, он относится к праграммированию. Впрочем, у тебя считается, что праграммирование это и есть математика:
>Программисты и есть математики по изоморфизму Карри-Говарда, но ты же не осилил
>>31015
Только вот в изоморфизме Больцмана-Фарадея, который никто кроме тебя на мейл.ру не понял, ничего о математике не утверждалось: там устанавливается соответстветвие между конструктивной теорией типов Мартина Льва и лямбда-исчислением.
Аноним 15/06/18 Птн 09:10:15 40489267
15214963019640.jpg 43Кб, 759x635
759x635

>>40488
> ничего о математике не утверждалось: там устанавливается соответстветвие между конструктивной теорией типов Мартина Льва и лямбда-исчислением.
Зачем ты лезешь спорить, если нихуя не понимаешь в предмете? В чем твоя мотивация писать всякую хуйню и коверкать названия и имена? Просто пройти мимо богородица не велит? Propositions as sets/types - другое название изоморфизма Карри-Говарда. Забей в гуглтранслейт и постарался сравнить перевод с тем, что ты выше вытужил про типы и лямбду. Ты поди и про более известное соответствие между логическими и теоретикомножественные операции не слышал. И такой вот гейний будет мне что-то пояснять, лол.
Аноним 15/06/18 Птн 09:14:09 40490268
>>40488
> Лямбда-калькулюс Барендрегта в математике не используется, он относится к праграммированию.
А я ведь цитировал на этот счёт де Брауна и приводил в пример его проект automath. Что вы за хлебушки, все просто же как 3 копейки...
Аноним 15/06/18 Птн 09:22:52 40491269
hare barendregt.png 12Кб, 468x265
468x265
>>40490
After Curry emphasized the syntactic correspondence between Hilbert-style deduction and combinatory logic, Howard made explicit in 1969 a syntactic analogy between the programs of simply typed lambda calculus and the proofs of natural deduction. Below, the left-hand side formalizes intuitionistic implicational natural deduction as a calculus of sequents (the use of sequents is standard in discussions of the Curry–Howard isomorphism as it allows the deduction rules to be stated more cleanly) with implicit weakening and the right-hand side shows the typing rules of lambda calculus.
>>40490
>automath де Брауна
Это который книгу Ландау "Основы анализа" переписал в твоей лямбда-нотации? Ты бы хоть предисловие к ней прочитал, что ли, оттуда совершенно ясны цель и назначение данной книги:
>на каких основных фактах как на аксиомах можно без пробелов построить анализ и как это построение можно начать
Это "основания математики", не математика, разницу тебе неоднократно объясняли.
Аноним 15/06/18 Птн 09:23:11 40492270
>>40488
> Лямбда-калькулюс Барендрегта в математике не используется,
Ты даже не знаешь, что такое и зачем основания математики, раз такое пишешь.
Аноним 15/06/18 Птн 09:26:49 40493271
quote-church-81[...].jpg 51Кб, 850x400
850x400
church.png 1498Кб, 1024x768
1024x768
1.5. Охранник должен знать:
- изоморфизм Карри-Говарда и тезис Чёрча;
- содержание диссертации Брауэра в переводе Гейтинга;
- пять уровней языка и четыре способа отрицания по Маннури;
- интерпретацию логических констант по Брауэру-Гейтингу-Колмогорову;
- теорию статистического обучения Вапника и модель spikgram Миколова;
- отличия машины Тьюринга от машины Поста.
1.6 Охранник обязан:
- отрицать закон исключённого третьего;
- отрицать любую математику, не выразимую через типизированную лямбду в MLTT или нормальные алгорифмы Маркова;
- переписать на прувере AUTOMATH де Брауна книгу "Основы математического анализа" Ландау;
- представить все формальные теории в терминах алфавитов, термов и манипуляций с ними;
- свести гомологическую алгебру к исчислению предикатов, используя нумерацию Гёделя.
Аноним 15/06/18 Птн 09:41:44 40494272
lambda-ЧОП.jpg 194Кб, 800x600
800x600
Был ли Александр Гротендик математиком с точки зрения известного изоморфизма предпучка Барендргета на категории кубов с теорий типов Льва-Мартинеза?
Аноним 15/06/18 Птн 09:43:49 40495273
Можно ли учить математике через программирование? Типа делаешь свой язык программирования где числа это палочки и прочее такое. Попозже оптимизируешь. Делаешь свой вольфрам альфа. Потом свой доказатель-проверятор теорем.
Аноним 15/06/18 Птн 09:46:37 40496274
>>40495
Можно. Иными методами просто не получится в силу изоморфизма Гагарина-Авогадро в категории представлений машин Поста.
Аноним 15/06/18 Птн 09:54:28 40497275
>>40495
> Можно ли учить математике через программирование?
Нужно. ,21 век таки.
> Типа делаешь свой язык программирования где числа это палочки и прочее такое.
Зачем велосипед, все давно есть. Coq тот же.
Аноним 15/06/18 Птн 11:36:30 40498276
Какой язык праграммирования/аперационная система лучше всех подходит для занятий математикой? Миша Вербицкий использует Emacs, но я так же слышал положительные отзывы об R Markdown. Хотелось бы узнать про рабочие инструменты великого математика Мартина the Northern Lion Лёфа.
Аноним 15/06/18 Птн 12:43:58 40499277
8577237887dcae8[...].jpg 298Кб, 683x1024
683x1024
>>40498
Тебе ж подпекает с того, что mltt весь твой манямир рушит, типа любой кудахтер в математике может ровно то же что и ты, как минимум не меньше, а по факту в разы больше. Петросянством прохудившуюся веру не заштопать, привыкай.
Аноним 15/06/18 Птн 14:45:51 40501278
>>40493
>теорию статистического обучения Вапника
А случаем диакон-конструктивист и вапниколюб из ML треда программача это не одно лицо?
Аноним 15/06/18 Птн 15:15:32 40502279
>>40479
>Немалая часть практически полезной алгебры формализована в коковской либе ssreflect
А что там есть?
Аноним 15/06/18 Птн 15:45:19 40503280
>>40501
Одно. Ещё в /dr/ его посты можно найти.
Аноним 15/06/18 Птн 15:54:36 40505281
>>40493
Кстати, мы уже выяснили, в какой категории построен изоморфизм Гротендика-Садовничего?
Аноним 15/06/18 Птн 16:00:06 40506282
>>40505
В категории Hask сильно каррированных типов.
Аноним 15/06/18 Птн 16:17:21 40508283
>>40506
Но ведь Hask - не категория.
Аноним 15/06/18 Птн 16:59:28 40514284
15262546320880.jpg 53Кб, 576x432
576x432
>>40501
>>40503
Из вас сыщики ещё хуже чем математики. В /др я за всю жизнь ни одного поста не написал. А форсил я много что и кого, от нечёткой логики до Настеньки пикрелейтед. Только все это никакого отношения к теме треда не имеет. Впрочем, с моих постов никогда и никто так не рвался, как местный кловн, который походу все мои посты за последний год (если не больше) собрал. Я даже и сам уже не припоминаю, когда я тут про Вапника с Миколовым писал.
Аноним 15/06/18 Птн 17:18:17 40518285
>>40470
>>40472
Все-таки идите и принимайте таблетки. А лучше сразу отправляйтесь в /b или в /fag и там детектите своих божков.

>>40471
Это все замечательно, но на вопрос, заданный в >>40467-посте, все-таки не отвечает никак.
Аноним 15/06/18 Птн 17:21:23 40519286
>>40484
Я надеюсь, что это такой троллинг тупостью. Для подобного тут вроде есть тред математических мемов, а тут тред вроде про другое.
Аноним 15/06/18 Птн 17:39:08 40521287
>>40519
Этот тред не первый в цепочке. Изначально цепочка началась с наркоманских тредов про определение натуральных чисел. Так что безумие в традициях этого треда, для серьезной беседы о чем-то конкретном лучше отпочковаться.
Аноним 15/06/18 Птн 18:41:39 40522288
15242843658930.png 163Кб, 645x729
645x729
>>40518
> Это все замечательно, но на вопрос, заданный в >>40467-посте, все-таки не отвечает никак.
Главная претензия местного подгоревшего дурачка к Брауэру и интуиционизму в том, что из него прямо следует, что бездушная машина в плане математики может ровно столько же, сколько человек. Точнее, это следует из конструктивизма, Брауэр бы с таким выводом не согласился, но тонкие различия неоинтуционизма и различных направлений конструктивизма далеко за пределами способностей к пониманию тутошних дегенератов. По идее, критиковать им было бы логичнее Чёрча и Поста, но для этого нужно их хотя бы почитать, а там букв много и они нерусские какие-то. Это как с критиками эволюции, которые хуесосят Дарвина только потому что в школе больше ни про кого не рассказывают, хотя на деле все их претензии относятся к современной СТЭ, а Дарвин вообще верующим был.
Аноним 15/06/18 Птн 19:04:04 40523289
>>40522
А что бесконечные множества ни в каком виде изучать нельзя, ты не упомянул.
Аноним 15/06/18 Птн 19:42:11 40525290
>>40514
>все мои посты за последний год (если не больше) собрал
Я думал может что-то новое придумаешь, чем упоминать автомат деБрауна по сто раз.
Аноним 15/06/18 Птн 19:42:18 40526291
>>40523
> А что бесконечные множества ни в каком виде изучать нельзя, ты не упомянул.
Можно. И даже упомянул, в какой статье Брауэр доказывает, что алеф-нуль единственная бесконечность, за которой могут стоять правила построения, и что нет ни одного внятного доказательства, что последующие алефы больше, чем алеф-нуль. Все это я упоминал и неоднократно.
Аноним 15/06/18 Птн 19:45:02 40527292
14939065393810.jpg 24Кб, 200x284
200x284
>>40525
> Я думал может что-то новое придумаешь, чем упоминать автомат деБрауна по сто раз.
Если бы ты хотя бы понял, о чем он, можно было бы и что-то более новое упомянуть. А так и этого слишком.
Аноним 15/06/18 Птн 19:47:47 40528293
>>40527
Но ты же не понял, что книга Ландау не имеет отношения к математике. Сам Ландау этого не скрывал, указал в предисловии даже.
Аноним 15/06/18 Птн 19:55:07 40530294
>>40526
Ну в inaccessible cardinals ты всё еще не веришь. Значит отрицаешь существование топосов, ведь они требуют аксиомы универсума (эквивалентна аксиоме недостижимого кардинала). Хотя ранее и про них что-то упоминал.
Аноним 15/06/18 Птн 20:04:31 40531295
>>40526
Допустим, что есть биекция f между N и множеством всех подмножеств N. Если x - натуральное число и f(x) = M, то x либо является элементом M, либо не является. В зависимости от этого будем называть натуральные числа соответственно: самопринадлежащие и несамопринадлежащие.

Пусть A - множество в точности всех несамопринадлежащих натуральных чисел. Так как f - биекция, существует натуральное число a такое, что f(a) = A.

Если a является самопринадлежащим, то a является элементом A и потому должно являться несамопринадлежащим. Противоречие.

Если a является несамопринадлежащим, то a является элементом A и потому является самопринадлежащим. Снова противоречие.

Таким образом, биекции f существовать не может.
Аноним 15/06/18 Птн 20:04:39 40532296
>>40528
> Но ты же не понял, что книга Ландау не имеет отношения к математике. Сам Ландау этого не скрывал, указал в предисловии даже.
Эта книга вообще не при чем. Речь о самом прувере automath и почему и что и как его возможности позволяют доказать в математике. Де Браун ясно писал, почему этот прувер не привязан ни к какой аксиоматике, в качестве таковой хоть 10 заповедей можно использовать.
Аноним 15/06/18 Птн 21:00:41 40533297
>>40521
Если подумать, то немного печально, что для бесед об основаниях математики надо отпочковаться от треда об основаниях математики.

>>40522
Так я ведь в том и дело, что я даже ни Брауэра, ни интуиционизм не упоминал. Я специально с самого начала вопрос сформулировал максимально широко, а в ответ получил какую-то шизофрению.

Более того, уже сколько постов прошло, а никто так и не сформулировал претензий к цитатам на пиках. Видимо и вправду это все насеменил один местный поехавший. Впрочем, ладно, бог с ним.
Аноним 15/06/18 Птн 23:17:56 40538298
>>40522
>ровно столько же, сколько человек.
Но машины не могут доказывать теоремы, только проверять.
Аноним 16/06/18 Суб 00:11:23 40539299
>>40538
> Но машины не могут доказывать теоремы, только проверять.
Могут. Т.н. тактики в коке кв раз для этого. Но ты веровай и дальше, что не могут, семень тут, неси хуйню про охранников. Вдруг правда поможет.
16/06/18 Суб 17:09:52 40573300
>>40539
Миллионы обезьян, печатающие на печатных машинках случайные символы тоже могут доказывать теоремы. Конструктивные по крайней мере. Вся суть конструктивизма кароче.
Аноним 16/06/18 Суб 17:50:59 40574301
>>40573
>Миллионы обезьян
Это ты про homo sapiens?

Ах, нет, забыл. Ведь у этих есть одно очень важное отличие от всех остальных обезьян: богоизбранность. Главное - верить.
16/06/18 Суб 18:00:26 40575302
>>40574
> мам я такой же умный как математики, ведь я тоже сделан из кварков и электронов)))
Любых обезьян, даже конструктивисты справятся.
Аноним 16/06/18 Суб 19:01:52 40576303
>>40573
>>40575
Угадал я значит, причина твоего копротивления - скрепы. Ничем ты не уникальнее обезьяны, и машина Тьюринга может ровно столько же сколько и ты, в том числе и в манипуляции с нарисованными значками, за которыми не стоит ничего. Алгоритмически неразрешимую задачу ты никак не решишь, впрочем и это уже обсуждали, ты тогда знатно обпучкался, показав что понятия не имеешь об идентификации систем. Короче, все с тобой ясно, опученный.
Аноним 16/06/18 Суб 20:20:17 40578304
>>40576
То есть - никак? Алгоритмически неразрешимое решается доказательством алгоритмической неразрешимости. См. Пенроуз, почему человек не машина Тьюринга.
Аноним 16/06/18 Суб 20:27:03 40579305
>>40576
Алгоритмически неразрешимые задачи легко решаются применением исключённого третьего.
16/06/18 Суб 20:50:21 40585306
>>40576
>и машина Тьюринга может ровно столько же сколько и ты
Доказательство где? Или ты адепт свидетелей машины Тюринга? Понятненько, верунство очередное.

Шёл как-то Иван по лесу. Глядит — счётчик Гейгера лежит. Обрадовался: "Это ж я все теоремы сейчас докажу!". Сел на пенёк и стал записывать. Счёлк. "О теоремку подвезли". Наслюнявил Иван карандаш и стал писать.

Долго так писал. Внезапно счётчик затрещал так, что Ивану захотелось третью руку — в две руки не успевал записывать — а потом внезапно затих. Пока Иван крутил находку, за спиной, близко-близко, раздался звучный бас Есенина-Вольпина:
— Так-так-так, что тут у нас? Теоремки доказываем?
Иван растеряно посмотрел на незванного гостя и промычал что-то среднее между "угу" и "при Сталине такой хуйни не было". Есенин-Вольпин взял тетрадочку, полистал и говорит:
— Всё верно, молодой человек, вот вам за ваши труды два яблочка.
— Но я ещё не закончил, жду вот когда счётчик снова теоремы доказывать станет, — растерялся Иван.
— О-о-о, юноша, так вы верующий, — покачал головой гость, — Веруете в эту вашу бесконечность. А вы её видели? А? Видели? То-то и оно, нет её и всё тут. Не будет больше трещать, все трески закончились в этом вашем совке. А вы тут сидите и веруете, что оно снова трескать будет. У-у-у, ненавижу совок ебаный.
Старик сжал кулаки и устремил взгляд в осеннее небо.
Тут из кустов выскочили санитары, повязали деда и поволокли куда-то, а он всё кричал: "Закончились трески! Я их ещё в прошлом году все использовал!"

Иван долго смотрел им в след, пока из оцепенения его не вывел заветный доказыватель теорем очередной серией тресков. Работа чуть было не закипела, но тут Иван заметил, что рядом стоит грузный мужчина в пижонской шубе и с тростью. Иван насторожился.
— О, яблочки. Разрешите угоститься, — сказал мужик и недождавшись ответа схватил яблоко и откусил здоровенный кусок, — Ну не смотрите на меня так, у вас яблока много, не жалейте для доброго человека.
— Всего-то два.
Мужик подовился:
— Простите, что? Вы в текущем году веруете в целые числа? А вы их видели то, целые числа эти? А? Видели? Коров небось считали, да яблоки, и думали, вот они — целые числа. Но это всего-лишь приближение реальности, в которой нет никаких целых чисел, ибо всё вокруг непрерывные физические поля, вот где в уравнении Шрёдингера целые числа?..
Но Иван не дал ему закончить, бросив всё, включая солитонный сгусток яблочной материи, он вскачил и стремглав помчался в чащу леса, чтобы жить там и больше никого не видеть, а питаться только супом из ромашек.
Аноним 16/06/18 Суб 21:21:36 40587307
>>40576
И как же тогда человечестов до конструктивизма и комплюктера вычисляло и пользовалось богомерзкими верованиями в физике?
Аноним 16/06/18 Суб 21:28:38 40588308
Аноним 16/06/18 Суб 22:09:35 40592309
Аноним 16/06/18 Суб 22:43:39 40593310
>>40578
> То есть - никак? Алгоритмически неразрешимое решается доказательством алгоритмической неразрешимости.
Это не решение.
> См. Пенроуз, почему человек не машина Тьюринга.
Извини уж, третьесортный научпоп я не читаю.
>>40579
> Алгоритмически неразрешимые задачи легко решаются применением исключённого третьего.
Исключенноетретье можно и в коке прописать. Это уход от решения, а не решение.
>>40585
> Доказательство где? Или ты адепт свидетелей машины Тюринга? Понятненько, верунство очередное.
Доказательство чего, мань? Того, что ты выше алгоритма не прыгнешь? Так это факт. См выше
>>40587
> И как же тогда человечестов до конструктивизма и комплюктера вычисляло и пользовалось богомерзкими верованиями в физике?
Чего несешь-то? Прочитай хоть на что отвечаешь.
Аноним 16/06/18 Суб 22:47:20 40594311
15290728202200.jpg 35Кб, 807x606
807x606
>>40579
> Алгоритмически неразрешимые задачи легко решаются применением исключённого третьего.
Проблему останова ты тоже исключённых третьим решишь? Да и правда, или остановится, или нет))))0) И как Тьюринг до такого гениального варианта не додумался?
Аноним 16/06/18 Суб 22:57:34 40595312
Исключенное третье в математике использовать это просто верх гениальности на самом деле. Зачем вычислять, если можно назвать ответ от балды, все равно он или правильный или нет. 3*3=? Ну или 7 или не 7, очевидно же))0))
Аноним 16/06/18 Суб 23:40:04 40596313
>>40593
Почитал я про кок и всё равно не вижу, где тут программа что-то доказывает сама. Приведи простой пример кода, который что-то доказывает. По сути мы просто задаём систему аксиом, пишем доказательство, запускаем шайтан-машину, и либо на выходе будет противоречие, либо всё ок.
Аноним 16/06/18 Суб 23:59:55 40597314
>>40593
>Чего несешь-то? Прочитай хоть на что отвечаешь.
Люди пользовались бесконечностями и прочими нормальными вещами, приходя к решению тех или иных задач, в отличии от догматиков с манятеориями в которых они не могут досчитать до двух.

Даже если под всем этим на самом деле конструктивное начало и все можно свести к нему, это не отменяет полезность, отвергаемых конструктивными сектантами, ментальных конструкций.
Аноним 17/06/18 Вск 00:01:44 40598315
>>40597
>ментальных конструкций
Ты этим словосочетанием больное место задел.
Аноним 17/06/18 Вск 00:02:56 40599316
>>40596
Ну там есть тактики вроде omega, которые докажут за тебя, если доказываемые вещи можно свести к Presburger arithmetic, но это именно что proof assistance, а не доказательство чего то нового машиной.

Мимо
17/06/18 Вск 00:57:19 40600317
>>40593
>Так это факт
Тогда тебе не составит труда его доказать.

>Почитал я про кок и всё равно не вижу, где тут программа что-то доказывает сама.
Никак не доказывает, тактики это чуть лучше, чем кататься ебалом по клаве, пока прувер не перестанет ругаться.
Аноним 17/06/18 Вск 01:22:35 40602318
>>40599
>если доказываемые вещи можно свести к Presburger arithmetic
Согласно тезису Чёрча это и есть вся математика.
17/06/18 Вск 01:33:29 40603319
Таким образом аргументация коконструктивста ИТТ сводится к тому, что верить ни в какие принципы нельзя. При этом он сам:

1. верит в целые числа
2. верит в (хоть и в потенциальную, но) бесконечность
3. верит в существование абстрактных идей
4. верит в то, что человеческий мозг в точности машина Тьюринга
5. верит что пека с виндой, лемуры, генератор случайных чисел и rule 110 могут доказывать теоремы, просто почему-то этого не делают, стесняются наверное

Можно ещё пройтись по вере в реальность и по органам чувств, но это же не /ph так что пока не будем.
Аноним 17/06/18 Вск 01:47:22 40604320
>>40585
Все хейтеры конструктивизма такие шизики или это особый экземпляр попался?
Аноним 17/06/18 Вск 01:51:12 40605321
15135989019340.png 389Кб, 504x597
504x597
>>40597
>ДИДЫ ВЫЧИСЛЯЛИ!!111
Аноним 17/06/18 Вск 01:58:53 40606322
>>40604
Я не хейтер конструктивизма, я просто не возвожу его в религию.
Аноним 17/06/18 Вск 02:41:22 40607323
>>40604
Ты думаешь, что бредовые идеи типа конструктивизма нужно обсуждать на серьёзных щщах. А на самом деле конструктивизм нужно сразу посылать нахуй. Как ферматиков, как православную арифметику.
Аноним 17/06/18 Вск 03:06:14 40608324
>>40607
> Ты думаешь, что бредовые идеи типа конструктивизма нужно обсуждать на серьёзных щщах. А на самом деле конструктивизм нужно сразу посылать нахуй.
Только потому что одному дегенерату с мейлру за свои скрепы обидно? Оно того не стоит.
Аноним 17/06/18 Вск 04:42:31 40609325
Предлагаю обсудить это >>40531 доказательство. Верное ли оно? Если нет, то где в нём ошибка?
Аноним 17/06/18 Вск 06:21:40 40612326
>>40609
Давай лучше вот это доказательство >>40595 обсудим. Если оно верно и в математике вообще допустимо так доказывать, это же вообще все меняет.
Аноним 17/06/18 Вск 06:32:30 40613327
>>40612
Но в том посте нет никаких доказательств же.
Аноним 17/06/18 Вск 07:22:30 40614328
15258856983421.jpg 29Кб, 460x460
460x460
>>40613
> Но в том посте нет никаких доказательств же.
Формально я имел в виду:
?(?, ?) =\/ != 42, где ?() любой оператор, ? в скобках - любая переменная или константа. В общем, ?(?, ?) - любое выражение или лямбда терм. Пример: 1+1 =\/ != 42. Вопрос, допустимо ли так доказывать, если исключенное третье считать допустимым для использования в математике? И если да, зачем тогда вообще математика, если любое выражение можно просто поместить в левую часть "уравнения или не уравнения", и оно будет истинным?
Аноним 17/06/18 Вск 09:14:50 40616329
>>40602
Ага, а умножение натуральных чисел это маняфантазии верунов.
Аноним 17/06/18 Вск 09:57:58 40617330
>>40596
> По сути мы просто задаём систему аксиом, пишем доказательство, запускаем шайтан-машину, и либо на выходе будет противоречие, либо всё ок.
Нет, плохо ты читал. Доказательство не пишем, пишем теорему или теоремы. А кок выдаёт доказательство, если оно возможно в используемой аксиоматике. Это не то же самое, что написать доказательство самому и проверить. Короче, опучкался ты, снова.
Аноним 17/06/18 Вск 12:03:59 40621331
>>40617
Только вот на практике тактики кока не справляются с доказательством содержательных теорем. И даже более того, как правило они не справляются просто с тем, чтобы находить доказательства для переходов очевидных с точки зрения квалифицированных в релевантной области математиков, которые были бы просто опущены в статье.

Аноним 17/06/18 Вск 12:57:49 40624332
>>40621
Какие детсадовские попытки заштопать манямир, даже за шиворот ссать жалко лол. Некоторые подмножества исчислений CiC в коке уже сейчас полностью разрешимы с помощью тактик. Насчет остальных - это только вопрос времени, т.к. там более сложные исчисления, не все из которых даже исследованы нормально, Барендрегт и еще 3,5 исследователя все точно не вывезут. Дело только в этом, но ты этого даже не понимаешь, как не понимаешь ,что вообще такое кок и что и как он делает. Отсюда и твои жалкие потуги, "на практике тактики кока не справляются с доказательством содержательных теорем", "очевидных с точки зрения квалифицированных в релевантной области математиков,".
17/06/18 Вск 13:51:25 40626333
>>40624
Люблю твои сказочки, захожу почитать перед сном как счётчики Гейгера, лемуры и петух доказывают теоремы. И всё сами! Жаль результатов нет, ну наверное просто тетрадочку с теоремами теряют. Ну или ты нассал себе за шиворот и штопаешь свой манямир, который в реальности состоит из 4.5 аутистов, который занимаются вопросами логики, а не математикой.
Аноним 17/06/18 Вск 13:51:39 40627334
>>40595
А что не так то? Там где тебе нужно знать точное значение это очевидно не подойдет, но если тебе нужно только знать что 7 или не 7 то в чем проблема то?
Аноним 17/06/18 Вск 13:59:46 40628335
>>40602
Корень из двух хотя бы до 5 знаков я смогу в твоей маняарифметике найти?
Продемонстрируй короткий кхе-кхе пример.

>>40605
Ну если дидовские методы позволяют, благодаря удобству дидовской математики, ебать законы природы и в хвост и в гриву, а в теории маняформализаторов вычислять можно только до одного то опять таки не вижу проблемы.

Только школьники и упоротые долбоебы будут в погоне за модой отвергать удобные вещи ради NEW SUPER COOL COQSTRUCTIVIST THIORY 2k18 COUNT FOR 3 POSIBEL.

И уж тем более долбоебизм называть только это МАТЕМАТИКОЙ. Все хуйня кроме пчел, да
17/06/18 Вск 14:01:27 40629336
Аноним 17/06/18 Вск 14:36:33 40630337
>>40627
> А что не так то?
Да все так в принципе. Считай, я всю математику доказал априори >>40614 круто, а? Прикинь, берешь любую теорию, делаешь ее арифметизацию геделевскими номерами, дальше как в моём посте. И все, либо 42 либо нет.
Аноним 17/06/18 Вск 14:38:07 40631338
>>40629
> Ой, а чё так кода много?
Я проще придумал >>40630 всю математику доказал, я ж крут, а?
Аноним 17/06/18 Вск 14:39:41 40632339
>>40630
Это все конструктивисты настолько не знакомы с математикой, или ты один такой?
Аноним 17/06/18 Вск 17:07:47 40638340
>>40632
> Это все конструктивисты настолько не знакомы с математикой, или ты один такой?
Давай так. Исключенное третье допустимо использовать как доказательство в математике? Да или нет?
Аноним 17/06/18 Вск 17:17:25 40639341
>>40638
Что значит "использовать как доказательство"? Это схема аксиом вообще-то. Ты какие книжки по логике читал?
Аноним 17/06/18 Вск 18:25:18 40643342
>>40638
Конечно, а как иначе? Приведи простенький пример, показывающий ущербность исключённого третьего.
Аноним 17/06/18 Вск 18:29:06 40644343
>>40643
>>40638
Ну правда, есть два состояния, истина и ложь, при таком раскладе нечто либо истинно, либо ложно, третьего состояния нет. В чём тут брешь по твоему?
Аноним 17/06/18 Вск 18:34:32 40645344
Аноним 17/06/18 Вск 19:17:03 40646345
>>40645
1+1 = \/ != 42, ну да, это верно. Либо равно, либо нет. Я не понял к чему ты это?
Аноним 17/06/18 Вск 19:18:06 40647346
>>40646
Просто это верно так же, как верно 2 = 2. В чём тут доказательство? Это всегда верно, да. Не понимаю тебя.
Аноним 17/06/18 Вск 21:18:23 40648347
>>40647
> Просто это верно так же, как верно 2 = 2.
Нет, не так же. 2=2 это вычисление. А 2 =\/ != 2 это исключенное третье.
Аноним 17/06/18 Вск 21:28:32 40649348
>>40648
Нет, 2=2 это закон тождества.
Аноним 18/06/18 Пнд 05:59:59 40656349
>>40649
> Нет, 2=2 это закон тождества.
Вообще-то в математике это доказывается. И "доказательство" уровня той картинки с Пифагором и подписью "хуле тут доказывать, и так видно" это не серьёзно.
Аноним 18/06/18 Пнд 06:37:15 40657350
>>40656
Вообще - нет, не доказывается. Символ равенства вводится не на уровне математических теорий, а на уровне формального языка. Аксиомы на него налагаются тоже не математикой, а нижележащей логикой.
Аноним 18/06/18 Пнд 09:14:49 40658351
>>40657
> Вообще - нет, не доказывается. Символ равенства вводится не на уровне математических теорий, а на уровне формального языка. Аксиомы на него налагаются тоже не математикой, а нижележащей логикой.
Сам себе противоречишь. Отношение равенства задается правилами, да. Применение правил этих в каждом конкретном случае возможно только путём вычисления результата. Конечно, так никто не делает, разве что прувер. Человек просто запоминает, что любое число равно самому себе. И в такой форме это уже является лингвистическим правилом, а не математическим, т к не при этом не используется вычислений.
Аноним 18/06/18 Пнд 09:55:25 40659352
150817716678.jpg 49Кб, 1280x720
1280x720
Есть ли математические основания на пучках онли без богомерзской вычислимости?
Аноним 18/06/18 Пнд 10:04:49 40660353
>>40659
> Есть ли математические основания на пучках онли без богомерзской вычислимости?
На пучках - HoTT, а без вычислимости - ZFC.
Аноним 18/06/18 Пнд 10:06:25 40661354
15126183241560.png 723Кб, 464x391
464x391
>>40660
А пучки канструктивны?
Аноним 18/06/18 Пнд 13:00:36 40665355
>>40658
Сначала прочитай учебники, потом пиши итт.
Аноним 18/06/18 Пнд 13:06:21 40666356
>>40665
> Сначала прочитай учебники, потом пиши итт.
Будто я что-то не так сказал.
Аноним 18/06/18 Пнд 13:34:19 40667357
Какие в конструктивизме аксиомы?
Аноним 18/06/18 Пнд 14:50:55 40668358
Аноним 18/06/18 Пнд 15:29:25 40669359
>>40661
Я так и не понял, зачем тот анон колоски к моей пикче приделал.
Лучше бы вместо аэропорта на фоне зал МГУ сделали.
Аноним 18/06/18 Пнд 15:33:06 40670360
Martin-LofPer.jpg 525Кб, 1600x1200
1600x1200
>>40667
В нём нет никакой веры, в нём есть только правила построения. Конструктивизм ведь создавался величайшими математиками, а не ебанатами с мейлру. Впрочем, всё это я объяснял уже сто раз, но вы на мейлру не способны осилить даже известные работы Тьюринга, что уж говорить про действительно глубокие работы Мартина-Лёфа и других 3,5 исследователей в этой области.
Аноним 18/06/18 Пнд 15:54:44 40671361
>>40669
>колоски
Урожаи и посевы Гротендика же.
Аноним 18/06/18 Пнд 16:08:18 40672362
>>40670
Правила построения - просто частный случай правил вывода. Ничего нового в них нет.
Аноним 18/06/18 Пнд 16:13:01 40673363
>>40671
Лол, странно что не вспомнил. Спасибо.
Аноним 18/06/18 Пнд 16:37:49 40674364
>>40670
Почему у тебя именно с Мартин-Лефа так жопа горит?
Аноним 18/06/18 Пнд 17:49:15 40676365
>>40668
Ты слился.

мимо
Аноним 18/06/18 Пнд 18:07:22 40677366
>>40670
Мань, тот факт, что исчисление для теории типов несколько отличается по формату от гильбертовских исчислений для классических теорий (в первых в основном все формулируется через правила, во вторых в основном через аксиомы) - это просто вопрос формата задания и те и другие исчисления на самом деле допускают переформулировки в обоих стилях. Что более существенно -это то, какие стили математических рассуждений эти исчисления призаны моделировать. В случае с теорией типов Марти-Лёфа соответствующий тип рассуждений - это рассуждение в терминах индуктивных конструкций. И такие рассуждения активно опираются на абстракцию потенциальной бесконечности (и да, для того чтобы принимать такие рассуждения нужно верить в эту абстракцию.
Аноним 18/06/18 Пнд 20:58:50 40681367
>>40677
> (и да, для того чтобы принимать такие рассуждения нужно верить в эту абстракцию.
Эта абстракция подразумевается например при задании правил построения типа N. Допустим, я в неё не верю. И что, у меня от этого перестанет работать например тактика ring в коке? Веровать можно в нечто изначально оторванное от построения, точнее в допустимость использования такого.
Аноним 19/06/18 Втр 09:11:43 40683368
>>40681
Стандартное определение типа N - это по существу определение натуральных чисел через приписывание палочек. Это действительно базовая вещь явно подкрепленная нашим практическим опытом. Но теория типов производит очень широкое обобщение этого и в ней таким образом строятся не только натуральные числа, а населяется вся вселенная типов, включающая замысловатые функционалы высших типов, вселенные (во внутреннем смысле) и т.п. И здесь связь с практическим опытом разумеется теряется, остается только верить в то, что все правила построения новых функционалов сохраняют потенциальную вычислимость на любых входах которые потенциально могут быть построены в рамках незаконченной вселенной.

Кстати, проблемы с теорией множеств носят такой же характер, только там они вместо переноса интуиции касающийся натуральных чисел на высшие типы, они перенесли интуицию касающуюся конечных множеств на произвольные. Что характерно, в первых попытках построить формальные теории и там и там нашли противоречия (см. парадокс Жирара и парадокс Рассела соответственно).
Аноним 19/06/18 Втр 10:21:53 40685369
>>40683
Ты думаешь, хоть кто-то итт не знает про парадокс Рассела?
Аноним 19/06/18 Втр 11:41:26 40686370
>>40683
> (см. парадокс Жирара и парадокс Рассела соответственно).
Парадокс Жирара тривиально обходится кумулятивной иерархией типов, я вообще не знаю, о чем Мартин-Леф думал, когда вводил правило type : type, очевидно же, что сразу надо было что-то вроде type i : type i+1.
> И здесь связь с практическим опытом разумеется теряется, остается только верить в то, что все правила построения новых функционалов сохраняют потенциальную вычислимость на любых входах которые потенциально могут быть построены в рамках незаконченной вселенной.
Это ещё у Брауэра решено, 2ой акт интуиционизма. Построение делается только на основании уже построенного ранее более простого, либо по некоторым критериям равенства с уже построенным. Какой угодно функционал своим к более простому, у того же Мартин-Лефа суждения (общие схемы посылок и заклбчений в правилах) рассматриваются по нарастающей сложности, для одной переменной, для двух и для n.
> Кстати, проблемы с теорией множеств носят такой же характер, только там они вместо переноса интуиции касающийся натуральных чисел на высшие типы, они перенесли интуицию касающуюся конечных множеств на произвольные.
И тут же обосрались, потому что всякие недостижимые кардиналы не строятся на основе конечных множеств, как построения в теории типов или интуиционизме, а просто вероваются от балды, причём нет даже внятных пруфов того, что алеф1 больше чем алеф-нуль, на что Брауэр указывал ещё в 1912 году.
Аноним 19/06/18 Втр 12:48:34 40688371
>>40686
>Парадокс Жирара тривиально обходится кумулятивной иерархией типов, я вообще не знаю, о чем Мартин-Леф думал, когда вводил правило type : type, очевидно же, что сразу надо было что-то вроде type i : type i+1.
Ну да, ровно также как обошли парадокс Рассела. А тот факт, что Мартин-Лёф облажался показывает, что ровно также как и у теоретико-множественников наивная интуиция теоретико-типовиков подвережена парадоксам.
>либо по некоторым критериям равенства с уже построенным
Это ключевое место. Фунции в теории типов могут применяться к любым термам соответствующего типа, в частности к термам которые будут введены после введения этой фунции. И чтобы считать, что даже какая-то очень простая фунция (например следования на натуральных числах) тотальна нужно предполагать, что любой терм который когда-либо может быть построен будет равен терму в канонической форме (т.е. в данном примере по нему можно вычислить конкретное натуральное число). Другими словами происходит использование глобальных свойств ещё незаконченной вселенной. На мой взгляд совершенно правильно называть это верой, если мы называем верой пригятие вселенной множеств фон Неймана.

Теорию множеств ты совсем не понимаешь. Недостижимые кардиналы прямой аналог вселенных в теории типов т.к. каппа недостижим если и только если капповый уровень вселенной фон Неймана модель ZFC. И если Брауэр не принимал аксиому степени, то конечно он не принимал существования несчетных мощностей. Просто одни люди произвели более широкре обобщение простой конечной математики, а некоторые (Брауэр) менее широкое.
Аноним 19/06/18 Втр 13:22:18 40690372
>>40688
> Другими словами происходит использование глобальных свойств ещё незаконченной вселенной. На мой взгляд совершенно правильно называть это верой,
А какие могут быть проблемы с правильно типизированными термами?
> Недостижимые кардиналы прямой аналог вселенных в теории типов
Вообще, разница в использовании актуальной бесконечности. В теории множеств это делать не стесняются, в отличие от. Но если ты говоришь, что речь об аналоге иерархий вселенных, и допустимо написать, например алеф-нуль : алеф1 и в целом алеф i : алеф i+1, тогда вообще интересно получается. Так ведь можно сказать и про мир идей Платона и тогда выходит, что Платон был конструктивистом, а в основаниях математики кроме конструктивизма ничего никогда и не было.
Аноним 19/06/18 Втр 13:48:24 40691373
>>40690
>в отличие от
RUSSIAN MOTHERFUCKER DO YOU SPEAK IT

>Так ведь можно сказать и про мир идей Платона и тогда выходит, что Платон был конструктивистом, а в основаниях математики кроме конструктивизма ничего никогда и не было.
Преемственность, слыхал о такой?
Никакого конструктивизма не было и нет, было развитие идей обычной математики. Просто несколько хитрецов грамотно пропиарились выделив это во что-то непохожее и назвав другим словом.
Аноним 19/06/18 Втр 14:09:53 40694374
>>40690
>А какие могут быть проблемы с правильно типизированными термами?
Никаких проблем с теорией типов у меня нет. Просто при рассуждениях в ней в общем случае неявно используется предположение, что все термы данного типа, которые потенциально могуть быть построены в процессе (сколь угодно длительной) деятельности в теории типов, могут быть полностью вычислены. Это сильное предполжение, на самом деле я не знаю, как такое предположение обосновать не аппелируя к законченному построению вселенной т.е. к актуальной бесконечности; что гаходит свое отражение в том, что в определенных версиях теории типов Мартин-Лёфа можно доказать непротиворечивость некоторых непредикативных классических теорий. Если ты хочешь верить в это и считать базовым принципом - пожалуйста. Но просто здесь нет принципиальной разницы с верующими в разные большие кардиналы.

Это впрочем не умаляет достоинств теории типов в смысле возможности извлечения конкретных алгоритмов из конкретных доказательств.
Аноним 19/06/18 Втр 14:36:01 40696375
>>40686
Алеф 1 больше Алеф 0 по определению, если ты не в курсе.
Аноним 19/06/18 Втр 15:19:49 40698376
>>40694
> Просто при рассуждениях в ней в общем случае неявно используется предположение, что все термы данного типа, которые потенциально могуть быть построены в процессе (сколь угодно длительной) деятельности в теории типов, могут быть полностью вычислены.
Почему "неявно"? Это явное предположение. И оно прямо вытекает из правил построения. Если у нас есть правила построения N, то из них прямо следует потенциальная построимость любого элемента этого типа. То же с любым другим типом, любой терм, являющийся элементом этого типа строится по правилам построения элемента этого типа, т.е. этот терм правильно типизирован, в противном случае он не является термом данного типа. Мы не можем взять этот элемент из мира идей Платона, мы его можем либо построить явно, либо задать общее правило построения, либо задать правила его вычисления из какого-то другого терма (бета- и др. редукции итд).
> Это сильное предполжение, на самом деле я не знаю, как такое предположение обосновать не аппелируя к законченному построению вселенной т.е. к актуальной бесконечности;
Вот ты говоришь, что я не понимаю теорию множеств, а ты похоже, не понимаешь разницу между потенциальной и актуальной бесконечностью. Правило построения "type i : type i+1" это потенциальная бесконечность, а аксиома "существует бесконечное множество" - это актуальная.
>>40696
> Алеф 1 больше Алеф 0 по определению, если ты не в курсе.
Если это понимать в смысле, указанном предыдущим оратором >>40688 то да, т.к. получается кумулятивная иерархия типов. Но тогда это конструктивизм простой, от которого тут кое-кто рвется уже пару лет. Если же понимать это с позиции теории множеств, то Брауэр пояснил, какие пробемы из этого вытекают.
>>40691
> Никакого конструктивизма не было и нет, было развитие идей обычной математики
Брауэр и за это пояснял, в чем разница. Ты тут точно ничего нового не скажешь, поверь.
Аноним 19/06/18 Втр 15:27:38 40699377
>>40698
Дай определение алефа-1. Ты его как-то по-своему понимаешь, похоже.
Аноним 19/06/18 Втр 15:31:55 40700378
>>40699
У алефа-1 в смысле теории множеств нет внятного определения, так как не даны правила построения.
Аноним 19/06/18 Втр 15:49:26 40701379
>>40700
Ты используешь этот термин. Что лично ты под ним понимаешь?
Аноним 19/06/18 Втр 15:55:12 40703380
>>40701
Я под ним понимаю некое религиозное верование. Алефы выше алефа-0 невозможно понять человеческим мозгом, так как для них нет правил построения. Это следует из применения тезиса Чёрча к пояснению Брауэра о невозможности вычисления алефа-1 и выше.
Аноним 19/06/18 Втр 15:56:41 40704381
Я вот думаю, конструктивизм, он как дальтонизм. Есть люди, спокойно воспринимающие цвета и видящие их все. А есть, те которые видят мир черно-белым. Конструктивисты, как дальтоники, неспособны понять бесконечность, когда нормальные люди абсолютно без проблемы работают с ней.
Аноним 19/06/18 Втр 15:59:12 40705382
>>40704
> Конструктивисты, как дальтоники, неспособны понять бесконечность, когда нормальные люди абсолютно без проблемы работают с ней.
С чем ты там работаешь? То, что ты понимаешь под "работой с бесконечностью" - чисто лингвистические, а не математические построения.
Аноним 19/06/18 Втр 15:59:20 40706383
Вот, и когда здоровый человек пытается рассказать дальтоники о других цветах, тот неспособен их представить и понять, пытается всё выразить своим ограниченым взгядом, и после неудачной попытки влючается ВРЁТИ ДРУГИХ ЦВЕТОВ НЕ СУЩЕСТВУЕТ, ВЫ В НИХ ВЕРИТЕ, ДРУГИЕ ЦВЕТА, КАК АЛЛАХ!
Аноним 19/06/18 Втр 16:00:46 40707384
>>40706
Рассказать можно и про гаррипоттера с файрболами. Того же уровня твое понимание бесконечности.
Аноним 19/06/18 Втр 16:01:08 40708385
>>40705
А что понимает здоровый человек, когда говорит о цветах, неспособных быть увиденными дальтоником?
Аноним 19/06/18 Втр 16:01:08 40709386
>>40703
Ты сделал утверждение об алефе-1. Ты отказываешься объяснить, что ты подразумеваешь под термином "алеф-1".
Аноним 19/06/18 Втр 16:01:48 40710387
Я вот думаю, алефизм, он как даунизм. Есть люди, спокойно понимающие разницу между абсолютной и потенциальной бесконечностью. А есть те, которые видят мир исключительно через свою веру. Алефисты, как дауны, неспособны понять концепцию правил построения, когда нормальные люди абсолютно без проблем понимают её и каждый день работают с правилами построения.
Аноним 19/06/18 Втр 16:02:42 40711388
>>40707
Как по-твоему можно выразить цвета разных оттенков через черный и белый? Как синий выразить через них? То же самое и с конструктивной математикой.
Аноним 19/06/18 Втр 16:03:12 40712389
>>40709
Я понимаю под этим термином объект религиозной веры вроде Христа или Аллаха, тут можно много чего подставить, но результат один - невычислимая хуета.
Аноним 19/06/18 Втр 16:04:56 40713390
>>40708
>>40711
Гуманитарные сказочки и левые аналогии, это очень убедительно в математике, да. Такие же аргументы у религиозных проповедников.
Аноним 19/06/18 Втр 16:06:27 40716391
>>40712
Если ты делаешь утверждение, в котором хотя бы одно слово не может быть тобою определено, - ты несешь ахинею. Ты сделал утверждение "нет пруфов того, что алеф-1 больше чем алеф-0".
Аноним 19/06/18 Втр 16:36:28 40726392
daltonizm1-1728[...].jpg 289Кб, 1728x800
1728x800
>>40706
Хех, что-то проиграл с твоего поста. Недели 2 назад даже гугл намекнул. В одном из рекламных сообщений впарашке выдало пикрил и сообщение о какой-то клинике которая обследует глаза. Я тогда отметил что это странно т.к. по моим запросам ничего подобного выдать не должно. Обычно любое рекламное объявление я примерно знаю почему мне выдало, а тут вдруг совсем не в тему. А после твоего поста внезапно ОСОЗНАЛ. Ведь в последнее время я пытаюсь вступить в секту, искал и качал все эти книжки что тут кидает конструктивофорсер, про ML теорию, машинку поста и т.д. На фоне чтения возникает много релейтед запросов в гугл. В общем все сходится. А киберпанк в лице гугла уже наступил
Аноним 19/06/18 Втр 17:09:03 40727393
Аноним 19/06/18 Втр 17:21:32 40728394
>>40698
>Правило построения "type i : type i+1" это потенциальная бесконечность, а аксиома "существует бесконечное множество" - это актуальная.
Анон, так он о том и говорит (если я правильно понял): мы предполагаем, что мы можем построить и вычислить каждый из термов, заданных этим правилом, но у нас для этого нет никаких оснований. Самый простой способ получить такое основание - считать, что вселенная уже построена, то есть все эти термы существуют (то есть свести это к актуальной бесконечности). В противном случае получается, что возможность построения у нас основана на такой же вере, как и у всех остальных математиков.
Аноним 19/06/18 Втр 17:26:58 40732395
>>40726
>сообщение о какой-то клинике которая обследует глаза.
>Обычно любое рекламное объявление я примерно знаю почему мне выдало, а тут вдруг совсем не в тему.
То есть о том, что ты много сидишь за компьютером и гугл предполагает, что у тебя от этого портится зрение, ты не подумал? Спишу на то, что ты приукрасил историю ради комического эффекта.
Аноним 19/06/18 Втр 17:46:21 40741396
137-rgb.jpg 17Кб, 274x274
274x274
Аноны, помогите построить синий цвет. Нужно конструктивное доказательство через смешение черного и белого цвета. Или что синий цвет, он как Аллах, в него верить надо?
(Автор этого поста был забанен. Помянем.)
Аноним 19/06/18 Втр 19:47:49 40746397
>>40728
> Самый простой способ получить такое основание - считать, что вселенная уже построена,
Т.е уверовать в это? Ведь не построена по факту-то.
> В противном случае получается, что возможность построения у нас основана на такой же вере, как и у всех остальных математиков.
Про возможность никто не говорил. Речь про правила построения. Которые не требуют никакой веры, т к они есть независимо от того, веруешь или нет.
Аноним 19/06/18 Втр 20:14:16 40747398
>>40732
Не думаю. И я ничего не преукрашивал
Аноним 19/06/18 Втр 20:15:25 40748399
>>40727
Тебе бы самому почитать что там по ссылке.
Аноним 19/06/18 Втр 21:21:24 40752400
>>40716
Определи мне Я, умник хуев.
Аноним 19/06/18 Втр 22:09:22 40753401
>>40748
Почитал, тебе процитировать?
>в от-ли-чи·е от
>Устойчивое сочетание.
>(от кого, чего) в противоположность кому, чему
Ты не нейтив спикер? Может тебе на simple russian переформулировать? Ты не стесняйся, анон, спрашивай - тут доска взаимопомощи, отвечаем на вопросы, помогаем друг другу. Можешь еще заглянуть в international math thread, анон: https://2ch.hk/math/res/27513.html - ты сам откуда будешь, из какой страны-языка?
Аноним 19/06/18 Втр 22:11:03 40754402
>>40746
>Т.е уверовать в это? Ведь не построена по факту-то.
Ну так он тебе об этом и говорит, вот!

>Про возможность никто не говорил.
Ну когда ты пишешь type i : type i + 1, ты же предполагаешь, что единицу мы можем прибавлять сколько угодно, пользуясь заданными правилами построения, так?
Аноним 19/06/18 Втр 22:34:09 40755403
Аноним 19/06/18 Втр 22:45:21 40756404
>>40754
> Ну когда ты пишешь type i : type i + 1, ты же предполагаешь, что единицу мы можем прибавлять сколько угодно, пользуясь заданными правилами построения, так?
Это прямо прописано в правиле, зачем там что-то предполагать? Незачем предположение, что уже все построено, т.к оно ничего не даёт дополнительно к правилу, даже если бы и правда было построено. Т.е имеем абсолютно ненужную сущность, вера в которую никакого смысла не имеет.
Аноним 19/06/18 Втр 23:09:00 40758405
>>40755
Анон, ну куда ты лезешь? Погугли, что такое эллипсис. И в следующий раз, когда запутаешься в окончаниях, просто сразу признай, что ты обосрался (с кем не бывает, анон), а не пытайся по ходу дела маневрировать в материях, о которых ты имеешь весьма и весьма смутное представление.

Продолжить дискуссию можем (можешь) в треде русского языка в /fl.
Аноним 19/06/18 Втр 23:36:11 40760406
>>40758
Ой, блять, ладно, если ты сам знаешь такие слова то поверю что намеренно. Но как НЕЙТИВ тебе заявляю, выглядит по-уебански, на манер английских deferred prepositions и так на русском не пишут.
Аноним 19/06/18 Втр 23:40:16 40761407
>>40760
Нормально выглядит. Конечно, похоже немного на ущербное "это зависит", но в пределах нормы.
мимо
Аноним 19/06/18 Втр 23:57:34 40762408
>>40758
>весьма и весьма
Тут нужна была запятая.
мимо лингвист
Аноним 20/06/18 Срд 02:01:27 40763409
>>40700
Алеф-1 можно явным образом определить как множество всех не более чем счетных ординалов. Легко видеть, что при таком определении алеф-1 не биективен алеф-0.
Аноним 20/06/18 Срд 05:06:06 40767410
>>40763
Множество не более чем счетных ординалов само по себе не более чем счётный ординал
Аноним 20/06/18 Срд 05:14:24 40768411
>>40767
Тогда оно является элементом самого себя, что запрещено аксиомой регулярности.
Аноним 20/06/18 Срд 07:24:29 40770412
>>40768
> Тогда оно является элементом самого себя
Подмножеством. К i+1 хоть сколько добавляй, так из алефа0 алеф1 не построить.
Аноним 20/06/18 Срд 09:04:34 40771413
>>40770
Если ординал, состоящий в точности из всех не более чем счетных ординалов, сам является счетным, то он является своим элементом. По определению. Понимаешь?
Аноним 20/06/18 Срд 13:41:56 40784414
>>40698
> Если у нас есть правила построения N, то из них прямо следует потенциальная построимость любого элемента этого типа.
В том то и дело, что этого недостаточно. Термы типа N могут быть сформулированы в терминах произвольных других типов, например можно формализовать подходящий кусок топологии и выписать терм обозначающий какой-нибудь числовой инвариант какого-нибудь пространства. В итоге вопрос о том, вычислимы ли произвольные термы данного конкретного типа зависит от всей системы в целом, а не только от определения данного конкретного тип; если взять какой-нибудь вариант теории типов в котором есть противоречие, то в ней будут термы типа N, которым не будет соответствовать никакого значение. И хотя с твоей стороны происходит заметание этого вопроса под ковер, наличие такого глобального свойства требует обоснования для каждого конкретного варианта теории типов.


На мой взгляд наиболее естественный способ обосновать, почему конкретный вариант теории типов работает как следует, т.е. все термы вычислимы - это построить её модель (в терминах рекурсивных функционалов высших типов).
Конечно можно говорить, что-то в духе того, что все определения типов, которые дают "квалифицированные" теоретико-типовики в некотором смысле "правильны" и сохраняют "правильность" теорий типов и во всех "правильных" теориях типов все вычислимо. Проблема в том, что если посмотреть, что должно соответствовать "правильности" с более формальной точки зрения, то наиболее родственно оно конструкциям возникающим в доказательствах сильной нормализуемости сильных лямбда исчислений и там определения таких свойств существенно опирается на квантификацию по бесконечным множествам (см. доказательство сильной нормализуемости системы F). Но как ни крути, либо нужно принять на веру, что (довольно туманная) интуиция теоретико-типовиков никогда не приводит к проблемам, либо дать обоснование в терминах бесконечных множеств.
Аноним 20/06/18 Срд 16:53:35 40790415
>>40784
>это построить её модель
Я не понимаю, как вообще можно доверять этому методу. Ведь у нас нет ни одной гарантированно свободной от противоречий теории, в которой можно было бы строить более-менее содержательные модели.
другой анон
Аноним 20/06/18 Срд 19:50:34 40799416
>>40760
Как минимум с конца 90-ых этот оборот широко употребляется в разговорной (форумной) речи. Не думаю, что тут есть какое-то влияние английского, если честно.

>>40762
Смищно.
Аноним 20/06/18 Срд 22:42:03 40803417
>>40790
>Ведь у нас нет ни одной гарантированно свободной от противоречий теории, в которой можно было бы строить более-менее содержательные модели.
Таким образом мы можем редуцировать корректность одной теории к другой. И если теория к которой происходит редукция в каком-нибудь смысле понятнее редуцируемой теории, то это до некоторой степени объясняет последнюю.

Кстати, как ты себе представляешь гарантии свободы от противоречий для какой-либо теории, которая формализует хотя бы арифметику натуральных чисел? Ведь для любой такой теории есть неограниченно много доказательств и поэтому гарантировать непротиворечивость можно только приняв какой-нибудь метод установления универсальных утверждений.
Аноним 21/06/18 Чтв 04:35:09 40808418
>>40784
> И хотя с твоей стороны происходит заметание этого вопроса под ковер, наличие такого глобального свойства требует обоснования для каждого конкретного варианта теории типов.
Твоя проблема в том, что ты не понял сути конструктивизма и поэтому пытаешься натянуть его на формализм как сову на глобус. А оно изначально создавалось не для этого, более того, формализация интуиционизма невозможна принципиально. Я уже пояснял за это, но местный шизик все закукарекал. Формализация понятия алгоритма (и интуиционизма Брауэра) невозможна по той простой причине, что таковая должна одновременно решать и проблему останова универсальной машины Тьюринга. Поэтому в конструктивизме речь только об уточнении понятия алгоритма (нормальные алгоритмы Маркова, машина Тьюринга итд). Именно по этой причине, о которой говорил ещё Брауэр, обосрался Гильберт со своей изначальной программой формализма.
> Но как ни крути, либо нужно принять на веру, что (довольно туманная) интуиция теоретико-типовиков никогда не приводит к проблемам, либо дать обоснование в терминах бесконечных множеств.
Вот ещё одно подтверждение, что ты не понимаешь тех соображений, которые вообще привели к созданию конструктивизма. MLTT корректна и непротиворечива не потому что преподобный рабби Леф так скозал, а по той простой причине, что в ней принципиально невыразимо невычислимое в ней же. Оно исходя из этого и создавалось. Противоречивость подобных теорий видно сразу же, самый известный пример - парадокс Жирара, суть которого в том, что при использовании правила построения type : type появляется возможность выразить в mltt парадокс Рассела, т.е невычислимую хуету. Менее известные примеры противоречивых лямбда исчислений есть у Барендрегта.
Аноним 21/06/18 Чтв 05:24:20 40810419
>>40784
> На мой взгляд наиболее естественный способ обосновать, почему конкретный вариант теории типов работает как следует, т.е. все термы вычислимы - это построить её модель (в терминах рекурсивных функционалов высших типов).
Это бессмысленно. Я тут миллион раз упоминал книжку "Programming in Martin-Lof type theory", авторов не помню, какие-то шведские куколды, так вот, она является наиболее полным изложением mltt и написана под руководством Мартин-Лефа. Так вот, там в предисловии прямым текстом написано, что mltt создавалась как основания и поэтому её представление в других теориях смысла не имеет, это наоборот другие теории должны выражаться в ней. Поэтому, единственный смысл, семантика mltt это вычислимость. Она выразима в терминах операционной семантики (в приложении они перечислены), что делает её не только основаниями, но и языком программирования (изоморфизм Карри-Говарда). Последнее касается не только конкретно mltt, но и CiC (Coq) и UTT (Idris) итд.
Аноним 21/06/18 Чтв 10:48:38 40816420
Аноним 21/06/18 Чтв 11:05:41 40817421
>>40810
>Последнее касается не только конкретно mltt, но и CiC (Coq) и UTT (Idris) итд.
А python и javascript тоже основаниями математики являются? Не для себя спрашиваю.
Аноним 21/06/18 Чтв 11:14:07 40818422
https://arxiv.org/pdf/1806.05538.pdf
>A marriage of category theory and set theory: a finitely axiomatized nonclassical first-order theory implying ZF
>Marcoen J.T.F. Cabbolet
>(Submitted on 11 Jun 2018)
>The main purpose of this paper is to introduce a finitely axiomatized theory that might be applicable as a foundational theory for
mathematics. For that matter, some twenty axioms in a formal language are introduced, which are to hold in a universe consisting of a class of objects, each of which is a set, and a class of arrows, each of which is a function on a set. One of the axioms is nonclassical: it states that, given a family of ur-functions - i.e. functions on a singleton - with disjunct domains, there exists a uniquely determined sum function on the union of these domains. This 'sum function axiom' is so powerful that it allows to derive ZF from a finite axiom scheme. In addition, it is shown that the Loewenheim-Skolem theorem does not hold for the present theory, which therefore can be considered stronger than ZF. Furthermore, the axioms of category theory are proven to hold: the present universe may therefore serve as an ontological basis for category theory. However, it has not been investigated whether any of the soundness and completeness properties hold for the present theory: the inevitable conclusion is therefore that only further research can establish whether the present results indeed constitute an advancement in the foundations of mathematics.
Аноним 21/06/18 Чтв 11:16:51 40819423
>>40817
> А python и javascript тоже основаниями математики являются?
Я ссылался на операционную семантику mltt, она очень простая. Coq на жабаскрипте давно существует, если что. Lean тоже есть на жабаскрипте, причём был ещё 2ой версии, где ядро HoTT. Так что ответ - да, изоморфизм Карри-Говарда допускает такую возможность.
Аноним 21/06/18 Чтв 16:46:58 40822424
>>40810
>mltt создавалась как основания и поэтому её представление в других теориях смысла не имеет, это наоборот другие теории должны выражаться в ней
Лол.
Аноним 21/06/18 Чтв 17:07:27 40825425
>>40822
Говоря проще, это лишнее. Бурбаки, Кантор, Гильберт теорию множеств через другие не представляли. И никто не лолкает. Так и тут, есть операционная семантика, этого достаточно для работоспособности mltt, зачем огород из пучков городить.
Аноним 21/06/18 Чтв 19:43:36 40830426
>>40808
>>40810
Это понятно, что ты в своем представление теории типов в качестве самодостаточных оснований следуешь за Мартин-Лёфом.
В принципе, с этим нет особых проблем. Есть довольно много математиков, которые привыкли думать о математике в бурбакистском ключе и поэтому для них аксиоматика Цермело-Френкеля представляет из себя формализацию самоочевидных принципов - у них уже есть преконцепция что такое множества и что с ними можно делать, а аксиомы просто соответствуют этой интуиции. Ровно также на существование имеет право и более маргинальная позиция людей думающих о математике в интуиционистских терминах для которых самоочевидной оказывается теория типов.
Не буду скрывать - я привык к бурбакисткому изложению математики и соответственно у меня развита именно интуиция касательно понятия множества, а не типа. Поэтому с неизбежностью я смотрю на интуиционизм и его формализации со стороны.
И как я уже довольно подробно расписал в нескольких предшествующих постах, анализируя их со стороны довольно прозрачно, что в них неявно заложены сильные и выходящие далеко за пределы вычислимой математики предположения (здесь под вычислимостью я понимаю вычислимость на натуральных числах) - особенно явно это проявляется в версиях с W-типами и вселенными.
>MLTT корректна и непротиворечива не потому что преподобный рабби Леф так скозал, а по той простой причине, что в ней принципиально невыразимо невычислимое в ней же.
Буллщит, феномен второй теоремы Гёделя о неполноте очень общий и чтобы доказать корректность (или хотя бы непротиворечивость) какого-либо метода рассуждений заведомо нужно выйти за его пределы.
>Противоречивость подобных теорий видно сразу же
Отмечу, что в теории множеств ровна такая же история с большими кардиналами. Из серьезных ошибочных попыток дать аксиому большого кардинала судя по всему был только кардинал Рейнхардта и не то, чтобы доказать его противоречивость было особо сложно.
Хотя, конечно, нельзя полностью исключать, что в будущем нетривиальные противоречия будут найдены, как для ZFC и её расширений так и для теорий типов

Аноним 21/06/18 Чтв 20:41:10 40832427
Конструктивисты, скажите, есть простые числа, смотришь на них и очевидно, что чем дальше, тем их меньше встречается. Евклид же доказал, что множество простых чисел бесконечно. Но он в доказательстве использовал отпротивное. Может ли быть так, что на самом деле множество простых конечно?
Аноним 21/06/18 Чтв 20:58:45 40833428
>>40825
А ничего, что Мартин-Лёф несколько раз давал противоречивые версии систем?
Нужно определять семантику, чтобы не было таких чудачеств.

Ты сначала ZFC осиль, потом будешь писать на моём дваче.
Аноним 21/06/18 Чтв 21:10:48 40834429
>>40830
Непротиворечивость ZFC можно доказать в более сильных теориях, например в M.
Аноним 21/06/18 Чтв 21:22:14 40835430
>>40834
Можно. Что сказать-то хотел?
Аноним 21/06/18 Чтв 21:36:04 40836431
>>40835
>в будущем нетривиальные противоречия будут найдены
Не будут.
Аноним 21/06/18 Чтв 21:40:31 40837432
>>40836
Если ты доказал непротиворечивость одной теории в другой, то ничто не мешает им обоим оказаться противоречивыми. Единственно это исключает возможность, что первая противоречива, а вторая - нет.
Аноним 22/06/18 Птн 01:00:10 40839433
>>40833
> на моём дваче.
Носатый, уходи.
>>40830
> Буллщит, феномен второй теоремы Гёделя о неполноте очень общий и чтобы доказать корректность (или хотя бы непротиворечивость) какого-либо метода рассуждений заведомо нужно выйти за его пределы.
Потому я и написал про операционную семантику, в терминах которой доказывается в т.ч непротиворечивость mltt. Насчёт геделя-шмеделя и прочего такого, попытка выразить это в теории типов приведёт только к ошибке, ибо невычислимая хуитка. Я тебе ещё раз скажу - ты лезешь с формализмом туда, где от него изначально старались избавиться по причине его безблагодатности. Поэтому и вместо аксиом там натуральная дедукция итд итп.
Аноним 22/06/18 Птн 01:50:50 40840434
>>40839
>Насчёт геделя-шмеделя и прочего такого, попытка выразить это в теории типов приведёт только к ошибке, ибо невычислимая хуитка.
Стандартное доказательство теорем о неполноте полностью конструктивно и в частности они приложимо к любой системе в которую можно погрузить гейтингову арифметику, в том числе к теориям типов.

Слышать о неприложимости формализма от тебя довольно смешно. То что ты называешь здесь формализмом это видимо просто общий метод широко применяемый в математической логике: чтобы исследовать некоторый метод математических рассуждений вначале нужно построить математическую модель понятия доказательства для данного случая, т.е. дать адекватное понятие формального доказательства, а затем исследовать это понятие математическими средствами. Идея о том, что переход от гильбертовского стиля исчисления к системе натуральной дедукции как-то принципиально мешает анализу системы просто показывает твое полное непонимание того, о чем ты говоришь. На самом деле метод приложим к любым методам рассуждения, которые могут быть описаны какой-нибудь рекурсивной процедурой. Учитывая тот факт, что немного ранее в этом треде ты сам защищал идею о том, что человеческий интеллект может быть заменен на компьютер, ....
Аноним 22/06/18 Птн 01:52:32 40841435
>чтобы исследовать некоторый метод математических рассуждений
-->
чтобы исследовать некоторый метод рассуждений
Аноним 22/06/18 Птн 02:04:22 40842436
>>40837
Тогда зачем вообще кто-то доказывает непротиворечивость?
Аноним 22/06/18 Птн 02:09:09 40843437
>>40842
Обычно, чтобы свести вопрос о непротиворечивости какой-нибудь менее понятной теории к вопросу о непротиворечивости более понятной теории. Характерный пример это доказательство непротиворечивости NFU в ZFC.
Аноним 22/06/18 Птн 02:22:09 40844438
>>40843
А зачем это делать?
Аноним 22/06/18 Птн 02:24:03 40845439