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

Двач.hk не отвечает.
Вы видите копию треда, сохраненную 6 декабря 2024 года.

Скачать тред: только с превью, с превью и прикрепленными файлами.
Второй вариант может долго скачиваться. Файлы будут только в живых или недавно утонувших тредах. Подробнее

Если вам полезен архив М.Двача, пожертвуйте на оплату сервера.

Оснований тред №4 5 июля 2017, 14:31 21361 В конец треда | Веб

67 Кб, 620x78017 Кб, 220x281298 Кб, 683x1024661 Кб, 1000x1334

Помимо трех основных направлений в основаниях - формализм, логицизм и интуиционизм, иногда возникали идеи построить математику на кардинально отличных от общепринятых принципах. Одно из таких направлений - Сигнифика, Significs. Попытка основать математику на основе естественного языка (т.к. язык и математика - это деятельность человека) принадлежит учителю Брауэра, голландскому математику и философу Герриту Маннури. Согласно его теории уровней языка (таких уровней 5), чисто формальный язык математики (5ый уровень) отличается от языка общения детей (1ый уровень) только степенью связи между словами и их сочетаниями (языковыми конструкциями). Идеи Маннури более чем на столетие опередили свое время, т.к. при его жизни не было методов автоматизированной работы с текстом (NLP, Natural Language Processing). В наше время такие методы развиты достаточно, чтобы поставить вопрос о построении вычислительной сигнифики (Computational Significs) для нужд математики, в т.ч. автоматизированного доказательства теорем и т.о. реализации на этих основах прувера, отличающегося принципом функционирования от всех остальных чуть менее чем полностью.
Предыдущий - https://2ch.hk/math/res/17772.html (М)
Архив тредов

Ответы136315972151226528893706442448015210

2 5 июля 2017, 15:10 2 21363

>>21361 (OP)
Кризис оснований закончился, когда теория множеств была аксиоматизирована.

Ответы1364

167 Кб, 782x543
3 5 июля 2017, 15:19 3 21364

>>21363
И сразу все бесконечности и исключенное третье сами посчитались. А Гильберту делать было нехуй, что он решил обосновывать арифметику финитарными методами, потому что чисто аксиоматически это оказалось сделать невозможно. Финитарными, Карл! До такого даже Брауэр не докатился, хотя и описал то, что Гильберт назвал "метаматематикой" задолго до Гильберта т.к. признавал потенциальную осуществимость, как абстракцию от действия над ментальными построениями "and so forth". Суть-то в чем? Невычислимые основания нельзя использовать на практике, н-р для доказательства непротиворечивости арифметики, на чем Гильберт и прогорел, скатившись в итоге к финитизму. Подобные же причины сделали необходимым создание вычислимых оснований - MLTT и HoTT. Если бы все можно было доказать в ZFC, никто бы не ебался с конструктивными основаниями.

Ответы1365

4 5 июля 2017, 15:29 4 21365

>>21364
>никто бы не ебался с конструктивными основаниями.
С ними никто не ебётся, кроме двух психов.

Ответы13661367

5 5 июля 2017, 15:31 5 21366

>>21365
Ну я тебе пример с непротиворечивостью арифметики привел. Нахуя нужны основания, пользуясь которыми нельзя обосновать что 1+1 будет 2? Это не то что не основания, это не математика даже.

Ответы1368

6 5 июля 2017, 15:33 6 21367

>>21365
>кроме двух психов.
Манямир, ты ж и сам это прекрасно знаешь. Пишешь просто чтобы возразить.

7 5 июля 2017, 15:58 7 21368

>>21366
Арифметика Пеано непротиворечива, и это доказано. В любой формальной арифметике со сложением можно доказать, что 1+1=2. В чем проблема-то?

Ответы1369

8 5 июля 2017, 16:34 8 21369

>>21368
>Арифметика Пеано непротиворечива, и это доказано.
Теоремой Гудстейна? Ты формально докажи непротиворечивость арифметики, а не правилами построения типа аксиом Пеано.

Ответы1370

9 5 июля 2017, 17:11 9 21370

>>21369
Это доказал трансфинитной индукцией Генцен, чем окончательно выполнил программу-минимум Гильберта. Как бе известнейший факт.

Ответы1372

10 5 июля 2017, 17:17 10 21372

>>21370
Доказательство Генцена еще зимой разбирали (тащи свою пасту).

Ответы1373

11 5 июля 2017, 17:24 11 21373

>>21372
Давай устроим полноценный диспут? Ты за свой интуиционизм, я за обычную математику.

Ответы1391

12 6 июля 2017, 04:39 12 21391

>>21373
Го пвп? Сейчас бы в 2017 намейлру опровергать интуиционизм. Ну что вы тут за аутисты? Вот ты ж даже не читаешь, что тебе пишут, не говоря о том чтобы попытаться понять. Помимо невычислимых нематематических верований вся используемая математика конструктивна и даже выразима в лямбда Р исчислении, что показал де Браун. Я это не писал уже сто раз? Писал. Так что ты опровергать собрался?

Ответы1398

13 6 июля 2017, 09:42 13 21398

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

Ответы1400

64 Кб, 715x1013
14 6 июля 2017, 13:13 14 21400

>>21398
> Ну, вначале ведь нужно уточнить позиции.
Я их уже 4ый тред уточняю + до этого тредов 5 как минимум в сци. Математика это все, что вычислимо, все что невычислимо это не математика. Именно поэтому всю математику можно изложить уже в лямбда Р исчислении (Automath де Брауна), да даже на машине Тьюринга, хотя это дальше от практики. Т.к конструктивный объект это обобщение натурального числа, любую математическую структуру можно свести к натуральному числу, геделевской нумерацией например, а вся математика точно так же сводится к арифметике. А все, что не сводится - это не математика, с этим только в церковь покемонов ловить. Не писал я этого сто раз? Писал ведь. И если после всего этого моя позиция остается гепонятной кому'то, я даже не знаю.

Ответы14015210

15 6 июля 2017, 15:14 15 21401

>>21400
Это слишком общие слова. Хотелось бы (и, похоже, не мне одному) узнать, что же конкретно ты относишь к области покемонов. Понятно, что ты запрещаешь изучать большие кардиналы и нестандартный анализ, но как далеко простираются запреты и не попадает ли вдруг под них вообще вся общая топология? Вот скажи, как в твоем учении выглядит введение разнообразных топологий на множестве вещественных чисел? Как, к примеру, топологию Зоргенфрея следует определять? Это конкретные вопросы, и я рассчитываю на конкретные ответы.

Ответы1410

16 6 июля 2017, 18:34 16 21410

Это не общие слова, а вполне конкретная конкретика. Математика = вычислимость, для определенности, пусть будет вычислимость на машине Тьюринга, хотя сойдет и любое другое уточнение понятия алгоритма. Невычислимое невычислимо, поэтому его нельзя вычислить, можно только верить. Потенциальная осуществимость осуществима потенциально, отличие от актуальной бесконечности - наличие правил построения.
>>21401
> Как, к примеру, топологию Зоргенфрея следует определять?
Дался тебе этот Зоргенфрей. Еще Брауэр показал, что континуум невычислим и уж точно не сводится к множеству вещественных чисел.

Ответы14111437

17 6 июля 2017, 18:36 17 21411

>>21410
Верно ли я понял, что ты запрещаешь вводить различные топологии на множестве вещественных чисел?

Ответы14131414

18 6 июля 2017, 18:48 18 21413

>>21411
Я думаю тут еще хуже, смотри он пишет
>Математика = вычислимость
И при этом следом
>континуум невычислим
Отсюда по его манялогике: вещественные числа эта манявера и четко твердо НИНУЖНО. Я тут подумал, а этого сумасшедшего легко косплеить.

19 6 июля 2017, 19:17 19 21414

>>21411
> Верно ли я понял, что ты запрещаешь вводить различные топологии на множестве вещественных чисел?
Ты ведь и сам понимаешь, даже без всякого конструктивизма, что это в любом случае будет аппроксимация с конкретным количеством знаков после запятой. Именно их ты и будешь вычислять. Нет никакого запрета, есть трезвый взгляд на тему. Брауэр, к слову, топологией занимался еще до интуиционизма.

Ответы1417

20 6 июля 2017, 21:17 20 21417

>>21414
О какой аппроксимации речь? В какой процедуре? Топология стрелки - это классический пример топологического пространства с неинтуитивными свойствами, и работает этот пример именно как цельное пространство.

Ответы1430

21 7 июля 2017, 10:36 21 21430

>>21417
Все эти ваши "цельные пространства" на самом деле дискретизация. Самый простой пример - интегральчики. Веровается, что с помощью предельного перехода размера интервалов dx к бесконечно малому получается нечто отличное от просто интервалов, хотя ни для кого не секрет, что любые численные методы интегрирования - это чистая дискретка. Т.о. имеем практически возможную аппроксимацию конечным числом интервалов dx, а предельный переход существует только на бамаге, ничего построимого и вычислимого за ним не стоит. Т.е. на самом деле вычисления не идут за пределы реально вычислимого. И опять же, я приводил конкретный пример - теория статистического обучения. Таких примеров можно привести еще сколько угодно, те же функции принадлежности в нечетких множествах. Т.е. на самом деле работает все так, как показал еще Брауэр - континуум невычислим, реально можно работать только с его дискретизацией.

Ответы1431

22 7 июля 2017, 10:41 22 21431

>>21430
>Веровается, что с помощью предельного перехода размера интервалов dx к бесконечно малому получается нечто отличное от просто интервалов, хотя ни для кого не секрет, что любые численные методы интегрирования - это чистая дискретка.
Какая разница, что там в реальности считают инженеры?
>Т.е. на самом деле вычисления не идут за пределы реально вычислимого.
А число Грэма?

Ответы1432

23 7 июля 2017, 12:29 23 21432

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

Ответы14341456

24 7 июля 2017, 12:51 24 21434

>>21432
>разницы между фактически построимым и абстракции потенциальной осуществимости
Тогда почему ты говоришь про какие-то там дискретные величины в интегралах? Там бесконечность, континуум! УХ!

Ответы1435

25 7 июля 2017, 13:19 25 21435

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

Ответы1436

26 7 июля 2017, 13:21 26 21436

>>21435
Если ты говоришь про потенциальность то зачем тогда упоминаешь интегральчики?
>Самый простой пример - интегральчики. Веровается, что с помощью предельного перехода размера интервалов dx к бесконечно малому получается нечто отличное от просто интервалов, хотя ни для кого не секрет, что любые численные методы интегрирования - это чистая дискретка.
У нас есть аналитический метод вычисления, без дискретки с континуумом!

27 7 июля 2017, 13:22 27 21437

>>21410
"Математика = вычислимость".
То есть математика - это один из разделов Computer Science?

Ответы1439

34 Кб, 600x823
28 7 июля 2017, 13:29 28 21439

>>21437
>математика - это один из разделов Computer Science?
Да, конструктивное доказательство чему - изоморфизм Карри-Говарда. Хотя так-то это всем умным людям из тех, кого Брауэр не разбудил это стало ясно уже после работ Тьюринга с Постом. Самое смешное, что с тех пор кроме кривляний разной степени толстоты возражений пока не поступало.

Ответы1440

29 7 июля 2017, 13:31 29 21440

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

Ответы1442

30 7 июля 2017, 13:33 30 21441

А что лемму вложенных отрезков думаешь? Можно же пересекать бесконечное число отрезков.

31 7 июля 2017, 13:34 31 21442

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

Ответы1443

32 7 июля 2017, 13:41 32 21443

>>21442
>Автоматическое доказательство коком ничем не отличается от автоматического доказательства человеком.
Во первых, тогда почему твой кок не может оперировать исключающим третьим, аксиомой выбора, и актульными бесконечностями, а человек может? Почему я например могу работать с вещественными числами(бесконечными последовательностями десятичных дробей), а твой кок нет?
Во вторых, доказательство коком сомниетльные, поскольку человек их не может увидеть. А раз мы не можем увидеть доказательство, то веруем в него. Как и веруем в доказательство проблемы черытёх красок, от которого плювался Гротендик.

Ответы1444

65 Кб, 310x350
мейлру образовательный 33 7 июля 2017, 13:47 33 21444

Я вижу, что во-первых, вопросы по конструктивной математике тут таки возникают, во-вторых, с матчастью тут совсем все плохо, настолько плохо, что хуже уже не бывает. Поэтому, вниманию самых маленьких предлагается такая книшка:
http://gen.lib.rus.ec/book/index.php?md5=2BBE15747B57CDB3BAF9F25BDFEC280B да, в совке издавали годные материалы по конструктивной математики даже для дошкольников и младших школьников. Все поясняется буквально на пальцах.
>>21443
>почему твой кок не может оперировать исключающим третьим, аксиомой выбора, и актульными бесконечностями, а человек может?
Во-первых, ты не можешь, ты вероваешь, что можешь. Во-вторых, в коке можно задать и исколюченное третье и даже Аллаха. Но, поскольку это неконструктивные сущности, за которыми не стоит никаких вычислимых в канонические элементы конструкций, это бесполезно.
>Почему я например могу работать с вещественными числами(бесконечными последовательностями десятичных дробей), а твой кок нет?
Давай, покажи. Тащи сюда полностью свои бесконечности.
>доказательство коком сомниетльные, поскольку человек их не может увидеть.
В третий раз тебе говорят, хватит писать мне хуйню, реально надоело. Если ты кок в глаза видел, то видел и доказательства, которые он выдает. А если бы еще слышал про лямбда-куб, исчисление конструкций итд, то даже и понял бы их.

Ответы144514461447

34 7 июля 2017, 13:50 34 21445

>>21444
Ты можешь с помощью кока доказать формулу, что сумма 1+2+3+...+n равна n(n-1)/2?

Ответы1602

35 7 июля 2017, 14:31 35 21446

>>21444
Зачем мне читать твою конструктивную литературу? Почему вместо нормального объяснения ты всё время крепишь скриншоты и отсылаешь к книжкам? Хочешь меня так в свою секту завербовать?
Один раз нормально распиши, а потом копипасть на однотипные ответы, довен.

Ответы1451

36 7 июля 2017, 14:48 36 21447

>>21444
>Во-первых, ты не можешь, ты вероваешь, что можешь.
Смотри, у нас есть множество действительных числе R.
Я беру и выбираю из него такое число x, что оно будет меньше 3 и больше 2.

Ответы1451

37 7 июля 2017, 17:23 37 21451

>>21447
>Смотри, у нас есть множество действительных числе R. Я беру и выбираю из него такое число x, что оно будет меньше 3 и больше 2.
И что дальше? Получаем дискретизацию континуума вещественными числами. Континуум не сводится к множеству R, т.к. между двумя вещественными числами всегда можно вставить еще. Даже если применим абстракцию потенциальной осуществимости и предположим, что такое деление можно вести сколько угодно далеко, все равно итогом будут вещественные числа, но не континуум.
>>21446
>Почему вместо нормального объяснения
Я не виноват, что вместо того, чтобы вникать в объяснения, ты закатываешь глаза и начинаешь кукарекать.
>Один раз нормально распиши
Я каждый раз нормально пишу. Нужно пытаться понять, а не кукарекать.
>Хочешь меня так в свою секту завербовать?
Деревянные по пояс тут точно не нужны. Правильно Максимка говорил, что в рашке никто не может в зависимые типы.

Ответы14571462

38 7 июля 2017, 21:17 38 21456

>>21432
>абстракции потенциальной осуществимости
Да у нас тут ВЕРА

Ответы1467

39 7 июля 2017, 21:19 39 21457

>>21451
>Я каждый раз нормально пишу.
>>20467
И да, когда ты там мне все простые числа перечислишь? Их же конечное число не так ли?

40 8 июля 2017, 01:30 40 21462

>>21451
>Я не виноват, что вместо того, чтобы вникать в объяснения, ты закатываешь глаза и начинаешь кукарекать.
Посылание читать Брауэера это не объеснения.
>Я каждый раз нормально пишу.
Ты даже сейчас не можешь нормально писать и скатываешься до оскорблений. Давай ссылку на пост с нормальными объяснениями, раз писал.
>Деревянные по пояс тут точно не нужны.
>— Ты издеваешься. Ты не можешь писать это всерьёз.
>— Я не виноват, что ты такой тупой.

Ответы1467

41 8 июля 2017, 10:05 41 21467

>>21462
>Посылание читать Брауэера это не объеснения.
Да ну, какой тебе Брауэр, ты вышеупомянутую книжку для дошкольников не осилишь. Хотя если бы осилил, много откровенно тупых вопросов бы отпало, там реально хорошо объясняют, лучше чем я. При всем неуважении к совку, научпоп там был мирового уровня. Но тебе не нужны объяснения (да, я сто раз объяснял, можешь опять вспомнить свою пасту), ты изначально исходишь из предположения, что я неправ, и уже с этой позиции рассматриваешь все остальное, безотносительно к его содержанию. Мне-то похуй, одно непонятно, зачем тогда тебе вообще сюда писать и пытаться что-то кому-то доказать.
>>21456
Вот как пример, что можно доказать тому, для которого абстракция и вера это одно и то же? Тут вообще говорить не о чем.

Ответы1468

42 8 июля 2017, 10:38 42 21468

