М.Двач / Математика

Оснований тред №5 7 окт 2017, 20:45 25624 В конец треда | Веб

64 Кб, 707x91916 Кб, 256x32626 Кб, 220x330157 Кб, 350x480

В любой науке ровно столько науки, сколько в ней математики. В любой математике ровно столько математики, сколько в ней вычислимости.
Предыдущий - https://2ch.hk/math/res/21361.html (М)

Ответы39176

170 Кб, 1440x900
2 7 окт 2017, 21:00 2 25626

На самом деле непреодолимой пропасти между конструктивным и неко нструктивным подходом нет. Поскольку и то и другое выразимо в языковых конструкциях, имеем просто еще один работающий пример релятивизма Маннури. Более того, легко показать изоморфизм между математическими формулами и соответствующим им языковыми конструкциями. Однако, проблему невычислимых верований такой подход не снимает. Но тут на самом деле только один возможный выход, и он был предложен еще Брауэром - выкинуть к хуям всю подобную ебулду из математики, или как минимум, перестать называть ее математикой. Тем более, что таких вещей немного и они все равно математике никак не помогают. Затыкать же открытые проблемы невычислимыми верованиями вообще очень плохая практика.

Ответы40360

3 7 окт 2017, 21:12 3 25628

Давайте так.
После Тьюринга математика делится на информатику и собственно математику.
Вычислимость, автоматы, пруверы = информатика.
Все остальные школы (ньютон-пуанкаре-гротендик) = традиционная математика.
Пруф ми ронг.

Ответы25629256322563625753

4 7 окт 2017, 21:15 4 25629

>>25628
>традиционная математика.
Либо выразима в типизированной лямбде, либо все те же невычислимые Аллахи.

5 8 окт 2017, 05:33 5 25632

>>25628
>Вычислимость, автоматы, пруверы = информатика.
Так называемая "информатика" это лишь частный случай математики.

Ответы25633

6 8 окт 2017, 05:40 6 25633

>>25632
Кто не каппа-дескриптивен, идёт нахуй.

Ответы25634

7 8 окт 2017, 05:43 7 25634

>>25633
Можно показать простой диагонализацией, что сама каппа-дескриптивность не является каппа-дескриптивной, следовательно она тоже идёт нахуй.

Ответы25635

8 8 окт 2017, 05:48 8 25635

>>25634
Что? Ты бредишь.

Ответы25639

9 8 окт 2017, 05:49 9 25636

>>25628
>Либо выразима в типизированной лямбде
Исключённое третье тоже спокойно выразимо если у тебя есть пустой тип и пи-типы, но это не делает его не невычислимым Аллахом.

10 8 окт 2017, 05:53 10 25639

>>25635
Да нет, это ведь очевидно. Каппа-дескриптивность не сохраняет копределы, а это необходимо, чтобы быть каппа-дескриптивным. Это доказал ещё Витгенштейн.

Ответы25644

11 8 окт 2017, 05:57 11 25644

>>25639
Каппа-дескриптивность - это конечный орграф. Что ты там диагонализировать собрался? Впрочем, я понял. Ты просто говоришь рандомные слова без всякого смысла.

Ответы25646

12 8 окт 2017, 06:00 12 25646

>>25644
Это без разницы на самом деле. Конечность или "бесконечность" тут не играет никакой роли. По индукции спокойно доказывается, что каппа-дескриптивность не каппа-дескриптивна. Следует из существования NNO в топосе графов.

Ответы25665256692567325675

13 8 окт 2017, 11:29 13 25664

Я уже перестаю понимать что тут происходит.

Ответы25666

115 Кб, 1240x698
14 8 окт 2017, 12:39 14 25665

>>25646
Двачую этого сударя

15 8 окт 2017, 12:50 15 25666

>>25664
Да что тут понимать - основания математики пусты. Можешь мыслить их как контейнер, в который можно положить всё что угодно. Не всем такая свобода по душе, они хотят непременно какой-то объектный фундамент.

Ответы256672567425680

16 8 окт 2017, 12:57 16 25667

>>25666
Да мне похуй на "пустоту" оснований математики, я на интуитивном уровне верую в теорию категорий, мне этого в принципе достаточно.
Конечно можно формально с помощью индукции показать (причём конструктивно), что она непротиворечива, но меня это особо не волнует.

17 8 окт 2017, 13:06 17 25668

Как конструктивно доказывать отрицание исключённого третьего?

18 8 окт 2017, 13:09 18 25669

>>25646
Хватит бредить.

Ответы25670

19 8 окт 2017, 13:10 19 25670

>>25669
Что, прости?

Ответы25671

20 8 окт 2017, 13:12 20 25671

>>25670
Что слышал.

Ответы25672

21 8 окт 2017, 13:12 21 25672

>>25671
Услышать то я услышал, но вот смысла не понял. Объяснишь?

Ответы25673

22 8 окт 2017, 13:14 22 25673

>>25672
Вот это >>25646 - бессмысленная чепуха.

23 8 окт 2017, 13:14 23 25674

>>25666
Конкретно что именно из этого бессмысленная чепуха?

24 8 окт 2017, 13:40 24 25675

>>25646
Ссылку на книгу или статью с определением каппа-дескриптивности приведи, а то непонятно про что ты говоришь.

Ответы256762567725681

25 8 окт 2017, 13:41 25 25676

>>25675
Тысячу раз уже приводил.

Ответы25683

26 8 окт 2017, 14:26 26 25677

>>25675
Каппа-дескриптивность = дескриптивность в некоторой каппа-библиотеке.

Ответы2568325693

27 8 окт 2017, 15:18 27 25680

>>25666
>основания математики пусты. Можешь мыслить их как контейнер, в который можно положить всё что угодно.
Коран сойдет? Основания математики - это то, на чем можно основать всю математику. Т.е. нечто даже потенциально противоречивое не подойдет, а это уже не "все, что угодно".
>Не всем такая свобода по душе, они хотят непременно какой-то объектный фундамент.
Математика - это самое точное знание, какое есть у человечества. Нет объективного фундамента - нет точного знания. Смешно считать мир идей Платона или любую другую религию точным знанием.

Ответы25682

28 8 окт 2017, 15:19 28 25681

>>25675
Sur quelques points d'algèbre homologique

Ответы25683

29 8 окт 2017, 15:31 29 25682

>>25680
А, ну ладно тогда. Удачи в поисках.

Ответы25684

30 8 окт 2017, 15:39 30 25683

>>25676
>>25677
>>25681

Неправильно.
Во-первых, нужен текст на русском или английском, во-вторых нужно указывать страницу.

Ответы25685256862568725689

31 8 окт 2017, 15:50 31 25684

>>25682
>Удачи в поисках.
Нашли уже, вопрос в том, чтобы реализовать, но и это в процессе. Воеводского вот жалко, то, что он помер, упомянутому процессу не на пользу.

32 8 окт 2017, 15:58 32 25685

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

33 8 окт 2017, 16:12 33 25686

>>25683
Да это ебнутый местный, его репортить за шитпостинг надо.

34 8 окт 2017, 16:20 34 25687

>>25683
>нужен текст на русском или английском
Если ты ещё французский не выучил, то сразу видно, что на математику тебе похуй по сути.

Ответы25688

35 8 окт 2017, 16:30 35 25688

>>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.

36 8 окт 2017, 16:44 36 25689

>>25683
Здесь такое не принято. Здесь просто называют фамилии. Чем малоизвестнее, тем лучше.

Ответы25690

37 8 окт 2017, 16:46 37 25690

>>25689
А кто-то виноват, что фамилии типа Мартин-Лёф и Брауэр тебе неизвестны? Это не повод подгорать и срать в треде.

Ответы25691

38 8 окт 2017, 17:02 38 25691

>>25690
Релятивизм Маннури, ATOM и MT, Бишоп, цифферкомплекс, Уолш, нумероны, изоморфизм Карри-Говарда - всё это входит в общеизвестный багаж знаний теоретика оснований? Ну окей. Если тебе позволено поступать так, то и я буду ссылаться на моих ученых без всяких дополнительных слов. Тебя интересует, что такое каппа-библиотека, - твои проблемы, ебись с гуглом самостоятельно.

Ответы25692

39 8 окт 2017, 17:09 39 25692

>>25691
Изоморфизм Карри-Говарда точно входит, как и интрерпретация логических констант по Брауэру-Гейтингу-Колмогорову, "это классика, это знать нада". За остальное я вполне доходчиво пояснял, при том по-русски.

Ответы25693

40 8 окт 2017, 17:10 40 25693

>>25692
Ну вот и я доходчиво пояснил за каппа-дескриптивность, в посте >>25677 .

Ответы25694

41 8 окт 2017, 17:12 41 25694

>>25693
Разница в том, что я на что-то ссылаюсь по теме, в связи с основаниями, а у тебя просто БАРЕНДРЕХТ.

Ответы25695

42 8 окт 2017, 17:16 42 25695

>>25694
Отнюдь. Я предельно точен в своих описаниях. Хочешь знать больше - повторяю, гугли самостоятельно. Твой ко-ко-конструктивизм гроша ломаного не стоит, объективно. Смотри, ты говоришь, что число пи построимо. Но ты даже банально не можешь сказать, какова цифра номер гугол после запятой в его десятичном представлении. Всех вычислительных мощностей этой вселенной не хватит, чтобы её найти. Значит, твоя абстракция потенциальной осуществимости ущербна, и от неё нужно отказаться в пользу каппа-библиотек.

Ответы25696

43 8 окт 2017, 17:23 43 25696

>>25695
>ты говоришь, что число пи построимо.
Я такого нигде и никогда не говорил. Более того, про вещественные числа я вообще говорил только то, что они фактически построимы только до конечного числа цифер после запятой, в каковом качестве и используются в любой математике, в т.ч. и неко нструктивной. Про абстракцию потенциальной осуществимости ты так и не понял, что это и зачем, чему я не удивлен. Итого, в сухом остатке от твоих предъяв одна батрушка.

Ответы25697

44 8 окт 2017, 17:30 44 25697

>>25696
Ну да, начались оправдания. А ведь до простой мысли, что Брауэр не гений на все времена, ты не додумался. Жемайтис изобрёл каппа-библиотеки, и это открытие уничтожило и конструктивистов, и даже ультра-финитистов. All hail Жемайтис.

Ответы25699

294 Кб, 490x750
45 8 окт 2017, 17:42 45 25699

>>25697
>до простой мысли, что Брауэр не гений на все времена, ты не додумался.
Но он гений на все времена. И до него никто не додумался поставить вопросы об основаниях так, как это сделал он. Хотя математике тысячи лет. А вот ты простой недотролль с мейлру.

Ответы2570225707

46 8 окт 2017, 17:49 46 25702

>>25699
Жемайтис решил проблемы, о которых Брауэр даже не думал. А ещё у тебя фиксация на мейлру.

Ответы25708

47 8 окт 2017, 19:12 47 25707

>>25699
Брауэр конечно великий человек, но гениальность его не в постановке вопроса об основаниях (об этом задумывался еще Кронекер) а в переоткрытии понятия интенциальности, независимо от Маха и Брентано.
Математике, впрочем, никак не тысячи лет, а около двух веков, ибо "алгебра это решение уравнений" и "чертежи без доказательств" к ней очевидно не относятся. Это не значит что ранее до математики никто не додумался, например были же Дезарг и Паскаль, но это не могло прижиться, поскольку общество до-индустриальной эпохи не обладало достаточными ресурсами, чтобы позволить ученым мужам всю жизнь заниматься лишь математикой. Соответственно, никто и не занимался основаниями, потому что дисциплины такой не было. С другой стороны, понятно, что Брауэр на голову выше таких людей как Курт Гёдель или Герман Вейль, последние прочитали Гуссерля, а Брауэр пере-придумал его сам.

48 8 окт 2017, 19:15 48 25708

>>25702
Жемайтис это генерал наподобие Бурбаки или персонаж повести Стругацких? В любом случае, он сильно уступает Дедекинду, так что я бы тут не бравировал каппа-фейсом.

Ответы25710

49 8 окт 2017, 19:41 49 25710

>>25708
Жемайтис - это известный логик, изобретатель каппа- и омикрон-библиотек.

Ответы25739

50 9 окт 2017, 18:47 50 25739

>>25710
Я с ним лично знаком, удивительный человек.

Ответы25740

51 9 окт 2017, 19:30 51 25740

>>25739
Он умер.

Ответы25742

52 9 окт 2017, 20:38 52 25742

>>25740
Это мне не мешает.

53 10 окт 2017, 05:28 53 25750

Java программисты занимаются основаниями математики. Из теории акторов известно что паралельные вычисления нельзя сгрупировать по логическим выводам. Из этого следует что арбитр (который выбирает кому отдать процессорное время из потоков) неразрешимая задача в общем случая. Поэтому арбитров пишут используя теорию вероятности попутно, с умным видом, обсуждая проблемы математики.

24 Кб, 200x284
54 10 окт 2017, 16:00 54 25753

Вот в этих тредах часто приводится "аргумент", >>25628 что типа математика это одно, а информатика это другое. В связи с чем вопрос - тута про изоморфизм Карри-Говарда вообще кто-то слышал? Осилить не пробовали было бы там что осиливать? Там же просто как 3 копейки, зато становится понятно, почему математику можно представить с помощью информатики и наоборот. И как и почему невычислимые верования при этом отсеиваются.

Ответы25754

55 10 окт 2017, 16:28 55 25754

>>25753
С тем же успехом можно утверждать, что любая наука - частный случай генеративной лингвистики, поэтому нет ничего кроме генеративной лингвистики.

Ты слишком сильно абстрагируешься и поэтому упускаешь из виду важные отличия информатики от математики.

Ответы2575525757

56 10 окт 2017, 16:29 56 25755

>>25754
>важные отличия информатики от математики
Примеры?

Ответы25756

57 10 окт 2017, 16:46 57 25756

>>25755
Ну, самое очевидное - разные дискурсивные поля. В математике в принципе нет понятия "стандарт оформления кода" и многих других специфичных для информатики понятий. А в информатике нет доминирующей аксиоматической теории, в которой всё строится, - тогда как в математике в основном играют внутри ZFC-TG-NBG.

Ответы257572575825760

58 10 окт 2017, 16:48 58 25757

>>25754
>С тем же успехом можно утверждать, что любая наука - частный случай генеративной лингвистики,
Если любую науку можно свести к генеративной лингвистике, почему бы и не утверждать подобное?
>поэтому нет ничего кроме генеративной лингвистики.
Э, нет. Не "нет ничего кроме Х", а "можно свести к Х". Если неважно, от какой именно печки танцевать по причине того, что нечто всегда можно свести к чему-то другому, то мы тут имеем пример работы релятивизма Маннури, но в качестве начала отсчета логичнее брать то, что удобнее и проще в практическом использовании. И я очень сомневаюсь, что любую науку проще всего представлять в генеративной лингвистике и изучать с этой точки зрения, даже если такая возможность реально существует.
>важные отличия информатики от математики.
Их нет, упомянутый изоморфизм как раз об этом. Вся математика, основанием которой может быть исчисление предикатов, представима в лямбда-П исчислении, именно этот факт лежит в основе первого прувера AUTOMATH де Брауна.
>>25756
Некоторая разница в терминологии, не более.

Ответы2575925762

59 10 окт 2017, 16:49 59 25758

>>25756
>В математике в принципе нет понятия "стандарт оформления кода"
Ты доказательства абсолютно в любом виде пишешь?
>А в информатике нет доминирующей аксиоматической теории
Это не говорит ничего о математике и информатике как о науках.

Ответы25762

60 10 окт 2017, 16:50 60 25759

>>25757
>представима в лямбда-П исчислении
Что ты имеешь ввиду под "представима"?

Ответы25761

61 10 окт 2017, 16:51 61 25760

>>25756
>в информатике нет доминирующей аксиоматической теории, в которой всё строится,
Типизированная лямбда же.
>тогда как в математике в основном играют внутри ZFC-TG-NBG.
Которые представимы в типизированной лямбде.

Ответы25763

62 10 окт 2017, 16:55 62 25761

>>25759
>Что ты имеешь ввиду под "представима"?
Скажем, "однозначно выразима" с помощью все того же изоморфизма Карри-Говарда. У де Брауна полно годных примеров, но меня опять же тут будут обвинять, что я всех своими евреями пугаю и даю ссылки на сложночитаемые источники.

101 Кб, 614x995
63 10 окт 2017, 16:56 63 25762

>>25757
>>25758
Информатика и математика различаются, и я показал вам отличия. Просто вы сидите на заоблачном уровне абстракции, и на нём эти отличия теряются. Но если вы снизите абстрактность, вы не сможете игнорировать разницу. А держаться на вашем уровне абстрактности и не снижать его вы сможете только в том случае, если так и останетесь сторонними философствующими наблюдателями, далёкими от реалий предметов, про которые чешете языками.

Пикрандом.

Ответы2576425765

64 10 окт 2017, 16:58 64 25763

>>25760
Все математики знают про ZFC.
Редкий информатик слышал про какую-то там типизированную лямбду.

Ответы2576425765

65 10 окт 2017, 17:00 65 25764

>>25762
>Но если вы снизите абстрактность
Извини, я математикой занимаюсь, а не какой-то хуйнёй.
>>25763
>Редкий информатик
Программисты и информатики это разные люди.

Ответы25766

66 10 окт 2017, 17:06 66 25765

>>25762
>Просто вы сидите на заоблачном уровне абстракции, и на нём эти отличия теряются.
Изоморфизм Карри-Говарда это не заоблачный уровень абстракции. Но уже с этих позиций вся разница, что ты назвал - это разница в терминологии.
>А держаться на вашем уровне абстрактности и не снижать его вы сможете только в том случае, если так и останетесь сторонними философствующими наблюдателями, далёкими от реалий предметов, про которые чешете языками.
Опять же, сложно найти что-то более практически применимое, чем изоморфизм Карри-Говарда, чему пример пруверы. Это не стороннее наблюдение, а самая что ни на есть практическая математика.
>>25763
>Редкий информатик слышал про какую-то там типизированную лямбду.
Это вообще ничего не меняет.

Ответы25769

67 10 окт 2017, 17:09 67 25766

>>25764
Выбор уровня абстрактности очень важен. Чем выше уровень, тем больше деталей теряется. На самом высоком уровне абстрактности между любыми двумя вещами нет разницы, любые две вещи - одна и та же вещь.

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

Если две вещи оказались отождествлены, то нужно посмотреть, за счет чего это произошло: из-за слишком высоко задранной планки абстрактности или же из-за более содержательных причин. И если оказалось, что из-за абстрактности, - оное отождествление не имеет никакой познавательной ценности.

Ответы2576725768

68 10 окт 2017, 17:11 68 25767

>>25766
Вот я и хочу спросить - как эта болтология соотностится с приведенным мной конкретным примером - изоморфизмом Карри-Говарда?

Ответы25769

69 10 окт 2017, 17:15 69 25768

>>25766
>На самом высоком уровне абстрактности между любыми двумя вещами нет разницы, любые две вещи - одна и та же вещь
Ты несёшь полную хуйню, никто тут не говорит про "самый высокий уровень абстракции".
Это уже никакого отношения не имеет даже к изначальной теме.

70 10 окт 2017, 17:16 70 25769

>>25765
Это разница не в терминологии, а в понятийном аппарате. Дискурсивное поле информатиков включает в себя идеи, которые ни в каком виде не содержатся в дискурсивном поле математиков. И обратно.

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

На твоём уровне абстрактности нет разницы между допотопной пекарней с четвертым пентиумом и модным айфоном. С абстрактной точки зрения - они одно и то же. Но реальность такова, что допотопная пекарня и айфон - две разные вещи.

Ответы25770

71 10 окт 2017, 18:18 71 25770

>>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 показывает, как в типизированной лямбде можно представить основания. А местные полтора философа на мейлру говорят, что вы все врети и математика это не информатика, яскозал! Очень убедительно.

Ответы257712577425781

72 10 окт 2017, 18:27 72 25771

>>25770
Действительно, ведь это разные уровни абстракции, поэтому и не математика.

Ответы25773

73 10 окт 2017, 18:29 73 25773

>>25771
Я еще раз попрошу уточнить что есть твое выражение "уровень абстракции" применительно к конкретному обсуждаемому примеру - изоморфизму Карри-Говарда.

74 10 окт 2017, 18:31 74 25774

>>25770
Информатика это часть математики, в чём проблема?

Ответы25776

75 10 окт 2017, 18:33 75 25775

Конструктивные основания противоречивы. Какой в них смысл тогда?

Ответы25776

76 10 окт 2017, 18:34 76 25776

>>25774
Или математика часть информатики.
>>25775
>Конструктивные основания противоречивы.
Ага, раз так на мейлру написали.

Ответы25777

77 10 окт 2017, 18:34 77 25777

>>25776
>Ага, раз так на мейлру написали.
В прошлом треде доказательство было ведь.

Ответы25778

78 10 окт 2017, 18:36 78 25778

>>25777
Не было. Нет и не может быть доказательств противоречивости MLTT, поскольку эта противоречивость непосредственно вычислима и была бы получена лет еще 30 назад.

Ответы25779

79 10 окт 2017, 18:37 79 25779