>>21467
>Да ну, какой тебе Брауэр, ты вышеупомянутую книжку для дошкольников не осилишь
Я не собираюсь читать какие-то книжки для того, чтобы доказать свою правоту анону с двачей. Это лишнее.
>ты изначально исходишь из предположения, что я неправ,
А я должен был считать изначально, что ты прав? У тебя не получилось доказать свою провату, и каждый раз ты только и делаешь, что уходишь от ответа:
Ну ты типа тупой, не поймёшь)))
Иди Брауэра читать)))
Да я уже сто раз объяснял)))
Это вера а не математика)))
Хватит уходить от вопросов, нам нужны ответы!
>да, я сто раз объяснял
Тогда дай ссылки на посты с объяснениями. А то только можешь отсылать читать свои книжки, да скиншоты лепить. Ты сам видно не до конца понимаешь всю эту мутотень с основаниями и поэтому нормально объяснить не можешь.
>Вот как пример, что можно доказать тому, для которого абстракция и вера это одно и то же?
Континуум или трансфитная индукция тоже абстрактная вещь, но ты называешь его верой.

Ответы1493

1,3 Мб, webm,
552x512
43 8 июля 2017, 13:15 43 21493

>>21468
>Я не собираюсь читать какие-то книжки для того, чтобы доказать свою правоту анону с двачей.
А что ты мне можешь доказать, если не понимаешь разницу между верой и абстракцией и между трансфинитной индукцией и континуумом? Смешно даже читать такое. А книжки нужны не для того, чтобы что-то кому-то доказать и самоутвердиться, а чтобы в вопросе разобраться. Для этого читать книжки - норма. К слову, это не ты тот деятель, который еще зимой обещал меня разгромить, доказав мне неправильность MLTT?

Ответы1496

44 8 июля 2017, 13:44 44 21496

>>21493
Вот бы сейчас использовать Успенского для борьбы с этими гадкими бесконечностями.

Ответы1499

45 8 июля 2017, 13:53 45 21499

>>21496
>Успенского
Ну раз Брауэра и Мартин-Лёфа тута не осилили, может быть хоть Успенский зайдет.

Ответы1505

46 8 июля 2017, 14:04 46 21505

>>21499
Который сам почему-то отзывается об интуиционизме неприязненно.

Ответы1507

47 8 июля 2017, 14:12 47 21507

>>21505
>Который сам почему-то отзывается об интуиционизме неприязненно.
Называя Брауэра "замечательным математиком"? Но допустим, в целом это возможно, ведь в совочке брауэровский интуиционизм считали буржуазным идеалистическим учением, в отличие от конструктивизма, который с вычислительной точки зрения то же самое. Опять же, если ты этого не можешь понять, почему это должны были понимать выжившие из ума старперы из КПСС? Они и логицизм Рассела считали тем же самым и даже заявляли, что это причина того, что Рассел призывал разбомбить совок ядерным оружием.

Ответы1509

48 8 июля 2017, 14:17 48 21508

Есть вещи, которые невозможно вычислить или узнать через машЫну. Есть истины, которым нет объяснения. Исходя из этого, именно в этот момент в сознании людей появляется вера во что-то сверхъестественное (и это не плохо). Об этом еще Гедель писал. Кончайте уже со своим конструктивизмом выебываться. Машина не может дать истинные ответы на все вопросы.

/thread

184 Кб, 672x511
49 8 июля 2017, 14:17 49 21509

>>21507
Недавняя книжка, появившаяся сильно после кпсс. Первое попавшееся место.

Ответы15451549

50 8 июля 2017, 15:29 50 21534

Зависимые типы я осилил, а вот исчисление конструкций пока нет. Чем примечательны, полезны, красивы исчисления конструкций, если объяснять для чайника?

Ответы1545

111 Кб, 819x227
51 8 июля 2017, 17:02 51 21545

>>21509
Хорошая книжка, автору сразу можно помочиться за шиворот и отправить доучиваться. Классическая матлогика не рассматривает смысл (т.е. семантику) выражений вообще, от слова никак. Там только синтаксис, о чем писал и Гильберт и Бурбаки.
>>21534
> исчисление конструкций пока нет.
С Барендрегта начни. Исчисление конструкций - просто наиболее полное лямбда-исчисление по Черчу, т.е. в кубе Барендрегта.

Ответы1564

83 Кб, 1015x140
52 8 июля 2017, 17:27 52 21549

>>21509
На пикрелейтед месте можно окропить автора уриной еще раз. Он даже конструктивное отрицание не осилил. "Недоказанный" и "неверный" конструктивно абсолютно разные понятия.

Ответы1564

53 8 июля 2017, 19:54 53 21564

>>21545
>>21549
Эй, конструктивист, ты упорот? Автор этого текста - твой собственный Успенский.

Ответы1565

54 8 июля 2017, 20:01 54 21565

>>21564
Ну я рад, дальше что? Написанного мной про конструктивное отрицание и семантику матлогики это не отменяет. Что за книжка-то?

Ответы1566

55 8 июля 2017, 20:04 55 21566

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

"Предисловие к математике".

Ответы1568

29 Кб, 1438x227
56 8 июля 2017, 20:07 56 21568

>>21566
Где книшку-то взял? На либгене нету.
>Ссылаешься на него как на большого авторитета
На конкретную книгу, которую читал лично и в которой ошибок не обнаружил.

57 9 июля 2017, 15:22 57 21597

>>21361 (OP)
Вопрос к конструктивистам. В конструктивизме 0.(9)=1?

Ответы16031607

58 9 июля 2017, 16:25 58 21602

>>21445
В принципе, конструктивно, как мне кажется, это можно доказать. Если я хорошо понимаю суть конструктивизма(а я узнал о нем из этого треда), то конструктивное доказательство будет выглядеть так:

У нас есть сумма (сложнее сумму возьмем): a/b+a/b²+a/b³+...+a/b^n = S. Но n – конечно, хоть и очень большое. И, чем больше n, тем смелее можно пренебречь последним членом суммы. Поэтому, для довольно больших n имеем:

a/b+a/b²+a/b³+...+a/b^(n-1) = bS–a
S = bS–a

Просто пренебрегаем последним членом.

Ответы16044453

59 9 июля 2017, 16:27 59 21603

>>21597
Впрочем, да. Но тут несколько новых понятий придется ввести.

Ответы1604

60 9 июля 2017, 16:29 60 21604

>>21602
>>21603

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

Ответы1607

61 9 июля 2017, 17:12 61 21607

Чем одно и то же >>21604 >>21597 спрашивать сотый раз, послушайте лучше умного человека.
https://www.youtube.com/watch?v=VDreWuWDUu0&t=1269s

Ответы20264908

62 16 июля 2017, 06:24 62 21956

А как с мнимой единицей у конструктивистов дела обстоят? Мы же просто верим в её существание, она имеет отличную природу от натуральных чисел.

Ответы1960

63 16 июля 2017, 09:54 63 21960

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

Ответы19911993

64 16 июля 2017, 21:54 64 21991

>>21960
Некоторые калькдяторы и бесконечность считают, мнимания единица имеет другию прировуд. Вот число один -это число. Но мнимая единица не имеет алгоритма построения.

Ответы1995

65 16 июля 2017, 22:51 65 21993

>>21960
Комплюктор не ПОНИмает сути производимых операий. Он просто следует алгоритму который в него вбили.

Ответы19941997

66 16 июля 2017, 22:55 66 21994

>>21993
>Комплюктор не ПОНИмает сути производимых операий. Он просто следует алгоритму который в него вбили.
Прямо как конструктивисты, лол.

67 16 июля 2017, 23:00 67 21995

>>21991
> Некоторые калькдяторы и бесконечность считают, мнимания единица имеет другию прировуд. Вот число один -это число. Но мнимая единица не имеет алгоритма построения.
Ты читать не умеешь? Вычисление это построение.

Ответы1996

68 16 июля 2017, 23:03 68 21996

>>21995
Как можно построить мнимую единицу?

Ответы1999

64 Кб, 460x500
69 16 июля 2017, 23:07 69 21997

>>21993
> Комплюктор не ПОНИмает сути производимых операий.
Суть, семантика производимых операций в MLTT это вычисление, т.е получение канонических элементов. Комплюктер понимает вычисление иак же как и не комплюктер, ты никогда и не при каких обстоятельствах не сведешь вычисление к тому, к чему его не сведет компьютер, следовательно твое понимание вычисления равнообъемно с компьютерным. И это сто раз уже писано, просто вы все иута деревянные по пояс.

Ответы1998

70 16 июля 2017, 23:09 70 21998

>>21997
А computer science - это чистая математика?

Ответы2000

71 16 июля 2017, 23:09 71 21999

>>21996
> Как можно построить мнимую единицу?
А как нельзя? Ее даже нарисовать можно, погугли. Суть построений в вычислимости, еще раз говорю. Построение это вычисление, ферштейн, нихт?

Ответы2001

72 16 июля 2017, 23:11 72 22000

>>21998
> А computer science - это чистая математика?
В рамках изоморфизма Карри- Говарда, если тебе эти слова о чем'то говорят.

Ответы2002

73 16 июля 2017, 23:14 73 22001

>>21999
Можно и бесконечность нарисовать, а ты мне найди число, которое в квадрате будет -1.

Ответы2003

74 16 июля 2017, 23:15 74 22002

>>22000
Нет, я плох в программировании.

Ответы2004

75 16 июля 2017, 23:28 75 22003

>>22001
> Можно и бесконечность нарисовать,
Бесконечность невычислима, комплексные числа вычислимы. Спать идите, аутисты.

Ответы20052009

76 16 июля 2017, 23:29 76 22004

>>22002
> Нет, я плох в программировании.
Это математика в том же объеме, что и програмиирование. Если слово 'изоморфизм' тебе о чем'то говорит.

77 16 июля 2017, 23:33 77 22005

>>22003
Откуда взялось i? Мы просто верим, что существует число, равно в квадрате -1?

Ответы2006

78 17 июля 2017, 00:10 78 22006

>>22005
> Откуда взялось i? Мы просто верим, что существует число, равно в квадрате -1?
Верования невычислимы, конструктивные объекты вычислимы. Комплексные числа вычислииы. Так ясно?

Ответы2007

79 17 июля 2017, 01:10 79 22007

>>22006
Чему равно пи мы знаем, но чему равно i?

Ответы2010

80 17 июля 2017, 02:44 80 22009

>>22003
>Бесконечность невычислима
Арифметика кардиналов вычислима.

81 17 июля 2017, 03:56 81 22010

>>22007
i = (0,1)

Ответы2011

82 17 июля 2017, 04:00 82 22011

>>22010
Это семантика. Всё равно, что сказать бесконечность = /inf.
Я хочу знать, чем оно равняется.

Ответы2012

83 17 июля 2017, 04:41 83 22012

>>22011
> Это семантика. Всё равно, что сказать бесконечность = /inf.
Тебе тролить тупостью не надоело? Конструктивно семантика это вычисление. Эта твоя запись /inf не вычислима ни во что, т.к не является каноническим элементом, не является она и неканоническтм элементом, поскольку не имеет правил вычисления в канонический элемент. Аллаха опять же в этой связи уже обсуждали. И открой для себя гугл, разберись с любым алгоритмом вычисления комплексных чисел, а не пиши одно и тоже сюда сто раз.

Ответы201320142022

84 17 июля 2017, 04:50 84 22013

>>22012
Повторяю, можно дать тебе алгоритм, с помощью которого ты сможешь работать с ординальной арифметикой.

85 17 июля 2017, 05:11 85 22014

>>22012
Вычисли мне i.

Ответы2018

проблемс? 86 17 июля 2017, 10:46 86 22018

>>22014
x <- 1
y <- 1
z <- complex(real = x, imaginary = y)
z
[1] 1+1i
as.complex(-1)
[1] -1+0i
is.complex(as.complex(-1))
[1] TRUE
z <- complex(real = 2, imaginary = 1)
Re(z)
[1] 2
Im(z)
[1] 1

Ответы2019

87 17 июля 2017, 10:50 87 22019

>>22018
Это лишь формальные операции над символами.

Ответы2020

88 17 июля 2017, 11:04 88 22020

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

Ответы20212022

89 17 июля 2017, 11:21 89 22021

>>22020
Чем тогда это отличается от Аллаh'а?

Ответы2022

90 17 июля 2017, 11:26 90 22022

>>22021
Я уже очень, очень много раз говорил чем. Последний раз в этом посте >>22012 но ты не вертись, а показывай свой вариант вычисления комплексных чисел >>22020

Ответы2023

91 17 июля 2017, 11:41 91 22023

>>22022
Определи канонический элемент, будь любезен.

Ответы2024

92 17 июля 2017, 11:54 92 22024

>>22023
Тоже много раз обсуждалось уже, со скринами и примерами. Все определения тута есть http://www.cse.chalmers.se/research/group/logic/book/book.pdf в первой части.

Ответы20252027

93 17 июля 2017, 11:56 93 22025

>>22024
Хватит кидать ссылки на книги. Я так же могу обсуждать работу мочидзуки, а когда у меня что-то спросить, то дать ссылки на статьи, и сказать сто раз обсуждалось, там же написано. Берёшь и объясняешь всё с нуля.

Ответы2026

94 17 июля 2017, 13:17 94 22026

>>22025
>Я так же могу обсуждать работу мочидзуки
Какой тебе Мочидзука, ты ж элементарное понятие вычислимости осилить не можешь. Ты даже понятие равенства по этой лекции >>21607 не осилишь.

95 17 июля 2017, 13:40 95 22027

>>22024
Вместо ответа давать ссылку на талмуд? Всё по методичке, лол. http://lurkmore.to/Правила_демагога

Ответы2028

96 17 июля 2017, 13:55 96 22028

>>22027
>вместо аргумента тащит на мейлру ссылку с лурки
>обвиняет кого-то в использовании методичек
Ясно.

Ответы2029

97 17 июля 2017, 14:00 97 22029

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

Ответы2030

62 Кб, 274x477
98 17 июля 2017, 14:18 98 22030

>>22029
В MLTT 4 суждения, 4 правила вывода, 4 основных типа и 4 правила построения выражений. Все это можно уместить на половину тетрадного листа. Тетраграмматон рабби Лёфа прост как 4 шекеля. Проблема только в том, что за всем этим стоит не пустой синтаксис ни о чем, как в формализме, а вычислимая конструктивная математика, где даже понятие равенства имеет вычислительное содержание. Это вам не невычислимые ни во что кардиналы и прочих Аллахов рисовать, тут уже не глиняная голова нужна, чтобы въехать.

Ответы20314454

99 17 июля 2017, 14:22 99 22031

>>22030
Если это так просто, то объясни же это. Зачем ссылки непонятно на что кидать.

Ответы2032

100 17 июля 2017, 14:23 100 22032

>>22031
>Зачем ссылки непонятно на что кидать.
Не "непонятно на что", а как раз на объяснения.

Ответы2033

101 17 июля 2017, 14:30 101 22033

>>22032
На многие сотни страниц. Совсем не половина тетрадного листа, как ты говоришь.

Ответы2034

102 17 июля 2017, 14:49 102 22034

>>22033
Аксиомы исчисления предикатов тоже немного места занимают. А книг с нормальным изложением меньше чем на сотню страниц так же нет. Поэтому возражение не принимается.

Ответы2037

103 17 июля 2017, 16:37 103 22037

>>22034
Бурбаки. Вся лежащая под математикой логика, включая исчисление предикатов, занимает страницы 31-65. Из них на собственно исчисление предикатов отводится четырнадцать страниц.

Ответы2038

456 Кб, 726x1084
104 17 июля 2017, 16:50 104 22038

>>22037
>Бурбаки
Пикрелейтед.
>Вся лежащая под математикой логика,
Не вся, ZFC не может в типы, а за что-нибудь уровня NBG у бурбаков нет ничего.
>занимает страницы 31-65. Из них на собственно исчисление предикатов отводится четырнадцать страниц.
Вся книжка Мартин-Лёфа 50 с небольшим страниц, собственно изложение самой теории даже не половина https://github.com/michaelt/martin-lof/blob/master/pdfs/Bibliopolis-Book-retypeset-1984.pdf

Ответы2039

124 Кб, 635x868
105 17 июля 2017, 17:03 105 22039

>>22038
На твоём пике математика в объёме, превышающем кандидатский курс (гомологическую алгебру не изучают даже в магистратуре, например). Речь шла о предикатах онли. Короче, показывай листок.
>за что-нибудь уровня NBG
Аксиоматика Бурбаки строго сильнее ZFC. Не слабее чем NBG+аксиома глобального выбора.

Ответы204020422044

106 17 июля 2017, 17:46 106 22040

>>22039
Аксиома S8 - обобщенный replacement, если непонятно.

107 17 июля 2017, 19:43 107 22042

>>22039
К этой картинке пояснений как раз под сотню страниц и нужно. Из самой картинки не выведешь тау (или эпсилон Гильберта) и т.д. Ну и главная претензия - вычислимость, конечно. Даже не исключенное третье, с этой хуиткой все ясно, вот самая последняя строка, А5. "Существует бесконечное множество", вот и Аллаха подвезли. В каком смысле оно существует? впрочем, все это опять же уже сто раз обсуждалось, сейчас пойдут аргументы про чернильную дыру и про то что актуальная бесконечность не хуже потенциальной осуществимости, бла-бла... К MLTT так не доебешься, пример - лекция выше, там даже равенство сводится к вычислимым построениям, а не просто к значку "=".

Ответы2059

108 17 июля 2017, 19:53 108 22044

>>22039
>Аксиоматика Бурбаки строго сильнее ZFC. Не слабее чем NBG+аксиома глобального выбора.
До двух считать научиться по их книгам можно?

Ответы20462059

109 17 июля 2017, 19:55 109 22046

>>22044
>До двух считать научиться по их книгам можно?
Нет, на единице застрянешь.
>получаем, что полная запись обыкновенной единицы состоит из 2 409 875 496 393 137 472 149 767 527 877 436 912 979 508 338 752 092 897 знаков и 871 880 233 733 949 069 946 182 804 910 912 227 472 430 953 034 182 177 связей, то есть полная запись терма, обозначающего единицу, заняла бы сто миллиардов квинтиллионов квинтиллионов книг

Ответы20532059

22 Кб, 333x249
110 17 июля 2017, 21:38 110 22053

>>22046
УРЕТЕ!!!! АДИН ЕТА СЕРЫЙ КОРДЕНАЛ ПУСТОВА МНОЖЕСТВА!!!! ДЖВА ЕТА КАРДЕНАЛ МНОЖАСТВА АДЫН!!! И ТАК ДАЛЕЕ!!!
Мне такой ответ встречался.

Ответы20552059

111 17 июля 2017, 21:54 111 22055

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

Ответы2056

112 17 июля 2017, 22:34 112 22056

>>22055
До двух досчитать нельзя

24 Кб, 632x198
113 18 июля 2017, 02:07 113 22059

>>22042
>В каком смысле оно существует?
Бессмысленная строка символов, которая в естественный язык транслируется как "существует бесконечное множество", является аксиомой.

>MLTT так не доебешься
Либо ты постишь листочек, либо ты - всего лишь ещё один сосачеребенок.

>>22044
Да.

>>22046
Это, конечно же, вздор.

>>22053
Неверно. Кардинал пустого множества - это 0. Число 1 - это кардинал множества {0}. Число 2 - это кардинал множества {0,1}.

Ответы20672071

114 18 июля 2017, 08:29 114 22067

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

Ответы2069

128 Кб, 639x613
115 18 июля 2017, 08:43 115 22069

>>22067
В книгах Бурбаки нет ничего "переусложненного", они очень легко читаются (пикрелейтед). Вообще, это такой детектор очень хороший: кто считает Бурбаки чем-то сложным, тот некомпетентный лапоть с шерстью на ушах.

Ответы20712072

116 18 июля 2017, 10:49 116 22071

>>22059
>Либо ты постишь листочек, либо ты - всего лишь ещё один сосачеребенок
Что ты разнервничался? Вон же у Максимки все есть http://groupoid.space/mltt/semantics/ с нескучным оформлением. Педивикия опять же.
>Это, конечно же, вздор.
Это эпсилон Гильберта, формализм курильщика.
>>22069
>Вообще, это такой детектор очень хороший: кто считает Бурбаки чем-то сложным, тот некомпетентный лапоть с шерстью на ушах.
Школьца-максималиста в тебе вижу я.

Ответы2073

117 18 июля 2017, 10:50 117 22072

>>22069
Иначе говоря, то что первый параграф ссылается на вторую главу, параграф шесть, пункт номер один, это признак хорошего, годного легко читающегося учебника.
Это ты так двачи тролируешь тупость или реально такой дурачек?

Ответы207320752078

118 18 июля 2017, 10:59 118 22073

>>22071
Хорошо, теперь давай по порядку. Что по Мартин-Лёфу есть proposition и что есть judgement? В предложенных тобой книгах эти термины используются, но определений им не дано.

>>22072
>ссылается
Впервые математическую книжку увидел, да?

Ответы2075

95 Кб, 815x428
119 18 июля 2017, 11:08 119 22075

>>22072
У бурбаков проблема не в этом. Я даже соглашусь, что это хорошая литература. А в том, что при попытке полной формализации того, о чем они пишут, мы очень быстро упремся в квинтиллионнобуквенные термы. Там же они с самого начала пишут, что для удобочитаемости текста он почти полностью состоит из соглашений, вольностей речи и т.д., откуда и столько отсылок к ранее определенным вещам. В MLTT такой хуйни нет, там все можно свести к вычислениям и вычислить полностью.
>>22073
>Что по Мартин-Лёфу есть proposition и что есть judgement? В предложенных тобой книгах эти термины используются, но определений им не дано.
Попочтец, плиз. Самая первая страница. Пропозишен = формула в матлогике (и множество, согласно изоморфизму Карри-Говарда), суждение = теорема. Совсем подробно - 4ая глава в programming in martin-löf's type theory.

Ответы2077

120 18 июля 2017, 11:13 120 22076

Спешите видеть, илитные математики-бурбакисты не могут досчитать до двух.
В то время как обычные пятимесячные младенцы УЖЕ умеют считать до двух.
Вот пруф
https://books.google.com.ua/books?id=s5KqmjDyxTMC&printsec=frontcover&hl=ru#v=onepage&q&f=false
Если откопаете полную версию то сможете узнать что даже макаки-резусы умеют считать до трех.
Тобишь буракисты это даже не уровень человеческой личинки. Они хуже макак.

121 18 июля 2017, 11:26 121 22077

>>22075
Я видел этот текст, и он мне непонятен. Прошу объяснить. Я прочитал столько книжек, что слово "формула" для меня не имеет само по себе никакого смысла, увы.
>из соглашений, вольностей речи и т.д.
Из сокращений; это другое. Это не неформальность, а лишь инкапсуляция и абстракция. Любую главу трактата можно рассмотреть как набор аксиом некой новой формальной теории, а все предыдущие главы забыть. В этой новой теории букв в знакосочетаниях будет гораздо меньше. Кроме того, трактат можно дополнить минус первой, минус второй и сколь угодно более низкоуровневыми главами - общность при этом будет повышаться, сложность грамматики - падать, количество букв в знакосочетаниях - увеличиваться. Например, язык начальной главы можно транслировать в морзянку. Математика окажется в таком случае теорией о громадных совокупностях точек и тире.

Ответы2079

122 18 июля 2017, 11:42 122 22078

>>22072
>тролируешь тупость
Это конструктивисты траллируют тупостью, когда говорят, что бесконечности нет и аксиома исключающего третьего вера.

Ответы2079

123 18 июля 2017, 11:48 123 22079

>>22077
>а лишь инкапсуляция и абстракция
Считающаяся в термы из квинтиллионов знаков. Это проблема, пони маешь? Потому что если мы захотим это на самом деле посчитать, то...
>Я прочитал столько книжек, что слово "формула" для меня не имеет само по себе никакого смысла, увы.
Значит, неправильные книжки читал. Я ж уточнил, что "формула" там имеет значение, обычное именно для матлогики. Ну и также можно считать пропозишен множеством.
>>22078
>когда говорят, что бесконечности нет
Ты для начала пойми о чем вообще тут говорят, потом в разговор лезь.

Ответы20804455

124 18 июля 2017, 12:02 124 22080

>>22079
>в термы из квинтиллионов знаков
Только если считающему угодно настолько сильно углубиться в абстракцию. Он вполне может остаться на одном из более высоких уровней, на них символов будет заметно меньше. Например, можно отказаться от трансляции кванторов и импликации, приняв их в синтаксис, тогда квинтиллионы мгновенно исчезнут. Алсо, не в термы, в знакосочетания.
>обычное именно для матлогики
Произвольная формула? Правильно построенная формула (элемент наименьшего класса формул, замкнутого относительно логических связок и содержащего все атомы)? Выводимая формула? Меня "hold to be true" смущает, это вообще о чем.

Ответы2081

64 Кб, 818x381
125 18 июля 2017, 12:34 125 22081

>>22080
>Меня "hold to be true" смущает, это вообще о чем.
Изоморфизм Карри-Говарда же. И интерпретация логических констант по Брауэру-Гейтингу-Колмогорову. Общеизвестно, что логические операции это то же самое, что операции над множествами. Истина - это 1, ложь = 0. Классически пропозишен - это функция принадлежности или характеристическая функция, принимающая значение 0 или 1 (не считая многозначных логик). Логическое "и" это пересечение множеств, "или" - объединение, импликация - отношение подмножества. Конструктивно же пропозишен - это множество пруф-объектов, т.е. построений, доказывающих, что данное множество не пусто. Т.о. по упомянутому изоморфизму Карри-Говарда, истинность пропозишена А - это ненулевое количество элементов х принадлежащих А, х:А. Доказательство "не А" - это построенное пустое множество. Отсюда уже видно, почему исключенное третье в общем случае не работает. Классически верно правило "А или не А", конструктивно мы должны доказать конкретно, А или не А, т.е. пусто множество А или нет. Это можно сделать только построив его. Конкретные методы построений получаются интерпретацией логических констант по Колмогорову, т.е. в простейшем случае это могут быть лямбда-термы, а все вышесказанное в таком случае можно свести к типизированной лямбде, откуда вычисление это есть лямбда-определимость. Итд итп.
>Только если считающему угодно настолько сильно углубиться в абстракцию. Он вполне может остаться на одном из более высоких уровней, на них символов будет заметно меньше.
Классически и так сойдет, конечно. тяп-ляп и готов кризис оснований Конструктивно нам нужна полная вычислимость, чего с бурбаками не выйдет вообще никак.

Ответы20822083

126 18 июля 2017, 12:55 126 22082

>>22081
>Конструктивно нам нужно уметь считать ящик и сдачу в магазине
Поправил тебя чутка

127 18 июля 2017, 13:17 127 22083

>>22081
>логические операции
А как быть, если нужны нелогические операции? От голого исчисления предикатов мало пользы, пользу приносят первопорядковые теории (исчисление предикатов плюс нелогические формулы).
>операции над множествами
Для корректности такого подхода нужно зафиксировать метатеорию множеств и внятно определить предметную область. Неоправданно сложный подход, чисто синтаксический подход гораздо яснее (а всё семантическое надстраивается на него в теории моделей).
>построений
Что считается построением?
>полная вычислимость
Вычислимость бесконечна вниз, если можно так выразиться. Всегда можно заменить атомарное действие фиксированного исполнителя подпрограммой для более низкоуровневого исполнителя. Полной вычислимости не бывает.

Ответы2084

128 18 июля 2017, 13:22 128 22084

>>22083
Собственно, на все вопросы в твоем посте ответ один - типизированная лямбда.
>Вычислимость бесконечна вниз, если можно так выразиться.
Только до канонических элементов, которые дальше невычислимы ни во что.

Ответы2085

129 18 июля 2017, 13:23 129 22085

>>22084
>канонических элементов
А что это такое?

Ответы2086

130 18 июля 2017, 13:32 130 22086

>>22085
По определению - замкнутые, насыщенные лямбда-термы нулевой арности. Ну или категоремы. Элементы, которые нельзя вычислить во что-то нижележащее, т.к. они сами по себе есть итоговые значение вычислений. Пример - натуральные числа, как элементы множества N они не сводятся к чему-либо более простому.

Ответы2087

131 18 июля 2017, 13:39 131 22087

>>22086
>категоремы
Я не знаю, что это такое. Но ведь, гм. Для натуральных чисел можно предложить много нижележащих теорий, разве нет?

Ответы2088

132 18 июля 2017, 13:44 132 22088

>>22087
>Для натуральных чисел можно предложить много нижележащих теорий, разве нет?
Вычислимых-то? Думаю, строго 0. Ниже нумералов Черча сложно что-то придумать, даже ординалы фон Неймана - это то же яйцо, вид сбоку. Впрочем, можешь и предложить, думаю медаль филдса за таконе точно не пожалеют.

Ответы2089

3 Кб, 217x78
133 18 июля 2017, 13:51 133 22089

>>22088
Теория, предложенная Бурбаки. Если не вводить теорию множеств во всей полноте, то арифметические построения можно описать знакосочетаниями вида пикрелейтед длиной не более чем в несколько миллионов символов (грубая оценка сверху, на самом деле меньше). Вполне реальный объём для современных компьютеров.

Ответы20902103

134 18 июля 2017, 14:00 134 22090

>>22089
Эпсилоны Гильберта считать со всеми квинтиллионами знаков? Вот ты спрашивал, что есть канонический объект. Вот этот хулиардквадриллионный терм для единицы - это как раз канонический элемент множества N по бурбакам, который ниже уже ни во что не считается. Это можно, конечно. Но грустно, когда ферма из асиков размером с взлетную полосу, будет считать 1+1 пару дней. Самое обидное, что итоговый результат будет тот же, что с нумералами Черча, т.е. натуральное число 2, которое, конечно можно представить еще какими-то квадриллионными термами, но остается вопрос - нижестоящая ли это теория или таки вышестоящая, т.к. использует более сложный алфавит, чем н-р натуральное число как слово в алфавите | по Маркову?

Ответы2091

135 18 июля 2017, 14:09 135 22091

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

Ответы2092

136 18 июля 2017, 14:44 136 22092

>>22091
>То есть канонический элемент - это всего лишь терм в формальном языке, который выбран для аксиоматической теории?
Точнее терм, который в данной теории нельзя свести ни к чему нижележащему. Но тут уже встает вопрос математического релятивизма (не путать с физикой), согласно которому, любую теорию можно выразить через любую другую, точнее между теорией А и В существует конечное количество теорий А1-Ан, причем теория А выразима в теории А1, а теория Ан - в теории В. В таком случае без разницы, какую теорию считать первичной, т.к. мы все равно можем придти к любой из них из любой другой. Чисто прагматически, более первичной удобнее считать более простую теорию, т.е. уж точно не стоит считать эпсилон-исчисление Гильберта основанием арифметики, потому что полнейший аутизм сначала учить детей в школе эпсилон-исчислению, а затем решать примеры 1+1. Конструктивно всю математику можно вывести из арифметики, прагматически это самый простой путь, гораздо проще и естественнее чем теория множеств, тем более в виде бурбакизма. Естественнее, потому что доказано, что понятие натурального числа врожденно и предшествует даже языковым способностям (такие нейрофизиологические модели как ATOM Уолша и теория метафор), если с более философской стороны, то Кант и Брауэр.

Ответы20932137

137 18 июля 2017, 15:45 137 22093

>>22092
Спасибо за ответы.

Бывает разная простота. Есть простота для решения задач, причем для разных классов задач простотой окажется разное - например, для решения уравнений вида x+a=b бурбаки очевидно не будут самым простым выбором. Есть простота для доказательства теорем, и вот здесь уже может оказаться наиболее простым выбором, скажем, определять дроби с помощью деления в столбик (анекдотический пример от Арнольда). Универсальной простоты не бывает.

138 19 июля 2017, 00:06 138 22103

>>22089
>компьютеров
Правильно, зачем чукче думать, пусть пекарня думает

Ответы2106

139 19 июля 2017, 04:11 139 22106

>>22103
> Правильно, зачем чукче думать, пусть пекарня думает
А чем твои думы в области математики, чукча, отличаются от дум пекарни в этой же области? Я просил привести примеры вычислимости, не сводящиеся у механическим преобразованиям выражений. Пока примеров не поступало.

Ответы2108

140 19 июля 2017, 06:48 140 22108

>>22106
Не вся математика сводится к вычислимости.

Ответы2109

141 19 июля 2017, 06:56 141 22109

>>22108
> Не вся математика сводится к вычислимости.
Старые песни о главном. Если что-то невычислимо, с какой стати это вообще математика? И да, что в математике не сводится к вычислимости? Исключенное третье, актуальная бесконечность и прочая религия?

Ответы2110

142 19 июля 2017, 06:57 142 22110

>>22109
Это ты сужаешь математику на computer science, ограничевая его её алгоритмами.

Ответы2111

143 19 июля 2017, 07:02 143 22111

>>22110
> Это ты сужаешь математику на computer science, ограничевая его её алгоритмами.
Примеры, примеры в студию. Что в математике не сводится к алгоритмам, где математика, не являющаяся преобразованием знакосочетаний и термов по заданным правилам? Формализм без формализма, давай примеры.

Ответы211221132169

144 19 июля 2017, 07:04 144 22112

>>22111
А как же алгоритмически неразрешимые проблемы?

Ответы2114

145 19 июля 2017, 07:04 145 22113

404 Кб, 1422x2000478 Кб, 1412x1994484 Кб, 1436x2010382 Кб, 1416x1997

>>22111

Ответы2116

146 19 июля 2017, 07:08 146 22114

>>22112
> А как же алгоритмически неразрешимые проблемы?
Ты можешь как-то решить алгоритмически неразрешимые проблемы? И как?

Ответы2115

147 19 июля 2017, 07:10 147 22115

>>22114
Той же аксиомой выбора люди успешно пользуются.

Ответы2117

148 19 июля 2017, 07:12 148 22116

>>22113
И что это? Ты хочешь сказать, что это неразрешимо алгоритмически, но разрешимо как-то иначе?

Ответы2125

149 19 июля 2017, 07:13 149 22117

>>22115
> Той же аксиомой выбора люди успешно пользуются.
Как пользуются?

Ответы2118

150 19 июля 2017, 07:14 150 22118

>>22117
Успешно. Сюда кидали скрины Энгелькинга, посмотри.

Ответы2119

151 19 июля 2017, 07:18 151 22119

>>22118
Ясно. Вчера по бурбакам пояснил за все эти сокращения, соглашения итд, остальное по аналогии. Не считая того, что в mltt аксиома выбора это не аксиома, а теорема и ее можно доказать. Тоже сто раз уже писал, давал ссылкуи постил скрины.