>>25778
Зайди в последний тред, там открытым текстом написано доказательство противоречивости HoTT.

Ответы25780

80 10 окт 2017, 18:40 80 25780

>>25779
>HoTT.
Вычислительная интерпретация НоТТ - открытая проблема. Это во-первых. Во-вторых, конструктивные основания - это MLTT. Ты даже изоморфизм Карри-Говарда понять не можешь, хотя его и школьнику можно объяснить, ну куда ты лезешь в НоТТ? Может быть, хватит уже цирка?..

Ответы25782

81 10 окт 2017, 18:41 81 25781

>>25770
Я отказываюсь продолжать с тобой разговор; ты сошёл с ума, ты ёбнутый.

Ответы25783

82 10 окт 2017, 18:42 82 25782

>>25780
>Вычислительная интерпретация НоТТ - открытая проблема.
Но противоречивость HoTT уже закрытая.
>Ты даже изоморфизм Карри-Говарда понять не можешь
Почему ты так уверен?
>ну куда ты лезешь в НоТТ?
А что такого?

Ответы25783

83 10 окт 2017, 18:46 83 25783

>>25781
>>25782
>А что такого?
Толку-то тебе рассуждать о том, чего не понимаешь даже приблизительно?

Ответы25784

84 10 окт 2017, 18:46 84 25784

>>25783
Почему я не понимаю этого даже приблизительно?

85 10 окт 2017, 21:41 85 25789

канструктивные основания пративоречивы. даже смысла нет, а жаль...
док-во в пред. треде.

Ответы25810

86 11 окт 2017, 22:22 86 25810

>>25789
Каждый раз, когда ты постишь в таком стиле, нарушается синхронность и один из внетелесных разумов погибает.

Ответы25814

87 11 окт 2017, 23:57 87 25814

>>25810
что, прасти?

Ответы25846

88 13 окт 2017, 22:33 88 25846

>>25814
Ты видимо не знаком с той ололомистической бодягой, которую Воеводский толкал в жж на пару с Михайловым.

Ответы2584925851

89 14 окт 2017, 07:46 89 25849

>>25846
Зато внетелесные разумы вычислимы.
Шах и мат веруны.

90 14 окт 2017, 13:23 90 25851

>>25846
Я с ним лично знаком, так что знаю про это.

Ответы25853

91 14 окт 2017, 13:49 91 25852

Есть какие-нибудь непротиворечивые основания? Я почти уверен, что любая теория множеств противоречива и противоречивость HoTT уже доказана. Что остаётся тогда?

Ответы2594026009

92 14 окт 2017, 14:37 92 25853

>>25851
Он умер.

Ответы2585525923

93 14 окт 2017, 14:38 93 25855

>>25853
Я в курсе.

94 17 окт 2017, 00:23 94 25923

>>25853
>Он умер.
Ну йобана.

62 Кб, 1123x349
95 17 окт 2017, 17:37 95 25939

Противоречивость конструктивных оснований, как и их непротиворечивость вычислима непосредственно. Так вот, ко всем кто хочет покукарековать за противоречивость конструктивных оснований, к своим кукарекам прилагать вычислимое доказательство противоречивости, в противном случае кукареки не принимаются к рассмотрению.

Ответы25942

96 17 окт 2017, 17:39 96 25940

>>25852
ZFC

Ответы2594125943

97 17 окт 2017, 17:40 97 25941

>>25940
Противоречивая хуйня, стало очевидно после доказательства независимости аксиомы выбора.

Ответы25943

98 17 окт 2017, 17:40 98 25942

>>25939
>Противоречивость конструктивных оснований
Что уже доказано в самих конструктивных основаниях.

Ответы25943

99 17 окт 2017, 17:41 99 25943

>>25940
>>25941
В ZFC верно исключенное третье, о чем вообще тут говорить.
>>25942
Где?

Ответы25944

100 17 окт 2017, 17:43 100 25944

>>25943
>Где?
В предыдущем треде.

Ответы25945

1 Мб, webm,
640x360, 0:07
101 17 окт 2017, 17:44 101 25945

>>25944
А, это ты. Давай, досвиданья.

Ответы25946

102 17 окт 2017, 17:47 102 25946

>>25945
Что ты хочешь этим сказать? Ты ебанутый, если тебе не очевидно, что из аксиомы Аллаха следует разрешимость типа путей для любого типа. Из чего следует тривиальность всех гомотопических групп любого типа, а можно построить сколько угодно типов с нетривиальными гомотопическими группами.

103 19 окт 2017, 23:00 103 26009

>>25852
Бамп вопросу. Сейчас пытаюсь доказать, что положительное разрешение данного вопроса эквивалентно:
1) существованию непротиворечивой теории типов где исключённое третье отрицается. (тривиально эквивалентно тому, что я пытаюсь доказать)
2) существованию теории типов, где двойное отрицание исключённого третьего недоказуемо. (эквивалентность уже почти доказал, но вот с существованием сложнее)

Что-нибудь уже известно про такие теории? Желательно, чтобы по "мощности" не уступала MLTT, хотя это конечно маловероятно.

Ответы26039

11 Кб, 238x363
104 21 окт 2017, 11:18 104 26039

>>26009
Непротиворечивые основания изложил еще Брауэр в 1907 году. Сама суть там в том, что их противоречивость принципиально невозможна в той мере, в которой не дропаются основные принципы (пример, что бывает, если их дропнуть - парадокс Жирара). Все, что было сделано на эту тему позднее, в т.ч. самим Брауэром - это адаптация его первоначальных идей к несовершенству людишек, которые не имеют физических возможностей работать со сколько-либо сложными ментальными построениями (или алгоритмическими, что то же самое по тезису Черча). Некий компромисс между самой идеей конструктивности и реальными возможностями в т.ч. вычислительных машин. Любая теория типов, MLTT хотя бы, это просто дальнейшее развитие брауэровской теории species/spreads/choice sequences.

Ответы2604026045

105 21 окт 2017, 13:09 105 26040

>>26039
Я не понимаю твой пост. Видимо такой теории типов пока нет, значит сам строить буду. Надеюсь, что мне всё удастся.

106 21 окт 2017, 15:47 106 26045

>>26039
Верно ли, что математический объект не называется существующим, если не известен способ его построения из натуральных чисел за конечное число шагов?

Ответы26046

107 21 окт 2017, 16:05 107 26046

>>26045
>построения из натуральных чисел
Что ты несёшь?

Ответы26047

108 21 окт 2017, 16:09 108 26047

>>26046
Вообще, любой конструктивный объект представим в виде натуральных чисел, поэтому основаниями конструктивной математики является арифметика, а не логика. Я даже Мартин-Лёфа цитировал на эту тему, даже со скринами страниц. Вопрос предыдущего оратора тоже обсуждали уже, ответ на его вопрос положителен с учетом абстракции потенциальной осуществимости, или lazy evaluation в функциональном программировании.

Ответы26050

109 21 окт 2017, 17:16 109 26050

>>26047
>с учетом абстракции потенциальной осуществимости
Вопрос как раз про то, как именно учитывать эту абстракцию.

Ответы26051

110 21 окт 2017, 17:26 110 26051

>>26050
>Вопрос как раз про то, как именно учитывать эту абстракцию.
Да я уж понял, что вопрос про это. Тут больше чем за год никто не понял, как это. Учитывать эту абстракцию очень просто, lazy evaluation называется. Т.е. вычисляется только то, что нужно для конкретного построения. Проще говоря, если мы работаем с множеством N, то нам не требуется веровать в наличие этого множества целиком, как объекта платоновского мира идей. Ах, ох, фофудью отобрали? Но ведь если задуматься, верование в это множество (с точки зрения платонизма) ничего не добавляет к возможностям работы с элементами этого множества.

Ответы2605226122

111 21 окт 2017, 17:28 111 26052

>>26051
То есть само множество N не называется при этом слово "существует", правильно?

Ответы2605326054

112 21 окт 2017, 17:35 112 26053

>>26052
Не он, но я вообще сомневаюсь в существовании множеств.

113 21 окт 2017, 17:35 113 26054

>>26052
Правильно. Есть такое понятие как https://en.wikipedia.org/wiki/Choice_sequence

Ответы26056

114 21 окт 2017, 17:44 114 26055

А рисование значков алеф^n можно назвать математикой?

Ответы2605826059

115 21 окт 2017, 17:55 115 26056

>>26054
Хорошо, спасибо.

116 21 окт 2017, 18:13 116 26058

>>26055
А ты умеешь их рисовать? Рукописный алеф совсем не похож на печатный алеф, он не как буква N.

Ответы26059

45 Кб, 763x512
117 21 окт 2017, 18:20 117 26059

>>26055
>>26058
Нарисовать-то все можно, вот только это каллиграфия, а не математика.

Ответы2606126066

254 Кб, 608x977
118 21 окт 2017, 18:21 118 26061

>>26059
Внимание на последний столбец. Именно так пишут алефы-беты-гимели спецы по теории множеств.

119 21 окт 2017, 20:08 119 26066

>>26059
Аллеф Един.

120 22 окт 2017, 18:51 120 26122

>>26051
Ты из ДС, где учишься? Думаю может тебя пригласить на семинар по этой вот тематике.

121 26 окт 2017, 09:12 121 26317

Сейчас учился рисовать значки алеф, бет и так далее. Это и есть "теория множеств"?

Ответы2632426352

12 Кб, 384x1024
122 26 окт 2017, 16:17 122 26324

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

Ответы2633926390

123 26 окт 2017, 22:21 123 26339

>>26324
Какие значки можно поучить для лучшего понимания теории множеств?

Ответы26361

124 27 окт 2017, 00:09 124 26352

>>26317
Это практика множеств.

387 Кб, 2480x3508
125 27 окт 2017, 02:23 125 26361

>>26339
Алеф, бет, гимель, маленькое с готическое, маленькие греческие омега, эпсилон, эта и дзета. Для дальнейшего исследования - маленькую латинскую эйч, большую греческую тета, еврейскую букву тав, маленькую греческую лямбда, маленькую латинскую k и некоторые другие символы, о которых я сейчас забыл.

559 Кб, 2216x1868
126 27 окт 2017, 13:17 126 26370

127 27 окт 2017, 22:44 127 26390

>>26324
Нужно учить именно рукописный вариант для хорошего понимания теории множеств?

Ответы26398

128 28 окт 2017, 02:19 128 26398

>>26390
Да.

129 1 ноя 2017, 07:57 129 26619

Как начать веровать в исключённое третье?

Ответы40918

130 4 ноя 2017, 03:17 130 26950

Что расскажите про трансфинитные множества в теории вычислимости?

Ответы26952

131 4 ноя 2017, 09:25 131 26952

>>26950
>трансфинитные множества
А такие существуют?

Ответы26961

132 4 ноя 2017, 13:49 132 26961

>>26952
хуйню написал сорян. Не перечислимые множества и теория вычислимости.

282 Кб, 604x511
133 13 дек 2017, 06:44 133 31573

Введение в типы. Смысл слова "вычислять термы".
http://philomatica.org/wp-content/uploads/2016/11/lamb_tuto.pdf

Ответы31574

134 13 дек 2017, 06:50 134 31574

>>31573
>тезис Чёрча
Помолился.

Ответы31575

135 13 дек 2017, 07:03 135 31575

>>31574
А Чёрч от него отошёл.

136 13 дек 2017, 12:23 136 31607

Что такое «интуитивная ясность»?

Ответы31611

137 13 дек 2017, 13:13 137 31611

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

Ответы37068

138 24 фев 2018, 18:10 138 37050

bump

139 26 фев 2018, 12:53 139 37068

>>31611
Я бы доверился в этом вопросе священникам и шизофреникам

Ответы37080

140 26 фев 2018, 17:33 140 37080

>>37068
Ну, каждому свое.

141 2 мар 2018, 15:04 141 37198

Воеводский в одной из своих последних лекций утверждал, что классическая математика сводится конструктивной.

Ответы37204

142 2 мар 2018, 15:05 142 37199

https://www.youtube.com/watch?v=ZVOo7T3GJmI

143 2 мар 2018, 15:34 143 37204

>>37198
Вот поэтому он и умер. Как и конструктивист местный. Мораль: хочешь жить не трогай конструктивную математику.

Ответы372213722937232

144 2 мар 2018, 20:15 144 37221

>>37204
Он не умер, а в /dr/ перекатился.

Ответы37235

145 2 мар 2018, 23:56 145 37229

>>37204
И то верно, желание познавать истину и желание жить - цели редко совпадающие.

146 3 мар 2018, 01:27 146 37232

>>37204
Это заговор жидомасонов ордена Исключённого Третьего.

147 3 мар 2018, 08:31 147 37235

>>37221
Дай ссыль

Ответы37236

148 3 мар 2018, 09:35 148 37236

>>37235
https://2ch.hk/dr/res/190437.html (М)
Ник - Coquus.

Ответы3723737241

149 3 мар 2018, 11:03 149 37237

>>37236
там автор хвастается, что выписывает какую-то притимтивную категорную хуйню

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

не, это просто школьник

Ответы3723837240

150 3 мар 2018, 11:57 150 37238

>>37237
Что ж тебе так припекает от чьей-то личности, да ещё и на анонимной борде? У тебя же все должно быть хорошо, академия ведь во всем права, никаких проблем в основаниях современного понимания науки и математики нет... так ведь?

151 3 мар 2018, 13:12 151 37240

>>37237
Он там пару раз упоминал, что пруверы пишет, так что это всё же он.

Ответы37244

152 3 мар 2018, 13:34 152 37241

>>37236
Тёмные уголки двача, двач наоборот какой-то. брр.

153 3 мар 2018, 14:13 153 37244

>>37240
>Это, вероятно, потому, что автор поста сам не понимает того, о чем пишет, - как какой-нибудь постмодернист. Это такой сорт кофейного помешательства: взять кучу баззвордов и пытаться их упорядочить, ничего не понимая сколько-нибудь глубоко.
>>175125
Слушай, ну похоже. И ник Coquus от coq.

116 Кб, 640x256
154 4 мар 2018, 15:05 154 37276

https://philologist.livejournal.com/9260668.html Математик Владимир Воеводский о своем мистическом опыте и "игре, хозяйкой которой является страх"

Ответы37289

155 4 мар 2018, 20:15 155 37289

>>37276
> Владимир Воеводский о своем мистическом опыте и "игре, хозяйкой которой является страх"
Пиздец, это же у него неврология была какая-то, а не мистика. От чего он умер?

Ответы3729137308

156 4 мар 2018, 20:30 156 37291

>>37289
ты хоть посмотри что неврология означает, знаток душ

Ответы37302

157 4 мар 2018, 22:56 157 37302

>>37291
> знаток душ
Груш. Поехавшим он явно не был, а тут такое - нарушения чувствительности, галюны, расстройства сна итд. 100% клиент невролога.

Ответы37304

158 4 мар 2018, 23:31 158 37304

>>37302
Тут такая забава, невролог с ходу никогда не определяет - его это клиент или нет. Он сначала просит посетить терапевта, как говорится "чтобы исключить другую патологию". Эта такая общая тенденция, когда сталкиваешься с непонятным, то первая, обывательская, реакция - подумать, что существует некий другой человек, который это понимает.

Ответы37399

159 5 мар 2018, 01:42 159 37308

>>37289
Википедия говорит, что от аневризмы. До неврологии далековато.

160 8 мар 2018, 17:42 160 37399

>>37304
Все проще: самый простой способ нихуя не делая как бы "вылечить" чувака это закормить его нейролептиками и антидепрессантами, поэтому все специалисты сейчас сталкивающиеся с чем-то сложнее того, решение чего в первой строчке гугла можно найти, сначала отправляют к психотерапевту, чтобы тот с вероятностью 90% после каких-то идиотских тестов сказал "да у вас депрессия" и прописал это самое.

161 30 мар 2018, 13:23 161 37987

https://youtu.be/E_dGqavx5AU?t=24m52s

Ответы37988

162 30 мар 2018, 15:07 162 37988

>>37987
Как в мат сообществе относятся к Вилдбергеру?

Ответы3800338008

163 30 мар 2018, 21:10 163 38003

>>37988
Как к земле.

164 30 мар 2018, 22:47 164 38008

>>37988
https://www.quora.com/Is-N-J-Wildberger-a-joke-or-a-genius-when-he-claims-that-mathematics-in-its-current-form-is-a-hoax/answer/Hans-Hyttel
Притворяются, что мы уже всё перетерли давно ты че и никаких проблем нет, кто не согласен ебанько.

165 1 апр 2018, 15:39 165 38063

https://www.youtube.com/watch?v=Bo2w25fDLwY

166 10 апр 2018, 00:45 166 38344

Принёс вам свет знаний.

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

Тем не менее были предприняты попытки расширения логического программирования для одновременных вычислений. Однако, Хьюитт и Ага в работе 1999 года утверждают, что результирующая система не является дедуктивной в следующем смысле: вычислительные шаги параллельных систем программирования логики не следуют дедуктивно из предыдущих шагов.

407 Кб, 480x726
167 19 апр 2018, 15:38 167 38588

168 27 апр 2018, 14:18 168 38836

https://mathoverflow.net/questions/298749/contemporary-philosophy-of-mathematics

169 7 мая 2018, 22:07 169 39176

>>25624 (OP)
Как вкатиться?

Ответы39207

170 9 мая 2018, 01:08 170 39207

>>39176
https://www.youtube.com/user/njwildberger MathFoundations

Ответы39246

171 10 мая 2018, 17:59 171 39246

>>39207
Он точно нормальный?
https://www.youtube.com/watch?v=XKy_VTBq0yk&list=PL5A714C94D40392AB&index=15

Ответы39249

172 10 мая 2018, 19:43 172 39249

>>39246
Да, самый лучший.

Ответы39254

173 11 мая 2018, 08:35 173 39254

>>39249
Он верует в "доказательство" от противного. Мы тут такое не приветствуем.

174 12 мая 2018, 00:40 174 39277

https://www.youtube.com/watch?v=wyLDF4j9-8o

175 12 мая 2018, 18:33 175 39288

Тут вам вопросы по петушку(coq) можно задавать или есть более специализированный тредик?

Ответы39293

176 13 мая 2018, 19:07 176 39293

>>39288
Задавай тут, все равно никто нихуя не знает.

Ответы39583

33 Кб, 413x709
177 18 мая 2018, 19:46 177 39563

Тут тред конструктивистов, да?
Помогите выбрать - Coq или Agda?
Я недоматематик-недопогромист, хочу просто немного поиграться с пруверами.
Agda привлекает использованием юникода в синтаксисе, Coq - тем что он более популярный, а следовательно (наверн) для него больше гайдов.

Ответы3956439576

178 18 мая 2018, 20:40 178 39564

>>39563
Ну, начни с Coq, например. С книжки Software Foundations by Benjamin C. Pierce.
Алсо http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AgdaVsCoq

Ответы39574

519 Кб, 471x606
179 19 мая 2018, 04:59 179 39574

>>39564
>последняя правка от 2010 года
С тех пор в этих языках ничего не поменялось?

438 Кб, 570x585
180 19 мая 2018, 05:32 180 39575

Алсо, за https://github.com/leanprover/lean можете что сказать?
Похоже на Агду, только проект кажется более живой.

181 19 мая 2018, 09:01 181 39576

>>39563
> Помогите выбрать - Coq или Agda?
Однозначно кок. Его больше 30 лет уже пилят, там полно тактик на все случаи жизни. Только ставить его лучше через OPAM, даже на шиндовс. И SSReflect к нему очень желательно доустановить. Lean скатили. Когда там было дополнительное ядро HoTT, то да. А так, обычный второсортный прувер.

Ответы3957739597

182 19 мая 2018, 11:17 182 39577

>>39576
ssreflect зачем нужен, в двух словах?
а то что-то взглянул и не понял

183 20 мая 2018, 13:13 183 39583

>>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?
Самое интересное что следующее упражнение, где импликация в другую сторону, я доказал сходу, а вот это нихуя.

Ответы39584

184 20 мая 2018, 13:20 184 39584

>>39583
Доказать, что из ложности "n или m" следует истинность "n и m ложны".
Связка " ИЛИ" или "+", значит, что существует три варианта, когда истина. Когда "ИЛИ", когда "+" или когда " "ИЛИ" и "+" "
Связка "ИЛИ" ложна тогда, когда ЛОЖНО ВСЕ.

Ты должна погрузиться В СУТЬ ИЛИ ИЛИ ИЛИ

185 20 мая 2018, 19:49 185 39587

Можно ли считать, что основания математики/философия математики и есть самая важная математика?

Ответы39588

186 20 мая 2018, 20:05 186 39588

>>39587
Да. Есенин-Вольпин, следовательно, один из важнейших математиков.

49 Кб, 704x396
187 21 мая 2018, 00:17 187 39597

>>39576
>там полно тактик на все случаи жизни. Только ставить его лучше через OPAM, даже на шиндовс. И SSReflect к нему очень желательно доустановить.
Ты уверен что мне это будет важно, учитывая
>хочу просто немного поиграться с пруверами.
?
Я сейчас выбираю Agda или Lean, просто из-за более приятного синтаксиса.