Ответы2120

152 19 июля 2017, 07:24 152 22120

>>22119
Я про скрины с Энгелькингом, прочитай его и посмотри.

Ответы2121

153 19 июля 2017, 07:29 153 22121

>>22120
> Я про скрины с Энгелькингом, прочитай его и посмотри.
Зачем? Там в любом случае нотация, формализмы и правила преобразований, т.е алгоритмы.

Ответы2122

154 19 июля 2017, 07:34 154 22122

>>22121
Где? Укажи на скринах?

Ответы2123

155 19 июля 2017, 07:40 155 22123

>>22122
Как в случае с комплексными числами, ты опять притащил сам не понимаешь что, и теперь пытаешься троллить тупостью. Мне это не интересно.

Ответы2124

156 19 июля 2017, 07:42 156 22124

>>22123
Тебе не надоело уходить от ответов?

157 19 июля 2017, 07:58 157 22125

>>22116
>это неразрешимо алгоритмически
this
там нет алгоритмов

Ответы2126

158 19 июля 2017, 08:14 158 22126

>>22125
> там нет алгоритмов
Есть правила работы с этим. Есть то, откуда это вывели, есть следствия, к которым это приводит. Если у тебя от слова 'алгоритм' бампельштильцхен, это не ко мне. И обяснять вещи, которые уже 3хлетний бы понял, мне так же неинтересно. Ты даже не можешь объяснить о чем речь вообще, мне это и темболее не нужно.

Ответы2136

159 19 июля 2017, 11:58 159 22136

>>22126
С аксиомой выбора так же. Есть следствия, к которым она приводит.

Ответы2139

160 19 июля 2017, 12:29 160 22137

>>22092
А есть идеи как учить школьников конструктивной математике? В смысле, наверное, большей работы со средствами доказательства теорем или что-то такое. Или может еще что?

Ответы2138

161 19 июля 2017, 12:44 161 22138

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

162 19 июля 2017, 12:49 162 22139

>>22136
> С аксиомой выбора так же. Есть следствия, к которым она приводит.
И что дальше? Ты хочешь сказать, что это не укладывается в понятия формализма, нотации или допустимых преобразований выражений, термов или знакосочетаний? Или что ты доказать-то пытаешься?

Ответы2140

163 19 июля 2017, 13:01 163 22140

>>22139
Тогда почему она - аллах, а другие аксиомы - не аллах?

Ответы2141

164 19 июля 2017, 13:05 164 22141

>>22140
Разницу между вычислимым и невычислимым обсуждали неоднократно даже в этом треде.

Ответы2143

165 19 июля 2017, 13:37 165 22143

>>22141
Она укладывается "в понятия формализма, нотации и допустимых преобразований выражений".

166 19 июля 2017, 18:31 166 22151

>>21361 (OP)

Господа, а хоть один человек в этом треде занимается вопросом оснований ПРОФЕССИОНАЛЬНО?

Сколько уже теорем доказали?
Или трёп сплошной?

Если есть хоть один - деанонься, публикацию свою покажи, будем на тебя ровняться.

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

Ответы2152

167 19 июля 2017, 18:48 167 22152

>>22151
Я ради стипухи взял одно недоказанное (оставим читателю в качестве упражнения) утверждение из маклейна и тиснул статью с его доказательством. Стипуху дали.

Ответы2153

168 19 июля 2017, 20:02 168 22153

>>22152
Погоди, а в какие журналы такую статью могли принять? А то я тут на хлебе и воде, а доказывать люблю.

Ответы21552159

169 19 июля 2017, 20:49 169 22155

>>22153
Вестник МухГУ.

170 19 июля 2017, 22:12 170 22159

>>22153
Как ты полюбил доказательства?

Ответы2177

171 20 июля 2017, 02:26 171 22169

>>22111
> Что в математике не сводится к алгоритмам
Десятая проблема Гильберта.

Ответы2170

172 20 июля 2017, 02:45 172 22170

>>22169
> Десятая проблема Гильберта.
Покажи как решить ее без алгоритмов.

Ответы217121722173

173 20 июля 2017, 02:52 173 22171

>>22170
Алгоритмами её точно не решить. Но это не значит, что без алгоритмов её решить нельзя. Ты же сам вроде должен быть против исключённого третьего?

Ответы2179

174 20 июля 2017, 03:12 174 22172

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

Ответы2179

175 20 июля 2017, 03:37 175 22173

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

Ответы2179

176 20 июля 2017, 07:58 176 22177

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

Ответы2186

177 20 июля 2017, 10:09 177 22179

>>22171
>Алгоритмами её точно не решить. Но это не значит, что без алгоритмов её решить нельзя.
Демагогия.
>>22172
Я уже просил не нести хуйни. Алгоритмически неразрешимые задачи никто не отменял.
>>22173
>Именно поиск закономерностей, обобщение и не сводится к алгоритмам, где математика, не являющаяся преобразованием знакосочетаний и термов по заданным правилам
И еще раз прошу не нести хуйни. То, что ты описал, называется идентификацией систем и реализуется очень большим количеством алгоритмов. Итого, ты не в теме абсолютно, а разжевывать такие азы мне неинтересно вообще никак.

Ответы21812189

178 20 июля 2017, 11:26 178 22181

>>22179
>Демагогия.
Разве?

Ответы2187

179 20 июля 2017, 12:08 179 22186

>>22177
Надо научиться играть в шахматы тогда хотя бы, дабы понять аналогию.

180 20 июля 2017, 12:36 180 22187

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

181 20 июля 2017, 13:00 181 22189

>>22179
>Демагогия.
Лол что? Ты пишешь , мол, раз алгоритмически задача неразрешима, то она неразрешима впринципе. Я говорю, что одно из другого не следует. Где тут демагогия?
>То, что ты описал, называется идентификацией систем и реализуется очень большим количеством алгоритмов
Например?
>Я уже просил не нести хуйни
>И еще раз прошу не нести хуйни.
>Итого, ты не в теме абсолютно, а разжевывать такие азы мне неинтересно вообще никак.
Демагогия.

Ответы21902191

182 20 июля 2017, 13:07 182 22190

>>22189
>Ты пишешь , мол, раз алгоритмически задача неразрешима, то она неразрешима впринципе. Я говорю, что одно из другого не следует. Где тут демагогия?
Давай так, пока не принесешь примера решения неалгоритмическими методами алгоритмически неразрешимой математической проблемы, можешь мне вообще не писать. У меня нет никакого желания даже пытаться объяснить человеку, не слышавшему про тезис Черча, из чего конкретно следует общая неразрешимость алгоритмически неразрешимых задач.

Ответы21932195

183 20 июля 2017, 13:12 183 22191

>>22189
>То, что ты описал, называется идентификацией систем
Ну и да, это не то, что я описал. Я о том, что, например, нет такого алгоритма, который бы, например, получая на вход последовательность чисел 2 5 12 27 58 121 ... мог бы найти закономерность, "догадаться", что это 2n-n или 2*предыдущее+номер. Разве такие алгоритмы есть? Человек же такую задачу может решить, потупив в последовательность минуту.

Ответы219321942197

184 20 июля 2017, 13:13 184 22193

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

185 20 июля 2017, 13:38 185 22194

>>22191
Ящитаю, что ты не догадался, а просто запомнил, может чуток обобщив.

Ответы2196

186 20 июля 2017, 13:43 186 22195

>>22190
> из чего конкретно следует
Нет, не следует. Перечитай, о чём он говорит.
>Алгоритмически неразрешимо
Или вот ещё пример. Нужно найти натуральные корни.
x5+2x3+3x2-60=0
По теореме Абеля — Руффини не существует формулы, алгоритма по которому можно найти корни этого уравнения, но подставив 2, догадавшись, мы получим решение. По твоему это уже не математика, а гадание на Аллахе?

Ответы2198

187 20 июля 2017, 13:46 187 22196

>>22194
>не догадался
Нет, вчера с корешем эксперимент проводили, он загадал вот эту последовательность и нужно было найти закономерность, правда мой ответ был, что это
a(n+1)=2a(n)+n, но не суть.
>обобщил
Вот это тоже, в математике это повсюду, а что это вообще? Как происходит обобщение? Как это алгоритмизировать?

188 20 июля 2017, 13:51 188 22197

>>22191
>Разве такие алгоритмы есть?
Деточка, дуй в школку, ну. Ты про идентификацию систем не слышал, зачем ты свою тупость используешь как доказательство чего-то? Это же настолько элементарная задача идентификации, что даже объяснять как ее решить алгоритмически, смешно. Простая регрессия на калькуляторе с этой задачей справится, достаточно расположить эти числа парами
> a = data.frame(
+ x = c(2,12,58),
+ y = c(5,27,121)
+ )
> a
x y
1 2 5
2 12 27
3 58 121
и применить регрессию:
> reg<-lm(y ~ x, data = a)
> new<-data.frame(x = c(121))
> predict(reg,newdata=new)
1
251.0897
Следующее значение твоего ряда 251. А вот теперь точно уебывай, потому что детский сад - это не тот уровень, на котором мне было бы интересно дискутировать.

Ответы219822222227

189 20 июля 2017, 13:56 189 22198

>>22195
>гадание на Аллахе
Как бы да, это и правда оно, как и доказательство от противного, ведь есть разница между построением объекта и доказательством того, что несуществование объекта противоречиво. Но решение ведь есть. И таких примеров использования Аллаха в математике сотни.
>>22197
Но следующее число 248, лол. Регрессия.

Ответы2201

190 20 июля 2017, 13:57 190 22199

Доказательство седьмой проблеммы Гилберта неконструктивно и использует не алгоритмические методы.

191 20 июля 2017, 13:59 191 22201

>>22198
Это простая линейная регрессия на датасете из 3х значений. Естественно, что это не самый лучший метод из существующих. Дело не в этом, а в том, что ты своеим неопниманием пытаешься что-то доказать. Буду репортить троллинг тупостью, в общем.

192 20 июля 2017, 14:24 192 22215

Почему актуальной бесконечности не существует?

Ответы2216

193 20 июля 2017, 14:26 193 22216

>>22215
Потому что ты дебил и она существует.
Пересчитай мне все числа между нулем и единицей. И когда я говорю все, я имю ввиду ВСЕ*

Ответы2217

194 20 июля 2017, 14:28 194 22217

>>22216
Зачем мне их пересчитовать? Как это докажет её существование?

Ответы2218

195 20 июля 2017, 14:31 195 22218

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

Ответы2219

196 20 июля 2017, 14:33 196 22219

>>22218
То есть актуальная бесконечность существует?

Ответы2229

197 20 июля 2017, 14:38 197 22222

>>22197
>>22212
Ну и да, там надо тогда уж
#R version 3.3.2
a <- data.frame(
x=1:6,
y=c(2,5,12,27,58,121)
)
a
reg<-lm(y ~ x, data = a)
new<-data.frame(x = c(7))
predict(reg,newdata=new)

x y
1 1 2
2 2 5
3 3 12
4 4 27
5 5 58
6 6 121
1
114.4

А у тебя вообще ерунда вышла. Так-то. Там x это номер члена потому что.

Ответы223022352237

198 20 июля 2017, 14:40 198 22227

>>22197
И скажи, конструктивизм всегда алгоритм предполагает разве? Построить значит предоставить алгоритм построения?

199 20 июля 2017, 14:41 199 22229

>>22219
Существует.

200 20 июля 2017, 14:54 200 22230

>>22222
Ты гет упустил, глупец.

201 20 июля 2017, 17:00 201 22235

>>22222
Ну и че ты сделал, сам-то понял? Там пары значений (х у), а у тебя х - просто последовательность натуральных чисел от 1 до 6

Ответы2241

202 20 июля 2017, 17:07 202 22237

>>22222
Короче, это же числовой ряд, из которого я сделал матрицу Ганкеля. Линейная регрессия недостаточно точно аппроксимирует такие нелинейные значения, да еше и датасет из 3х пар, но мой результат почти такой же как у этого шизика, а твой в 2 раза неправильный.

203 20 июля 2017, 18:11 203 22241

>>22235
>Там пары значений
Так y от x должно зависеть,а ты просто взял значения y и поделил их на две части, лол.
>х - просто последовательность натуральных чисел от 1 до 6
Ну правильно, y=2x-x,
> твой в 2 раза неправильный.
Да он и не должен быть правильным, как ты вообще умудрился применять линейную регрессию, когда очевидна эксп зависимость. То, что у тебя получилось "почти такой же" простое совпадение.

Ответы2242

204 20 июля 2017, 18:20 204 22242

>>22241
>То, что у тебя получилось "почти такой же" простое совпадение.
Это не совпадение, а аппроксимация. Точной она и не могла быть, т.к. зависимость нелинейная, а я использовал линейную регрессию + датасет никакой. Еще раз: из датасета была сделана матрица Ганкеля, что соответствует NARX-модели а потом линейной регрессией была проведена идентификация системы y = f(x). Регрессией т.о. была получена аппроксимация функции f, но т.к. в реальной системе эта функция нелинейна и датасет размером близок к 0, то вышла некоторая, согласись, довольно небольшая ошибочка для данных условий. Похоже, кроме меня про такое никто не слышал? Страшно вы живете, а.

Ответы2243

205 20 июля 2017, 18:27 205 22243

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

Ответы2244

206 20 июля 2017, 18:33 206 22244

>>22243
Линейная регрессия - не решение нелинейной проблемы. В остальном идентификация систем как раз для нахождения неизвестных зависимостей выходов от входов. Даже кусочно-линейная аппроксимация (скажем, моделью Такаги-Сугено) функции выхода от входа на таком датасете была бы точнее. Ну и про теоремы об универсальной аппроксимации тут тоже не слышали, эх, африка.

Ответы22452250

207 20 июля 2017, 18:43 207 22245

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

Ответы22472251

208 20 июля 2017, 18:45 208 22247

>>22245
>сделать можно
Иногда.

209 20 июля 2017, 18:48 209 22250

>>22244
Ну и применять линейную регрессию можно только в предположении линейности зависости. Иначе смысла в такой "аппроксимации" нет никакого.

Ответы2251

210 20 июля 2017, 18:52 210 22251

>>22245
>речь шла о том, как алгоритмически получить из данных точную формулу, породившую их. Неалгоритмически это сделать можно.
Во-первых, идентификацией системы это сделать можно. Конкретных примеров полно. Во-вторых, то, что ты называешь "неалгоритмически" на самом деле алгоритм.
>>22250
Я понял твой уровень знаний в этой теме, дальше меня на эту тему можешь не смешить.

Ответы2253

211 20 июля 2017, 18:56 211 22253

>>22251
>полно примеров
Хватит нести чушь и заниматься демагогией, примеров полно так неси хотя бы один.
> "неалгоритмически" на самом деле алгоритм
Ага, всё алгоритм, просто мы ещё не поняли этого. Сектант.
>уровень знаний
>в любой непонятной ситуации lm(y~x,data=a)

Ответы2254

212 20 июля 2017, 19:01 212 22254

>>22253
>примеров полно так неси хотя бы один.
Одна из многих монографий в тему http://b-ok.org/book/448591/9b866b Просвещаем темное африканской быдло, прямо на мейлру!

Ответы2255

213 20 июля 2017, 19:03 213 22255

>>22254
Берёшь и копипастишь оттуда сюда пример
> как алгоритмически получить из данных точную формулу, породившую их.
Я не собираюсь искать на тысяче страниц то, чего там нет.
>применяет демагогию
>называет кого-то быдлом
Пока быдло тут только ты.

214 20 июля 2017, 19:22 214 22265

>>21361 (OP)
Конструктивизм — computer science. Computer science не математика.

Ответы2272

215 20 июля 2017, 19:34 215 22272

>>22265
благодаря соответствию карри-говарда можно сказать, что математика — computer science.
>Computer science не математика
В таком случае математика не математика

Ответы2279

216 20 июля 2017, 19:39 216 22274

Спрошу тут,, вроде тред по теме :^)
Есть одно задание "доказать ¬(p ↔ ¬p) не используя исключённое третье"
Внизу код на lean с доказательством, но мне интересно - нет ли у меня лишних шагов и можно ли это доказать попроще?
Я не знаю насколько сильно lean отличается от более популярного coq, т.ч. на всякий случай некоторые пояснения: mp - выделяет левую импликацию из iff, mpr - соответственно, правую
implies.trans - естественно, транзитивность импликации
Всё остальное думаю в приведённом фрагменте по идее должно быть понятно

lemma both_implies_and {p q₁ q₂ : Prop} : (p → q₁) → (p → q₂) → p → q₁ ∧ q₂ :=
λ h₁ h₂ hp, and.intro (h₁ hp) (h₂ hp)

lemma and_with_not_self {p : Prop} : ¬(¬p ∧ p) := flip and.elim id

lemma T₁ {p : Prop} : ¬(p ↔ ¬p) :=
assume h : p ↔ ¬p,
let hff : p → ¬p ∧ p := both_implies_and h.mp (h.mpr ∘ h.mp),
hnp : ¬p := implies.trans hff and_with_not_self
in hnp (h.mpr hnp)

Ответы2291

217 20 июля 2017, 19:44 217 22279

>>22272
http://www.scott-a-s.com/cs-is-not-math/

218 20 июля 2017, 20:03 218 22283

>>22282