188 21 мая 2018, 02:22 188 39606

Смешно читать, как гуманитарии обсуждают легитимность математич.доказательства. Я работаю на стыке философии и математики и у меня много мат.статей в престижных англоязычных журналах по математике. Так вот, как все выглядит в математике на самом деле. Есть просто профессиональные статьи по математике -- их проверить легко (я сам регулярно пишу рецензии для западных мат.журналов), а есть статьи по математике, притендующие на серьезный результат. Обычно такие статьи не менее, чем страниц на 50 без всякой воды. Вдумайтесь сколько там шагов в доказательстве! Иногда несколько тысяч! Проверить такие статьи -- архитрудная задача. На это способны математики высочайшего класса! Чтобы проверить такую статью, нужно это доказательство повторить вслед за автором. Чтение такой статьи -- это не чтение Сартра перед сном. Оно забирает уйму времени и уйму сил. Поэтому здесь действительно возникает эффект консенсуса. Статью проверили пару десятков человек и этого достаточно для признания. А вдруг они ошиблись?

Ответы39616

189 21 мая 2018, 17:44 189 39616

>>39606
>А вдруг они ошиблись?
Для этого и нужны пруверы и конструктивисты. Чтобы ухмыляться и потирать ручки каждый раз, когда кто-то ошибается.

Ответы39780

190 25 мая 2018, 18:50 190 39780

>>39616
> конструктивисты
Конструктивизм тут вообще не при чем. Ещё де Браун писал про Automath, что это исчисление не привязано к конкретной аксиоматике, а речь всего лишь о лямбдаР. В коке же гораздо более продвинутое CiC. Никто не запрещает туда что угодно прописать, хоть аксиому исключённого третьего, хоть десять заповедей. Любую ебулду можно доказывать в рамках прописанной аксиоматики. Проблема не в этом, а в том, что конечное доказательство к прописанной ебулде и сведется.

191 26 мая 2018, 01:18 191 39784

Хочу перекатиться из математики в основания. Больше всего интересуют кубы Барендрегта и конструктивизм в смысле Маннури. Что почитать?

Ответы39786

192 26 мая 2018, 04:23 192 39786

>>39784
> конструктивизм в смысле Маннури
Он не был конструктивистом.

Ответы39787

193 26 мая 2018, 04:27 193 39787

>>39786
Я этого и не говорил.

194 27 мая 2018, 13:52 194 39857

Смогу ли я упражнения и всю теорию из книжки Зорича по матанализу прорешать и формализовать в Coq?

Ответы3986639873

195 27 мая 2018, 15:53 195 39866

>>39857
Если есть формализация анализа в той полноте, которой требует Зорич, то да. Если нет — то вряд ли. Формализация для компухтерный пруверов это титанический труд, заходи лет через 10.

http://www.ens-lyon.fr/LIP/AriC/MSC2014/clelay.pdf
Посмотри эти слайды, там мелькают названия либ.

196 27 мая 2018, 17:36 196 39873

>>39857
Только если сможешь себя клонировать.

296 Кб, 500x375
197 2 июня 2018, 14:23 197 40054

https://www.youtube.com/watch?v=U75S_ZvnWNk
За Вайлдбергером соскучились? У него новая серия видеороликов всё о том же, о старом выходит. Будет пояснять по хардкору почему современная теория множество - религиозная вера, и на чём нужно строить правильный фундамент для математики на натуральных числах, конечно же.
Спешите видеть.

Ответы4006540090

198 2 июня 2018, 18:32 198 40065

>>40054
Он хотя бы раз употребил словосочетание "доказать Аллаха" или слово "Аллах"?

Алсо, пикрелейтед давно пора ставить в шапку раздела вместо того лысого поца.

Ответы40080

199 2 июня 2018, 22:43 199 40080

>>40065
>вместо того лысого поца
Ты поуважительнее будь, тут тебе не тифаретник.

Ответы40099

200 3 июня 2018, 11:27 200 40090

>>40054
> Будет пояснять по хардкору почему современная теория множество - религиозная вера
За это Брауэр пояснил чуть более 100 лет назад.
> на чём нужно строить правильный фундамент для математики на натуральных числах, конечно же.
Будто не так.

Ответы40124

201 3 июня 2018, 15:03 201 40099

>>40080
Извините, Александр Николаич.

202 3 июня 2018, 23:07 202 40124

>>40090
>За это Брауэр пояснил чуть более 100 лет назад.
Что меня возмущает в Ваилдбергере так это то, что он откровенно игнорирует всю историю интуиционизма, конструктивизма, ультрафинитизма и т.п. Как будто он первый предложил основывать математику на натуральных числах и алгоритмах.

Ответы40225

203 7 июня 2018, 08:21 203 40225

>>40124
А вдруг он не в курсе просто и независимо к этим идеям пришёл?

Ответы40226

204 7 июня 2018, 08:57 204 40226

>>40225
Ну положим независимо - вполне можно в это поверить. То что он игнорирует предшествующие исследования в этом направление говорит либо о том, что он практически ничего не знает о развитие мысли в основаниях математики, либо о том, что все-таки он слышал о конструктивизме, но предпочитает о нем не упоминать. Даже если верно первое, это все-равно плохо о нем говорит - значит он уже много лет пропагандирует свои идеи об основаниях математики и не удосужился прочесть хотя бы что-то уровня статьи в википедии о предмете. Хотя я думаю, что верно второе - он производит впечатление более-менее образованного математика - и ему просто приятнее делать вид что он совершенно оригинален.

205 8 июня 2018, 23:43 205 40273

Я залетный.
Что-то читаю основания, ну там про ZFC, про модели ZFC, и чувствую, что меня хотят наебать. Ну серьезно, все эти von Neumann universe, inacessible cardinals, каждая модель ZFC имеет модель ZFC; существуют модели ZFC, в которых ZFC is inconsistent.
Понял, что не хочу всего этого, хочу палочки к палочкам приписывать, как дедушка Марков завещал.

Ответы40277

206 9 июня 2018, 00:04 206 40277

>>40273
Третья проблема Гильберта гарантирует, что приписывания палочек к палочкам не хватит, чтобы заниматься математикой, то есть теория длин и объёмов необходимо должна использовать рассуждения с бесконечностью. Поэтому однажды кому-то всё-таки придётся строить хорошую, рациональную теорию бесконечного. Текущая стандартная теория множеств несовершенна, многие нужные бесконечности в неё не влезают. Но реформа бесконечного будет, по-видимому, нескоро. Сейчас размышления о теории бесконечного - окраинная часть науки, почти маргинальная. Некоторые философы пытаются сделать свою ТМ, но у них ничего не получается и не сможет получиться, ибо заниматься такими вещами может только математик, очень хорошо изучивший современную математику, а не хуй с горы. Сейчас философы и логики просто априорно что-нибудь постулируют, не заботясь о реальном устройстве науки, и поэтому все их кадавры - мертворожденные.

Ответы40293

20 Кб, 351x351
207 9 июня 2018, 21:22 207 40293

>>40277
> Третья проблема Гильберта гарантирует, что приписывания палочек к палочкам не хватит, чтобы заниматься математикой, то есть теория длин и объёмов необходимо должна использовать рассуждения с бесконечностью.
Есть бесконечность здорового человека и курильщика. Брауэр за это пояснил в своей вступительной речи по случаю назначения профессором в 1912 году, статья "intuitionism and formalism". Он там на пальцах поясняет, почему алеф-нуль - единственная допустимая бесконечность, а континуум ни к какому алефу сводиться не может. Опять же, и тут сто раз обсуждали отличие актуальной бесконечности от потенциальной, по-моему никто так нихуя и не понял.

Ответы4029440295402964031040326

208 9 июня 2018, 22:07 208 40294

>>40293
>алеф-нуль - единственная допустимая бесконечность
Единственное объяснение этому скандальному заявлению, которое было озвучено итт, - религиозно-мистическое. Если у тебя есть какие-нибудь другие - произноси их. В противном случае ты просто фрик, как Катющег.

Ответы40304

109 Кб, 298x376
209 9 июня 2018, 22:29 209 40295

>>40293
О, коконструктивист вернулся. Как жизнь вообще? Как объект? Всё охраняешь?

Ответы4030240307

210 9 июня 2018, 22:36 210 40296

>>40293
> 15197005162890.jpg
>Опять же, и тут сто раз обсуждали отличие актуальной бесконечности от потенциальной, по-моему никто так нихуя и не понял.
Внезапно, эта картинка идеально передаёт твои эмоции.

916 Кб, 245x183
211 10 июня 2018, 00:32 211 40302

>>40295

212 10 июня 2018, 04:37 212 40304

>>40294
> Единственное объяснение этому скандальному заявлению, которое было озвучено итт, - религиозно-мистическое.
Тыскозал?
> Если у тебя есть какие-нибудь другие - произноси их.
Я и принёс. В виде названия конкретной статьи.

Ответы40311

213 10 июня 2018, 10:31 213 40307

>>40295
Он пришёл и ты заикаться начал.

214 10 июня 2018, 13:07 214 40310

>>40293
> Он там на пальцах поясняет, почему алеф-нуль - единственная допустимая бесконечность
Для начала N определить нужно.

Ответы40321

215 10 июня 2018, 14:05 215 40311

>>40304
>Я и принёс
Там написано "интуиционистскозал"

Ответы40321

216 10 июня 2018, 17:37 216 40321

>>40310
> Для начала N определить нужно.
О, N-петух. Так он и определил. Правда, не в этой статье, а раньше.
>>40311
> Там написано "интуиционистскозал"
Тыскозал, что там это написано?

Ответы40322

217 10 июня 2018, 17:47 217 40322

>>40321
>Тыскозал, что там это написано?
Да, япрочетал.

Ответы40327

218 10 июня 2018, 18:34 218 40326

>>40293
Причём самому Брауэру на его интуиционизм было строго поебать всюду кроме философских семинаров. В своих работах по топологии он вплоть до середины XX века пользовался ZFC/NBG, на пенсии начал экспериментировать с аксиомой детерминированности.

Ответы40329

69 Кб, 960x878
219 10 июня 2018, 18:34 219 40327

>>40322
> Да, япрочетал.
Искать знакомые буквы и понимать прочитанное - слишком разные вещи, на примере Брауэра это особенно хорошо заметно. Я вот не сразу въехал в его аргументацию по поводу того, почему восприятие пространства нельзя считать априорным суждением, и т.о в этом вопросе не прав не только Кант, но и автор т.н metaphor theory, объясняющей нейрофизиологию понятия числа, времени итп метрик. И у Брауэра это не просто "ятакскозал", а конкретное математическое доказательство.

220 10 июня 2018, 18:37 220 40328

Давайте придумаем иное слово для бесконечности.

Ответы403684036940374

221 10 июня 2018, 18:40 221 40329

>>40326
Не совсем так. Топологию к интуиционизму он привязал ещё до своего профессорства, просто задача полной реформы математики неподьемна для одного человека, даже если это Брауэр. Поэтому и приходилось пользоваться устаревшими методами.

222 11 июня 2018, 18:17 222 40360

>>25626
Скинь этот R скрипт пж

223 11 июня 2018, 23:38 223 40368

>>40328
Батхерт древних греков.

224 12 июня 2018, 00:06 224 40369

>>40328
Актуальной или потенциальной?

225 12 июня 2018, 11:25 225 40374

>>40328
> Давайте придумаем иное слово для бесконечности.
Так давно уже. Брауэр писал, что одно из свойств two-ity, выводимое путём ее рассмотрения, это "and so forth" (и так далее), возможность продолжать построение дальше. Что и есть потенциальная бесконечность. Насчёт актуальной - разницы нет как называть объект религиозной веры.

Ответы4038140393

226 12 июня 2018, 21:01 226 40381

>>40374
А, ну раз так Браузер писал, то так оно и есть. Слово Браузера - закон.

Ответы40956

227 13 июня 2018, 03:44 227 40393

>>40374
В реальности потенциальной бесконечности не бывает. Текст рано или поздно схлопнется в чер(ниль)ну дыру.

Ответы40398

181 Кб, 1920x1080
228 13 июня 2018, 12:29 228 40398

>>40393
> В реальности потенциальной бесконечности не бывает. Текст рано или поздно схлопнется в чер(ниль)ну дыру.
А это не потенциальная бесконечность. Ты за все это время так и не понял, что это вообще такое, ладно ты, этого не понял и тот кловн, которого ты сейчас цитируешь про чернильную дыру. Не поняли про потенциальную бесконечность, не поняли про существование математического объекта. Вообще нихуяшеньки не поняли, если называть вещи своими именами. И такие вот гейнии мне что-то предъявлять будут и за математику пояснять, пиздец.

Ответы40399

229 13 июня 2018, 12:59 229 40399

>>40398
Нельзя "и так далее" сделать в реальном мире.

Ответы40401

123 Кб, 500x339
230 13 июня 2018, 13:17 230 40401

>>40399
> Нельзя "и так далее" сделать в реальном мире.
Потому оно и называется потенциальным. Strict evaluation такого выражения и приведёт к дыре. Однако, есть ещё lazy evaluation, которое к дыре не приводит. И тем не менее оно возможно в реальном мире, т.к у нас есть правила построения, та самая потенциальная бесконечность. Впрочем, все это за последнюю пару лет мильен раз обсуждалось, посему нот зис шит егейн.

Ответы404214042740430

231 13 июня 2018, 17:03 231 40421

>>40401
Значит, это просто верунство. Всё эти лэзи-городки. В то, чего в реальности быть не может.

Ответы40423

283 Кб, 604x505
232 13 июня 2018, 18:00 232 40423

>>40421
> Значит, это просто верунство. Всё эти лэзи-городки. В то, чего в реальности быть не может.
Охуительные истории. Проснись, это не только может быть в реальности, это уже давно есть в любом языке с зависимыми типами. А вот чего в реальности действительно нет и быть не может, так это актуальной бесконечности и платоновского мира идей. Такое только в религии бывает.

233 13 июня 2018, 18:38 233 40425

Это забавно. Я периодически появляюсь на этой доске (и математических тредах в /sci/ до её появления) уже весьма давно. И каждый раз, когда речь заходит о том, что очень больших чисел в реальности не существует ровно также как и бесконечных объектов, конструктивист начинает юлить и уходит от содержательного обсуждения.

Ответы40428

234 13 июня 2018, 18:54 234 40427

>>40401
>оно возможно в реальном мире
Возможно? То есть, мы не можем сказать, что это существует и просто верим?
То есть потенциальная бесконечность может быть, а может и не быть? Чем это отличается от Аллаха?

709 Кб, 992x1403
235 13 июня 2018, 19:09 235 40428

>>40425
> И каждый раз, когда речь заходит о том, что очень больших чисел в реальности не существует ровно также как и бесконечных объектов,
С этим - к свидетелям алефов. Про отличия фактического построения от правил построения мне нечего добавить к уже сказанному. Мозги купите, что ли.

Ответы40433

236 13 июня 2018, 19:29 236 40430

>>40401
И в чем тогда преимущество если и там и там ты построить ничего не можешь?

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

В каком-то треде видел ты или не ты еще копротивлялся за биологическую обусловленность математики, т.е. то что там в каком-то участке мозга есть что-то похожее на числа в конструктивном смысле, а значит только такая математика - тру. Это вообще кек.

Ответы4043140435

237 13 июня 2018, 19:54 237 40431

>>40430
> Это вопрос интерпретации. Я могу сказать что правила построения бесконечности - это нарисовать ее символ на листочке и принципиально это ничем не отличается от твоих ленивых манядогм.
Думай что хочешь, мне до бороды на самом деле. Если ты не видишь разницы, более того, не понимаешь объяснений, что тут сказать.
> В каком-то треде видел ты или не ты еще копротивлялся за биологическую обусловленность математики, т.е. то что там в каком-то участке мозга есть что-то похожее на числа в конструктивном смысле, а значит только такая математика - тру. Это вообще кек.
С этой темой могу сказать то же самое, что выше. Если тебе не очевидна связь идей Брауэра с современными моделями типа ATOM или MT которая неверна, т.к пространство не может быть априорным суждением, что заметил ещё Сеченов, могу только посочувствовать. Биологически обусловлена не только математика, но и вся вообще деятельность человека. Ну если это тяжеловато понять, остаётся религия.

Ответы40432

238 13 июня 2018, 20:00 238 40432

>>40431
>Ну если это тяжеловато понять, остаётся религия.
Вижу что ты решил остановиться на религии.

P.S. Если бы тебе было до бороды ты вообще бы не отстаивал свои догмы в этом треде

239 13 июня 2018, 21:01 239 40433

>>40428
Ладно, давай разберем не примере.
Утверждение. Для любого натурального n есть простое p большее его.
Доказательство. Число n!+1 взаимно просто со всеми числами <=n, следовательно найдется простое p между n+1 и n!+1.

У меня есть такие вопросы:
1) Конструктивно ли это рассуждение?
2) Можно ли применить его к числу в десятичной системе исчисления n=1000000000000000000000000000000000000000000000000000000000000000000000000?
3) Есть ли принципиальная разница между верой в то, что для этого конкретного n найдется p, основываемая на этом рассуждение (т.е. используя существование числа 1000000000000000000000000000000000000000000000000000000000000000000000000!+1), от веры в то, что нет доказательств противоречия в ZFC длиной <=10000000, обосновываемой на базе существования недостижимого кардинала?

240 13 июня 2018, 21:12 240 40435

>>40430
>Это вообще кек.
Разве? Почему?

Ответы40441

241 14 июня 2018, 00:49 241 40441

>>40435
Потому что это такое же верунство.

Ответы4044440455

242 14 июня 2018, 04:50 242 40444

>>40441
> Потому что это такое же верунство.
Это физиология, дебилок.

Ответы40446

243 14 июня 2018, 12:58 243 40446

>>40444
>Это физиология, дебилок.
И при чем тут математика?

Ответы40447

71 Кб, 850x400
244 14 июня 2018, 13:49 244 40447

>>40446
> И при чем тут математика?
При том, что математика это деятельность человека, никакого мира идей Платона нет. Причём тут математика, написано на пикрелейтед, который сто раз постился.

Ответы4046740484

245 14 июня 2018, 16:29 245 40455

>>40441
Верунство во что? Не понимаю. Ты отрицаешь, что математикой занимаются люди, или что?

Ответы40460

246 14 июня 2018, 17:56 246 40456

А что, интуиционист действительно считает, что всю математику вне секты Брауэра нужно выкинуть и забыть?

Ответы40458

247 14 июня 2018, 18:02 247 40458

>>40456
Нет, так как он считает, что математики вне секты Браузера не существует.

248 14 июня 2018, 19:03 248 40460

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

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

Все твои посты сводятся к пустословию в стиле "мне лень в n раз объяснять", "я уже n раз писал", "мне это не интересно", "не конструктивно - не мотематика, Я СКОЗАЛ" и т.д. с периодисческими ссылками на свои же посты, где точно так же нет никакой конкретики или сепеульки, и с ссылками на книжки на многие сотни страниц.

Ответы4046240467

48 Кб, 419x484
249 14 июня 2018, 19:09 249 40461

В чем смысл обсуждать интуиционизм Брауэра с тем, кто не знает, что это. Ещё меньше смысла не читая Брауэра пытаться его "опровергнуть" своим незнанием предмета. Вы хотя бы это понимаете?

Ответы404644046740484

250 14 июня 2018, 19:13 250 40462

>>40460
> Я СКОЗАЛ"
Мань, ты не туда воюешь. Это мне нужно писать, а не рандомному собеседнику, охуевающему с уровня твоей аргументации а-ля детский сад штаны на лямках. Я ни разу не использовал аргумент "яскозал", а вот ты только им и пользуешься.

Ответы40463

251 14 июня 2018, 19:38 251 40463

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

>Я ни разу не использовал аргумент "яскозал"
"я это уже тыщу раз писал" - это как раз уровень я скозал. Еще бы ты начал прямо яскозакать и мамок ебать, было бы совсем потешно.

Ответы40467

252 14 июня 2018, 20:09 252 40464

>>40461
В чем смысл обсуждать библию и Христа с тем, кто не знает, что это. Ещё меньше смысла не читая библию пытаться её "опровергнуть" своим незнанием предмета. Вы хотя бы это понимаете?

Ответы40467

253 14 июня 2018, 20:28 253 40465

Вот я с начала этого треда успел продвинутую алгебру заботать, научился доказывать клёвые штуки про группы и поля. А что нового узнал ты, интуиционист-кун?

Ответы4046640479

254 14 июня 2018, 20:31 254 40466

>>40465
>А что нового узнал ты, интуиционист-кун?
Его вера в непогрешимость браузера ещё сильнее усилилась.

Ответы4046740956

255 14 июня 2018, 20:51 255 40467

>>40460
>в привычном для твоей демагогии стиле
Что? Это мой второй пост в этом треде. Мне так и хочется предложить тебе принять таблетки, но я воздержусь.

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

>>40447
>>40461
Цитаты вот на этих картинках мне видятся весьма здравыми. Кто-нибудь из несогласных с ними может внятно объяснить, с чем именно он несогласен? Или у вас тут просто какая-то специальная олимпиада? Опять же, извиняюсь, но со стороны вот эти >>40466 >>40464 >>40463 >>40460 посты выглядят нерелейтед бредом шизика, которого непонятно почему еще тут не забанили. Это какой-то троллинг или я чего-то не понимаю?