мимокрок: Давайте переведём разговор в конструктивное русло.
Мне кажется, что Lean - это продукт без бущущего, поддерживаемый исключительно Майкрософтовским пиаром.

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

Ответы2285

219 20 июля 2017, 20:18 219 22285

>>22283
Лично я учу lean, потому что в его изучение проще заход, он написан на плюсах которые, в отличие от окамла, я знаю и кодобаза достаточно компактна и организована чтобы лазить по исходникам когда хочется понять как всё устроено, плюс мне неважна дропнутая поддержка HoTT
А будущее его лично мне пофигу

Ответы229923022305

220 20 июля 2017, 22:47 220 22291

>>22274
додумался до менее ебанутого решения
lemma Ex₂ {p : Prop} : ¬(p ↔ ¬p) :=
λ (h : p ↔ p → false),
let hp := h.mpr (λ hpₗ, h.mp hpₗ hpₗ)
in h.mp hp hp
всем спасибо

221 21 июля 2017, 14:00 221 22299

>>22285
Справедливое утверждение. Написание на С существенно облегчает понимание. Вы всё правильно делаете, я в ближайшие пару месяцев тоже вкачусь.

Ответы2302

222 21 июля 2017, 15:00 222 22302

>>22299
>>22285
Поясните, как код прувера на крестах облегчает понимание лямбда-калькулюса, исчисления конструкций и т.д? Ведь для этого достаточно кода на том же коке или лине + понимания самих формализмов.

Ответы2305

223 21 июля 2017, 15:16 223 22305

>>22302
я (>>22285) по сорцам собирался лазить не чтобы т.о. учить лямба-калькулюс и CoC а чисто из программерского интереса как оно написано, ну и плюс в лине наличествуют тактики частично/полностью на плюсах - можно будет разбираться как они работают.

224 23 июля 2017, 13:12 224 22354

Чет нашел какой-то вероятностный метод и википедия дает прямо в определении, что это неконструктивный метод доказательства. И че?

225 27 июля 2017, 02:24 225 22481

А конструктивная математика и конечная математика — это одно и тоже?

Ответы248424932496

226 27 июля 2017, 07:50 226 22484

>>22481
Нет.

227 27 июля 2017, 12:44 227 22493

>>22481
Конструктивная математика - это конченная математика.

228 27 июля 2017, 15:58 228 22496

>>22481
А как это проверить?

Ответы2501

229 27 июля 2017, 19:02 229 22501

>>22496
Очевидно с помощью Сuсk.

552 Кб, 770x522
230 28 июля 2017, 09:36 230 22514

Пони маете, ваша проблема в том, что вы не видите полной картины. Вы даже внятно не сможете объяснить зачем вообще нужны основания и аксиоматика и для чего там исчисление предикатов, например. С конструктивными основаниями в этом смысле все для вас еще хуже, все эти изоморфизмы карри'говарда, ВНК интерпретации, вычислимость, суждения, натуральная дедукция итд итп сами по себе требуют неких усилий для понимания, но еще хуже, что даже если отдаленное понимание присутствует, то все эти вещи не складываются в целую картинку, тому що мозгов у вас як у хлебушка где все естественно вытекает одно из другого, как итог, конструктивная математика, а уж тем более MLTT для вас выглядит как какая'то лютая оккультная ебулда, бессмысленная и беспощадная, хотя по факту все там просто и понятно.

Ответы251636014459

231 28 июля 2017, 09:52 231 22516

>>22514
>все эти изоморфизмы карри'говарда, ВНК интерпретации, вычислимость, суждения, натуральная дедукция итд итп сами по себе требуют неких усилий для понимания
Только если ты совсем отбитый.

232 29 июля 2017, 04:38 232 22550

А вещественные числа существуют?

Ответы25544460

233 29 июля 2017, 09:47 233 22554

>>22550
Нет, кончено! Раз их нельзя запрограмировать на компуктере, то не существует!

Ответы2555

234 29 июля 2017, 10:01 234 22555

>>22554
Запрограммировать то можно, но я в любом случае сомневаюсь в их существовании.

235 30 июля 2017, 16:53 235 22586

Дяденьки, научите меня евклидовой геометрии.

Ответы2602

236 30 июля 2017, 21:23 236 22602

>>22586
http://gen.lib.rus.ec/book/index.php?md5=8B5E381A16C8DA0C96C60B0F666CA20E

1,7 Мб, webm,
450x360, 0:18
237 8 авг 2017, 11:25 237 22889

>>21361 (OP)
Конструктивисто-петух опять разгулялся. Не видел его с 2012-го года - с тредов про китайца.

Ответы2902

238 8 авг 2017, 15:04 238 22902

>>22889
>с 2012-го года
Про что несет. Я про интуиционизм и конструктивную математику узнал в августе 2016го.

Ответы29032912

239 8 авг 2017, 15:12 239 22903

>>22902
Как ты про неё узнал?

Ответы2904

240 8 авг 2017, 15:33 240 22904

>>22903
Прочитал у Максимки статью про MLTT, заинтересовало, почитал Мартин-Лёфа и с удивлением обнаружил, что нихуя не понимаю, о чем вообще речь, хотя изложено стройно и логично. Более пристально взглянув на эту тему, понял что причина в том, что за MLTT стоит нечто мне неведомое, из принципов чего и исходит Мартин-Лёф. Это и оказалось конструктивной математикой. Ну а там на каком-то этапе нагуглил Брауэра и понеслось.

241 8 авг 2017, 17:06 241 22910

Отрицание бесконечности и конструктивный подход гут. Отрицание закона исключённого третьего бэд. Есть ли где-то система оснований с первым без второго?

Ответы291129164461

242 8 авг 2017, 17:10 242 22911

>>22910
>Отрицание бесконечности
>Отрицание закона исключённого третьего бэд.
О какой системе идёт речь?

Ответы2913

243 8 авг 2017, 17:15 243 22912

>>22902
Вернее 2013-го.
http://arhivach.org/thread/5822/
Он здесь уже забивал последний гвоздь в крышку гроба формализма. Потом последовала череда подобных тредов, навроде теперешних, а затем он пропал.

244 8 авг 2017, 17:17 244 22913

>>22911
В плане из второго следует первое?Или наоборот?

Ответы2915

245 8 авг 2017, 17:21 245 22915

>>22913
Не знаю конструктивных оснований в которых отрицается исключённое третье. Недоказуемость и отрицание это разные вещи.
¬¬(P ∨ ¬ P) теорема в большинстве "видов" конструктивной математики.

212 Кб, 400x321
246 8 авг 2017, 17:22 246 22916

>>22910
Ультрафинитизм Пахома Есенина-Вольпина ж. Поскольку все там конечно, исключенное третье доказывается напрямую простым перебором.

Ответы29172963

247 8 авг 2017, 17:25 247 22917

>>22916
>>22916
>Ультрафинитизм
> все там конечно
>исключенное третье доказывается напрямую простым перебором.
Во, вот это. Спасибо.

248 8 авг 2017, 21:25 248 22925

Сделайте что-то вроде "конструктивизм и конструктивные доказательства интерактивно и в
картинках для школьников".

Ответы29262970

249 8 авг 2017, 21:44 249 22926

>>22925
Зачем для школьников, если скоро людям в математике вообще места не будет? Сделают поисковик по доказанным компом теоремам, только нужно будет научиться запросы правильные формировать и вся "человеческая" математика будет прикладной.

Ответы2957

250 9 авг 2017, 19:52 250 22957

>>22926
Скоро очень скоро
youtu.be/ZxrP3MA2Iwo?t=29

251 9 авг 2017, 21:16 251 22963

>>22916
Хотите смешную шутку? Приготовились? В ультрафинитизме все конечные! Ахаха!

252 10 авг 2017, 11:42 252 22970

>>22925
>"конструктивизм и конструктивные доказательства интерактивно и в картинках для школьников"
Для школьников смысла нет, в картинках тем более. Если не лезть в философскую сторону вопроса, во что тут все равно никто не может, то самый простой путь - осваивать кок. Возможно, самый простой учебник по коку - software foundations Пирса https://softwarefoundations.cis.upenn.edu/current/index.html

Ответы2988

253 11 авг 2017, 01:05 253 22988

>>22970
Agda получше будет, разве нет? Тем более для начинающего.

Ответы2995

254 11 авг 2017, 10:33 254 22995

>>22988
Чем получше? Там с одной установкой пердолинга не оберешься https://hackage.haskell.org/package/Agda-2.5.2/readme + я не знаю внятных IDE под нее, емакс тот еще аутизм от аутистов для аутистов, как ни крути. Кок хотя бы в установке и использовании не сложнее блокнота.

255 17 авг 2017, 23:33 255 23435

Конструктивист - это умственно отсталый человек, для которого из истинности А не следует ложность не-А. О чём вы тут спорите с умственно отсталыми 4 треда подряд?

Ответы3436

256 17 авг 2017, 23:42 256 23436

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

Ответы3451

257 18 авг 2017, 01:20 257 23451

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

Ответы3452

258 18 авг 2017, 01:30 258 23452

>>23451
>но даунам не достаточно доказательства того что А - истинна для того чтобы убедится что не-А - ложь
Что ты несёшь, ебанутый?
P => ¬¬P теорема даже в минимальной логике.
>как будто бывает третье состояние когда А и истинна и ложь одновременно блять
¬¬(P ∨ ¬P) теорема в конструктивной логике.

Ответы3453

259 18 авг 2017, 01:48 259 23453

>>23452
>состояние когда А и истинна и ложь одновременно блять
Я тебя не так прочитал, ты оказывается ещё более тупой чем я думал.
Это ничего общего с исключённым третьим не имеет, ¬ (P ∧ ¬ P) спокойно доказывается в конструктивных основаниях.

260 18 авг 2017, 16:51 260 23498

Как искать в поисковике теорем?

261 19 авг 2017, 12:01 261 23515

Шел уже десятый тред, если считать со /сци, а кое-кто так до сих пор и не понял, что конструктивное доказательство - это построение, а построение - это конструктивное доказательство. И кроме как их построений конструктивным доказательствам взяться неоткуда, а в особенности из каких-то априорных аксиом, в которые нужно веровать вместо собственно процесса построения или задания правил для построения, если уж касаться потенциальной осуществимости или lazy evaluation. Как так могло случиться, что в 21 веке кому-то греет попу необъодимость непосредственно доказать хотя бы один дизъюнкт для доказательства истинности дизъюнкции? Откуда такие хуйлопаны вообще берутся? Я не понимаю.

Ответы35163518

262 19 авг 2017, 12:06 262 23516

>>23515
О чём ты? Не понимаю твой пост, извини.

263 19 авг 2017, 13:10 263 23518

>>23515
Я вот понял, например. Меня больше интересует вопрос удобства реального использования. С этим, как я понимаю, пока довольно печально.

Ответы35193529

82 Кб, 720x990
264 19 авг 2017, 13:26 264 23519

>>23518
>интересует вопрос удобства реального использования. С этим, как я понимаю, пока довольно печально.
Потому что у большинства "врети" случилось еще во времена работ Поста, Тьюринга и Черча, который все это подытожил, написав, что найдены границы математических способностей человека. Хотя так и оказалось, и выше вычислимости все равно не прыгнешь, верунов и сейчас полно. Благо, прогресс не стоит на месте, и хотя реальной математикой занимаются единицы типа Мартин-Лёфа и Воеводского, уже сейчас видно, что все идет к полной автоматизации математики.

Ответы352035303533

265 19 авг 2017, 13:30 265 23520

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

Ответы3521

266 19 авг 2017, 13:32 266 23521

>>23520
>восьмидесятых тоже все бодренько так шло к полной автоматизации вообще любой интеллектуальной деятельности - чем все закончилось мы знаем.
Ты о чем?

Ответы3522

267 19 авг 2017, 13:34 267 23522

>>23521
Ээ... AI Winter, все дела?

Ответы3523

268 19 авг 2017, 13:37 268 23523

>>23522
Для этого даже сейчас техническое развитие никакое, какие уж тут 80-е.

269 19 авг 2017, 15:20 269 23529

>>23518
>реального использования
Реального использования чего?

270 19 авг 2017, 15:21 270 23530

>>23519
Что ты подразумеваешь под "верунами"?

Ответы3531

271 19 авг 2017, 15:29 271 23531

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

Ответы3533

272 19 авг 2017, 15:56 272 23533

>>23519
>который все это подытожил, написав, что найдены границы математических способностей человека.
Заскринил твой пост. Это пиздец.

>>23531
Это не математика, а комьютер саенс, и к математике отношение не имеет. Ты даже того же Энгелькинга не осилил. Прямо пропаганда Рыбников стайл.

Ответы35343535

273 19 авг 2017, 16:05 273 23534

>>23533
>к математике отношение не имеет
Почему подмножество математики не имеет отношения к математике?

274 19 авг 2017, 16:06 274 23535

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

Ответы35363537

275 19 авг 2017, 16:13 275 23536

>>23535
Никто не спорит с Чёрчем и Тьюрингом. Чёрч и Тьюринг не сводили всю математику к вычислимости.

276 19 авг 2017, 16:14 276 23537

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

Ответы35383539

277 19 авг 2017, 16:14 277 23538

>>23537
*чем
-быстрофикс

278 19 авг 2017, 16:18 278 23539

>>23537
Ты никак не сможешь воспользоваться тем, что несчетно. Но ты всегда можешь написать значок бесконечности, алеф0,1,...,1488 и т.д. и думать, что пользуешься. Хотя по факту пользуешься значками, не несущими в себе ничего, т.к. содержимое, которое за ними предполагается, нельзя ни во что вычислить. Это и есть религия натуральная, поскольку у них там тоже есть значки, символ Аллаха, например. Суть примерно одна.

Ответы35403560

279 19 авг 2017, 16:20 279 23540

>>23539
>Ты никак не сможешь воспользоваться тем, что несчетно
А как же действительные числа?

Ответы35413543

280 19 авг 2017, 16:21 280 23541

>>23540
Все существующие вычислимы, их множество счётно.

Ответы3542

281 19 авг 2017, 16:22 281 23542

>>23541
>их множество счётно
Множество действительных чисел?

Ответы3545

282 19 авг 2017, 16:24 282 23543

>>23540
Опять сотый раз по кругу обсуждать одно и то же не вижу смысла. Вещественные числа обсуждали, более того, Тьюринг в своей работе "On computable numbers" машину Тьюринга представлял как имитацию действий человека, вычисляющего такие числа. Отсюда проблема останова, бла-бла и т.д., что уже сто раз обсуждалось.

Ответы3544

283 19 авг 2017, 16:25 283 23544

>>23543
По твоему множество действительных чисел счётно?

Ответы3548

284 19 авг 2017, 16:25 284 23545

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

Ответы3546

285 19 авг 2017, 16:25 285 23546

>>23545
А есть несуществующие действительные числа?

Ответы3547

286 19 авг 2017, 16:25 286 23547

>>23546
>есть несуществующие
Хм...

287 19 авг 2017, 16:25 287 23548

>>23544
Я уже сто раз говорил, что нет. Нет, нет, оно несчетно, т.к. это мощность континуума, а еще Брауэр показал, почему континуум невычислим. Итд итп.. Скушно, короче.

Ответы35493552

288 19 авг 2017, 16:26 288 23549

>>23548
>нет, оно несчетно
>Ты никак не сможешь воспользоваться тем, что несчетно
А как же действительные числа?

Ответы3550

289 19 авг 2017, 16:27 289 23550

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

Ответы35513553

290 19 авг 2017, 16:28 290 23551

>>23550
Я пользуюсь не числом, а R, множеством действительных чисел.

Ответы3558

291 19 авг 2017, 16:28 291 23552

>>23548
Я тут недавно читаю это треды. Похоже, что они реально ебанутые или необучаемые.

292 19 авг 2017, 16:29 292 23553

>>23550
> числом с конечным количеством знаков после запятой
Это не число, а приближение числа.

Ответы35543555

293 19 авг 2017, 16:31 293 23554

>>23553
МИМО. ЛОЛШТО?

Ответы3556

294 19 авг 2017, 16:32 294 23555

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

Ответы3557

295 19 авг 2017, 16:32 295 23556

>>23554
pi,e например. Вычислены только до какого-то знака, приблизительно значит.

296 19 авг 2017, 16:33 296 23557

>>23555
Только когда нам нужно вычислить результат. Мы вполне можем работать с тем же pi или e чисто алгебраически. И это уже будет точное значение.

Ответы3561

297 19 авг 2017, 16:34 297 23558

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

Ответы35593560

298 19 авг 2017, 16:35 298 23559

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

Ответы3561

299 19 авг 2017, 16:36 299 23560

>>23539
>Ты никак не сможешь воспользоваться тем, что несчетно.
А скрины с Энгелькинга? Раз ими никто не пользуется, то почему практически в каждом учебнике анализа вводят множество R, мощность которого больше, чем Q.
>Это и есть религия натуральная, поскольку у них там тоже есть значки, символ Аллаха, например. Суть примерно одна.
Вопрос в том, что считать существующим. Почему, если множества вещественных чисел счетно, об этом не говорят в тех же учебниках матана, но вводят в заблуждение, говоря, что есть и другие мощности?

>>23558
И в чем проблема в бесконечном процессе вычисления?

Ответы3564

300 19 авг 2017, 16:37 300 23561