Ответы4047040471405184052240929

19 Кб, 241x80
256 14 июня 2018, 21:26 256 40470

>>40467
> Это мой второй пост в этом треде

Ответы40518

257 14 июня 2018, 21:31 257 40471

>>40467
Тебя приняли за человека, который некоторое время назад совершенно упорото, люто, дико, безумно воевал с математикой, подняв на знамена почему-то Брауэра. В адекватный разговор с тем человеком пытались, но понимания с его стороны не нашли. Он так затерроризировал сначала тред в /sci, а потом и всю эту доску, что аноны до сих пор реагируют очень нервно, стоит лишь тени этого безумца промелькнуть где-нибудь в уголке.

Ответы404724047940518

258 14 июня 2018, 21:34 258 40472

>>40471
Да это он же, ты что, не видишь? Он уже второй раз на моей памяти "пропадает", ждёт, чтобы на доску пришли ньюфаги, а потом возвращается за свежей едой.

Ответы40473404744047540518

259 14 июня 2018, 21:35 259 40473

>>40472
Ну или это мятежная душа Брауэра кочует из тела в тело. Как вариант.

260 14 июня 2018, 21:37 260 40474

>>40472
Есть некоторый шанс, что всё-таки не он. Впрочем, не пофиг ли.

261 14 июня 2018, 22:42 261 40475

>>40472
Проиграл
Потому что очень похоже на правду

47 Кб, 512x680
262 15 июня 2018, 05:58 262 40479

>>40465
> Вот я с начала этого треда успел продвинутую алгебру заботать, научился доказывать клёвые штуки про группы и поля.
Немалая часть практически полезной алгебры формализована в коковской либе ssreflect. Проще было кок поразбирать.
> А что нового узнал ты, интуиционист-кун?
А я таки нашёл общий подход к реализации изначальной программы Брауэра, чего он сделать не смог. Без всякой теории типов, машин Тьюринга и тезисов Чёрча, сам Брауэр бы не доебался. Алсо я говорил, что пилю прувер по мере возможности, так вот, почти готово :3
>>40471
> В адекватный разговор с тем человеком пытались, но понимания с его стороны не нашли.
Не было адекватного разговора. С самого 2016 года весь разговор с вашей стороны был точно такой же как сейчас, с маняаргументацией, от невменяемости которой хуеют даже мимокрокодилы.
> совершенно упорото, люто, дико, безумно воевал с математикой, подняв на знамена почему-то Брауэра.
Я никогда с математикой не воевал. С моей стороны на этот счёт было только утверждение о религиозном характере некоторых верований, которые натащили в математику ещё древние греки, а именно исключенное третье, актуальные бесконечности и платоновский мир идей. Ну и некоторые производные от этих верований, вроде догмы Гильберта.

Ответы404824048440502

263 15 июня 2018, 07:29 263 40482

>>40479
>практически полезной
Практически полезной для чего/кого?

Ответы40487

264 15 июня 2018, 08:04 264 40484

93 Кб, 850x400278 Кб, 503x335

>>40447>>40461
>>40479
В твоём понимании "математикой" называются теоретические основы функционального программирования, центральным результатом которых является "изоморфизм" Бойля-Кавендиша, устанавливающий связь между написанной на Clojure праграммой и канструктивным доказательством в смысле некоего Лёфа. Ничего из математики в общепринятом смысле ты при этом не знаешь.

Ответы4048740519

265 15 июня 2018, 08:41 265 40487

>>40484
> В твоём понимании "математикой" называются теоретические основы функционального программирования,
Нет, конечно же. Ты даже этого не понял, о чем тут говорить вообще.
>>40482
> Практически полезной для чего/кого?
Для чего/кого вообще полезна алгебра.

Ответы40488

266 15 июня 2018, 08:56 266 40488

200 Кб, 851x400106 Кб, 850x400

>>40487
Лямбда-калькулюс Барендрегта в математике не используется, он относится к праграммированию. Впрочем, у тебя считается, что праграммирование это и есть математика:
>Программисты и есть математики по изоморфизму Карри-Говарда, но ты же не осилил
>>31015
Только вот в изоморфизме Больцмана-Фарадея, который никто кроме тебя на мейл.ру не понял, ничего о математике не утверждалось: там устанавливается соответстветвие между конструктивной теорией типов Мартина Льва и лямбда-исчислением.

Ответы404894049040492

43 Кб, 759x635
267 15 июня 2018, 09:10 267 40489

>>40488
> ничего о математике не утверждалось: там устанавливается соответстветвие между конструктивной теорией типов Мартина Льва и лямбда-исчислением.
Зачем ты лезешь спорить, если нихуя не понимаешь в предмете? В чем твоя мотивация писать всякую хуйню и коверкать названия и имена? Просто пройти мимо богородица не велит? Propositions as sets/types - другое название изоморфизма Карри-Говарда. Забей в гуглтранслейт и постарался сравнить перевод с тем, что ты выше вытужил про типы и лямбду. Ты поди и про более известное соответствие между логическими и теоретикомножественные операции не слышал. И такой вот гейний будет мне что-то пояснять, лол.

268 15 июня 2018, 09:14 268 40490

>>40488
> Лямбда-калькулюс Барендрегта в математике не используется, он относится к праграммированию.
А я ведь цитировал на этот счёт де Брауна и приводил в пример его проект automath. Что вы за хлебушки, все просто же как 3 копейки...

Ответы40491

12 Кб, 468x265
269 15 июня 2018, 09:22 269 40491

>>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 де Брауна
Это который книгу Ландау "Основы анализа" переписал в твоей лямбда-нотации? Ты бы хоть предисловие к ней прочитал, что ли, оттуда совершенно ясны цель и назначение данной книги:
>на каких основных фактах как на аксиомах можно без пробелов построить анализ и как это построение можно начать
Это "основания математики", не математика, разницу тебе неоднократно объясняли.

270 15 июня 2018, 09:23 270 40492

>>40488
> Лямбда-калькулюс Барендрегта в математике не используется,
Ты даже не знаешь, что такое и зачем основания математики, раз такое пишешь.

271 15 июня 2018, 09:26 271 40493

51 Кб, 850x4001,5 Мб, 1024x768

1.5. Охранник должен знать:
- изоморфизм Карри-Говарда и тезис Чёрча;
- содержание диссертации Брауэра в переводе Гейтинга;
- пять уровней языка и четыре способа отрицания по Маннури;
- интерпретацию логических констант по Брауэру-Гейтингу-Колмогорову;
- теорию статистического обучения Вапника и модель spikgram Миколова;
- отличия машины Тьюринга от машины Поста.
1.6 Охранник обязан:
- отрицать закон исключённого третьего;
- отрицать любую математику, не выразимую через типизированную лямбду в MLTT или нормальные алгорифмы Маркова;
- переписать на прувере AUTOMATH де Брауна книгу "Основы математического анализа" Ландау;
- представить все формальные теории в терминах алфавитов, термов и манипуляций с ними;
- свести гомологическую алгебру к исчислению предикатов, используя нумерацию Гёделя.

Ответы4050140505

194 Кб, 800x600
272 15 июня 2018, 09:41 272 40494

Был ли Александр Гротендик математиком с точки зрения известного изоморфизма предпучка Барендргета на категории кубов с теорий типов Льва-Мартинеза?

273 15 июня 2018, 09:43 273 40495

Можно ли учить математике через программирование? Типа делаешь свой язык программирования где числа это палочки и прочее такое. Попозже оптимизируешь. Делаешь свой вольфрам альфа. Потом свой доказатель-проверятор теорем.

Ответы4049640497

274 15 июня 2018, 09:46 274 40496

>>40495
Можно. Иными методами просто не получится в силу изоморфизма Гагарина-Авогадро в категории представлений машин Поста.

275 15 июня 2018, 09:54 275 40497

>>40495
> Можно ли учить математике через программирование?
Нужно. ,21 век таки.
> Типа делаешь свой язык программирования где числа это палочки и прочее такое.
Зачем велосипед, все давно есть. Coq тот же.

276 15 июня 2018, 11:36 276 40498

Какой язык праграммирования/аперационная система лучше всех подходит для занятий математикой? Миша Вербицкий использует Emacs, но я так же слышал положительные отзывы об R Markdown. Хотелось бы узнать про рабочие инструменты великого математика Мартина the Northern Lion Лёфа.

Ответы40499

298 Кб, 683x1024
277 15 июня 2018, 12:43 277 40499

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

278 15 июня 2018, 14:45 278 40501

>>40493
>теорию статистического обучения Вапника
А случаем диакон-конструктивист и вапниколюб из ML треда программача это не одно лицо?

Ответы4050340514

279 15 июня 2018, 15:15 279 40502

>>40479
>Немалая часть практически полезной алгебры формализована в коковской либе ssreflect
А что там есть?

280 15 июня 2018, 15:45 280 40503

>>40501
Одно. Ещё в /dr/ его посты можно найти.

Ответы40514

281 15 июня 2018, 15:54 281 40505

>>40493
Кстати, мы уже выяснили, в какой категории построен изоморфизм Гротендика-Садовничего?

Ответы40506

282 15 июня 2018, 16:00 282 40506

>>40505
В категории Hask сильно каррированных типов.

Ответы40508

283 15 июня 2018, 16:17 283 40508

>>40506
Но ведь Hask - не категория.

53 Кб, 576x432
284 15 июня 2018, 16:59 284 40514

>>40501
>>40503
Из вас сыщики ещё хуже чем математики. В /др я за всю жизнь ни одного поста не написал. А форсил я много что и кого, от нечёткой логики до Настеньки пикрелейтед. Только все это никакого отношения к теме треда не имеет. Впрочем, с моих постов никогда и никто так не рвался, как местный кловн, который походу все мои посты за последний год (если не больше) собрал. Я даже и сам уже не припоминаю, когда я тут про Вапника с Миколовым писал.

Ответы40525

285 15 июня 2018, 17:18 285 40518

>>40470
>>40472
Все-таки идите и принимайте таблетки. А лучше сразу отправляйтесь в /b или в /fag и там детектите своих божков.

>>40471
Это все замечательно, но на вопрос, заданный в >>40467-посте, все-таки не отвечает никак.

Ответы40522

286 15 июня 2018, 17:21 286 40519

>>40484
Я надеюсь, что это такой троллинг тупостью. Для подобного тут вроде есть тред математических мемов, а тут тред вроде про другое.

Ответы40521

287 15 июня 2018, 17:39 287 40521

>>40519
Этот тред не первый в цепочке. Изначально цепочка началась с наркоманских тредов про определение натуральных чисел. Так что безумие в традициях этого треда, для серьезной беседы о чем-то конкретном лучше отпочковаться.

Ответы40533

163 Кб, 645x729
288 15 июня 2018, 18:41 288 40522

>>40518
> Это все замечательно, но на вопрос, заданный в >>40467-посте, все-таки не отвечает никак.
Главная претензия местного подгоревшего дурачка к Брауэру и интуиционизму в том, что из него прямо следует, что бездушная машина в плане математики может ровно столько же, сколько человек. Точнее, это следует из конструктивизма, Брауэр бы с таким выводом не согласился, но тонкие различия неоинтуционизма и различных направлений конструктивизма далеко за пределами способностей к пониманию тутошних дегенератов. По идее, критиковать им было бы логичнее Чёрча и Поста, но для этого нужно их хотя бы почитать, а там букв много и они нерусские какие-то. Это как с критиками эволюции, которые хуесосят Дарвина только потому что в школе больше ни про кого не рассказывают, хотя на деле все их претензии относятся к современной СТЭ, а Дарвин вообще верующим был.

Ответы405234053340538

289 15 июня 2018, 19:04 289 40523

>>40522
А что бесконечные множества ни в каком виде изучать нельзя, ты не упомянул.

Ответы40526

290 15 июня 2018, 19:42 290 40525

>>40514
>все мои посты за последний год (если не больше) собрал
Я думал может что-то новое придумаешь, чем упоминать автомат деБрауна по сто раз.

Ответы40527

291 15 июня 2018, 19:42 291 40526

>>40523
> А что бесконечные множества ни в каком виде изучать нельзя, ты не упомянул.
Можно. И даже упомянул, в какой статье Брауэр доказывает, что алеф-нуль единственная бесконечность, за которой могут стоять правила построения, и что нет ни одного внятного доказательства, что последующие алефы больше, чем алеф-нуль. Все это я упоминал и неоднократно.

Ответы4053040531

24 Кб, 200x284
292 15 июня 2018, 19:45 292 40527

>>40525
> Я думал может что-то новое придумаешь, чем упоминать автомат деБрауна по сто раз.
Если бы ты хотя бы понял, о чем он, можно было бы и что-то более новое упомянуть. А так и этого слишком.

Ответы40528

293 15 июня 2018, 19:47 293 40528

>>40527
Но ты же не понял, что книга Ландау не имеет отношения к математике. Сам Ландау этого не скрывал, указал в предисловии даже.

Ответы40532

294 15 июня 2018, 19:55 294 40530

>>40526
Ну в inaccessible cardinals ты всё еще не веришь. Значит отрицаешь существование топосов, ведь они требуют аксиомы универсума (эквивалентна аксиоме недостижимого кардинала). Хотя ранее и про них что-то упоминал.

295 15 июня 2018, 20:04 295 40531

>>40526
Допустим, что есть биекция f между N и множеством всех подмножеств N. Если x - натуральное число и f(x) = M, то x либо является элементом M, либо не является. В зависимости от этого будем называть натуральные числа соответственно: самопринадлежащие и несамопринадлежащие.

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

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

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

Таким образом, биекции f существовать не может.

Ответы40609

296 15 июня 2018, 20:04 296 40532

>>40528
> Но ты же не понял, что книга Ландау не имеет отношения к математике. Сам Ландау этого не скрывал, указал в предисловии даже.
Эта книга вообще не при чем. Речь о самом прувере automath и почему и что и как его возможности позволяют доказать в математике. Де Браун ясно писал, почему этот прувер не привязан ни к какой аксиоматике, в качестве таковой хоть 10 заповедей можно использовать.

297 15 июня 2018, 21:00 297 40533

>>40521
Если подумать, то немного печально, что для бесед об основаниях математики надо отпочковаться от треда об основаниях математики.

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

Более того, уже сколько постов прошло, а никто так и не сформулировал претензий к цитатам на пиках. Видимо и вправду это все насеменил один местный поехавший. Впрочем, ладно, бог с ним.

298 15 июня 2018, 23:17 298 40538

>>40522
>ровно столько же, сколько человек.
Но машины не могут доказывать теоремы, только проверять.

Ответы40539

299 16 июня 2018, 00:11 299 40539

>>40538
> Но машины не могут доказывать теоремы, только проверять.
Могут. Т.н. тактики в коке кв раз для этого. Но ты веровай и дальше, что не могут, семень тут, неси хуйню про охранников. Вдруг правда поможет.

Ответы40573

sage 300 16 июня 2018, 17:09 300 40573

>>40539
Миллионы обезьян, печатающие на печатных машинках случайные символы тоже могут доказывать теоремы. Конструктивные по крайней мере. Вся суть конструктивизма кароче.

Ответы4057440576

301 16 июня 2018, 17:50 301 40574

>>40573
>Миллионы обезьян
Это ты про homo sapiens?

Ах, нет, забыл. Ведь у этих есть одно очень важное отличие от всех остальных обезьян: богоизбранность. Главное - верить.

Ответы40575

sage 302 16 июня 2018, 18:00 302 40575

>>40574
> мам я такой же умный как математики, ведь я тоже сделан из кварков и электронов)))
Любых обезьян, даже конструктивисты справятся.

Ответы40576

303 16 июня 2018, 19:01 303 40576

>>40573
>>40575
Угадал я значит, причина твоего копротивления - скрепы. Ничем ты не уникальнее обезьяны, и машина Тьюринга может ровно столько же сколько и ты, в том числе и в манипуляции с нарисованными значками, за которыми не стоит ничего. Алгоритмически неразрешимую задачу ты никак не решишь, впрочем и это уже обсуждали, ты тогда знатно обпучкался, показав что понятия не имеешь об идентификации систем. Короче, все с тобой ясно, опученный.

Ответы40578405794058540587

304 16 июня 2018, 20:20 304 40578

>>40576
То есть - никак? Алгоритмически неразрешимое решается доказательством алгоритмической неразрешимости. См. Пенроуз, почему человек не машина Тьюринга.

Ответы40593

305 16 июня 2018, 20:27 305 40579

>>40576
Алгоритмически неразрешимые задачи легко решаются применением исключённого третьего.

Ответы4059340594

sage 306 16 июня 2018, 20:50 306 40585

>>40576
>и машина Тьюринга может ровно столько же сколько и ты
Доказательство где? Или ты адепт свидетелей машины Тюринга? Понятненько, верунство очередное.

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

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

Иван долго смотрел им в след, пока из оцепенения его не вывел заветный доказыватель теорем очередной серией тресков. Работа чуть было не закипела, но тут Иван заметил, что рядом стоит грузный мужчина в пижонской шубе и с тростью. Иван насторожился.
— О, яблочки. Разрешите угоститься, — сказал мужик и недождавшись ответа схватил яблоко и откусил здоровенный кусок, — Ну не смотрите на меня так, у вас яблока много, не жалейте для доброго человека.
— Всего-то два.
Мужик подовился:
— Простите, что? Вы в текущем году веруете в целые числа? А вы их видели то, целые числа эти? А? Видели? Коров небось считали, да яблоки, и думали, вот они — целые числа. Но это всего-лишь приближение реальности, в которой нет никаких целых чисел, ибо всё вокруг непрерывные физические поля, вот где в уравнении Шрёдингера целые числа?..
Но Иван не дал ему закончить, бросив всё, включая солитонный сгусток яблочной материи, он вскачил и стремглав помчался в чащу леса, чтобы жить там и больше никого не видеть, а питаться только супом из ромашек.

sage 306 16 июня 2018, 20:50 306 40585

>>40576
>и машина Тьюринга может ровно столько же сколько и ты
Доказательство где? Или ты адепт свидетелей машины Тюринга? Понятненько, верунство очередное.

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

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

Иван долго смотрел им в след, пока из оцепенения его не вывел заветный доказыватель теорем очередной серией тресков. Работа чуть было не закипела, но тут Иван заметил, что рядом стоит грузный мужчина в пижонской шубе и с тростью. Иван насторожился.
— О, яблочки. Разрешите угоститься, — сказал мужик и недождавшись ответа схватил яблоко и откусил здоровенный кусок, — Ну не смотрите на меня так, у вас яблока много, не жалейте для доброго человека.
— Всего-то два.
Мужик подовился:
— Простите, что? Вы в текущем году веруете в целые числа? А вы их видели то, целые числа эти? А? Видели? Коров небось считали, да яблоки, и думали, вот они — целые числа. Но это всего-лишь приближение реальности, в которой нет никаких целых чисел, ибо всё вокруг непрерывные физические поля, вот где в уравнении Шрёдингера целые числа?..
Но Иван не дал ему закончить, бросив всё, включая солитонный сгусток яблочной материи, он вскачил и стремглав помчался в чащу леса, чтобы жить там и больше никого не видеть, а питаться только супом из ромашек.

Показать весь текст
Ответы40588405924059340604

307 16 июня 2018, 21:21 307 40587

>>40576
И как же тогда человечестов до конструктивизма и комплюктера вычисляло и пользовалось богомерзкими верованиями в физике?

Ответы40593

308 16 июня 2018, 21:28 308 40588

>>40585
Кек новый мем

309 16 июня 2018, 22:09 309 40592

>>40585
>Ивану захотелось третью руку
https://www.youtube.com/watch?v=Xhsl6j6xOEM

310 16 июня 2018, 22:43 310 40593

>>40578
> То есть - никак? Алгоритмически неразрешимое решается доказательством алгоритмической неразрешимости.
Это не решение.
> См. Пенроуз, почему человек не машина Тьюринга.
Извини уж, третьесортный научпоп я не читаю.
>>40579
> Алгоритмически неразрешимые задачи легко решаются применением исключённого третьего.
Исключенноетретье можно и в коке прописать. Это уход от решения, а не решение.
>>40585
> Доказательство где? Или ты адепт свидетелей машины Тюринга? Понятненько, верунство очередное.
Доказательство чего, мань? Того, что ты выше алгоритма не прыгнешь? Так это факт. См выше
>>40587
> И как же тогда человечестов до конструктивизма и комплюктера вычисляло и пользовалось богомерзкими верованиями в физике?
Чего несешь-то? Прочитай хоть на что отвечаешь.

Ответы405964059740600

35 Кб, 807x606
311 16 июня 2018, 22:47 311 40594

>>40579
> Алгоритмически неразрешимые задачи легко решаются применением исключённого третьего.
Проблему останова ты тоже исключённых третьим решишь? Да и правда, или остановится, или нет))))0) И как Тьюринг до такого гениального варианта не додумался?

312 16 июня 2018, 22:57 312 40595