>>23557
>Только когда нам нужно вычислить результат
Естественно. Когда результат не нужон, можно и Аллахов подсчитывать.
>>23559
>Пользоваться одним экономнее.
Вот только это не пользование, а вера в пользование. Потому что настоящее пользование - это вычисление. И опять же, все это я уже не помню сколько раз писал.

Ответы35623563

301 19 авг 2017, 16:37 301 23562

>>23561
Что плохого в вере в пользование?

Ответы3564

302 19 авг 2017, 16:38 302 23563

>>23561
>Потому что настоящее пользование - это вычисление
ТЫСКОЗАЛ? Вот это как раз сектанство. Напиши ты pi или 3,141592653589793238462643 что принципиально поменяется?

Ответы35653567

303 19 авг 2017, 16:39 303 23564

>>23560
>И в чем проблема в бесконечном процессе вычисления?
В том, что оно не закончится никогда и сл-но, не может считаться вычислимостью.
>>23562
>Что плохого в вере в пользование?
В вере нет ничего плохого, веруй на здоровье. Вот только математикой свою веру называть не нужно.

Ответы356635683569357135733578

304 19 авг 2017, 16:39 304 23565

>>23563
Причём заметь первое абсолютно точное значение, а второе лишь аппроксимация.

305 19 авг 2017, 16:39 305 23566

>>23564
>В том, что оно не закончится никогда и сл-но, не может считаться вычислимостью.
А оно должно закончится?

306 19 авг 2017, 16:40 306 23567

>>23563
>Напиши ты pi или 3,141592653589793238462643 что принципиально поменяется?
Сто раз писал, что. Даже в этом треде. Вы ж читать не умеете, какая вам математика.

Ответы3570

307 19 авг 2017, 16:40 307 23568

>>23564
>В том, что оно не закончится никогда
Ну например с рациональными числами там всегда будет период, да, будет повторяться бесконечно, но детерминированно, что плохого то?

308 19 авг 2017, 16:40 308 23569

>>23564
Я сам не уверен что верую, просто интересуюсь.

309 19 авг 2017, 16:40 309 23570

>>23567
Я по твоему должен все твои посты перечитывать?

310 19 авг 2017, 16:41 310 23571

>>23564
>Вот только математикой свою веру называть не нужно.
Как её называть тогда?

Ответы3572

311 19 авг 2017, 16:42 311 23572

>>23571
Веру? Верой и называй, очевидно же.

Ответы3574

312 19 авг 2017, 16:42 312 23573

>>23564
Вот только не надо свою веру в калькуляторы называть математикой.

Ответы3575

313 19 авг 2017, 16:42 313 23574

>>23572
Нужно более подробное название, вера разная бывает.

Ответы3576

314 19 авг 2017, 16:43 314 23575

>>23573
Вычислимость - это вычислимость, а не вера. Вычислимое можно вычислить, в невычислимое можно только веровать.

Ответы3579

315 19 авг 2017, 16:44 315 23576

>>23574
"Математикопоклонничество" пусть будет. Поклоняетесь значкам без фактического содержания.

Ответы357735813585

316 19 авг 2017, 16:45 316 23577

>>23576
>"Математикопоклонничество" пусть будет.
Слишком длинно.

317 19 авг 2017, 16:46 317 23578

>>23564
Какие разделы математики ты считаешь верой в Аллаха?

Ответы3580

318 19 авг 2017, 16:46 318 23579

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

319 19 авг 2017, 16:47 319 23580

>>23578
Неконструктивные основания. Просто концентрированная вера.

Ответы35823583

320 19 авг 2017, 16:47 320 23581

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

Ответы3584

321 19 авг 2017, 16:47 321 23582

>>23580
99% математики - вера?

Ответы3583

322 19 авг 2017, 16:48 322 23583

>>23580
То есть любая математика невозможная в конструктивных основаниях?
>>23582
Далеко не 99%.

323 19 авг 2017, 16:49 323 23584

>>23581
Пример с вещественными числами разобрали буквально десяток постов назад. У тебя ж память как у хлебушка.

Ответы3587

324 19 авг 2017, 16:49 324 23585

>>23576
Ты так и не ответил на вопрос
>Ты никак не сможешь воспользоваться тем, что несчетно.
>А скрины с Энгелькинга? Раз ими никто не пользуется, то почему практически в каждом учебнике анализа вводят множество R, мощность которого больше, чем Q.

Ответы3586

325 19 авг 2017, 16:50 325 23586

>>23585
Ответил.

Ответы35883590

326 19 авг 2017, 16:50 326 23587

>>23584
Причём тут вещественные числа? Я про вычисления в целом.

Ответы3589

327 19 авг 2017, 16:50 327 23588

>>23586
В своём манямирке?

Ответы3589

328 19 авг 2017, 16:51 328 23589

>>23587
>Я про вычисления в целом.
Вот в том и проблема. Стоит разобрать любой конкретный пример и видно все содержание твоего "целого".
>>23588
В этом треде пару раз.

Ответы35913592

329 19 авг 2017, 16:51 329 23590

>>23586
>Ты никак не сможешь воспользоваться тем, что несчетно.
Все пользуются, как же так? Еретики?

Ответы3593

330 19 авг 2017, 16:52 330 23591

>>23589
>В этом треде пару раз.
Номер поста?

331 19 авг 2017, 16:53 331 23592

>>23589
>Вот в том и проблема
В чём? Ты будешь спорить, что вычисления это правила перемалывания значков?

Ответы3595

332 19 авг 2017, 16:53 332 23593

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

Ответы3594

333 19 авг 2017, 16:53 333 23594

>>23593
Так ты ещё и /по/рашник, лол. Ну так давай ссылку или проследуй нахуй. Нихуя ты не ответил, я следил, спустил на тормозах свой обосрамс, думая, что никто не заметит.

334 19 авг 2017, 16:53 334 23595

>>23592
Не все значки одинаково полезны, опять же, разница обсуждалась.

Ответы3596

335 19 авг 2017, 16:54 335 23596

>>23595
Вера в полезность достаточный критерий для тебя?

Ответы3597

336 19 авг 2017, 16:56 336 23597

>>23596
Сто раз писалось про канонические и неканонические элементы и выражения и т.д. Мне реально лениво каждую сотню постов переписывать все, мною уже сто раз писанное. Ну необучаемые вы тута, бывает. Для мейлру это норма, как и для рашки в целом.

Ответы35983599

337 19 авг 2017, 16:57 337 23598

>>23597
>Сто раз писалось
>не может скопипастить
Просто пукнул в лужу, ясно.

338 19 авг 2017, 16:57 338 23599

>>23597
Ты можешь один раз написать, заскринить, а после кидать скрины со своим ответом. Ты просто тупой и троллишь тупостью.

Ответы3600

339 19 авг 2017, 16:58 339 23600

>>23599
Одно из двух. Третьего не дано
>Ты просто тупой и троллишь тупостью.

Ответы36023614

340 19 авг 2017, 16:59 340 23601

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

Ответы3604

341 19 авг 2017, 17:00 341 23602

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

Ответы3605

342 19 авг 2017, 17:00 342 23604

>>23601
Просто тут 3.5 математика на всю борду, да и те на первом курсе мухгу обучаются.

343 19 авг 2017, 17:00 343 23605

>>23602
Нет, осознанно. Если неосознанно, значит просто тупой. Третьего не дано. Нельзя быть тупым и троллить тупостью одновременно.

Ответы3606

344 19 авг 2017, 17:01 344 23606

>>23605
Как скажешь.

Ответы3607

345 19 авг 2017, 17:02 345 23607

>>23606
Лол.

346 19 авг 2017, 17:57 346 23614

>>23600
>Третьего не дано
А если в моих основаниях дано?

Ответы3617

347 19 авг 2017, 18:23 347 23615

Какие есть основания где можно доказать, что аксиома Аллаха (выбора) не верна?

348 19 авг 2017, 19:06 348 23617

>>23614
Тогда у тебя нет оснований для беспокойства.

213 Кб, 691x414
349 20 авг 2017, 11:31 349 23628

Ответы3629

350 20 авг 2017, 11:51 350 23629

>>23628
Рамануджан очень кстати. Заниматься математикой без математического образования и культуры, не имея понятия о формализме как о методе вообще, можно только одним способом - манипуляцией с ментальными построениями.

Ответы3637

351 20 авг 2017, 23:10 351 23637

>>23629
Есть книжка, мол, как стать как Сринивас из позиций конструктивной математики? Да и вообще "конструктивная математика и психология", "конструктивная математика и сознание", "конструктивная математика и эмоции" да прочее?

Ответы37134463

352 22 авг 2017, 01:03 352 23706

>>21361 (OP)
Слышал про HoTT, разобрался в нём. Он, вроде какой-то в прямом смысле недоделанный.
В чём его проблема? (Пишите смело факты)
Вроде есть какая-то недоказанная гипотеза. Что она за зверь?

Ответы37123713

353 22 авг 2017, 09:02 353 23712

>>23706
>Voevodsky's model is non-constructive since it uses in a substantial way the axiom of choice.
>The problem of finding a constructive way of interpreting the rules of the Martin-Lof type theory that in addition satisfies the univalence axiom and canonicity for natural numbers remains open.
>Computational interpretation of homotopy type theory is an open problem.

Ответы3730

354 22 авг 2017, 12:10 354 23713

>>23637
>как стать как Сринивас
Он же с детства свои умения развивал. Вся его жизнь как одно доказательство тезиса Черча. А вообще, http://gen.lib.rus.ec/book/index.php?md5=74ED3244789E3A66301750212342D470 1ая глава.
>>23706
> HoTT,
Я в ней не разбирался, как по мне - какая-то странная надстройка над MLTT.

355 22 авг 2017, 21:25 355 23730

>>23712
Ух, прояснил, спасибо.

Единственное, что непонятно : "Computational interpretation of homotopy type theory is an open problem."

Что это такое, "вычислительная интерпретация"?
Есть более простые примеры, показывающие суть понятия?

Ответы3731

356 22 авг 2017, 21:45 356 23731

>>23730
>Единственное, что непонятно : "Computational interpretation of homotopy type theory is an open problem." Что это такое, "вычислительная интерпретация"?
Ну так все ж треды об этом. Суть конструктивной математики в том, что она вычислима. Что-то у них с этими гомотопиями пока не вычисляется, причем там жи и написано, что именно:
>Voevodsky's model is non-constructive since it uses in a substantial way the axiom of choice.
Полностью конструктивной модели пока нет.
>Есть более простые примеры, показывающие суть понятия?
Машина Тьюринга.

Ответы3928

357 27 авг 2017, 21:21 357 23928

>>23731
А где конкретно в тексте аксиома выбора существенно используется? Про это что-нибудь знаете?

Ответы3983

358 28 авг 2017, 20:09 358 23979

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

Ответы3983

359 28 авг 2017, 20:37 359 23983

>>23928
Конкретнее не знаю, я НоТТ не читал.
>>23979
Барендрехт, не? http://ttic.uchicago.edu/~dreyer/course/papers/barendregt.pdf

Ответы4019

360 30 авг 2017, 12:26 360 24019

>>23983
очень годное чтиво, спасибо.

мимоанон

361 30 авг 2017, 17:19 361 24026

Аноны, поясните за вычислимость утверждений формальной теории. Вот есть некая аксиоматическая теория и есть некое утверждение. Можно ли вычислить истино оно или ложно?

Ответы4054

362 30 авг 2017, 22:05 362 24037

Но ведь проект компьютеров пятого поколения не удался.

23 Кб, 712x254
363 31 авг 2017, 13:17 363 24054

>>24026
Ты путаешь вычислимость и выводимость в формальной системе. Второе вообще никак не подразумевает первого. Возьмем например истинность формулы в исчислении пропозишенов. Поскольку классически, по закону исключенного третьего, пропозишен может быть истинный или ложный, то мы можем по методу Тарского нарисовать Аллаха таблицу с этой формулой пикрелейтед, из которой выводима ложность или истинность этой формулы исходя из ложности или истинности входящих в нее пропозишенов. В данном примере, классически эта формула истинна в любом случае. Прикол же в том, что конструктивно (исходя из интерпретации логических констант, в частности, свойств импликации, по Гейтингу) эта формула (известная как формула Пирса) невычислима.

Ответы40554077

364 31 авг 2017, 14:40 364 24055

>>24054
Вы ничего не понимаете в выводимости. Она не связана с интерпретацией.

Ответы4057

365 31 авг 2017, 16:54 365 24057

>>24055
Читать не умеем? Я не утверждал, что выводимость связана с интерпретацией.

Ответы4062

366 31 авг 2017, 18:38 366 24062

>>24057
Формула F выводима, если существует хотя бы одна конечная последовательность формул, в которой последняя формула - это F, а любая предшествующая формула есть либо аксиома, либо получается применением модус поненс. Понятие "выводимость" не зависит от понятий "истинно" и "ложно".

Ответы4066

367 31 авг 2017, 19:20 367 24066

>>24062
Ну и? Из выводимости формулы никак не следует ее вычислимость, пример я привел - это формула Пирса.

Ответы4068

368 31 авг 2017, 19:52 368 24068

>>24066
В огороде бузина, а в Киеве дядька. Ты зачем таблицу истинности нарисовал?

Ответы4071

369 31 авг 2017, 20:13 369 24071

>>24068
А ты пост почитай, там написано.

Ответы4075

370 31 авг 2017, 20:36 370 24075

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

371 31 авг 2017, 21:07 371 24077

>>24054
А вот вы тоже напутали: формула Пирса невыводима в интуиционисткой логике, поскольку существует модель Крипке, где она не истинна.

Вычислимость функции - это про другое: существует такая машина Тьюринга, которая по заданным аргументам некоторой функции за конечное число ходов предъявит значение этой функции.

Так вот иногда доказательством импликации A->B является вычислимая функция f:A-->B, преобразующая доказательство утверждения А в доказательство утверждения B.

В силу неизвестных мне чудес(т.е. изоморфизму Карри-Ховарда) оказалось, что всё, что выведено из интуиционистских аксиом - может быть собрано из таких вычислимых функций.

То есть уже не надо заново строить машины Тьюринга - просто бери и пользуйся интуиционисткой логикой как конструктором. Оттуда и "конструктивизм", он же - "интуиционизм".

Невычислимо же - доказательство формулы Пирса, если его воспринимать как функцию.

---------------

Я это всё написал, но мне хотелось бы дополнительного контроля - всё же верно я рассказал?

Ответы4083

372 31 авг 2017, 21:37 372 24083

>>24077
>Так вот иногда доказательством импликации A->B является вычислимая функция f:A-->B, преобразующая доказательство утверждения А в доказательство утверждения B.
И именно в таких случаях мы можем говорить об истинности в конструктивном смысле слова. Поскольку суть конструктивной выводимости - вычислимость. А не общие недоказуемые заявления.
>В силу неизвестных мне чудес(т.е. изоморфизму Карри-Ховарда) оказалось, что всё, что выведено из интуиционистских аксиом - может быть собрано из таких вычислимых функций.
Интерпретация логических констант по Брауэру-Гейтингу-Колмогорову это называется. Конкретно чаще всего речь о конструктивной логике Гейтинга.

Ответы4086

373 31 авг 2017, 22:08 373 24086

>>24083
Окей, мы согласны.

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

Зачем нам тогда вычислимый вариант?

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

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

Это похоже на мечты, которые разрушил Гёдель, только в новой обложке.

как вам такой вброс?

Ответы4087

55 Кб, 707x919
374 31 авг 2017, 22:19 374 24087

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

Ответы40904115

375 31 авг 2017, 23:34 375 24090

>>24087
>это вычислимость, как ни крути
веруны неисправимы.

Ответы4120

376 1 сен 2017, 00:58 376 24115

>>24087
>Границы математических способностей хоть человека хоть роботов - это вычислимость
Эта фраза лишена смысла. Не отличается от фразы "направление лингвистических одаренностей арийцев - это гладиолус".

Ответы41184119

377 1 сен 2017, 06:14 377 24118

>>24115
Нет.

Ответы4155

378 1 сен 2017, 11:20 378 24119

>>24115
Давай я тебе объясгю, почему это не так. Вот ты написал в своем посте то, что написал. Но почему ты так написал? Потому что тебе свербит, и обязательно нужно что-то мне ответить? Или потому что ты можешь доказать эти свои слова, например, конкретным примером, начисто опровергающим тезис Черча тут стоит заметить, что сама эта фраза принадлежит как раз Черчу? Я уверен, что опровергнуть тезис Черча ты не можешь, это если предположить, что его опровержение вообще возможно, хотя в настоящее время человечеству ничего такого неизвестно. Тогда о чем твоя батрушка вообще? Не пони маю.

Ответы4155

379 1 сен 2017, 11:23 379 24120

>>24090
>веруны
Во что веруны-то? Вычислимость - это непосредственный конструктивный объект, а не объект веры как всякие не считающиеся ни во что значки алефов и бесконечностей.

Ответы4123

380 1 сен 2017, 12:51 380 24123

>>24120
Будь добр, приведи пример "конструктивного объекта". А то непонятно, что ты под этим подразумеваешь. (Объекты какие-то... Функция - понятно что такое, а объект - уже непонятно)

Ответы4124

381 1 сен 2017, 12:58 381 24124

>>24123
>приведи пример "конструктивного объекта"
Да я уже и не помню сколько раз приводил. Толку все равно 0.
>Функция - понятно что такое, а объект - уже непонятно)
И что по-твоему есть функция?

Ответы41264128

382 1 сен 2017, 13:49 382 24125

Ещё раз, какую пользу работающему математику проиносит отказ от
1) исключённого третьего,
2) аксиомы выбора.

383 1 сен 2017, 13:54 383 24126

>>24124

Определение функции:
(F:A-->B) <-> ( ( F is subset of A x B ) and ( forall a in A there exist exatly one b in B such that (a,b) in F ) )

384 1 сен 2017, 13:55 384 24127

*exactly

385 1 сен 2017, 14:14 385 24128

>>24124
я понимаю твою усталость, но всё-таки интересно об этом поговорить

386 1 сен 2017, 23:30 386 24155

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

Ответы4173

387 2 сен 2017, 11:33 387 24173

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

388 7 сен 2017, 23:08 388 24424

>>21361 (OP)
Вычислимость - это действительно очень интересная тема.

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

Если предлагать тему, то вопрос:"чем надозаниматься?" Где открыт фронт работ, доступный для студентоты с двачей?

Ответы4448

389 8 сен 2017, 13:06 389 24448

>>24424
>Будем надеяться, что местный её фанат направит большую часть своей энергии в продуктивное русло вроде обсуждения с высокой строгостью необходимых теорем.
Пробовал, не заходит. Закатывания глаз и кукареканья бесноватых начинаются примерно на фразе "изоморфизм Карри-Говарда". А без этого уже не объяснить, почему лямбдаР (AUTOMATH де Брауна, например) это то же самое, что исчисление предикатов. Про что-то более сложное (Кок тот же) и говорить нечего.

Ответы4449

390 8 сен 2017, 13:40 390 24449

>>24448
Тебе задают вопросы, а ты их игнорируешь.

Ответы4456

391 8 сен 2017, 15:24 391 24453

>>21602
>Просто пренебрегаем последним членом
>И, чем больше n, тем смелее можно пренебречь последним членом суммы.
Гармонический ряд обоссывает эту логику.

392 8 сен 2017, 15:29 392 24454

>>22030
>Проблема только в том, что за всем этим стоит не пустой синтаксис ни о чем, как в формализме, а вычислимая конструктивная математика, где даже понятие равенства имеет вычислительное содержание.
Вот в чём твоя проблема. Ты приравниваешь синтаксические конструкции к смысловым, и из этого выводишь, будто твой конструктивизм чем-то отличается от формализма. Проснись, ты обосрался!

Ответы4456

393 8 сен 2017, 15:35 393 24455

>>22079
>Считающаяся в термы из квинтиллионов знаков. Это проблема, пони маешь? Потому что если мы захотим это на самом деле посчитать, то...
Ты с ума сошёл? Зачем каждый раз заново выводить всю предшествующую математику, если теорема - это и есть ёбанный квинтиллион знаков, полностью доказанный? Аксиомы-то остались неизменны, зачем каждый раз перепроверять вывод?

394 8 сен 2017, 15:44 394 24456

>>24449
>Тебе задают вопросы, а ты их игнорируешь.
Мне начинают нести такую ахинею, что уши вянут. Вот типичный пример >>24454 какой-то школотрон думает, что опроверг интуиционизм в 2017 году. И что отвечать в таком случае? Я, разумеется, мог бы процитировать Брауэра https://projecteuclid.org/euclid.bams/1183422499 Гейтинга или Маннури по поводу разницы между интуиционизмом и формализмом, а она есть, и существенная. Но кто здесь хотя бы поймет о чем вообще речь? Никто, очевидно же. Тут чуть выше никто так и не въехал в разницу между классической и конструктивной логикой для формулы Пирса какие же вы деграданты, пиздец просто. Как итог, получу еще больше неинтересного мне кукареканья и истерик.

Ответы4464

50 Кб, 809x301
395 8 сен 2017, 16:02 395 24459

>>22514
>Вы даже внятно не сможете объяснить зачем вообще нужны основания и аксиоматика и для чего там исчисление предикатов, например.
Чтобы не обосраться, как на пике - т.е. всегда применять методы, адекватные данным и задачам. Основания нужны потому что, как показывает практика, обосраться можно даже в элементарных вещах.

Ответы4477

396 8 сен 2017, 16:03 396 24460

>>22550
Существуют объекты, достаточно точно описываемые вещественнозначными функциями вещественного же аргумента.

397 8 сен 2017, 16:04 397 24461

>>22910
>Отрицание бесконечности и конструктивный подход гут.
И чем же он гут?

398 8 сен 2017, 16:11 398 24463

>>23637
Жак Адамар, "Исследование психологии процесса изобретения в математике"

399 8 сен 2017, 16:23 399 24464

>>24456
>разницы между интуиционизмом и формализмом
Всего-навсего другой набор аксиом, вот и всё. Но маняучёным не дают покоя лавры Пуанкаре, Римана и Гильберта, поэтому очень уж хочется сделать что-нибудь "особенное" поэтому они придумывают никому ненужные системы с крайне геморроидальным выводом даже простейших теорем и эпатажно отрицают то, что успешно применяется на практике годами.

Ответы4465

400 8 сен 2017, 16:31 400 24465

>>24464
>Всего-навсего другой набор аксиом, вот и всё.
Я тебя услышал, ага. А ничего, что у Брауэра вообще аксиом не было? А про логические отрицания ты что знаешь? По Маннури, конструктивное отрицание - это choice negation, отрицание в классической логике - exclusion negation. Из чего следует 4 разновидности только двойного отрицания, из которых только 2 эквивалентны утверждению (двойные choice и exclusion negation). Если их миксануть, интереснее получается. Но логика никому не интересна, проще ж веровать в аксиомы полученные Гильбертом в виде скрижалей на горе сион.

Ответы4466

401 8 сен 2017, 16:37 401 24466

>>24465
Ты, похоже, плохо представляешь себе, что такое аксиома. Если у Брауэра аксиом не было, то не было и определений. А без определений не о чем и размышлять. То, что в работах этого господина аксиомы присутствуют неявно, без огромной надписи АКСИОМЫ и пронумерованного списка может и рвёт шаблон, но сущности не меняет.

Ответы4467

402 8 сен 2017, 16:50 402 24467

>>24466
>Ты, похоже, плохо представляешь себе, что такое аксиома.
И что же это такое? В натуральной дедукции аксиома - это логическое заключение без посылок, т.е. нечто, принимаемое без предшествующего контекста, из которого это нечто можно вывести, т.е. нечто, ниоткуда не выводимое, а принимаемое "как есть". С такой позиции даже в MLTT аксиом нет, т.к. там 4 правила вывода и все они начинаются с контекста. Про Брауэра и говорить нечего, он даже конструктивную логику Гейтинга назвал "любопытным, но бесплодным примером", сам Гейтинг тоже явно оговаривал, почему конструктивная логика не формализует брауэровского интуиционизма.

Ответы4470

403 8 сен 2017, 17:05 403 24470

>>24467
>это логическое заключение без посылок
>логическое заключение без посылок
Уже сама эта фраза полностью демаскирует полное незнание тобой терминологии, которой ты так презрительно разбрасываешься. Аксиома - это утверждение о свойствах, элементарная часть определения. Связка аксиом и образует полное определение.
>принимаемое без предшествующего контекста
Аксиомы не являются выросшей на пустом месте игрой ума. Они были сформированы с учётом опыта обращения человечества с числами. Они строго очертили неясные до той поры понятия и позволили прежде всего без опасений выводить новые и новые следствия. Они показали границы применимости методов, с их помощью можно всегда ответить на вопрос "А правильно ли я поступаю? Не пытаюсь ли я сложить красное с длинным?" Они позволили, наконец прояснить собственно пути математики, сделав рассуждения кристально прозрачными.
Интуиционизм же является не более, чем оголтелым скептицизмом, который сомневается даже в собственном здравомыслии. И странное дело: интуиционизм яростно отрицает одно и столь же яростно отстаивает другое совершенно не желая признавать за собой место обычной формальной системы.
>там 4 правила вывода и все они начинаются с контекста.
А контекст-то с чего начинается? А правила на чём основываются?

Ответы44714498

4 Кб, 562x103
404 8 сен 2017, 17:27 404 24471

>>24470
>Уже сама эта фраза полностью демаскирует полное незнание тобой терминологии, которой ты так презрительно разбрасываешься.
Вообще-то я привел вполне официальное определение аксиомы, пикрелейтед http://www.cs.cornell.edu/courses/cs3110/2013sp/lectures/lec15-logic-contd/lec15.html
>Аксиомы не являются выросшей на пустом месте игрой ума. Они были сформированы с учётом опыта обращения человечества с числами. Они строго очертили неясные до той поры понятия и позволили прежде всего без опасений выводить новые и новые следствия. Они показали границы применимости методов, с их помощью можно всегда ответить на вопрос "А правильно ли я поступаю? Не пытаюсь ли я сложить красное с длинным?" Они позволили, наконец прояснить собственно пути математики, сделав рассуждения кристально прозрачными.
Я чуть выше ссылался на статью Брауэра, он там как раз поясняет за необоснованность таких методов, когда нечто, выведенное из конечного априори и бездоказательно обобщается на бесконечное. Как исключенное третье, например.
>Интуиционизм же является не более, чем оголтелым скептицизмом, который сомневается даже в собственном здравомыслии.
Требование построения доказательства - это не оголтелый скептицизм, а вполне резонное условие для математики, которая вообще-то является самым точным знанием, известным человечеству. Верования там неуместны вообще никак. И где в интуиционизме сомнения в собственном здравомыслии?
>А контекст-то с чего начинается?
С конструктивных объектов.
>А правила на чём основываются?
На возможных манипуляциях с элементами контекста.

Ответы44724503

405 8 сен 2017, 17:37 405 24472

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

Ответы4473

255 Кб, 660x465
406 8 сен 2017, 17:56 406 24473

>>24472
>Ты понимаешь что у тебя "логический вывод" из ничего?
Я-то пони маю. Теперь и ты вроде начинаешь. Аксиома - это логический вывод из ничего, в противном случае это бы не аксиомой называлось.
>Да, некоторые вещи приходиться принимать без доказательств.
В церкви - сколько угодно. Но не в математике.
>Правда в том, что если мы вот прям счас откатимся в каменный век интуиционизма и забудем большую часть теорем существования - нам придётся лишиться очень, очень многого.
Например? Чего многого-то? Полторы все равно невычислимые фофудьи типа исключенного третьего - это немного. И раз они все равно невычислимы, считай, что мы их и так лишены, использовать-то все равно нельзя, только рисовать.
>В "формализме" доказательства строятся настолько замечательно, что их можно проверить исключительно основываясь на синтаксисе.
Из которого нельзя вывести ничего кроме этого синтаксиса. Самый простейший пример - формулу Пирса и таблицы тарского я уже упоминал.
>В том, что интуиционисты начинали с классики. Затем они зачем-то её кастрировали, переформулировали и вуаля - новая теория.
Ой, всё... В каком месте Брауэр начинал с классики? Ты же его даже не читал, но осуждаешь, как совки Пастернака. Даже ту картинку с Брауэром на дачке и 1 и 2 актами интуиционизма, которую я сто раз постил, не читал.
>И как же они определяются?
>Почему это они возможны?
А вот тут опять надо писать страшные слова, с которых бесноватых корежит - интрерпретация логических констант по Брауэру-Гейтингу-Колмогорову.

Ответы4477

407 8 сен 2017, 18:24 407 24477

>>24473
> Аксиома - это логический вывод из ничего
Это не логический вывод, потому что предпосылок нет.
>В церкви - сколько угодно. Но не в математике.
Ты хочешь сказать, что можешь доказать непротиворечивость кокструктивистской хуйни средствами самой теории? Она только кажется тебе убедительной, в основном из-за своей радикальности, но на имеет под собой ровно столько же оснований, что и любые другие непротиворечивые основания математики. Интуиционистский неуместный аскетизм предлагает резать всё циркулярной пилой и ножом - ну а хули, режет же, чего ещё надо?
>Полторы все равно невычислимые фофудьи типа исключенного третьего - это немного. И раз они все равно невычислимы, считай, что мы их и так лишены
Теоремы существования кокструктивизмом не признаются, однако часто, чтобы рассчитать то, существование чего доказывает теорема, необходимо провести над этим чем-то определённые манипуляции. Прямо как здесь: >>24459
допустимость операций определяется сходимостью ряда, что определяется существованием предела. Более того, поскольку сам придел - понятие неарифмитическое, он впринципе выпадает из рассмотрения конструктивистской секты. И что же конструктивисту делать, если его инженер попросит рассчитать работу?
>Из которого нельзя вывести ничего кроме этого синтаксиса.
Ты сравниваешь тёплое с мягким. Синтаксис позволяет проверить правильность умозаключений, но отнюдь не призван заменить работающую голову.
>В каком месте Брауэр начинал с классики?
Он начал с изучения классической математики. Он не сделал свои выводы, сидя на дачке с полной изоляцией от внешнего мира.
>интрерпретация логических констант по Брауэру-Гейтингу-Колмогорову.
Эти константы были положены, постулированы, как постулируется существование множества натуральных чисел. Кстати об N - оно ж бесконечно, а значит необходима очень ловкая логическая конструкция, которая позволяет манипулировать натуральными числами, не так ли?

Ответы4482

86 Кб, 491x661
408 8 сен 2017, 19:56 408 24482

>>24477
>Это не логический вывод, потому что предпосылок нет.
Я же даже скрин логического вывода аксиомы дал. Врети?..
>Он начал с изучения классической математики.
Он с нее не начал, а просто изучал в школке и в универе, как и все остальные. Это разные вещи.
>Эти константы были положены, постулированы, как постулируется существование множества натуральных чисел.
Множество натуральных чисел задано правилами его построения, там нечего постулировать.
>Кстати об N - оно ж бесконечно, а значит необходима очень ловкая логическая конструкция, которая позволяет манипулировать натуральными числами, не так ли?
Не так. Опять же, обсуждали уже все это. В том числе и отличие актуальных бесконечностей от абстракции потенциальной осуществимости.

Ответы4483

409 8 сен 2017, 20:36 409 24483

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

Ответы448545104607

410 8 сен 2017, 21:10 410 24485

>>24483
> Какие проблемы устраняет отказ от актуальной бесконечности и принятие потенциальной, вот что интересует меня в первую очередь.
Актуальная бесконечность невычислима.

Ответы44864490

411 8 сен 2017, 21:10 411 24486

>>24485
>невычислима
И что?

Ответы4487

412 8 сен 2017, 21:35 412 24487

>>24486
Невычислимое может быть принято только на веру. Математика - это не верунство.

Ответы4489

413 8 сен 2017, 22:03 413 24489

>>24487
Вычислимость сама по себе -верунство.

414 8 сен 2017, 22:06 414 24490

>>24485
Докажи.

415 9 сен 2017, 07:57 415 24498

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

Ответы4501

416 9 сен 2017, 11:32 416 24501

>>24498
>кажется,
Крестись. Разве я виноват, что про натуральную дедукцию ты от меня позавчера услышал? Подумой, ты ж даже аргументы не воспринимаешь. Я тебе даю ссылку и даже конкретный скрин, ты глаза закатил и пытаешься доказать мне, что это я что-то не знаю.

Ответы4502

417 9 сен 2017, 11:50 417 24502

>>24501
Ээ... Шта? Это мой первый пост в этом треде. Креститься надо, да.

Ответы4503

418 9 сен 2017, 11:51 418 24503

>>24502
Я вот об этом >>24471 если что.

Ответы4504

419 9 сен 2017, 12:02 419 24504

>>24503
Ээ... Прочитай, кому был адресован мой пост. Ты, кажется, просто триггеришься на определенные слова своей вечной мантрой про "я дал скрин, прочитайте, вы ничего не понимаете, уже тысячу раз объяснял". Ты точно не бот?

420 9 сен 2017, 15:41 420 24510

>>24483
>Какие проблемы устраняет отказ от актуальной бесконечности и принятие потенциальной, вот что интересует меня в первую очередь.
А что вообще актуальная бесконечность делает в математике? Это даже не математический объект. Проблема как раз в этом. В математику за тысячи лет понатащили всякой хуйни, никакого отношения к ней не имеющей. В основном из третьесортной философии типа платонизма. Причем, в самые основания понатащили. А потом вжух и кризис оснований.

Ответы4607

421 10 сен 2017, 02:15 421 24607

>>24483
>>24510
Что такое "актуальная бесконечность"?

Ответы4611

156 Кб, 787x830
422 10 сен 2017, 12:36 422 24611

>>24607
У тебя еще есть время научиться пользоваться гуглом. В чебурнете такой возможности уже не будет, поторопись.

Ответы4612

34 Кб, 357x333
423 10 сен 2017, 12:39 423 24612

>>24611
Похоже на хуйню какую-то, даже скорее всего выдуманную и несуществующую.
Зачем мне время тратить на поиски её в гугле? Тем более если я гос. веб сайтам не совсем доверяю в таких вопросах.

Ответы4616

424 10 сен 2017, 15:14 424 24616

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

Ответы4622

425 10 сен 2017, 17:00 425 24622

>>24616
Но математика действительно к вычислимости не сводится.

Ответы4623

426 10 сен 2017, 17:04 426 24623

>>24622
Примеры будут?

Ответы4624

427 10 сен 2017, 17:18 427 24624

>>24623
Теория множеств - это математика?