Исключенное третье в математике использовать это просто верх гениальности на самом деле. Зачем вычислять, если можно назвать ответ от балды, все равно он или правильный или нет. 3*3=? Ну или 7 или не 7, очевидно же))0))

Ответы4061240627

313 16 июня 2018, 23:40 313 40596

>>40593
Почитал я про кок и всё равно не вижу, где тут программа что-то доказывает сама. Приведи простой пример кода, который что-то доказывает. По сути мы просто задаём систему аксиом, пишем доказательство, запускаем шайтан-машину, и либо на выходе будет противоречие, либо всё ок.

Ответы4059940617

314 16 июня 2018, 23:59 314 40597

>>40593
>Чего несешь-то? Прочитай хоть на что отвечаешь.
Люди пользовались бесконечностями и прочими нормальными вещами, приходя к решению тех или иных задач, в отличии от догматиков с манятеориями в которых они не могут досчитать до двух.

Даже если под всем этим на самом деле конструктивное начало и все можно свести к нему, это не отменяет полезность, отвергаемых конструктивными сектантами, ментальных конструкций.

Ответы4059840605

315 17 июня 2018, 00:01 315 40598

>>40597
>ментальных конструкций
Ты этим словосочетанием больное место задел.

316 17 июня 2018, 00:02 316 40599

>>40596
Ну там есть тактики вроде omega, которые докажут за тебя, если доказываемые вещи можно свести к Presburger arithmetic, но это именно что proof assistance, а не доказательство чего то нового машиной.

Мимо

Ответы40602

sage 317 17 июня 2018, 00:57 317 40600

>>40593
>Так это факт
Тогда тебе не составит труда его доказать.

>Почитал я про кок и всё равно не вижу, где тут программа что-то доказывает сама.
Никак не доказывает, тактики это чуть лучше, чем кататься ебалом по клаве, пока прувер не перестанет ругаться.

318 17 июня 2018, 01:22 318 40602

>>40599
>если доказываемые вещи можно свести к Presburger arithmetic
Согласно тезису Чёрча это и есть вся математика.

Ответы4061640628

sage 319 17 июня 2018, 01:33 319 40603

Таким образом аргументация коконструктивста ИТТ сводится к тому, что верить ни в какие принципы нельзя. При этом он сам:

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

Можно ещё пройтись по вере в реальность и по органам чувств, но это же не /ph так что пока не будем.

320 17 июня 2018, 01:47 320 40604

>>40585
Все хейтеры конструктивизма такие шизики или это особый экземпляр попался?

Ответы4060640607

389 Кб, 504x597
321 17 июня 2018, 01:51 321 40605

>>40597
>ДИДЫ ВЫЧИСЛЯЛИ!!111

Ответы40628

322 17 июня 2018, 01:58 322 40606

>>40604
Я не хейтер конструктивизма, я просто не возвожу его в религию.

323 17 июня 2018, 02:41 323 40607

>>40604
Ты думаешь, что бредовые идеи типа конструктивизма нужно обсуждать на серьёзных щщах. А на самом деле конструктивизм нужно сразу посылать нахуй. Как ферматиков, как православную арифметику.

Ответы40608

324 17 июня 2018, 03:06 324 40608

>>40607
> Ты думаешь, что бредовые идеи типа конструктивизма нужно обсуждать на серьёзных щщах. А на самом деле конструктивизм нужно сразу посылать нахуй.
Только потому что одному дегенерату с мейлру за свои скрепы обидно? Оно того не стоит.

325 17 июня 2018, 04:42 325 40609

Предлагаю обсудить это >>40531 доказательство. Верное ли оно? Если нет, то где в нём ошибка?

Ответы40612

326 17 июня 2018, 06:21 326 40612

>>40609
Давай лучше вот это доказательство >>40595 обсудим. Если оно верно и в математике вообще допустимо так доказывать, это же вообще все меняет.

Ответы40613

327 17 июня 2018, 06:32 327 40613

>>40612
Но в том посте нет никаких доказательств же.

Ответы40614

29 Кб, 460x460
328 17 июня 2018, 07:22 328 40614

>>40613
> Но в том посте нет никаких доказательств же.
Формально я имел в виду:
?(?, ?) =\/ != 42, где ?() любой оператор, ? в скобках - любая переменная или константа. В общем, ?(?, ?) - любое выражение или лямбда терм. Пример: 1+1 =\/ != 42. Вопрос, допустимо ли так доказывать, если исключенное третье считать допустимым для использования в математике? И если да, зачем тогда вообще математика, если любое выражение можно просто поместить в левую часть "уравнения или не уравнения", и оно будет истинным?

Ответы40630

329 17 июня 2018, 09:14 329 40616

>>40602
Ага, а умножение натуральных чисел это маняфантазии верунов.

330 17 июня 2018, 09:57 330 40617

>>40596
> По сути мы просто задаём систему аксиом, пишем доказательство, запускаем шайтан-машину, и либо на выходе будет противоречие, либо всё ок.
Нет, плохо ты читал. Доказательство не пишем, пишем теорему или теоремы. А кок выдаёт доказательство, если оно возможно в используемой аксиоматике. Это не то же самое, что написать доказательство самому и проверить. Короче, опучкался ты, снова.

Ответы40621

331 17 июня 2018, 12:03 331 40621

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

Ответы40624

332 17 июня 2018, 12:57 332 40624

>>40621
Какие детсадовские попытки заштопать манямир, даже за шиворот ссать жалко лол. Некоторые подмножества исчислений CiC в коке уже сейчас полностью разрешимы с помощью тактик. Насчет остальных - это только вопрос времени, т.к. там более сложные исчисления, не все из которых даже исследованы нормально, Барендрегт и еще 3,5 исследователя все точно не вывезут. Дело только в этом, но ты этого даже не понимаешь, как не понимаешь ,что вообще такое кок и что и как он делает. Отсюда и твои жалкие потуги, "на практике тактики кока не справляются с доказательством содержательных теорем", "очевидных с точки зрения квалифицированных в релевантной области математиков,".

Ответы40626

sage 333 17 июня 2018, 13:51 333 40626

>>40624
Люблю твои сказочки, захожу почитать перед сном как счётчики Гейгера, лемуры и петух доказывают теоремы. И всё сами! Жаль результатов нет, ну наверное просто тетрадочку с теоремами теряют. Ну или ты нассал себе за шиворот и штопаешь свой манямир, который в реальности состоит из 4.5 аутистов, который занимаются вопросами логики, а не математикой.

334 17 июня 2018, 13:51 334 40627

>>40595
А что не так то? Там где тебе нужно знать точное значение это очевидно не подойдет, но если тебе нужно только знать что 7 или не 7 то в чем проблема то?

Ответы40630

335 17 июня 2018, 13:59 335 40628

>>40602
Корень из двух хотя бы до 5 знаков я смогу в твоей маняарифметике найти?
Продемонстрируй короткий кхе-кхе пример.

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

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

И уж тем более долбоебизм называть только это МАТЕМАТИКОЙ. Все хуйня кроме пчел, да

sage 336 17 июня 2018, 14:01 336 40629

https://coq.inria.fr/distrib/8.2/contribs/QArithSternBrocot.sqrt2.html
Ой, а чё так кода много? Я думал omega напишу и мне петух всё докажет.

Ответы40631

337 17 июня 2018, 14:36 337 40630

>>40627
> А что не так то?
Да все так в принципе. Считай, я всю математику доказал априори >>40614 круто, а? Прикинь, берешь любую теорию, делаешь ее арифметизацию геделевскими номерами, дальше как в моём посте. И все, либо 42 либо нет.

Ответы406314063240645

338 17 июня 2018, 14:38 338 40631

>>40629
> Ой, а чё так кода много?
Я проще придумал >>40630 всю математику доказал, я ж крут, а?

339 17 июня 2018, 14:39 339 40632

>>40630
Это все конструктивисты настолько не знакомы с математикой, или ты один такой?

Ответы40638

340 17 июня 2018, 17:07 340 40638

>>40632
> Это все конструктивисты настолько не знакомы с математикой, или ты один такой?
Давай так. Исключенное третье допустимо использовать как доказательство в математике? Да или нет?

Ответы406394064340644

341 17 июня 2018, 17:17 341 40639

>>40638
Что значит "использовать как доказательство"? Это схема аксиом вообще-то. Ты какие книжки по логике читал?

Ответы40645

342 17 июня 2018, 18:25 342 40643

>>40638
Конечно, а как иначе? Приведи простенький пример, показывающий ущербность исключённого третьего.

Ответы4064440645

343 17 июня 2018, 18:29 343 40644

>>40643
>>40638
Ну правда, есть два состояния, истина и ложь, при таком раскладе нечто либо истинно, либо ложно, третьего состояния нет. В чём тут брешь по твоему?

Ответы40645

344 17 июня 2018, 18:34 344 40645

>>40639
>>40643
>>40644
Тогда получается, что я прав вот в этом >>40630 иваще иваще.

Ответы40646

345 17 июня 2018, 19:17 345 40646

>>40645
1+1 = \/ != 42, ну да, это верно. Либо равно, либо нет. Я не понял к чему ты это?

Ответы40647

346 17 июня 2018, 19:18 346 40647

>>40646
Просто это верно так же, как верно 2 = 2. В чём тут доказательство? Это всегда верно, да. Не понимаю тебя.

Ответы40648

347 17 июня 2018, 21:18 347 40648

>>40647
> Просто это верно так же, как верно 2 = 2.
Нет, не так же. 2=2 это вычисление. А 2 =\/ != 2 это исключенное третье.

Ответы40649

348 17 июня 2018, 21:28 348 40649

>>40648
Нет, 2=2 это закон тождества.

Ответы40656

349 18 июня 2018, 05:59 349 40656

>>40649
> Нет, 2=2 это закон тождества.
Вообще-то в математике это доказывается. И "доказательство" уровня той картинки с Пифагором и подписью "хуле тут доказывать, и так видно" это не серьёзно.

Ответы40657

350 18 июня 2018, 06:37 350 40657

>>40656
Вообще - нет, не доказывается. Символ равенства вводится не на уровне математических теорий, а на уровне формального языка. Аксиомы на него налагаются тоже не математикой, а нижележащей логикой.

Ответы40658

351 18 июня 2018, 09:14 351 40658

>>40657
> Вообще - нет, не доказывается. Символ равенства вводится не на уровне математических теорий, а на уровне формального языка. Аксиомы на него налагаются тоже не математикой, а нижележащей логикой.
Сам себе противоречишь. Отношение равенства задается правилами, да. Применение правил этих в каждом конкретном случае возможно только путём вычисления результата. Конечно, так никто не делает, разве что прувер. Человек просто запоминает, что любое число равно самому себе. И в такой форме это уже является лингвистическим правилом, а не математическим, т к не при этом не используется вычислений.

Ответы40665

49 Кб, 1280x720
352 18 июня 2018, 09:55 352 40659

Есть ли математические основания на пучках онли без богомерзской вычислимости?

Ответы40660

353 18 июня 2018, 10:04 353 40660

>>40659
> Есть ли математические основания на пучках онли без богомерзской вычислимости?
На пучках - HoTT, а без вычислимости - ZFC.

Ответы40661

723 Кб, 464x391
354 18 июня 2018, 10:06 354 40661

>>40660
А пучки канструктивны?

Ответы40669

355 18 июня 2018, 13:00 355 40665

>>40658
Сначала прочитай учебники, потом пиши итт.

Ответы40666

356 18 июня 2018, 13:06 356 40666

>>40665
> Сначала прочитай учебники, потом пиши итт.
Будто я что-то не так сказал.

Ответы40668

357 18 июня 2018, 13:34 357 40667

Какие в конструктивизме аксиомы?

Ответы40670

358 18 июня 2018, 14:50 358 40668

>>40666
Да, не так.

Ответы40676

359 18 июня 2018, 15:29 359 40669

>>40661
Я так и не понял, зачем тот анон колоски к моей пикче приделал.
Лучше бы вместо аэропорта на фоне зал МГУ сделали.

Ответы40671

525 Кб, 1600x1200
360 18 июня 2018, 15:33 360 40670

>>40667
В нём нет никакой веры, в нём есть только правила построения. Конструктивизм ведь создавался величайшими математиками, а не ебанатами с мейлру. Впрочем, всё это я объяснял уже сто раз, но вы на мейлру не способны осилить даже известные работы Тьюринга, что уж говорить про действительно глубокие работы Мартина-Лёфа и других 3,5 исследователей в этой области.

Ответы406724067440677

361 18 июня 2018, 15:54 361 40671

>>40669
>колоски
Урожаи и посевы Гротендика же.

Ответы40673

362 18 июня 2018, 16:08 362 40672

>>40670
Правила построения - просто частный случай правил вывода. Ничего нового в них нет.

363 18 июня 2018, 16:13 363 40673

>>40671
Лол, странно что не вспомнил. Спасибо.

364 18 июня 2018, 16:37 364 40674

>>40670
Почему у тебя именно с Мартин-Лефа так жопа горит?

365 18 июня 2018, 17:49 365 40676

>>40668
Ты слился.

мимо

366 18 июня 2018, 18:07 366 40677

>>40670
Мань, тот факт, что исчисление для теории типов несколько отличается по формату от гильбертовских исчислений для классических теорий (в первых в основном все формулируется через правила, во вторых в основном через аксиомы) - это просто вопрос формата задания и те и другие исчисления на самом деле допускают переформулировки в обоих стилях. Что более существенно -это то, какие стили математических рассуждений эти исчисления призаны моделировать. В случае с теорией типов Марти-Лёфа соответствующий тип рассуждений - это рассуждение в терминах индуктивных конструкций. И такие рассуждения активно опираются на абстракцию потенциальной бесконечности (и да, для того чтобы принимать такие рассуждения нужно верить в эту абстракцию.

Ответы40681

367 18 июня 2018, 20:58 367 40681

>>40677
> (и да, для того чтобы принимать такие рассуждения нужно верить в эту абстракцию.
Эта абстракция подразумевается например при задании правил построения типа N. Допустим, я в неё не верю. И что, у меня от этого перестанет работать например тактика ring в коке? Веровать можно в нечто изначально оторванное от построения, точнее в допустимость использования такого.

Ответы40683

368 19 июня 2018, 09:11 368 40683

>>40681
Стандартное определение типа N - это по существу определение натуральных чисел через приписывание палочек. Это действительно базовая вещь явно подкрепленная нашим практическим опытом. Но теория типов производит очень широкое обобщение этого и в ней таким образом строятся не только натуральные числа, а населяется вся вселенная типов, включающая замысловатые функционалы высших типов, вселенные (во внутреннем смысле) и т.п. И здесь связь с практическим опытом разумеется теряется, остается только верить в то, что все правила построения новых функционалов сохраняют потенциальную вычислимость на любых входах которые потенциально могут быть построены в рамках незаконченной вселенной.

Кстати, проблемы с теорией множеств носят такой же характер, только там они вместо переноса интуиции касающийся натуральных чисел на высшие типы, они перенесли интуицию касающуюся конечных множеств на произвольные. Что характерно, в первых попытках построить формальные теории и там и там нашли противоречия (см. парадокс Жирара и парадокс Рассела соответственно).

Ответы4068540686

369 19 июня 2018, 10:21 369 40685

>>40683
Ты думаешь, хоть кто-то итт не знает про парадокс Рассела?

370 19 июня 2018, 11:41 370 40686

>>40683
> (см. парадокс Жирара и парадокс Рассела соответственно).
Парадокс Жирара тривиально обходится кумулятивной иерархией типов, я вообще не знаю, о чем Мартин-Леф думал, когда вводил правило type : type, очевидно же, что сразу надо было что-то вроде type i : type i+1.
> И здесь связь с практическим опытом разумеется теряется, остается только верить в то, что все правила построения новых функционалов сохраняют потенциальную вычислимость на любых входах которые потенциально могут быть построены в рамках незаконченной вселенной.
Это ещё у Брауэра решено, 2ой акт интуиционизма. Построение делается только на основании уже построенного ранее более простого, либо по некоторым критериям равенства с уже построенным. Какой угодно функционал своим к более простому, у того же Мартин-Лефа суждения (общие схемы посылок и заклбчений в правилах) рассматриваются по нарастающей сложности, для одной переменной, для двух и для n.
> Кстати, проблемы с теорией множеств носят такой же характер, только там они вместо переноса интуиции касающийся натуральных чисел на высшие типы, они перенесли интуицию касающуюся конечных множеств на произвольные.
И тут же обосрались, потому что всякие недостижимые кардиналы не строятся на основе конечных множеств, как построения в теории типов или интуиционизме, а просто вероваются от балды, причём нет даже внятных пруфов того, что алеф1 больше чем алеф-нуль, на что Брауэр указывал ещё в 1912 году.

Ответы4068840696

371 19 июня 2018, 12:48 371 40688

>>40686
>Парадокс Жирара тривиально обходится кумулятивной иерархией типов, я вообще не знаю, о чем Мартин-Леф думал, когда вводил правило type : type, очевидно же, что сразу надо было что-то вроде type i : type i+1.
Ну да, ровно также как обошли парадокс Рассела. А тот факт, что Мартин-Лёф облажался показывает, что ровно также как и у теоретико-множественников наивная интуиция теоретико-типовиков подвережена парадоксам.
>либо по некоторым критериям равенства с уже построенным
Это ключевое место. Фунции в теории типов могут применяться к любым термам соответствующего типа, в частности к термам которые будут введены после введения этой фунции. И чтобы считать, что даже какая-то очень простая фунция (например следования на натуральных числах) тотальна нужно предполагать, что любой терм который когда-либо может быть построен будет равен терму в канонической форме (т.е. в данном примере по нему можно вычислить конкретное натуральное число). Другими словами происходит использование глобальных свойств ещё незаконченной вселенной. На мой взгляд совершенно правильно называть это верой, если мы называем верой пригятие вселенной множеств фон Неймана.

Теорию множеств ты совсем не понимаешь. Недостижимые кардиналы прямой аналог вселенных в теории типов т.к. каппа недостижим если и только если капповый уровень вселенной фон Неймана модель ZFC. И если Брауэр не принимал аксиому степени, то конечно он не принимал существования несчетных мощностей. Просто одни люди произвели более широкре обобщение простой конечной математики, а некоторые (Брауэр) менее широкое.

Ответы4069040698

372 19 июня 2018, 13:22 372 40690

>>40688
> Другими словами происходит использование глобальных свойств ещё незаконченной вселенной. На мой взгляд совершенно правильно называть это верой,
А какие могут быть проблемы с правильно типизированными термами?
> Недостижимые кардиналы прямой аналог вселенных в теории типов
Вообще, разница в использовании актуальной бесконечности. В теории множеств это делать не стесняются, в отличие от. Но если ты говоришь, что речь об аналоге иерархий вселенных, и допустимо написать, например алеф-нуль : алеф1 и в целом алеф i : алеф i+1, тогда вообще интересно получается. Так ведь можно сказать и про мир идей Платона и тогда выходит, что Платон был конструктивистом, а в основаниях математики кроме конструктивизма ничего никогда и не было.

Ответы4069140694

373 19 июня 2018, 13:48 373 40691

>>40690
>в отличие от
RUSSIAN MOTHERFUCKER DO YOU SPEAK IT

>Так ведь можно сказать и про мир идей Платона и тогда выходит, что Платон был конструктивистом, а в основаниях математики кроме конструктивизма ничего никогда и не было.
Преемственность, слыхал о такой?
Никакого конструктивизма не было и нет, было развитие идей обычной математики. Просто несколько хитрецов грамотно пропиарились выделив это во что-то непохожее и назвав другим словом.

Ответы4069840727

374 19 июня 2018, 14:09 374 40694

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

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

Ответы40698

375 19 июня 2018, 14:36 375 40696

>>40686
Алеф 1 больше Алеф 0 по определению, если ты не в курсе.

Ответы40698

376 19 июня 2018, 15:19 376 40698

>>40694
> Просто при рассуждениях в ней в общем случае неявно используется предположение, что все термы данного типа, которые потенциально могуть быть построены в процессе (сколь угодно длительной) деятельности в теории типов, могут быть полностью вычислены.
Почему "неявно"? Это явное предположение. И оно прямо вытекает из правил построения. Если у нас есть правила построения N, то из них прямо следует потенциальная построимость любого элемента этого типа. То же с любым другим типом, любой терм, являющийся элементом этого типа строится по правилам построения элемента этого типа, т.е. этот терм правильно типизирован, в противном случае он не является термом данного типа. Мы не можем взять этот элемент из мира идей Платона, мы его можем либо построить явно, либо задать общее правило построения, либо задать правила его вычисления из какого-то другого терма (бета- и др. редукции итд).
> Это сильное предполжение, на самом деле я не знаю, как такое предположение обосновать не аппелируя к законченному построению вселенной т.е. к актуальной бесконечности;
Вот ты говоришь, что я не понимаю теорию множеств, а ты похоже, не понимаешь разницу между потенциальной и актуальной бесконечностью. Правило построения "type i : type i+1" это потенциальная бесконечность, а аксиома "существует бесконечное множество" - это актуальная.
>>40696
> Алеф 1 больше Алеф 0 по определению, если ты не в курсе.
Если это понимать в смысле, указанном предыдущим оратором >>40688 то да, т.к. получается кумулятивная иерархия типов. Но тогда это конструктивизм простой, от которого тут кое-кто рвется уже пару лет. Если же понимать это с позиции теории множеств, то Брауэр пояснил, какие пробемы из этого вытекают.
>>40691
> Никакого конструктивизма не было и нет, было развитие идей обычной математики
Брауэр и за это пояснял, в чем разница. Ты тут точно ничего нового не скажешь, поверь.

Ответы406994072840784

377 19 июня 2018, 15:27 377 40699

>>40698
Дай определение алефа-1. Ты его как-то по-своему понимаешь, похоже.

Ответы40700

378 19 июня 2018, 15:31 378 40700

>>40699
У алефа-1 в смысле теории множеств нет внятного определения, так как не даны правила построения.

Ответы4070140763

379 19 июня 2018, 15:49 379 40701

>>40700
Ты используешь этот термин. Что лично ты под ним понимаешь?

Ответы40703

380 19 июня 2018, 15:55 380 40703

>>40701
Я под ним понимаю некое религиозное верование. Алефы выше алефа-0 невозможно понять человеческим мозгом, так как для них нет правил построения. Это следует из применения тезиса Чёрча к пояснению Брауэра о невозможности вычисления алефа-1 и выше.

Ответы40709

381 19 июня 2018, 15:56 381 40704

Я вот думаю, конструктивизм, он как дальтонизм. Есть люди, спокойно воспринимающие цвета и видящие их все. А есть, те которые видят мир черно-белым. Конструктивисты, как дальтоники, неспособны понять бесконечность, когда нормальные люди абсолютно без проблемы работают с ней.

Ответы40705

382 19 июня 2018, 15:59 382 40705

>>40704
> Конструктивисты, как дальтоники, неспособны понять бесконечность, когда нормальные люди абсолютно без проблемы работают с ней.
С чем ты там работаешь? То, что ты понимаешь под "работой с бесконечностью" - чисто лингвистические, а не математические построения.

Ответы40708

383 19 июня 2018, 15:59 383 40706

Вот, и когда здоровый человек пытается рассказать дальтоники о других цветах, тот неспособен их представить и понять, пытается всё выразить своим ограниченым взгядом, и после неудачной попытки влючается ВРЁТИ ДРУГИХ ЦВЕТОВ НЕ СУЩЕСТВУЕТ, ВЫ В НИХ ВЕРИТЕ, ДРУГИЕ ЦВЕТА, КАК АЛЛАХ!

Ответы4070740726

384 19 июня 2018, 16:00 384 40707

>>40706
Рассказать можно и про гаррипоттера с файрболами. Того же уровня твое понимание бесконечности.

Ответы40711

385 19 июня 2018, 16:01 385 40708

>>40705
А что понимает здоровый человек, когда говорит о цветах, неспособных быть увиденными дальтоником?

Ответы40713

386 19 июня 2018, 16:01 386 40709

>>40703
Ты сделал утверждение об алефе-1. Ты отказываешься объяснить, что ты подразумеваешь под термином "алеф-1".

Ответы40712

387 19 июня 2018, 16:01 387 40710

Я вот думаю, алефизм, он как даунизм. Есть люди, спокойно понимающие разницу между абсолютной и потенциальной бесконечностью. А есть те, которые видят мир исключительно через свою веру. Алефисты, как дауны, неспособны понять концепцию правил построения, когда нормальные люди абсолютно без проблем понимают её и каждый день работают с правилами построения.

388 19 июня 2018, 16:02 388 40711

>>40707
Как по-твоему можно выразить цвета разных оттенков через черный и белый? Как синий выразить через них? То же самое и с конструктивной математикой.

Ответы40713

389 19 июня 2018, 16:03 389 40712

>>40709
Я понимаю под этим термином объект религиозной веры вроде Христа или Аллаха, тут можно много чего подставить, но результат один - невычислимая хуета.

Ответы40716

390 19 июня 2018, 16:04 390 40713

>>40708
>>40711
Гуманитарные сказочки и левые аналогии, это очень убедительно в математике, да. Такие же аргументы у религиозных проповедников.

391 19 июня 2018, 16:06 391 40716

>>40712
Если ты делаешь утверждение, в котором хотя бы одно слово не может быть тобою определено, - ты несешь ахинею. Ты сделал утверждение "нет пруфов того, что алеф-1 больше чем алеф-0".

Ответы40752

289 Кб, 1728x800
392 19 июня 2018, 16:36 392 40726

>>40706
Хех, что-то проиграл с твоего поста. Недели 2 назад даже гугл намекнул. В одном из рекламных сообщений впарашке выдало пикрил и сообщение о какой-то клинике которая обследует глаза. Я тогда отметил что это странно т.к. по моим запросам ничего подобного выдать не должно. Обычно любое рекламное объявление я примерно знаю почему мне выдало, а тут вдруг совсем не в тему. А после твоего поста внезапно ОСОЗНАЛ. Ведь в последнее время я пытаюсь вступить в секту, искал и качал все эти книжки что тут кидает конструктивофорсер, про ML теорию, машинку поста и т.д. На фоне чтения возникает много релейтед запросов в гугл. В общем все сходится. А киберпанк в лице гугла уже наступил

Ответы40732

393 19 июня 2018, 17:09 393 40727

>>40691
>>в отличие от
>RUSSIAN MOTHERFUCKER DO YOU SPEAK IT
https://ru.wiktionary.org/wiki/в_отличие_от
Тебе учебник для страшеклассников по русскому языку посоветовать?

Ответы40748

394 19 июня 2018, 17:21 394 40728

>>40698
>Правило построения "type i : type i+1" это потенциальная бесконечность, а аксиома "существует бесконечное множество" - это актуальная.
Анон, так он о том и говорит (если я правильно понял): мы предполагаем, что мы можем построить и вычислить каждый из термов, заданных этим правилом, но у нас для этого нет никаких оснований. Самый простой способ получить такое основание - считать, что вселенная уже построена, то есть все эти термы существуют (то есть свести это к актуальной бесконечности). В противном случае получается, что возможность построения у нас основана на такой же вере, как и у всех остальных математиков.

Ответы40746

395 19 июня 2018, 17:26 395 40732

>>40726
>сообщение о какой-то клинике которая обследует глаза.
>Обычно любое рекламное объявление я примерно знаю почему мне выдало, а тут вдруг совсем не в тему.
То есть о том, что ты много сидишь за компьютером и гугл предполагает, что у тебя от этого портится зрение, ты не подумал? Спишу на то, что ты приукрасил историю ради комического эффекта.

Ответы40747

17 Кб, 274x274
396 19 июня 2018, 17:46 396 40741

Аноны, помогите построить синий цвет. Нужно конструктивное доказательство через смешение черного и белого цвета. Или что синий цвет, он как Аллах, в него верить надо?
(Автор этого поста был забанен. Помянем.)

397 19 июня 2018, 19:47 397 40746

>>40728
> Самый простой способ получить такое основание - считать, что вселенная уже построена,
Т.е уверовать в это? Ведь не построена по факту-то.
> В противном случае получается, что возможность построения у нас основана на такой же вере, как и у всех остальных математиков.
Про возможность никто не говорил. Речь про правила построения. Которые не требуют никакой веры, т к они есть независимо от того, веруешь или нет.

Ответы40754

398 19 июня 2018, 20:14 398 40747

>>40732
Не думаю. И я ничего не преукрашивал

399 19 июня 2018, 20:15 399 40748

>>40727
Тебе бы самому почитать что там по ссылке.

Ответы40753

400 19 июня 2018, 21:21 400 40752

>>40716
Определи мне Я, умник хуев.

401 19 июня 2018, 22:09 401 40753

>>40748
Почитал, тебе процитировать?
>в от-ли-чи·е от
>Устойчивое сочетание.
>(от кого, чего) в противоположность кому, чему
Ты не нейтив спикер? Может тебе на simple russian переформулировать? Ты не стесняйся, анон, спрашивай - тут доска взаимопомощи, отвечаем на вопросы, помогаем друг другу. Можешь еще заглянуть в international math thread, анон: https://2ch.hk/math/res/27513.html (М) - ты сам откуда будешь, из какой страны-языка?

Ответы40755

402 19 июня 2018, 22:11 402 40754

>>40746
>Т.е уверовать в это? Ведь не построена по факту-то.
Ну так он тебе об этом и говорит, вот!

>Про возможность никто не говорил.
Ну когда ты пишешь type i : type i + 1, ты же предполагаешь, что единицу мы можем прибавлять сколько угодно, пользуясь заданными правилами построения, так?

Ответы40756

403 19 июня 2018, 22:34 403 40755

>>40753
Блин, ну не тролль пжл "нейтив"
https://ru.wikipedia.org/wiki/Предлог

Второе предложение процитировать или сам прочтешь?

Ответы40758

404 19 июня 2018, 22:45 404 40756

>>40754
> Ну когда ты пишешь type i : type i + 1, ты же предполагаешь, что единицу мы можем прибавлять сколько угодно, пользуясь заданными правилами построения, так?
Это прямо прописано в правиле, зачем там что-то предполагать? Незачем предположение, что уже все построено, т.к оно ничего не даёт дополнительно к правилу, даже если бы и правда было построено. Т.е имеем абсолютно ненужную сущность, вера в которую никакого смысла не имеет.

405 19 июня 2018, 23:09 405 40758

>>40755
Анон, ну куда ты лезешь? Погугли, что такое эллипсис. И в следующий раз, когда запутаешься в окончаниях, просто сразу признай, что ты обосрался (с кем не бывает, анон), а не пытайся по ходу дела маневрировать в материях, о которых ты имеешь весьма и весьма смутное представление.

Продолжить дискуссию можем (можешь) в треде русского языка в /fl.

Ответы4076040762

406 19 июня 2018, 23:36 406 40760

>>40758
Ой, блять, ладно, если ты сам знаешь такие слова то поверю что намеренно. Но как НЕЙТИВ тебе заявляю, выглядит по-уебански, на манер английских deferred prepositions и так на русском не пишут.

Ответы4076140799

407 19 июня 2018, 23:40 407 40761

>>40760
Нормально выглядит. Конечно, похоже немного на ущербное "это зависит", но в пределах нормы.
мимо

408 19 июня 2018, 23:57 408 40762

>>40758
>весьма и весьма
Тут нужна была запятая.
мимо лингвист

Ответы40799

409 20 июня 2018, 02:01 409 40763

>>40700
Алеф-1 можно явным образом определить как множество всех не более чем счетных ординалов. Легко видеть, что при таком определении алеф-1 не биективен алеф-0.

Ответы40767

410 20 июня 2018, 05:06 410 40767

>>40763
Множество не более чем счетных ординалов само по себе не более чем счётный ординал

Ответы40768

411 20 июня 2018, 05:14 411 40768

>>40767
Тогда оно является элементом самого себя, что запрещено аксиомой регулярности.

Ответы40770

412 20 июня 2018, 07:24 412 40770

>>40768
> Тогда оно является элементом самого себя
Подмножеством. К i+1 хоть сколько добавляй, так из алефа0 алеф1 не построить.

Ответы40771

413 20 июня 2018, 09:04 413 40771

>>40770
Если ординал, состоящий в точности из всех не более чем счетных ординалов, сам является счетным, то он является своим элементом. По определению. Понимаешь?

414 20 июня 2018, 13:41 414 40784

>>40698
> Если у нас есть правила построения N, то из них прямо следует потенциальная построимость любого элемента этого типа.
В том то и дело, что этого недостаточно. Термы типа N могут быть сформулированы в терминах произвольных других типов, например можно формализовать подходящий кусок топологии и выписать терм обозначающий какой-нибудь числовой инвариант какого-нибудь пространства. В итоге вопрос о том, вычислимы ли произвольные термы данного конкретного типа зависит от всей системы в целом, а не только от определения данного конкретного тип; если взять какой-нибудь вариант теории типов в котором есть противоречие, то в ней будут термы типа N, которым не будет соответствовать никакого значение. И хотя с твоей стороны происходит заметание этого вопроса под ковер, наличие такого глобального свойства требует обоснования для каждого конкретного варианта теории типов.

На мой взгляд наиболее естественный способ обосновать, почему конкретный вариант теории типов работает как следует, т.е. все термы вычислимы - это построить её модель (в терминах рекурсивных функционалов высших типов).
Конечно можно говорить, что-то в духе того, что все определения типов, которые дают "квалифицированные" теоретико-типовики в некотором смысле "правильны" и сохраняют "правильность" теорий типов и во всех "правильных" теориях типов все вычислимо. Проблема в том, что если посмотреть, что должно соответствовать "правильности" с более формальной точки зрения, то наиболее родственно оно конструкциям возникающим в доказательствах сильной нормализуемости сильных лямбда исчислений и там определения таких свойств существенно опирается на квантификацию по бесконечным множествам (см. доказательство сильной нормализуемости системы F). Но как ни крути, либо нужно принять на веру, что (довольно туманная) интуиция теоретико-типовиков никогда не приводит к проблемам, либо дать обоснование в терминах бесконечных множеств.

Ответы407904080840810

415 20 июня 2018, 16:53 415 40790

>>40784
>это построить её модель
Я не понимаю, как вообще можно доверять этому методу. Ведь у нас нет ни одной гарантированно свободной от противоречий теории, в которой можно было бы строить более-менее содержательные модели.
другой анон

Ответы40803

416 20 июня 2018, 19:50 416 40799

>>40760
Как минимум с конца 90-ых этот оборот широко употребляется в разговорной (форумной) речи. Не думаю, что тут есть какое-то влияние английского, если честно.

>>40762
Смищно.

Ответы40816

417 20 июня 2018, 22:42 417 40803

>>40790
>Ведь у нас нет ни одной гарантированно свободной от противоречий теории, в которой можно было бы строить более-менее содержательные модели.
Таким образом мы можем редуцировать корректность одной теории к другой. И если теория к которой происходит редукция в каком-нибудь смысле понятнее редуцируемой теории, то это до некоторой степени объясняет последнюю.

Кстати, как ты себе представляешь гарантии свободы от противоречий для какой-либо теории, которая формализует хотя бы арифметику натуральных чисел? Ведь для любой такой теории есть неограниченно много доказательств и поэтому гарантировать непротиворечивость можно только приняв какой-нибудь метод установления универсальных утверждений.

418 21 июня 2018, 04:35 418 40808

>>40784
> И хотя с твоей стороны происходит заметание этого вопроса под ковер, наличие такого глобального свойства требует обоснования для каждого конкретного варианта теории типов.
Твоя проблема в том, что ты не понял сути конструктивизма и поэтому пытаешься натянуть его на формализм как сову на глобус. А оно изначально создавалось не для этого, более того, формализация интуиционизма невозможна принципиально. Я уже пояснял за это, но местный шизик все закукарекал. Формализация понятия алгоритма (и интуиционизма Брауэра) невозможна по той простой причине, что таковая должна одновременно решать и проблему останова универсальной машины Тьюринга. Поэтому в конструктивизме речь только об уточнении понятия алгоритма (нормальные алгоритмы Маркова, машина Тьюринга итд). Именно по этой причине, о которой говорил ещё Брауэр, обосрался Гильберт со своей изначальной программой формализма.
> Но как ни крути, либо нужно принять на веру, что (довольно туманная) интуиция теоретико-типовиков никогда не приводит к проблемам, либо дать обоснование в терминах бесконечных множеств.
Вот ещё одно подтверждение, что ты не понимаешь тех соображений, которые вообще привели к созданию конструктивизма. MLTT корректна и непротиворечива не потому что преподобный рабби Леф так скозал, а по той простой причине, что в ней принципиально невыразимо невычислимое в ней же. Оно исходя из этого и создавалось. Противоречивость подобных теорий видно сразу же, самый известный пример - парадокс Жирара, суть которого в том, что при использовании правила построения type : type появляется возможность выразить в mltt парадокс Рассела, т.е невычислимую хуету. Менее известные примеры противоречивых лямбда исчислений есть у Барендрегта.

Ответы40830

419 21 июня 2018, 05:24 419 40810

>>40784
> На мой взгляд наиболее естественный способ обосновать, почему конкретный вариант теории типов работает как следует, т.е. все термы вычислимы - это построить её модель (в терминах рекурсивных функционалов высших типов).
Это бессмысленно. Я тут миллион раз упоминал книжку "Programming in Martin-Lof type theory", авторов не помню, какие-то шведские куколды, так вот, она является наиболее полным изложением mltt и написана под руководством Мартин-Лефа. Так вот, там в предисловии прямым текстом написано, что mltt создавалась как основания и поэтому её представление в других теориях смысла не имеет, это наоборот другие теории должны выражаться в ней. Поэтому, единственный смысл, семантика mltt это вычислимость. Она выразима в терминах операционной семантики (в приложении они перечислены), что делает её не только основаниями, но и языком программирования (изоморфизм Карри-Говарда). Последнее касается не только конкретно mltt, но и CiC (Coq) и UTT (Idris) итд.

Ответы408174082240830

420 21 июня 2018, 10:48 420 40816

>>40799
Как оборот?

421 21 июня 2018, 11:05 421 40817

>>40810
>Последнее касается не только конкретно mltt, но и CiC (Coq) и UTT (Idris) итд.
А python и javascript тоже основаниями математики являются? Не для себя спрашиваю.

Ответы40819

422 21 июня 2018, 11:14 422 40818

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.

423 21 июня 2018, 11:16 423 40819

>>40817
> А python и javascript тоже основаниями математики являются?
Я ссылался на операционную семантику mltt, она очень простая. Coq на жабаскрипте давно существует, если что. Lean тоже есть на жабаскрипте, причём был ещё 2ой версии, где ядро HoTT. Так что ответ - да, изоморфизм Карри-Говарда допускает такую возможность.

424 21 июня 2018, 16:46 424 40822

>>40810
>mltt создавалась как основания и поэтому её представление в других теориях смысла не имеет, это наоборот другие теории должны выражаться в ней
Лол.

Ответы40825

425 21 июня 2018, 17:07 425 40825

>>40822
Говоря проще, это лишнее. Бурбаки, Кантор, Гильберт теорию множеств через другие не представляли. И никто не лолкает. Так и тут, есть операционная семантика, этого достаточно для работоспособности mltt, зачем огород из пучков городить.

Ответы40833

426 21 июня 2018, 19:43 426 40830

>>40808
>>40810
Это понятно, что ты в своем представление теории типов в качестве самодостаточных оснований следуешь за Мартин-Лёфом.
В принципе, с этим нет особых проблем. Есть довольно много математиков, которые привыкли думать о математике в бурбакистском ключе и поэтому для них аксиоматика Цермело-Френкеля представляет из себя формализацию самоочевидных принципов - у них уже есть преконцепция что такое множества и что с ними можно делать, а аксиомы просто соответствуют этой интуиции. Ровно также на существование имеет право и более маргинальная позиция людей думающих о математике в интуиционистских терминах для которых самоочевидной оказывается теория типов.
Не буду скрывать - я привык к бурбакисткому изложению математики и соответственно у меня развита именно интуиция касательно понятия множества, а не типа. Поэтому с неизбежностью я смотрю на интуиционизм и его формализации со стороны.
И как я уже довольно подробно расписал в нескольких предшествующих постах, анализируя их со стороны довольно прозрачно, что в них неявно заложены сильные и выходящие далеко за пределы вычислимой математики предположения (здесь под вычислимостью я понимаю вычислимость на натуральных числах) - особенно явно это проявляется в версиях с W-типами и вселенными.
>MLTT корректна и непротиворечива не потому что преподобный рабби Леф так скозал, а по той простой причине, что в ней принципиально невыразимо невычислимое в ней же.
Буллщит, феномен второй теоремы Гёделя о неполноте очень общий и чтобы доказать корректность (или хотя бы непротиворечивость) какого-либо метода рассуждений заведомо нужно выйти за его пределы.
>Противоречивость подобных теорий видно сразу же
Отмечу, что в теории множеств ровна такая же история с большими кардиналами. Из серьезных ошибочных попыток дать аксиому большого кардинала судя по всему был только кардинал Рейнхардта и не то, чтобы доказать его противоречивость было особо сложно.
Хотя, конечно, нельзя полностью исключать, что в будущем нетривиальные противоречия будут найдены, как для ZFC и её расширений так и для теорий типов

426 21 июня 2018, 19:43 426 40830

>>40808
>>40810
Это понятно, что ты в своем представление теории типов в качестве самодостаточных оснований следуешь за Мартин-Лёфом.
В принципе, с этим нет особых проблем. Есть довольно много математиков, которые привыкли думать о математике в бурбакистском ключе и поэтому для них аксиоматика Цермело-Френкеля представляет из себя формализацию самоочевидных принципов - у них уже есть преконцепция что такое множества и что с ними можно делать, а аксиомы просто соответствуют этой интуиции. Ровно также на существование имеет право и более маргинальная позиция людей думающих о математике в интуиционистских терминах для которых самоочевидной оказывается теория типов.
Не буду скрывать - я привык к бурбакисткому изложению математики и соответственно у меня развита именно интуиция касательно понятия множества, а не типа. Поэтому с неизбежностью я смотрю на интуиционизм и его формализации со стороны.
И как я уже довольно подробно расписал в нескольких предшествующих постах, анализируя их со стороны довольно прозрачно, что в них неявно заложены сильные и выходящие далеко за пределы вычислимой математики предположения (здесь под вычислимостью я понимаю вычислимость на натуральных числах) - особенно явно это проявляется в версиях с W-типами и вселенными.
>MLTT корректна и непротиворечива не потому что преподобный рабби Леф так скозал, а по той простой причине, что в ней принципиально невыразимо невычислимое в ней же.
Буллщит, феномен второй теоремы Гёделя о неполноте очень общий и чтобы доказать корректность (или хотя бы непротиворечивость) какого-либо метода рассуждений заведомо нужно выйти за его пределы.
>Противоречивость подобных теорий видно сразу же
Отмечу, что в теории множеств ровна такая же история с большими кардиналами. Из серьезных ошибочных попыток дать аксиому большого кардинала судя по всему был только кардинал Рейнхардта и не то, чтобы доказать его противоречивость было особо сложно.
Хотя, конечно, нельзя полностью исключать, что в будущем нетривиальные противоречия будут найдены, как для ZFC и её расширений так и для теорий типов

Показать весь текст
Ответы4083440839

427 21 июня 2018, 20:41 427 40832

Конструктивисты, скажите, есть простые числа, смотришь на них и очевидно, что чем дальше, тем их меньше встречается. Евклид же доказал, что множество простых чисел бесконечно. Но он в доказательстве использовал отпротивное. Может ли быть так, что на самом деле множество простых конечно?

428 21 июня 2018, 20:58 428 40833

>>40825
А ничего, что Мартин-Лёф несколько раз давал противоречивые версии систем?
Нужно определять семантику, чтобы не было таких чудачеств.

Ты сначала ZFC осиль, потом будешь писать на моём дваче.

Ответы40839

429 21 июня 2018, 21:10 429 40834

>>40830
Непротиворечивость ZFC можно доказать в более сильных теориях, например в M.

Ответы40835

430 21 июня 2018, 21:22 430 40835

>>40834
Можно. Что сказать-то хотел?

Ответы40836

431 21 июня 2018, 21:36 431 40836

>>40835
>в будущем нетривиальные противоречия будут найдены
Не будут.

Ответы40837

432 21 июня 2018, 21:40 432 40837

>>40836
Если ты доказал непротиворечивость одной теории в другой, то ничто не мешает им обоим оказаться противоречивыми. Единственно это исключает возможность, что первая противоречива, а вторая - нет.

Ответы40842

433 22 июня 2018, 01:00 433 40839

>>40833
> на моём дваче.
Носатый, уходи.
>>40830
> Буллщит, феномен второй теоремы Гёделя о неполноте очень общий и чтобы доказать корректность (или хотя бы непротиворечивость) какого-либо метода рассуждений заведомо нужно выйти за его пределы.
Потому я и написал про операционную семантику, в терминах которой доказывается в т.ч непротиворечивость mltt. Насчёт геделя-шмеделя и прочего такого, попытка выразить это в теории типов приведёт только к ошибке, ибо невычислимая хуитка. Я тебе ещё раз скажу - ты лезешь с формализмом туда, где от него изначально старались избавиться по причине его безблагодатности. Поэтому и вместо аксиом там натуральная дедукция итд итп.

Ответы40840

434 22 июня 2018, 01:50 434 40840

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

Слышать о неприложимости формализма от тебя довольно смешно. То что ты называешь здесь формализмом это видимо просто общий метод широко применяемый в математической логике: чтобы исследовать некоторый метод математических рассуждений вначале нужно построить математическую модель понятия доказательства для данного случая, т.е. дать адекватное понятие формального доказательства, а затем исследовать это понятие математическими средствами. Идея о том, что переход от гильбертовского стиля исчисления к системе натуральной дедукции как-то принципиально мешает анализу системы просто показывает твое полное непонимание того, о чем ты говоришь. На самом деле метод приложим к любым методам рассуждения, которые могут быть описаны какой-нибудь рекурсивной процедурой. Учитывая тот факт, что немного ранее в этом треде ты сам защищал идею о том, что человеческий интеллект может быть заменен на компьютер, ....

Ответы40849

435 22 июня 2018, 01:52 435 40841

>чтобы исследовать некоторый метод математических рассуждений
-->
чтобы исследовать некоторый метод рассуждений

436 22 июня 2018, 02:04 436 40842

>>40837
Тогда зачем вообще кто-то доказывает непротиворечивость?

Ответы40843

437 22 июня 2018, 02:09 437 40843

>>40842
Обычно, чтобы свести вопрос о непротиворечивости какой-нибудь менее понятной теории к вопросу о непротиворечивости более понятной теории. Характерный пример это доказательство непротиворечивости NFU в ZFC.

Ответы40844

438 22 июня 2018, 02:22 438 40844

>>40843
А зачем это делать?

Ответы40845

439 22 июня 2018, 02:24 439 40845

>>40844
Зачем заниматься математикой?

Ответы40846

440 22 июня 2018, 02:26 440 40846

>>40845
Зачем доказывать непротиворечивость одной теории множеств в другой теории множеств? Это ничего не даёт.

Ответы40847

441 22 июня 2018, 02:29 441 40847

>>40846
NFU вовсе не тоже самое, что обычные теории множеств в духе ZFC. Там существует множество всех множеств и тому подобные объекты. В результате там возможен в некоторых отношениях более естественный метод формализации теории категорий.

Ответы40848

442 22 июня 2018, 02:38 442 40848

>>40847
От того, что непротиворечивость NFU сведена к непротиворечивости ZFC, ничего нового мы не получили. По-прежнему непонятно, есть ли противоречия в NFU. Непонятно, легко ли их найти.

>метод формализации теории категорий
Категория функторов между двумя большими категориями существует? Категория эндофункторов Set, в частности? Категория всех категорий? infty-категории можно?

Ответы40850

443 22 июня 2018, 02:43 443 40849

>>40840
> принципиально мешает анализу системы
Ты б меня так читал, как отчитываешь. Не мешает оно анализу системы, речь о том, что эта система и без анализа обойдётся. 2 акта интуиционизма Брауэра не нуждаются в формализации, как не нуждается в ней и операционная семантика mltt. Просто потому что это не так работает. Ну формализуешь ты это, дальше что? То, в чем ты это формализуешь, тоже вообще то формализовать придётся. И дальше и дальше. Ты думаешь, что теория множеств истина в последней инстанции? Так её тоже опучкать можно.

Ответы4085540859

444 22 июня 2018, 02:49 444 40850

>>40848
>Категория функторов между двумя большими категориями существует?
Да.
>Категория всех категорий?
Да и она является своим собственным объектом.
>infty-категории можно?
Наверное, но нужно вникать. Проблема с NF и NFU состоит в том, что в них множества ведут себя не вполне так мы привыкли - в частности Set не будет декартова замкнута.

>По-прежнему непонятно, есть ли противоречия в NFU.
ZFC в отличие от NFU это теория с которой очень много работали. И если там и есть противоречия, то их совершенно нетривиально найти.

Ответы4085140852

445 22 июня 2018, 03:00 445 40851

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

>их совершенно нетривиально найти.
Вовсе нет. Сведение к ZFC никак не повлияло на сложность поиска противоречий в NFU, поскольку сложность не является инвариантом логических теорий, а полностью зависит от синтаксических инструментов, предоставляемых теорией. Даже если в теории A найти противоречия сложно и если непротиворечивость теории B сводится к непротиворечивости A, - вполне может быть так, что в B найти противоречия очень просто.

Ответы40856

446 22 июня 2018, 06:35 446 40852

>>40850
>в частности Set не будет декартова замкнута
Норм, и так сойдёт.

447 22 июня 2018, 07:10 447 40853

Можно ли на коке искать противоречивость теорий? Типа задал систему аксиом, включил кока, кока посчитал и выдал противоречие. В программах компьютерных же ошибки обнаруживаются, тут тоже можно по идее.

448 22 июня 2018, 09:21 448 40855

>>40849
> Ну формализуешь ты это, дальше что?
Например, даже не вдаваясь в детали формализации, а исходя лишь из возможности такую осуществить я уже сразу могу сказать, что твой способ рассуждений либо противоречив, либо не может гарантировать свою собственную непротиворечивость.
>То, в чем ты это формализуешь, тоже вообще то формализовать придётся.
Зачем? Если мне нужен будет мета-анализ средств которые я сам использовал, то да. Но в общем случае нет, анализ это просто математические результаты, которые имеют некоторое отношение к философии математики. Ты же не говоришь физикам, что когда они анализируют физический мир математическими средствами, то они должны построить математическую модель того, как им удалось построить математическую модель.
>Ты думаешь, что теория множеств истина в последней инстанции?
В отличие от тебя я не считаю, что если мне кажется что-то интуитивно ясным, то это и есть истина в последней истанции. Наиболее убедительными я нахожу ультрафинитистские доказательства, центральная идея здесь состоит в том, чтобы доказательства на каждом конкретном обозримом примере соответствовали действительно осуществимым вычислениям; таким образом это фрагмент математики опирающийся на реальную физику. Проблема в том, что разумеется это очень ограничивающий взгляд на допустимую математику. Поэтому я часто и пользуюсь более сильными средствами, понимая, что основная гарантия их корректности состоит в том, что пока нам не удалось обнаружить проблемы с нашей интуицией.

Ответы4086940874

449 22 июня 2018, 09:38 449 40856

>>40851
>В который раз убеждаюсь, что теоретико-множественные попытки формализовать категории не нужны
Проблема в том, что если я не упускаю, чего-нибудь, то никаких принципиально более адекватных формализаций, чем погружение в теорию множеств нет. На самом деле очень интересно было бы найти понятную и объемлющую формализацию теоретико-категорных рассуждений в собственно категорных терминах.

>Вовсе нет. Сведение к ZFC никак не повлияло на сложность поиска противоречий в NFU, поскольку сложность не является инвариантом логических теорий, а полностью зависит от синтаксических инструментов, предоставляемых теорией. Даже если в теории A найти противоречия сложно и если непротиворечивость теории B сводится к непротиворечивости A, - вполне может быть так, что в B найти противоречия очень просто.
Нет. Ты же найдя какую-нибудь новую переформулировку гипотезы Римана наверное справедливо решишь, что переформулировка скорее-всего тоже очень сложная задача. Ровно также и здесь, мы знаем, что нахождение противоречия в ZFC это действительно сложная проблема и то, что мы нашли вопрос к которому он сводится говорит нам о том, что это скорее всего это тоже очень сложная проблема; центральное отличие состоит в том, что здесь мы можем решить проблему только в одну сторону.

Ответы40857

450 22 июня 2018, 10:07 450 40857

>>40856
>никаких принципиально более адекватных формализаций
Вообще, есть ETCC и ETCS от Lawvere. Не знаю, насколько они удачны, но они есть.

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

Ответы4085840860

451 22 июня 2018, 10:13 451 40858

>>40857
Using this metaphor, SEAR can be thought of as an ETCS-car which comes preassembled with a nice slick control panel. Or, using an alternate metaphor, ZFC is like Windows, ETCS is like UNIX, and SEAR is like OS X (or maybe Ubuntu). With SEAR you get a nice familiar interface with which it is easy to do standard things, there is less cruft than you get with ZFC, and behind the scenes you have all the power of ETCS (and more). (Of course, if you like Microsoft products, then this metaphor probably does not appeal to you.)

452 22 июня 2018, 10:32 452 40859

>>40849
>Ну формализуешь ты это, дальше что?
Т.е. вот она вера?

453 22 июня 2018, 11:31 453 40860

>>40857
Его формализация категории Set просто переформулировка теории множест. Формализация же Cat, насколько я слышал изначально была с пробелами и исправленная версия в итоге вышла весьма корявой, хотя я сам не смотрел.

>Нет, не решу
ОК. Но это довольно самонадейно. Конечно, сложные задачи решаются при помощи переформулировок, но все-таки это в норме не произвольные переформулировки, а правильно подобранные.

Ответы40861

454 22 июня 2018, 11:43 454 40861

>>40860
>просто переформулировка теории множест
Вот, кстати, сомневаюсь. Насколько я помню, в ETCS ни в каком виде не включена схема подстановки, то есть у него даже существование алефа номер омега-нулевое недоказуемо. Нет?

>не произвольные переформулировки
Однако нет причин считать апиори, что переформулировка задачи обязательно будет не менее сложна, чем исходная задача. В каждом конкретном случае нужно конкретное исследование.

Ответы40862

455 22 июня 2018, 12:56 455 40862

>>40861
>Вот, кстати, сомневаюсь.
Да, вроде действительно буквально она соответствовала не собственно ZFC, а теория множеств Цермело. Но дело в том, что в любом случае этот подход ничего особенно не дает по сравнению с формализацией теории категорий в теории множеств.

>Однако нет причин считать апиори что переформулировка задачи обязательно будет не менее сложна, чем исходная задача
Полных гарантий у нас конечно нет. Но например мне кажется довольно абсурдным рассчитывать, что если взять случайную из огромного числа известных NP-полных задач, которые никто особо не анализировал за исключерием доказательства их NP полноты и расчитывать, что анализируя эту задачу будут хорошие шансы решить P vs NP. Я не говорю, что возможность легко найти решение полностью исключена, просто исходя из моего опыта занятия математикой я считаю, что это маловероятно.

Ответы40864

456 22 июня 2018, 13:56 456 40863

Как уверовать в операционную семантику MLTT?

457 22 июня 2018, 14:27 457 40864

>>40862
Причины, по которым ты испытываешь чувство абсурдности, у тебя не вполне отрефлексированы, как мне кажется. Ты фокусируешь внимание на NP-полноте. Но можно посмотреть шире и увидеть, что вообще большинство задач не решены даже схематично. И поэтому если взять случайную задачу, то решить её, скорее всего, будет очень трудно, независимо от того, эквивалентна ли она какой-либо из известных сложных задач. Я согласен с тем, что если взять случайную из NP-полных задач и пытаться её решить, то будет тяжко. Но я думаю, что эта сложность вызвана не тем, что задача эквивалентна NP-полной, а тем, что задача попросту не относится к узенькому классу ранее изученных человечеством задач. И я считаю, что доказательство NP-полноты задачи не будет свидетельством, что эту задачу очень сложно решить (а вот экспериментальный факт, что задача не решается применением стандартных методов, таким свидетельством будет). Так и с формальными теориями: то, что теория эквивалентна ZFC, не будет свидетельством, что в теории сложно найти противоречие. Зато факт, что долгий поиск противоречий не даёт результатов, таким свидетельством таки будет.

Ответы40865

458 22 июня 2018, 15:50 458 40865

>>40864
На самом деле здесь мы приходим к очень важному для успешного получения интересных теорем, но очень субъективному вопросу о том, как оценивать шансы на успех тех или иных подходов к решению проблем. Когда мы говорим о проблемах, которые безуспешно в течение долгого времени пытались решить многие в том числе действительно талантливые математики, то решения как правило приходят из применения существенно новых методов. При этом я полагаю, что для того, чтобы улучшить шансы на успех кроме того, чтобы подход был действительно новым, желательно иметь какие-нибудь (неформальные) объяснения, почему он избегает проблем предшествующих подходов и в целом иметь какой-нибудь план действий.

Если посмотреть на какую-нибудь очередную графовую NP-полную задачу в качестве подхода к решению P vs NP, то по существу он не удовлетворяет ни одному из трех критериев. В случае поиска противоречия в NF вместо ZFC, здесь до некоторой степение есть новизна (NFU в самом деле сильно отличается от привычных теорий множеств), но по остальным критерия все также выглядит плохо.

Если говорить не о вопросах о непротиворичивости, а более обычных действительно важных открытых вопросах, т.е. связанных со многими другими вопросами. Я лично считаю, что за ними как правило лежит некоторое фундаментальное недопонимание сооответствующей предметной области. И их решение с должно устранить это недопонимание. Выбор правильного контекста (т.е. переформулировки) и составляет существенную часть этого прояснения ситуации.

459 22 июня 2018, 17:58 459 40869

>>40855
> В отличие от тебя я не считаю, что если мне кажется что-то интуитивно ясным, то это и есть истина в последней истанции.
А где и когда я вообще хоть что-то про "интуитивную ясность" говорил?..

460 22 июня 2018, 20:06 460 40873

https://pat.keldysh.ru/~roman/doc/Turchin/1983_Turchin__The_Cybernetic_Foundation_of_Mathematics.pdf

461 22 июня 2018, 23:32 461 40874

>>40855
> Ты же не говоришь физикам, что когда они анализируют физический мир математическими средствами, то они должны построить математическую модель того, как им удалось построить математическую модель.
Будешь смеяться, но именно это можно предъявить и не только физикам. Идентификация систем часто может тривиально решить проблему, над которой даже очень умный исследователь будет биться долго.

462 23 июня 2018, 12:58 462 40879

Ну понял. Типа алгебра это когда палочки считаем. А геометрия?

Ответы4088040886

463 23 июня 2018, 13:12 463 40880

>>40879
Математика состоит из того, что линеаризуется – то есть в абелевой категории и тд (условно алгебра) и того, что нет (условно: топология; нлаб, стакс проджект).
Счет палочек это computer science. по изоморфизму Карри-Кетчупа и есть математика.

Ответы40883

464 23 июня 2018, 14:49 464 40883

>>40880
>нлаб, стакс проджект
А нагуглевыемые названия можно?

Ответы40884

465 23 июня 2018, 14:59 465 40884

>>40883
http://stacks.math.columbia.edu
https://ncatlab.org

466 23 июня 2018, 16:09 466 40886

>>40879
> Ну понял. Типа алгебра это когда палочки считаем. А геометрия?
Алгебра - гамалогии, геометрия - тапалогии. Все вместе - пучки. Что тут непонятного.

Ответы40888

50 Кб, 960x492
467 23 июня 2018, 16:29 467 40887

Неконструктивные основания математики из-за исключённого третьего и догмы Гильберта вообще нефальсифицируемы, т.о научность неконструктивной математики примерно на уровне астрологии, это чистое хипстерство.

Ответы4088840889

468 23 июня 2018, 16:40 468 40888

>>40886
Охуенно, лучше и не скажешь.
>>40887
>научность
>фальсифицируемость
Как там в 1946? Человек, который решил изучать вместо математики основания, а вместо науки философию науки, называет кого-то хипстером, спешите видеть. Тот же Гильберт для физики сделал намного больше, чем все твои кумиры от Брауэра до Поппера.
Впрочем, ничего нового. К 1970-м все уже убедились в неадекватности фальсификационизма, что изначальное требование фальсифицируемости слишком сильное,более поздние же формулировки вроде методологии исследовательских программ, не налагают никаких содержательных ограничений вообще. Apparently you didn't catch the memo.

Ответы40891

469 23 июня 2018, 17:17 469 40889

>>40887
Америку открыл, всем давно известно, что математика не наука. Алсо сам этот критерий тоже нефальсифицируем, сам себе не удовлеторяет.

Ответы4089040891

470 23 июня 2018, 17:32 470 40890

>>40889
Чего он не может осознать на протяжении семи тредов уже, а довольно простая мысль, казалось бы: те, кто занимается наукой (или математикой); и те, кто дает определения науке, кто выясняет, что является наукой, а что нет, и каким критериям наука обязана удовлетворять – два разных множества людей, не пересекающихся никак, дизъюнктивных, вообще.
>этот критерий тоже нефальсифицируем, сам себе не удовлеторяет
Можно показать (было показано учениками Поппера) что этому критерию в его изначальной формулировке не удовлетворяет ничего вообще. То есть это бессмысленное абсолютно занятие, философия науки это разговор слепого о живописи.

Ответы4089440895

471 23 июня 2018, 17:33 471 40891

>>40889
> Америку открыл, всем давно известно, что математика не наука.
Только неконструктивная, по озвученным мной причинам.
> Алсо сам этот критерий тоже нефальсифицируем, сам себе не удовлеторяет.
Это как?
>>40888
> Впрочем, ничего нового. К 1970-м все уже убедились в неадекватности фальсификационизма,
Все хипстеры убедились, потому что им напекло от нефальсифицируемости их религии? Или что? Что там неадекватного?
> изначальное требование фальсифицируемости слишком сильное,
С чего бы? Нормальное, адекватное требование, которому удовлетворяет любая наука, если это наука, а не вера.

Ответы40896

472 23 июня 2018, 17:36 472 40894

>>40890
> философия науки это разговор слепого о живописи
Это надо отлить в граните, выражаясь словами классика.

Ответы40947

473 23 июня 2018, 17:37 473 40895

>>40890
> простая мысль, казалось бы: те, кто занимается наукой (или математикой); и те, кто дает определения науке, кто выясняет, что является наукой, а что нет, и каким критериям наука обязана удовлетворять – два разных множества людей, не пересекающихся никак, дизъюнктивных, вообще.
Это не "простая мысль", а простая вера. У Вапника очень хорошо за критерий Поппера изложено применительно к машинному обучению. Я понимаю, что ты скажешь, что это не наука, т.к не гамалогии, но это только твоё личное мнение, с реальностью не связанное.

Ответы40906

474 23 июня 2018, 17:37 474 40896

>>40891
>Это как?
Он ненаучен, его нельзя фальсифицировать.

Ответы40897

475 23 июня 2018, 17:40 475 40897

>>40896
> Он ненаучен, его нельзя фальсифицировать.
Можно. Допустим, что критерий Поппера неверен. Тогда получается, что астрология, херомантия, вера в жопу хэнка итд - это науки. М?

Ответы40898

476 23 июня 2018, 17:41 476 40898

>>40897
Нет, не получается. У тебя ещё и с логикой беда.

Ответы40901

477 23 июня 2018, 17:44 477 40901

>>40898
> Нет, не получается.
Почему? Ты можешь назвать критерий научности теории лучше попперовского?

Ответы40902

478 23 июня 2018, 17:47 478 40902

>>40901
Потому что из того, что научная теория может быть принципиально неопровержимой не следует, что хиромантия и астрология науки. Могу, наука это то, чем занимаются учёные.

Ответы40903

479 23 июня 2018, 17:48 479 40903

>>40902
> Могу, наука это то, чем занимаются учёные.
Учёные дрочат, мочатся в сортире. Это наука?

Ответы4090440905

480 23 июня 2018, 17:49 480 40904

>>40903
Конечно.

481 23 июня 2018, 17:50 481 40905

>>40903
Ну правда, я уверен, что многие теоремы были доказаны во время сранья или мытья яиц. Конечно это наука.

482 23 июня 2018, 18:46 482 40906

>>40895
>у Вапника
Теперь понятно откуда ветер дует. У Вапника изложено про Поппера, у Лёфа изложено про Канта, у Маннури про Витгенштейна. То есть даже самого Поппера ты не читал, как и любое явление в истории человеческой мысли рассматриваешь его исключительно с позиций своей секты.
>Все хипстеры убедились
Почему прямые ученики Поппера, с которыми он вел дискуссии это бесполезные хипстеры, а сам Поппер нет? Потому что про Поппера написал Вапник, вот почему. Что одобрено церковью конструктивизма, то не оспаривается. Только вычисляется.
>Что там неадекватного?
А я уже объяснял, два треда подряд, только ты прослушал. И ссылки приводил. Не имеет значения даже, применим ли этот критерий к самому себе. К реальной науке он совершенно не применим. Что показано (Куном, Лакатосом и др) не из каких-то философских принципов, а путем рассмотрения контрпримеров, в первую очередь.
Если бы этот принцип понимался буквально, и его последовательно и строго применяли, наука бы перестала существовать. Поскольку ни одна успешная теория не может ему удовлетворить.
>Тогда получается, что астрология, херомантия, вера в жопу хэнка итд - это науки
Даю тебе определение из действительности, а не из шизанутого манямирка. Наука это то, за что дают гранты. Как только научнут давать за астрологию – можешь называть её наукой. В общем-то, ничего плохого в астрологии в узком смысле нет, это такая вспомогательная дисциплина на стыке метеорологии и какой-нибудь биохимии. Как с торсионными полями, которые придумал Картан – изначально вполне научная концепция была, но в нынешнем виде это понятно что. Профанация же и обман есть во всех областях науки: пример в математике – конструктивизм.
>Учёные дрочат, мочатся в сортире
Как и все люди, кстати. Начни выяснять в чем состоит здравый смысл научного сообщества и каких конвенций оно придерживается и ты окажешься гораздо ближе к пониманию что такое наука, чем изучая интерпретацию Вапника предложений Поппера.

Ответы4090740911

55 Кб, 640x489
483 23 июня 2018, 19:48 483 40907

>>40906
> Наука это то, за что дают гранты.
> здравый смысл научного сообщества
> К реальной науке он совершенно не применим. Что показано (хипстером, сойбоями и др)
Я тебя услышал. Из твоего монолога я понял, что печет тебе с того, что гамалогии нефальсифицируемы аки боженька, и никакого отношения к научным знаниям не имеют. А виноват в этом Маннури, разумеется. Кто ж ещё.

Ответы40915

3 Кб, 100x100
484 23 июня 2018, 20:01 484 40911

>>40906
>пример в математике – конструктивизм.
OH SNAP

Ответы40912

485 23 июня 2018, 20:06 485 40912

>>40911
Конструктивисты не получают новых результатов. Они просто раз в десятилетие берут какое-нибудь утверждение школьного уровня, например теорему Больцано-Коши, и пытаются передоказать конструктивно. Обычно ничего не получается.

Ответы409134091540950

486 23 июня 2018, 20:08 486 40913

>>40912
Перепощу в тред с цитатами.

487 23 июня 2018, 20:57 487 40915

>>40907
Не услышал. Единственный способ донести до тебя информацию это прочитать твоих кумиров и найти у них цитаты, где утверждается то же самое.
Смотри пример: Поппер молодец, Кун и Лакатос – сойбои, хипстеры и тд. В реальности это представители одной и той же школы Поппера. Но: Поппера упомянул Вапник, а его учеников нет.
Другой пример: с критикой Поппера высказался Витгенштейн (инцидент с кочергой). Получается он тоже сойбой. Ох вейт. Витгенштейна упоминал Миколов! Конструктивист protection comes in. И т.д.
То есть, ты просто будешь игнорировать любые идеи, даже не пытаясь разобраться, если они не в полном согласии с твоими догмами; называть бесполезным хипстерством и тд, других оснований тебе не нужно. Догмы же в защите не нуждаются, достаточно self-reference, криков про вычислимость, смешных картинок, оскорблений.
>>40912
Ну переписать книгу Ландау "Основы анализа" на прувере Автомат чем не результат. Или там нумерацией Гёделя свести производные функторы к исчислению палочек на машине Тьюринга.
Не важно как нелепо это, он a priori не признаёт существенным ничего другого, вычислимость это и есть математика, математика это и есть вычислимость.
Не важно что там утверждали разные люди по этому поводу, если упомянуть Гротендика или там Манина это апелляция к авторитетам, а если какого-то конструктивиста – к вычислимости. Проходили уже, серьёзную дискуссию вести невозможно.

Ответы40917

488 23 июня 2018, 21:15 488 40917

>>40915
> если они не в полном согласии с твоими догмами; н
У меня нет догм. Догмы и вера у тебя, поскольку что тебе ещё остаётся с нефальсифицируемой религией. Разве что в очередной раз Миколова вспомнить.
> Не важно как нелепо это, он a priori не признаёт существенным ничего другого, вычислимость это и есть математика, математика это и есть вычислимость.
Но ведь так и есть. Альтернатив никогда и не было, разве что как ты предлагаешь, считать наукой только то, за что дают гранты.
> Не важно что там утверждали разные люди по этому поводу, если упомянуть Гротендика или там Манина
Не важно, конечно. Утверждения в математике не стоят ничего, важны доказательства. А о каком вообще доказательстве можно говорить применительно к вере в нефальсифицируемое исключенное третье?

Ответы40929

407 Кб, 480x726
489 23 июня 2018, 21:23 489 40918

>>26619
>исключённое
Сначала обдумай "парадокс лжеца", а затем - "теоремы Гёделя о неполноте",
после этого - можешь возомнить логический элемент полным по Гёделю и охуеть.

Ответы40937

490 23 июня 2018, 21:24 490 40919

Браузер, Мортин Лев, Маняури, Church(Церковь) - виликие мотематики. Вычеслимость программ писать умеют на алгоритмах. Как коде монкей. А исключающая вера - это третие. Вот - мы не можешь вычилсть знак ((100!)!))! у пи, значит, нам ничего не известно об этом знаке, то есть нельзя сказать одназначно ответить - эта цифра 3 или нет. Тут кроме двух ещё и третий вариант может быть. Так Браузер СКОЗАЛ! вычислимость палочки рисуют разные. ПАЛКА ПАЛКА ОГУРЕЧИК - ПОЛУЧИСЯ ЧЕЛОВЕЧИК)))))))))))) Кто в тезис Церкви не верит, тот не математик получается. А олгоритмы изучает не computer science а математика. Гамалогии - веры и нинужны. Пародкс ЖИРАФА не действителен. Аксиома - выбора вернуство, без неё в математике легко обойтись. Так только с канечными множествыми можно делать. Так так так, что тут у нас информатика?