Ответы4626

428 10 сен 2017, 17:29 428 24626

>>24624
Местами. В оригинальном своем виде это невычислимая аксиоматика, в качестве оснований непригодная как минимум из-за исключенного третьего. Если даже довести до ума, все равно не идет дальше лямбда-Р в кубе Барендрегта, а в 2017 это несерьезно.

Ответы46274638

429 10 сен 2017, 17:38 429 24627

>>24626
Когда там конструктивисты гипотезу Римана докажут? А то в 2017 как то не серьезно.

Ответы4629

430 10 сен 2017, 17:45 430 24629

>>24627
А неконструктивисты когда? Все-то вас тянет ко всякой бесконечной комбинаторной хуйне из прошлого тысячелетия типа ферзей да римановых ноликов.

Ответы46304659

431 10 сен 2017, 17:49 431 24630

>>24629
>А неконструктивисты когда?
Оставляем эту почетную проблему вам, а то у вас совсем как-то плохо. Почти никаких задач не решаете, всё дрочите на свою вычислимость.

432 10 сен 2017, 18:18 432 24638

>>24626
Окей, а каков порядок ℤ? Или у вас не существует бесконечных групп?

Ответы4670

433 10 сен 2017, 19:21 433 24659

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

Ответы4663

434 10 сен 2017, 19:35 434 24663

>>24659
Каким образом?

Ответы4668

435 11 сен 2017, 03:46 435 24668

>>24663
Любая NP-полная задача сводится к любой NP-полной.

Ответы4676

436 11 сен 2017, 06:01 436 24670

>>24638
>Окей, а каков порядок ℤ?
У ℤ нет конечного порядка.
>Или у вас не существует бесконечных групп?
Существуют группы, которые не являются конечными.

437 11 сен 2017, 09:31 437 24672

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

Ответы4673

438 11 сен 2017, 09:38 438 24673

>>24672
А меня вот бесит аксиома пары. Каждый раз, как о ней думаю, аж зубы сводит, так сильно эту аксиому ненавижу. Блядские веруны в пару, так бы и запретил.

Ответы4674

439 11 сен 2017, 09:40 439 24674

>>24673
Я не использую теорию множеств, я же не совсем конченный.

440 11 сен 2017, 11:13 440 24676

>>24668
>Любая NP-полная задача сводится к любой NP-полной.
И что? Класс задач, разрешимость которых можно проверить на машине Тьюринга за не более чем полиномиальное от размера входных данных время - это далеко не вся "наука о вычислимости". И это чудо капустное кого-то будет селюком называть.

441 14 сен 2017, 10:21 441 24801

>>21361 (OP)
Какова природа математической истины? Вот 1+1=2 это вроде как истина, но истина не такая как "Расстояние от моей лобковой кости до конца головки моего члена в эрегированном стоянии составляет 13см, что является средним и нормальным значением". Знаю людей утверждающих что математика это вообще не про истину и не про объективность, а просто маняфантазёрство.

Ответы48044806

442 14 сен 2017, 12:39 442 24804

>>24801
-> /ph

309 Кб, 1902x2842
443 14 сен 2017, 13:16 443 24806

>>24801
>Какова природа математической истины?
Классически в математике истинно то, что непротиворечиво. Конструктивно - истинно то, что построимо, т.е. конструктивные объекты и доказуемве / выводимые / наблюдаемые их свойства.
>Вот 1+1=2 это вроде как истина, но истина не такая как "Расстояние от моей лобковой кости до конца головки моего члена в эрегированном стоянии составляет 13см, что является средним и нормальным значением".
Есть мнение, что точно такая же. Пикрелейтед, выделенное. Математический релятивизм Маннури - утверждение о сводимости любого концепта к любому другому, т.е. если есть концепт A и другой концепт В, то первый можно свести ко второму через конечное число промежуточных концептов A1,...,An таких, что концепт А представим в форме концепта А1, а концепт An представим в виде концепта В. Концепты, например, могут быть любыми математическими объектами, принадлежащими любой аксиоматике, теории и т.д. В твоем примере даже этого не требуется, поскольку в обоих случаях речь о натуральных числах, к которым напрямую сводятся оба твои примера.

Ответы4807

444 14 сен 2017, 13:25 444 24807

>>24806
>если есть концепт A и другой концепт В, то первый можно свести ко второму через конечное число промежуточных концептов A1,...,An таких, что концепт А представим в форме концепта А1, а концепт An представим в виде концепта В.
Давай конструктивное доказательство.

Ответы4808

445 14 сен 2017, 13:33 445 24808

>>24807
Типизированная лямбда же. К ней легко свести даже естественный язык,как пример - семантика Монтегю, есть еще целая монография Ранте, где естественный язык анализируется с позиции MLTT и наоборот. А на естественном языке можно описать хоть твою мамку. Опять же, по Маннури, есть 5 уровней языка, от естественного разговорного до полностью формального, н-р матлогика, и разница между этими уровнями относительная, а не абсолютная. Так что доказать можно и конструктивно, через типизированную лямбду, т.к. любой концепт так или иначе можно представить лямбда-термом.

Ответы4810

446 14 сен 2017, 13:38 446 24810

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

Ответы4812

447 14 сен 2017, 13:49 447 24812

>>24810
Можно, причем элементарно - через обобщение номинальной дефиниции и редукций (дельта, бета, иота, дзета) до кое-чего интересного. Когда-нибудь допилю свой мега-гитлер прувер, будет конструктивное доказательство.

Ответы48144847

448 14 сен 2017, 13:52 448 24814

>>24812
>до кое-чего интересного
Можно подробнее?

Ответы4855

449 15 сен 2017, 09:31 449 24847

>>24812
А планируешь прувер сделать онлайновым? Сейчас типа все современные пруверы имеют онлайн морду.

Ответы4855

450 15 сен 2017, 13:45 450 24855

>>24814
Подробнее долго. Когда-нибудь руки дойдут, запилю нормальный пейпер.
>>24847
>планируешь прувер сделать онлайновым?
Полноценная реализация изначально планируется онлайновой, т.к. все нужное проще всего реализовать средствами гугловской облачной платформы https://cloud.google.com/ и не привязанной ни к какой конкретной операционке. Кто бы еще все это сделал, т.к. я в гуглооблако не могу. Локально почти все нужное (кроме OCR для математической нотации (LaTeX и AMS-TeX) реализуемо в R, это уже посильно для меня, было бы еще свободного времени побольше а быдлопроблем поменьше.

Ответы486648675179

451 15 сен 2017, 23:21 451 24866

>>24855
Что такое пейпер, как на английском пишется?

Ответы5169

452 15 сен 2017, 23:25 452 24867

>>24855
Был тут рукастый анон, который сайт создавал, может он поможет. Как тебе его сайт был?

Ответы5185

453 17 сен 2017, 03:09 453 24908

>>21607
Отличное видео. У него как я понимаю вообще мало записанных лекций?

54 Кб, 1024x768
454 25 сен 2017, 02:39 454 25169

>>24866

455 25 сен 2017, 15:06 455 25179

>>24855

Ты же понимаешь, что в тебе борются два волка?
Один - волк-программист, другой волк-математик.

19 Кб, 267x325
456 25 сен 2017, 19:44 456 25185

>>24867
Хорен что ли?))

457 26 сен 2017, 20:14 457 25210

>>21400
>>21361 (OP)
Надо ли перестать использовать классическую логику?

Ответы5211

458 26 сен 2017, 20:17 458 25211

>>25210
Не нужно вообще начинать даже. Это как вирус.

Ответы52125213

459 26 сен 2017, 20:22 459 25212

>>25211
Хорошо, а тогда как с помощью киинтуиционисткой логики доказать, например, неразрешимость проблемы останвки?

460 26 сен 2017, 20:22 460 25213

>>25211
там же явным образом используется исключение третьего.

Ответы5215

461 26 сен 2017, 21:21 461 25215

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

Ответы5282

462 28 сен 2017, 22:35 462 25282

>>25215
Хорошо, порекомендуй тогда, пожалуйста, монографии по конструктивной математике.

Ну то есть уважаемые труды, где много теорем.

463 29 сен 2017, 00:56 463 25283

Посоны, лисп учить или нет?

Ответы5284

464 29 сен 2017, 01:11 464 25284

>>25283
Он милый

Ответы5285

465 29 сен 2017, 01:13 465 25285

>>25284
А скема?

Ответы5286

466 29 сен 2017, 01:22 466 25286

>>25285
Да одно и тоже

467 29 сен 2017, 01:26 467 25287

Посоны, микроядра кто нибудь доказывал? Че там жопа или реал вкатится и бабосы рубить под пивасик?

468 29 сен 2017, 01:27 468 25288

Посоны, я тут короче кнута решаю. Всё правильно делаю?

469 29 сен 2017, 01:31 469 25289

Посоны, емакс учить или таблеток лучше?

470 1 окт 2017, 10:40 470 25375

Воеводский умер, я в шоке :((

Ответы537653775383

471 1 окт 2017, 10:54 471 25376

>>25375
https://news.ycombinator.com/item?id=15375717

472 1 окт 2017, 11:12 472 25377

>>25375
Пиздец, ужасная новость. Вроде как-то фиолетово, когда слышишь подобные известия, ну не друг и не родственник умер, но тут не по себе.

473 1 окт 2017, 15:32 473 25383

>>25375
Очередная победа теоретико-множественного подхода.

Ответы53875390

474 1 окт 2017, 17:55 474 25387

>>25383
Проиграл на весь театр.

Ответы5388

475 1 окт 2017, 18:37 475 25388

>>25387
Синъити, верни мне мой театр! Заебал.
Ходж

Ответы5389

476 1 окт 2017, 19:10 476 25389

>>25388
Не верну, я обиделся на всех.

477 1 окт 2017, 19:12 477 25390

>>25383
>Очередная победа теоретико-множественного подхода.
Единственная, я бы сказал. Других не подвозили, начиная с того самого 11-го симпозиума в Палермо в 1897 году, когда Бурали-Форти торжественно помочился Кантору за шиворот, уничтожив его как математика.

Ответы5394

478 1 окт 2017, 20:25 478 25394

>>25390
У Кантора хотябы есть что критиковать.

Ответы5395

479 1 окт 2017, 20:31 479 25395

>>25394
У любого найдется, что критиковать. Одно дело критика, другое - доказательство противоречивости и т.о. бесполезности всей теории.

480 1 окт 2017, 20:44 480 25396

Брауэр, к слову, не только задолго до Геделя и обсера Гильберта с его изначальной программой, показал несостоятельность формализма как оснований математики. И даже не только вывел суть математики как ментальных построений, что подтвердилось уже в нулевых годах 21 века (модели ATOM, MT, о чем уже писалось). Его взгляды на природу и физику как науку очень похожи на то, что сейчас известно как квантово-волновой дуализм и эффект наблюдателя (во II части его диссертации и немного в самом начале III части есть некоторое количество цитат на эту тему), он же был профессором кафедры математики и физики. К сожалению, я в квантмехе практически нихуя не понимаю давно забытый материал из учебников не считается, чтобы сделать более грамотное сравнение. Даже его определение дискретного и непрерывного в интуиции времени как основе математики можно было бы рассмотреть с точки зрения квантово-волнового дуализма.

Ответы5397

481 1 окт 2017, 20:52 481 25397

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

Ответы5398

482 1 окт 2017, 20:56 482 25398

>>25397
Кто "мы"-то? Я один тута. Разве то, что из некоей теории можно вывести нечто такое, до чего остальная наука дошла десятилетия спустя, не говорит в пользу правильности этой теории7

Ответы5399

483 1 окт 2017, 20:59 483 25399

>>25398
Да-да, конечно. Если Кузанский о множественности миров кукарекал, то это он на самом деле теорию струн открыл.

Ответы5400

484 1 окт 2017, 21:04 484 25400

>>25399
>множественности миров
Это одна из возможных интерпретаций же. А корпускулярно-волновой дуализм - медицинский факт.

Ответы5401

485 1 окт 2017, 21:07 485 25401

>>25400
Да-да. И вот так, легким движением ушей, Кузанский записывается в отцы-основатели квантовой механики.

486 2 окт 2017, 02:08 486 25408

Можно ли считать любовь к теории мн*жеств психическим расстройством?

Ответы5415

487 2 окт 2017, 18:17 487 25415

>>25408
Ну зачем же сразу расстройство. У нас свобода вероисповедания. Кто-то в Аллаха верует, кто-то в платоновский мир идей. Другой вопрос, что ни то ни другое - это не математика.

Ответы54235427

488 2 окт 2017, 20:57 488 25423

>>25415
Чем же ты объясняешь очевидную популярность теории множеств? Видимо ты просто не умеешь ей правильно пользоваться, поэтому в отрицание скатываешься.

Ответы54275439

489 2 окт 2017, 21:07 489 25427

>>25415
Тут даже не про веру в Аллаха, хотя и она конечно даёт о себе знать.
>>25423
Скорее всего это объясняется пока ещё неизвестным вирусом. Другого объяснения не вижу.

490 3 окт 2017, 07:58 490 25439

>>25423
>Чем же ты объясняешь очевидную популярность ислама? Видимо ты просто не умеешь правильно веровать, поэтому в куфр скатываешься.
Я тебя услышал.

Ответы54565458

491 3 окт 2017, 23:07 491 25456

>>25439
Ок, ты мечтаешь о вычслимости.

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

Либо выдумывать свою конструктивную науку и в ней болтаться без конца.

Я тебя спрашиваю: где результат?
Какую реальную проблему помогла решить вычислимость теорем?

Сможешь хотя бы 3 примера реальных задач привести.
За которые тебе заплатят деньги. Классическая логика и обычные основания математики - дают рабочий инструмент.
Нахрена из кувалды делать микроскоп?

Ответы54655475

492 4 окт 2017, 00:15 492 25458

>>25439
Ваша анальная фиксация на исламе поражает, вас в детстве насиловал отчим дагестанец?

493 4 окт 2017, 06:23 493 25459

ℵ_∞

494 4 окт 2017, 09:01 494 25465

>>25456
Действительно, согласен. Вот ещё что думаю:
У них контринтуитивное отрицание закона исключенного третьего.
Утверждение: Конструктивист петух или конструктивист не петух. Но зная, что конструктивист петух, мы не можем определить истинность этого утверждения!

Ответы5473

495 4 окт 2017, 13:32 495 25473

>>25465
почитай по теме чуть больше, ты пока не разобрался

Ответы5486

496 4 окт 2017, 15:07 496 25475

>>25456
Пришёл ты в /матх/
о вычислимости мечтаешь ты
сосни-ка хуйца
Навеяло

497 5 окт 2017, 02:03 497 25486

>>25473
А пачиму в канструктивных оснонваниях отрцицается исключённае третье????????

Ответы5552

498 5 окт 2017, 23:41 498 25552

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

Ответы5553

499 5 окт 2017, 23:46 499 25553

>>25552
сагласен! я вот ещё кстате вычислил что канструктивные основания пративоречивы!!
ведь в них отрицается исключённае третье и доказывается двойное отрицание исключённого третьего!!
другими словами просто фууу....

500 6 окт 2017, 00:25 500 25554

так... я даказал в гаматапической теории типав что исключённое третье неверно. из этого следует пративоречивость канструктивной
математики.

теорема: канструктивная математика противоречива.

доказательство:

исключённая третье говорит нам, что верно - для всех типав X и для всех точак x и y в X наличие пути из x в y разрешимо.
то есть у нас есть терм назавём его الله.
الله : Π (X : U) . Π (x, y : X) . x = y ∐ x ≠ y
الله X x y := "тут применяем наше исключённае третье"
читаем как "الله имеет тип "для всех термав принадлежащих универсуму U (типав) и для любых термав x и y типа Х наличие пути из х в у разрешимо""
из этого следует что все типы являются 0-типами!
теперь подставляем x вместо у и палучаем что все гаматопические группы (любого типа!!!) тривиальны!

куда можно это опубликовать?

Ответы5569

7 Кб, 1200x1200
501 6 окт 2017, 00:26 501 25555

извените...
там в конце доказательство должен был быть знак как на скриншоте.

502 6 окт 2017, 20:03 502 25569

>>25554
улыбнул, но лучше бы ты по теме что-нибудь писал про вычислимость. Очень кайфовая тема.

Ответы5574

503 7 окт 2017, 01:53 503 25574

>>25569
тут дажы вычислимасть не нужна чтобы доказать пративаречивость вычислимасти.

504 7 окт 2017, 20:45 504 25625

Перекат https://2ch.hk/math/res/25624.html (М)

Тред закрытОбновить закрытый тред
Двач.hk не отвечает.
Вы видите копию треда, сохраненную 6 декабря 2024 года.

Скачать тред: только с превью, с превью и прикрепленными файлами.
Второй вариант может долго скачиваться. Файлы будут только в живых или недавно утонувших тредах. Подробнее

Если вам полезен архив М.Двача, пожертвуйте на оплату сервера.

« /math/В начало тредаВеб-версияНастройки/a//b//mu//s//vg/Все доски

Пользуетесь скринридером — пишите, что можно улучшить.
Host-Food.ru — надёжный хостинг от 12 руб/мес | Free DNS
Зеркала М.Двача: m2ch.hk, m2ch.lib, m2chfapiswfw2wcakptqp4o6ltgchvjuxfab7urxlduraomtlnhw5xad.onion