Ответы40934

491 23 июня 2018, 21:31 491 40920

Аноны, поясните за потенциальную бесконечность. Это что-то из Плутоновского мира идей? Плутонисты опять соснули?

26 Кб, 644x800
492 23 июня 2018, 21:31 492 40921

О, опять петросянство пошло, Вдумайся, вся вообще история неконструктивной математики закончилась кризисом оснований, провалом программы Гильберта, верой в мир идей Платона и нефальсифицируемое исключенное третье.

Ответы4092240923

493 23 июня 2018, 21:32 493 40922

>>40921
> вся вообще история неконструктивной математики закончилась
Это, мягко говоря, не так. Анус твой закончился, а не математика.

Ответы40925

494 23 июня 2018, 21:36 494 40923

>>40921
>верой в мир идей Платона
А потенциальная бесконечность - тоже из плутоновской оперы?

495 23 июня 2018, 21:38 495 40924

Пилите перекат, Браузеры.

Ответы40956

496 23 июня 2018, 21:41 496 40925

>>40922
> Это, мягко говоря, не так.
Это так. Осталось только гранты получать под смузи на коворкингах, сам же признал. Исключенное третье и актуальные бесконечности это тупик. Остаётся только вычислимость.
> Анус твой закончился
Скрепы болят? Неважно во что ты там вероваешь, алгоритмически неразрешимые проблемы не решаются никак. И ты никуда не денешься от этого факта.

Ответы4092640927

497 23 июня 2018, 21:42 497 40926

>>40925
>алгоритмически неразрешимые проблемы не решаются никак.
Аксиома выбора не вызывает противоречий.

Ответы40928

498 23 июня 2018, 21:45 498 40927

>>40925
Математика доказала теорему Ферма.
А чего добился конструктивизм за последние ну хотя бы сто лет?

Ответы40933

499 23 июня 2018, 21:46 499 40928

>>40926
> Аксиома выбора не вызывает противоречий.
Нет конечно. И исключенное третье не вызывает. Откуда противоречия в нефальсифицируемой религии.

Ответы40930

500 23 июня 2018, 21:48 500 40929

>>40917
Фальсификационизм это и есть религия, он был опровергнут, неоднократно на примерах конкретных ситуаций в истории науки было показано, что принцип фальсифицируемости не работает. Ты это игнорируешь, говоря о сойбоях, хипстерах. Прочитай в словаре, что такое "догма".
>считать наукой только то, за что дают гранты
За всю историю начиная с 17-го века, как только наука возникла, никому не удалось дать внятного и содержательного определения тому что такое наука, изложить критерии, которым должна удовлетворять научная теория.
Почему – любому ученому это и так понятно; сойбои же вроде Поппера это слепцы в картинной галерее и просто не понимают, о чем говорят.
Как ты не понял, что такое языковые игры. У Витгенштейна, не в пересказе Миколова или кого ещё, под этим понимались informal rules. То, чему можно научиться, но что нельзя формализовать. Как научиться? Abrichten, дрессировка, реальная практика. Это и есть здравый смысл ученого. Ему он понятен без явно высказанных критериев и определений, тебе же и твоим кумирам никакие определения не помогут. Потому что вместо науки и математики они занимались хуйней, называемой "основания математики" и "философия науки".
>Утверждения в математике не стоят ничего
Только если это не утверждения твоих любимых авторов, на них ты ссылаться не стесняешься. Отстаивая точку зрения, высказанную Маннури, приводить как аргумент слова самого Маннури, и т.д.
Для тебя не подлежит сомнению любое утверждение высказанное конструктивистом, оно автоматически верно, потому что вычислимо. Соответственно вся математика сводится к деятельности конструктивистов по проверке написанными нематематиками типа Ландау книг.
А если привести нетривиальный пример деятельности Вейля, Серра, Гротендика, то он сводится к "перекладывание палочек + верунство". Особенно легко игнорировать то, назначение чего тебе изначально не было известно, та же гомологическая алгебра.
Мне-то это ясно, конечно, я просто ещё раз озвучиваю, чтобы мимо проходящие типа >>40467 понимали, с кем имеют дело.

500 23 июня 2018, 21:48 500 40929

>>40917
Фальсификационизм это и есть религия, он был опровергнут, неоднократно на примерах конкретных ситуаций в истории науки было показано, что принцип фальсифицируемости не работает. Ты это игнорируешь, говоря о сойбоях, хипстерах. Прочитай в словаре, что такое "догма".
>считать наукой только то, за что дают гранты
За всю историю начиная с 17-го века, как только наука возникла, никому не удалось дать внятного и содержательного определения тому что такое наука, изложить критерии, которым должна удовлетворять научная теория.
Почему – любому ученому это и так понятно; сойбои же вроде Поппера это слепцы в картинной галерее и просто не понимают, о чем говорят.
Как ты не понял, что такое языковые игры. У Витгенштейна, не в пересказе Миколова или кого ещё, под этим понимались informal rules. То, чему можно научиться, но что нельзя формализовать. Как научиться? Abrichten, дрессировка, реальная практика. Это и есть здравый смысл ученого. Ему он понятен без явно высказанных критериев и определений, тебе же и твоим кумирам никакие определения не помогут. Потому что вместо науки и математики они занимались хуйней, называемой "основания математики" и "философия науки".
>Утверждения в математике не стоят ничего
Только если это не утверждения твоих любимых авторов, на них ты ссылаться не стесняешься. Отстаивая точку зрения, высказанную Маннури, приводить как аргумент слова самого Маннури, и т.д.
Для тебя не подлежит сомнению любое утверждение высказанное конструктивистом, оно автоматически верно, потому что вычислимо. Соответственно вся математика сводится к деятельности конструктивистов по проверке написанными нематематиками типа Ландау книг.
А если привести нетривиальный пример деятельности Вейля, Серра, Гротендика, то он сводится к "перекладывание палочек + верунство". Особенно легко игнорировать то, назначение чего тебе изначально не было известно, та же гомологическая алгебра.
Мне-то это ясно, конечно, я просто ещё раз озвучиваю, чтобы мимо проходящие типа >>40467 понимали, с кем имеют дело.

Показать весь текст
Ответы40931

501 23 июня 2018, 21:52 501 40930

>>40928
>И исключенное третье не вызывает.
Тоже верно. Без шуток.

502 23 июня 2018, 21:53 502 40931

>>40929
>Фальсификационизм это и есть религия
Кокоструктивист нашел себе новую секту. Или вступил ещё в одну. Мультисектант.

503 23 июня 2018, 21:57 503 40933

>>40927
Я ему это уже говорил, он считает что доказательство великой теоремы Ферма это конструктивный результат, даже какую-то уродскую формулировку в терминах своей теории типов приплёл, типа, вот, я пруверы знаю.
Не хочет человек понимать, при чем там эллиптические кривые и теория представлений, что поделать, слепому новые глаза не дашь, а конкретно этого ещё и из галереи не вывести, нравится ему людей пугать, похоже.

504 23 июня 2018, 21:58 504 40934

>>40919
>Вот - мы не можешь вычилсть знак ((100!)!))! у пи, значит, нам ничего не известно об этом знаке, то есть нельзя сказать одназначно ответить - эта цифра 3 или нет.
Ой, где-то был тут алгоритм вычисления N-ного знака у числа Pi... А вот же: https://habr.com/post/179829/
Возможно, можно было бы его адаптировать и под факториалы эти, не?

Ответы4093540936

505 23 июня 2018, 22:00 505 40935

>>40934
Тогда вычисли мне ((100!)!))!
Нельзя скозать тут будит 3 или нет исключеннёное третие исключенно111!

Ответы4093940952

506 23 июня 2018, 22:02 506 40936

>>40934
Ты что ослеп? Нельзя сказать, какая цифра будет, значит, исключающее третье неприменимо здесь.

Ответы40939

507 23 июня 2018, 22:04 507 40937

>>40918
Аххах, если лжец сказал, что он пиздит - значит он не пиздит,
и он вполне правдиво сказал, что он пиздит - а значит пиздит.
А если он пиздит, что он пиздит то он правду говорит что он пиздит.
Раз он правду говорит про то, что он пиздит, то он либо не лжец (правда же),
либо таки лжец и правдиво утверждает, что таки пиздит.
Тут кстати, тоже закон исключённого третьего. И третьего не дано.
Или таки дано? Лол.

508 23 июня 2018, 22:04 508 40938

Гротендик был против компьютерной математики и пруверов, хуесосил теорему о раксраске карт. Он что нематиматик, раз алгоритмы не признаёт?

Ответы4094240943

509 23 июня 2018, 22:06 509 40939

>>40935 >>40936
Ну, откуда я знаю, а вдруг таки-можно, поэтому я это и вкинул вам.

Ответы40940

510 23 июня 2018, 22:07 510 40940

>>40939
Только утрафинизм! Толька хардкоре!

511 23 июня 2018, 22:08 511 40941

Браузер, пили перекат!

Ответы40956

512 23 июня 2018, 22:13 512 40942

>>40938
Гротендик считал, что тупо перебор - некрасивое решение. Задача не решена по-настоящему, пока не придумана общая красивая теория, позволяющая решать целый класс аналогичных задач.

513 23 июня 2018, 22:13 513 40943

>>40938
Манина наш конструктивист лишил статуса математика и за меньшие пригрешения: тот упомянул в своей книге существование невычислимых функций.
С Гротендиком же смешно получилось: конструктивист много говорил про топосы, пока не узнал, что в топосе Гротендика используется аксиома недостижимого кардинала. Пришлось срочно маневрировать и убеждать, что у Гротендика, который данное понятие ввел, определение неверное, вот, у Лавера верное или еще у кого. С Воеводским и теоремой о гомоморфизме норменного вычета похожее было, оказалось: кумир занимался гамалогиями до святой теории типов. Предательство почти.

Ответы40944

514 23 июня 2018, 22:20 514 40944

>>40943
Что самое смешное, Ловер (именно так его фамилию принято транскрибировать на русский) не конструктивист ни разу, и даже посрался недавно с каким-то индусом, попытавшимся сделать конструктивную версию ETCS на основе теории Мартин-Лёфа.
https://arxiv.org/abs/1201.6272

Ответы40945

515 23 июня 2018, 22:22 515 40945

>>40944
А ещё оказывается, это был не рандомный индус, а заслуженный коллега Мартин-Лёфа.
Смешно получилось.
http://staff.math.su.se/palmgren/

516 23 июня 2018, 23:58 516 40947

>>40894
Немного гуманитарно на самом деле.
Теоретически слепой может воспринимать живопись, если найти удобный способ перекодировать ее в те категории восприятия, которые доступны слепому.

Ответы40948

517 24 июня 2018, 00:01 517 40948

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

518 24 июня 2018, 00:19 518 40949

А с какой позицией выступает конструктивист? Вся не математика - не математика, занимайтесь программированием? Или что?

Ответы40951

60 Кб, 700x525
519 24 июня 2018, 00:26 519 40950

>>40912
Содомит

520 24 июня 2018, 00:34 520 40951

>>40949
Почти. Видимо корректнее будет сформулировать как то, что математика, программирование и теория типов - это одно и тоже.

521 24 июня 2018, 00:43 521 40952

>>40935
А нельзя ли как-нибудь это индукцией доказать?
Или кококтивисты ее тоже не используют?

Оснований тред №6 522 24 июня 2018, 00:48 522 40953

509 Кб, 2634x112455 Кб, 650x341120 Кб, 950x473287 Кб, 1240x698

>В любой науке ровно столько науки, сколько в ней математики.
>В любой математике ровно столько математики, сколько в ней вычислимости.

Предыдущий, тонет тут: https://2ch.hk/math/res/25624.html (М)
Архивач: https://arhivach.cf/thread/369697/ (У кого не открывается - попробуйте HTTP.)

Ответы40956

523 24 июня 2018, 01:01 523 40956

>>40953 >>40924 >>40941
Перекат: https://2ch.hk/math/res/40955.html (М)
Перекат: http://arhivach.cf/thread/369744/
Перекат: >>40955 (OP)
Перекот: https://2ch.hk/math/res/40955.html (М)
Перекот: http://arhivach.cf/thread/369744/
Перекот: >>40955 (OP)
Перекіт: https://2ch.hk/math/res/40955.html (М)
Перекіт: http://arhivach.cf/thread/369744/
Перекіт: >>40955 (OP)

>>40381
>Браузер писал, то так оно и есть. Слово Браузера - закон.
Вот это было излишне, ибо на принципах интерпретатора:
>>40466
>непогрешимость браузера ещё сильнее усилилась

Тред закрытОбновить закрытый тред
« /math/В начало тредаВеб-версияНастройки/a//b//mu//s//vg/Все доски

Скачать тред только с превьюс превью и прикрепленными файлами

Второй вариант может долго скачиваться. Файлы будут только в живых или недавно утонувших тредах.Подробнее

Пользуетесь скринридером — пишите, что можно улучшить.
Host-Food.ru — надёжный хостинг от 12 руб/мес | Free DNS
Зеркала М.Двача: m2ch.hk, m2ch.lib, m2chfapiswfw2wcakptqp4o6ltgchvjuxfab7urxlduraomtlnhw5xad.onion