Помимо трех основных направлений в основаниях - формализм, логицизм и интуиционизм, иногда возникали идеи построить математику на кардинально отличных от общепринятых принципах. Одно из таких направлений - Сигнифика, Significs. Попытка основать математику на основе естественного языка (т.к. язык и математика - это деятельность человека) принадлежит учителю Брауэра, голландскому математику и философу Герриту Маннури. Согласно его теории уровней языка (таких уровней 5), чисто формальный язык математики (5ый уровень) отличается от языка общения детей (1ый уровень) только степенью связи между словами и их сочетаниями (языковыми конструкциями). Идеи Маннури более чем на столетие опередили свое время, т.к. при его жизни не было методов автоматизированной работы с текстом (NLP, Natural Language Processing). В наше время такие методы развиты достаточно, чтобы поставить вопрос о построении вычислительной сигнифики (Computational Significs) для нужд математики, в т.ч. автоматизированного доказательства теорем и т.о. реализации на этих основах прувера, отличающегося принципом функционирования от всех остальных чуть менее чем полностью. Предыдущий - https://2ch.hk/math/res/17772.html Архив тредов
>>21363 И сразу все бесконечности и исключенное третье сами посчитались. А Гильберту делать было нехуй, что он решил обосновывать арифметику финитарными методами, потому что чисто аксиоматически это оказалось сделать невозможно. Финитарными, Карл! До такого даже Брауэр не докатился, хотя и описал то, что Гильберт назвал "метаматематикой" задолго до Гильберта т.к. признавал потенциальную осуществимость, как абстракцию от действия над ментальными построениями "and so forth". Суть-то в чем? Невычислимые основания нельзя использовать на практике, н-р для доказательства непротиворечивости арифметики, на чем Гильберт и прогорел, скатившись в итоге к финитизму. Подобные же причины сделали необходимым создание вычислимых оснований - MLTT и HoTT. Если бы все можно было доказать в ZFC, никто бы не ебался с конструктивными основаниями.
>>21365 Ну я тебе пример с непротиворечивостью арифметики привел. Нахуя нужны основания, пользуясь которыми нельзя обосновать что 1+1 будет 2? Это не то что не основания, это не математика даже.
>>21368 >Арифметика Пеано непротиворечива, и это доказано. Теоремой Гудстейна? Ты формально докажи непротиворечивость арифметики, а не правилами построения типа аксиом Пеано.
>>21373 Го пвп? Сейчас бы в 2017 намейлру опровергать интуиционизм. Ну что вы тут за аутисты? Вот ты ж даже не читаешь, что тебе пишут, не говоря о том чтобы попытаться понять. Помимо невычислимых нематематических верований вся используемая математика конструктивна и даже выразима в лямбда Р исчислении, что показал де Браун. Я это не писал уже сто раз? Писал. Так что ты опровергать собрался?
>>21391 Ну, вначале ведь нужно уточнить позиции. Первым делом я бы хотел выяснить объём и границы того, что ты называешь "всей используемой математикой". От общих вопросов - не отсекается ли тобой, скажем, вся теория множеств и вся современная алгебра, и до таких частностей, как возможно ли определить топологию Зоргенфрея на числовой прямой. Согласись, вполне справедливая хотелка.
>>21398 > Ну, вначале ведь нужно уточнить позиции. Я их уже 4ый тред уточняю + до этого тредов 5 как минимум в сци. Математика это все, что вычислимо, все что невычислимо это не математика. Именно поэтому всю математику можно изложить уже в лямбда Р исчислении (Automath де Брауна), да даже на машине Тьюринга, хотя это дальше от практики. Т.к конструктивный объект это обобщение натурального числа, любую математическую структуру можно свести к натуральному числу, геделевской нумерацией например, а вся математика точно так же сводится к арифметике. А все, что не сводится - это не математика, с этим только в церковь покемонов ловить. Не писал я этого сто раз? Писал ведь. И если после всего этого моя позиция остается гепонятной кому'то, я даже не знаю.
>>21400 Это слишком общие слова. Хотелось бы (и, похоже, не мне одному) узнать, что же конкретно ты относишь к области покемонов. Понятно, что ты запрещаешь изучать большие кардиналы и нестандартный анализ, но как далеко простираются запреты и не попадает ли вдруг под них вообще вся общая топология? Вот скажи, как в твоем учении выглядит введение разнообразных топологий на множестве вещественных чисел? Как, к примеру, топологию Зоргенфрея следует определять? Это конкретные вопросы, и я рассчитываю на конкретные ответы.
Это не общие слова, а вполне конкретная конкретика. Математика = вычислимость, для определенности, пусть будет вычислимость на машине Тьюринга, хотя сойдет и любое другое уточнение понятия алгоритма. Невычислимое невычислимо, поэтому его нельзя вычислить, можно только верить. Потенциальная осуществимость осуществима потенциально, отличие от актуальной бесконечности - наличие правил построения. >>21401 > Как, к примеру, топологию Зоргенфрея следует определять? Дался тебе этот Зоргенфрей. Еще Брауэр показал, что континуум невычислим и уж точно не сводится к множеству вещественных чисел.
>>21411 Я думаю тут еще хуже, смотри он пишет >Математика = вычислимость И при этом следом >континуум невычислим Отсюда по его манялогике: вещественные числа эта манявера и четко твердо НИНУЖНО. Я тут подумал, а этого сумасшедшего легко косплеить.
>>21411 > Верно ли я понял, что ты запрещаешь вводить различные топологии на множестве вещественных чисел? Ты ведь и сам понимаешь, даже без всякого конструктивизма, что это в любом случае будет аппроксимация с конкретным количеством знаков после запятой. Именно их ты и будешь вычислять. Нет никакого запрета, есть трезвый взгляд на тему. Брауэр, к слову, топологией занимался еще до интуиционизма.
>>21414 О какой аппроксимации речь? В какой процедуре? Топология стрелки - это классический пример топологического пространства с неинтуитивными свойствами, и работает этот пример именно как цельное пространство.
>>21417 Все эти ваши "цельные пространства" на самом деле дискретизация. Самый простой пример - интегральчики. Веровается, что с помощью предельного перехода размера интервалов dx к бесконечно малому получается нечто отличное от просто интервалов, хотя ни для кого не секрет, что любые численные методы интегрирования - это чистая дискретка. Т.о. имеем практически возможную аппроксимацию конечным числом интервалов dx, а предельный переход существует только на бамаге, ничего построимого и вычислимого за ним не стоит. Т.е. на самом деле вычисления не идут за пределы реально вычислимого. И опять же, я приводил конкретный пример - теория статистического обучения. Таких примеров можно привести еще сколько угодно, те же функции принадлежности в нечетких множествах. Т.е. на самом деле работает все так, как показал еще Брауэр - континуум невычислим, реально можно работать только с его дискретизацией.
>>21430 >Веровается, что с помощью предельного перехода размера интервалов dx к бесконечно малому получается нечто отличное от просто интервалов, хотя ни для кого не секрет, что любые численные методы интегрирования - это чистая дискретка. Какая разница, что там в реальности считают инженеры? >Т.е. на самом деле вычисления не идут за пределы реально вычислимого. А число Грэма?
>>21431 >Какая разница, что там в реальности считают инженеры? Типа ты можешь посчитать больше, чем инженер, причем в какой-то своей реальности? Вычислимость это вычислимость, машину Тьюринга, Поста и другие подобные вещи ты не перевычисляешь, это факт. >А число Грэма? Обсуждали уже. Тебе в слове "вычислимое" что непонятно? Опять сказка про белого бычка из-за непонимания разницы между фактически построимым и абстракции потенциальной осуществимости? Извини, не интересно.
>>21432 >разницы между фактически построимым и абстракции потенциальной осуществимости Тогда почему ты говоришь про какие-то там дискретные величины в интегралах? Там бесконечность, континуум! УХ!
>>21434 Я понял, что тебе непонятно слово "потенциально", еще в прошлом году. Поэтому, давай так - ты разбираешься с этим понятием, потом приходишь сюда спрашивать. До этого не вижу ни одной причины повторять миллион раз одно и то же, причем тому, кто принципиально не способен воспринимать объяснения на эту тему.
>>21435 Если ты говоришь про потенциальность то зачем тогда упоминаешь интегральчики? >Самый простой пример - интегральчики. Веровается, что с помощью предельного перехода размера интервалов dx к бесконечно малому получается нечто отличное от просто интервалов, хотя ни для кого не секрет, что любые численные методы интегрирования - это чистая дискретка. У нас есть аналитический метод вычисления, без дискретки с континуумом!
>>21437 >математика - это один из разделов Computer Science? Да, конструктивное доказательство чему - изоморфизм Карри-Говарда. Хотя так-то это всем умным людям из тех, кого Брауэр не разбудил это стало ясно уже после работ Тьюринга с Постом. Самое смешное, что с тех пор кроме кривляний разной степени толстоты возражений пока не поступало.
>>21439 Но ведь ты веришь, в то, что например, доказательство на компьютере коком верно, поскольку человек не может его проверить. Ту же проблему четырёх красок взять!
>>21440 Я еще раз прошу не нести хуйни, т.к. в теме ты не понимаешь совсем, что видно за километр. Автоматическое доказательство коком ничем не отличается от автоматического доказательства человеком. Машину Тьюринга можно сделать из бумажной ленты и все нужное делать руками, это ничем не будет отличаться от неручной машины Тьюринга. Другой вопрос, что это займет гораздо больше времени. Я еще раз скажу - вычислимость это вычислимость, она одна, других не бывает.
>>21442 >Автоматическое доказательство коком ничем не отличается от автоматического доказательства человеком. Во первых, тогда почему твой кок не может оперировать исключающим третьим, аксиомой выбора, и актульными бесконечностями, а человек может? Почему я например могу работать с вещественными числами(бесконечными последовательностями десятичных дробей), а твой кок нет? Во вторых, доказательство коком сомниетльные, поскольку человек их не может увидеть. А раз мы не можем увидеть доказательство, то веруем в него. Как и веруем в доказательство проблемы черытёх красок, от которого плювался Гротендик.
Я вижу, что во-первых, вопросы по конструктивной математике тут таки возникают, во-вторых, с матчастью тут совсем все плохо, настолько плохо, что хуже уже не бывает. Поэтому, вниманию самых маленьких предлагается такая книшка: http://gen.lib.rus.ec/book/index.php?md5=2BBE15747B57CDB3BAF9F25BDFEC280B да, в совке издавали годные материалы по конструктивной математики даже для дошкольников и младших школьников. Все поясняется буквально на пальцах. >>21443 >почему твой кок не может оперировать исключающим третьим, аксиомой выбора, и актульными бесконечностями, а человек может? Во-первых, ты не можешь, ты вероваешь, что можешь. Во-вторых, в коке можно задать и исколюченное третье и даже Аллаха. Но, поскольку это неконструктивные сущности, за которыми не стоит никаких вычислимых в канонические элементы конструкций, это бесполезно. >Почему я например могу работать с вещественными числами(бесконечными последовательностями десятичных дробей), а твой кок нет? Давай, покажи. Тащи сюда полностью свои бесконечности. >доказательство коком сомниетльные, поскольку человек их не может увидеть. В третий раз тебе говорят, хватит писать мне хуйню, реально надоело. Если ты кок в глаза видел, то видел и доказательства, которые он выдает. А если бы еще слышал про лямбда-куб, исчисление конструкций итд, то даже и понял бы их.
>>21444 Зачем мне читать твою конструктивную литературу? Почему вместо нормального объяснения ты всё время крепишь скриншоты и отсылаешь к книжкам? Хочешь меня так в свою секту завербовать? Один раз нормально распиши, а потом копипасть на однотипные ответы, довен.
>>21444 >Во-первых, ты не можешь, ты вероваешь, что можешь. Смотри, у нас есть множество действительных числе R. Я беру и выбираю из него такое число x, что оно будет меньше 3 и больше 2.
>>21447 >Смотри, у нас есть множество действительных числе R. Я беру и выбираю из него такое число x, что оно будет меньше 3 и больше 2. И что дальше? Получаем дискретизацию континуума вещественными числами. Континуум не сводится к множеству R, т.к. между двумя вещественными числами всегда можно вставить еще. Даже если применим абстракцию потенциальной осуществимости и предположим, что такое деление можно вести сколько угодно далеко, все равно итогом будут вещественные числа, но не континуум. >>21446 >Почему вместо нормального объяснения Я не виноват, что вместо того, чтобы вникать в объяснения, ты закатываешь глаза и начинаешь кукарекать. >Один раз нормально распиши Я каждый раз нормально пишу. Нужно пытаться понять, а не кукарекать. >Хочешь меня так в свою секту завербовать? Деревянные по пояс тут точно не нужны. Правильно Максимка говорил, что в рашке никто не может в зависимые типы.
>>21451 >Я не виноват, что вместо того, чтобы вникать в объяснения, ты закатываешь глаза и начинаешь кукарекать. Посылание читать Брауэера это не объеснения. >Я каждый раз нормально пишу. Ты даже сейчас не можешь нормально писать и скатываешься до оскорблений. Давай ссылку на пост с нормальными объяснениями, раз писал. >Деревянные по пояс тут точно не нужны. >— Ты издеваешься. Ты не можешь писать это всерьёз. >— Я не виноват, что ты такой тупой.
>>21462 >Посылание читать Брауэера это не объеснения. Да ну, какой тебе Брауэр, ты вышеупомянутую книжку для дошкольников не осилишь. Хотя если бы осилил, много откровенно тупых вопросов бы отпало, там реально хорошо объясняют, лучше чем я. При всем неуважении к совку, научпоп там был мирового уровня. Но тебе не нужны объяснения (да, я сто раз объяснял, можешь опять вспомнить свою пасту), ты изначально исходишь из предположения, что я неправ, и уже с этой позиции рассматриваешь все остальное, безотносительно к его содержанию. Мне-то похуй, одно непонятно, зачем тогда тебе вообще сюда писать и пытаться что-то кому-то доказать. >>21456 Вот как пример, что можно доказать тому, для которого абстракция и вера это одно и то же? Тут вообще говорить не о чем.
>>21467 >Да ну, какой тебе Брауэр, ты вышеупомянутую книжку для дошкольников не осилишь Я не собираюсь читать какие-то книжки для того, чтобы доказать свою правоту анону с двачей. Это лишнее. >ты изначально исходишь из предположения, что я неправ, А я должен был считать изначально, что ты прав? У тебя не получилось доказать свою провату, и каждый раз ты только и делаешь, что уходишь от ответа: Ну ты типа тупой, не поймёшь))) Иди Брауэра читать))) Да я уже сто раз объяснял))) Это вера а не математика))) Хватит уходить от вопросов, нам нужны ответы! >да, я сто раз объяснял Тогда дай ссылки на посты с объяснениями. А то только можешь отсылать читать свои книжки, да скиншоты лепить. Ты сам видно не до конца понимаешь всю эту мутотень с основаниями и поэтому нормально объяснить не можешь. >Вот как пример, что можно доказать тому, для которого абстракция и вера это одно и то же? Континуум или трансфитная индукция тоже абстрактная вещь, но ты называешь его верой.
>>21468 >Я не собираюсь читать какие-то книжки для того, чтобы доказать свою правоту анону с двачей. А что ты мне можешь доказать, если не понимаешь разницу между верой и абстракцией и между трансфинитной индукцией и континуумом? Смешно даже читать такое. А книжки нужны не для того, чтобы что-то кому-то доказать и самоутвердиться, а чтобы в вопросе разобраться. Для этого читать книжки - норма. К слову, это не ты тот деятель, который еще зимой обещал меня разгромить, доказав мне неправильность MLTT?
>>21505 >Который сам почему-то отзывается об интуиционизме неприязненно. Называя Брауэра "замечательным математиком"? Но допустим, в целом это возможно, ведь в совочке брауэровский интуиционизм считали буржуазным идеалистическим учением, в отличие от конструктивизма, который с вычислительной точки зрения то же самое. Опять же, если ты этого не можешь понять, почему это должны были понимать выжившие из ума старперы из КПСС? Они и логицизм Рассела считали тем же самым и даже заявляли, что это причина того, что Рассел призывал разбомбить совок ядерным оружием.
Есть вещи, которые невозможно вычислить или узнать через машЫну. Есть истины, которым нет объяснения. Исходя из этого, именно в этот момент в сознании людей появляется вера во что-то сверхъестественное (и это не плохо). Об этом еще Гедель писал. Кончайте уже со своим конструктивизмом выебываться. Машина не может дать истинные ответы на все вопросы.
Зависимые типы я осилил, а вот исчисление конструкций пока нет. Чем примечательны, полезны, красивы исчисления конструкций, если объяснять для чайника?
>>21509 Хорошая книжка, автору сразу можно помочиться за шиворот и отправить доучиваться. Классическая матлогика не рассматривает смысл (т.е. семантику) выражений вообще, от слова никак. Там только синтаксис, о чем писал и Гильберт и Бурбаки. >>21534 > исчисление конструкций пока нет. С Барендрегта начни. Исчисление конструкций - просто наиболее полное лямбда-исчисление по Черчу, т.е. в кубе Барендрегта.
>>21509 На пикрелейтед месте можно окропить автора уриной еще раз. Он даже конструктивное отрицание не осилил. "Недоказанный" и "неверный" конструктивно абсолютно разные понятия.
>>21566 Где книшку-то взял? На либгене нету. >Ссылаешься на него как на большого авторитета На конкретную книгу, которую читал лично и в которой ошибок не обнаружил.
>>21445 В принципе, конструктивно, как мне кажется, это можно доказать. Если я хорошо понимаю суть конструктивизма(а я узнал о нем из этого треда), то конструктивное доказательство будет выглядеть так:
У нас есть сумма (сложнее сумму возьмем): a/b+a/b²+a/b³+...+a/b^n = S. Но n – конечно, хоть и очень большое. И, чем больше n, тем смелее можно пренебречь последним членом суммы. Поэтому, для довольно больших n имеем:
Все же, я не понимаю, чем конструктивистов не устраивает бесконечность. С ней ведь размышлять удобнее. Но, на самом деле, можно сформулировать бесконечность таким образом, чтобы ее смогла юзать и машина. Однако самого смысла она не поймет, очевидно.
>>21956 Как я и говорю, основная проблема местных поциентов - категорическое неумение пользовпться головой. В нее не только кушать можно, прикинь. Вот твой вопрос, объясни, к чему он вообще? Ты ни разу не слышал, что даже некоторые калькуляторы могут считать комплексные числа, не говоря о любом нормальном языке программтрования? А если комплексные числа построимы, т.е вычислимы, что можно сказать об их конструктивности, сам догадаешься, или это слишком сложно?
>>21960 Некоторые калькдяторы и бесконечность считают, мнимания единица имеет другию прировуд. Вот число один -это число. Но мнимая единица не имеет алгоритма построения.
>>21991 > Некоторые калькдяторы и бесконечность считают, мнимания единица имеет другию прировуд. Вот число один -это число. Но мнимая единица не имеет алгоритма построения. Ты читать не умеешь? Вычисление это построение.
>>21993 > Комплюктор не ПОНИмает сути производимых операий. Суть, семантика производимых операций в MLTT это вычисление, т.е получение канонических элементов. Комплюктер понимает вычисление иак же как и не комплюктер, ты никогда и не при каких обстоятельствах не сведешь вычисление к тому, к чему его не сведет компьютер, следовательно твое понимание вычисления равнообъемно с компьютерным. И это сто раз уже писано, просто вы все иута деревянные по пояс.
>>21996 > Как можно построить мнимую единицу? А как нельзя? Ее даже нарисовать можно, погугли. Суть построений в вычислимости, еще раз говорю. Построение это вычисление, ферштейн, нихт?
>>22005 > Откуда взялось i? Мы просто верим, что существует число, равно в квадрате -1? Верования невычислимы, конструктивные объекты вычислимы. Комплексные числа вычислииы. Так ясно?
>>22011 > Это семантика. Всё равно, что сказать бесконечность = /inf. Тебе тролить тупостью не надоело? Конструктивно семантика это вычисление. Эта твоя запись /inf не вычислима ни во что, т.к не является каноническим элементом, не является она и неканоническтм элементом, поскольку не имеет правил вычисления в канонический элемент. Аллаха опять же в этой связи уже обсуждали. И открой для себя гугл, разберись с любым алгоритмом вычисления комплексных чисел, а не пиши одно и тоже сюда сто раз.
>>22019 Как и любое вычисление? Давай, покажи вычисление комплексного числа, не сводящееся к вычислению, ебани духовненько, а не как бездушный кудахтер.
>>22021 Я уже очень, очень много раз говорил чем. Последний раз в этом посте >>22012 но ты не вертись, а показывай свой вариант вычисления комплексных чисел >>22020
>>22024 Хватит кидать ссылки на книги. Я так же могу обсуждать работу мочидзуки, а когда у меня что-то спросить, то дать ссылки на статьи, и сказать сто раз обсуждалось, там же написано. Берёшь и объясняешь всё с нуля.
>>22025 >Я так же могу обсуждать работу мочидзуки Какой тебе Мочидзука, ты ж элементарное понятие вычислимости осилить не можешь. Ты даже понятие равенства по этой лекции >>21607 не осилишь.
>>22028 Неужели для того, чтобы понять твою аргументацию, нужно читать все эти жуткие сотни страниц и смотреть многие часы лекций? Классическую теорию множеств можно изложить за несколько минут, аксиоматическую вплоть до форсинга - за вечер.
>>22029 В MLTT 4 суждения, 4 правила вывода, 4 основных типа и 4 правила построения выражений. Все это можно уместить на половину тетрадного листа. Тетраграмматон рабби Лёфа прост как 4 шекеля. Проблема только в том, что за всем этим стоит не пустой синтаксис ни о чем, как в формализме, а вычислимая конструктивная математика, где даже понятие равенства имеет вычислительное содержание. Это вам не невычислимые ни во что кардиналы и прочих Аллахов рисовать, тут уже не глиняная голова нужна, чтобы въехать.
>>22033 Аксиомы исчисления предикатов тоже немного места занимают. А книг с нормальным изложением меньше чем на сотню страниц так же нет. Поэтому возражение не принимается.
>>22034 Бурбаки. Вся лежащая под математикой логика, включая исчисление предикатов, занимает страницы 31-65. Из них на собственно исчисление предикатов отводится четырнадцать страниц.
>>22037 >Бурбаки Пикрелейтед. >Вся лежащая под математикой логика, Не вся, ZFC не может в типы, а за что-нибудь уровня NBG у бурбаков нет ничего. >занимает страницы 31-65. Из них на собственно исчисление предикатов отводится четырнадцать страниц. Вся книжка Мартин-Лёфа 50 с небольшим страниц, собственно изложение самой теории даже не половина https://github.com/michaelt/martin-lof/blob/master/pdfs/Bibliopolis-Book-retypeset-1984.pdf
>>22038 На твоём пике математика в объёме, превышающем кандидатский курс (гомологическую алгебру не изучают даже в магистратуре, например). Речь шла о предикатах онли. Короче, показывай листок. >за что-нибудь уровня NBG Аксиоматика Бурбаки строго сильнее ZFC. Не слабее чем NBG+аксиома глобального выбора.
>>22039 К этой картинке пояснений как раз под сотню страниц и нужно. Из самой картинки не выведешь тау (или эпсилон Гильберта) и т.д. Ну и главная претензия - вычислимость, конечно. Даже не исключенное третье, с этой хуиткой все ясно, вот самая последняя строка, А5. "Существует бесконечное множество", вот и Аллаха подвезли. В каком смысле оно существует? впрочем, все это опять же уже сто раз обсуждалось, сейчас пойдут аргументы про чернильную дыру и про то что актуальная бесконечность не хуже потенциальной осуществимости, бла-бла... К MLTT так не доебешься, пример - лекция выше, там даже равенство сводится к вычислимым построениям, а не просто к значку "=".
>>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 связей, то есть полная запись терма, обозначающего единицу, заняла бы сто миллиардов квинтиллионов квинтиллионов книг
>>22053 Зачем тебе с ординалов фон Неймана так бомбануло? И чем они хуже аутизма уровня гильбертовского эпсилона, при использовании которого получаются термы размером в квинтиллионы знаков?
>>22042 >В каком смысле оно существует? Бессмысленная строка символов, которая в естественный язык транслируется как "существует бесконечное множество", является аксиомой.
>MLTT так не доебешься Либо ты постишь листочек, либо ты - всего лишь ещё один сосачеребенок.
>>22059 >Это, конечно же, вздор Сильное заявление... Обсирают бурбакистов, конечно же, бетежки которые не смогли их осилить, а не из за того что книги переусложненная хуйня.
>>22067 В книгах Бурбаки нет ничего "переусложненного", они очень легко читаются (пикрелейтед). Вообще, это такой детектор очень хороший: кто считает Бурбаки чем-то сложным, тот некомпетентный лапоть с шерстью на ушах.
>>22059 >Либо ты постишь листочек, либо ты - всего лишь ещё один сосачеребенок Что ты разнервничался? Вон же у Максимки все есть http://groupoid.space/mltt/semantics/ с нескучным оформлением. Педивикия опять же. >Это, конечно же, вздор. Это эпсилон Гильберта, формализм курильщика. >>22069 >Вообще, это такой детектор очень хороший: кто считает Бурбаки чем-то сложным, тот некомпетентный лапоть с шерстью на ушах. Школьца-максималиста в тебе вижу я.
>>22069 Иначе говоря, то что первый параграф ссылается на вторую главу, параграф шесть, пункт номер один, это признак хорошего, годного легко читающегося учебника. Это ты так двачи тролируешь тупость или реально такой дурачек?
>>22071 Хорошо, теперь давай по порядку. Что по Мартин-Лёфу есть proposition и что есть judgement? В предложенных тобой книгах эти термины используются, но определений им не дано.
>>22072 >ссылается Впервые математическую книжку увидел, да?
>>22072 У бурбаков проблема не в этом. Я даже соглашусь, что это хорошая литература. А в том, что при попытке полной формализации того, о чем они пишут, мы очень быстро упремся в квинтиллионнобуквенные термы. Там же они с самого начала пишут, что для удобочитаемости текста он почти полностью состоит из соглашений, вольностей речи и т.д., откуда и столько отсылок к ранее определенным вещам. В MLTT такой хуйни нет, там все можно свести к вычислениям и вычислить полностью. >>22073 >Что по Мартин-Лёфу есть proposition и что есть judgement? В предложенных тобой книгах эти термины используются, но определений им не дано. Попочтец, плиз. Самая первая страница. Пропозишен = формула в матлогике (и множество, согласно изоморфизму Карри-Говарда), суждение = теорема. Совсем подробно - 4ая глава в programming in martin-löf's type theory.
Спешите видеть, илитные математики-бурбакисты не могут досчитать до двух. В то время как обычные пятимесячные младенцы УЖЕ умеют считать до двух. Вот пруф https://books.google.com.ua/books?id=s5KqmjDyxTMC&printsec=frontcover&hl=ru#v=onepage&q&f=false Если откопаете полную версию то сможете узнать что даже макаки-резусы умеют считать до трех. Тобишь буракисты это даже не уровень человеческой личинки. Они хуже макак.
>>22075 Я видел этот текст, и он мне непонятен. Прошу объяснить. Я прочитал столько книжек, что слово "формула" для меня не имеет само по себе никакого смысла, увы. >из соглашений, вольностей речи и т.д. Из сокращений; это другое. Это не неформальность, а лишь инкапсуляция и абстракция. Любую главу трактата можно рассмотреть как набор аксиом некой новой формальной теории, а все предыдущие главы забыть. В этой новой теории букв в знакосочетаниях будет гораздо меньше. Кроме того, трактат можно дополнить минус первой, минус второй и сколь угодно более низкоуровневыми главами - общность при этом будет повышаться, сложность грамматики - падать, количество букв в знакосочетаниях - увеличиваться. Например, язык начальной главы можно транслировать в морзянку. Математика окажется в таком случае теорией о громадных совокупностях точек и тире.
>>22077 >а лишь инкапсуляция и абстракция Считающаяся в термы из квинтиллионов знаков. Это проблема, пони маешь? Потому что если мы захотим это на самом деле посчитать, то... >Я прочитал столько книжек, что слово "формула" для меня не имеет само по себе никакого смысла, увы. Значит, неправильные книжки читал. Я ж уточнил, что "формула" там имеет значение, обычное именно для матлогики. Ну и также можно считать пропозишен множеством. >>22078 >когда говорят, что бесконечности нет Ты для начала пойми о чем вообще тут говорят, потом в разговор лезь.
>>22079 >в термы из квинтиллионов знаков Только если считающему угодно настолько сильно углубиться в абстракцию. Он вполне может остаться на одном из более высоких уровней, на них символов будет заметно меньше. Например, можно отказаться от трансляции кванторов и импликации, приняв их в синтаксис, тогда квинтиллионы мгновенно исчезнут. Алсо, не в термы, в знакосочетания. >обычное именно для матлогики Произвольная формула? Правильно построенная формула (элемент наименьшего класса формул, замкнутого относительно логических связок и содержащего все атомы)? Выводимая формула? Меня "hold to be true" смущает, это вообще о чем.
>>22080 >Меня "hold to be true" смущает, это вообще о чем. Изоморфизм Карри-Говарда же. И интерпретация логических констант по Брауэру-Гейтингу-Колмогорову. Общеизвестно, что логические операции это то же самое, что операции над множествами. Истина - это 1, ложь = 0. Классически пропозишен - это функция принадлежности или характеристическая функция, принимающая значение 0 или 1 (не считая многозначных логик). Логическое "и" это пересечение множеств, "или" - объединение, импликация - отношение подмножества. Конструктивно же пропозишен - это множество пруф-объектов, т.е. построений, доказывающих, что данное множество не пусто. Т.о. по упомянутому изоморфизму Карри-Говарда, истинность пропозишена А - это ненулевое количество элементов х принадлежащих А, х:А. Доказательство "не А" - это построенное пустое множество. Отсюда уже видно, почему исключенное третье в общем случае не работает. Классически верно правило "А или не А", конструктивно мы должны доказать конкретно, А или не А, т.е. пусто множество А или нет. Это можно сделать только построив его. Конкретные методы построений получаются интерпретацией логических констант по Колмогорову, т.е. в простейшем случае это могут быть лямбда-термы, а все вышесказанное в таком случае можно свести к типизированной лямбде, откуда вычисление это есть лямбда-определимость. Итд итп. >Только если считающему угодно настолько сильно углубиться в абстракцию. Он вполне может остаться на одном из более высоких уровней, на них символов будет заметно меньше. Классически и так сойдет, конечно. тяп-ляп и готов кризис оснований Конструктивно нам нужна полная вычислимость, чего с бурбаками не выйдет вообще никак.
>>22081 >логические операции А как быть, если нужны нелогические операции? От голого исчисления предикатов мало пользы, пользу приносят первопорядковые теории (исчисление предикатов плюс нелогические формулы). >операции над множествами Для корректности такого подхода нужно зафиксировать метатеорию множеств и внятно определить предметную область. Неоправданно сложный подход, чисто синтаксический подход гораздо яснее (а всё семантическое надстраивается на него в теории моделей). >построений Что считается построением? >полная вычислимость Вычислимость бесконечна вниз, если можно так выразиться. Всегда можно заменить атомарное действие фиксированного исполнителя подпрограммой для более низкоуровневого исполнителя. Полной вычислимости не бывает.
>>22083 Собственно, на все вопросы в твоем посте ответ один - типизированная лямбда. >Вычислимость бесконечна вниз, если можно так выразиться. Только до канонических элементов, которые дальше невычислимы ни во что.
>>22085 По определению - замкнутые, насыщенные лямбда-термы нулевой арности. Ну или категоремы. Элементы, которые нельзя вычислить во что-то нижележащее, т.к. они сами по себе есть итоговые значение вычислений. Пример - натуральные числа, как элементы множества N они не сводятся к чему-либо более простому.
>>22087 >Для натуральных чисел можно предложить много нижележащих теорий, разве нет? Вычислимых-то? Думаю, строго 0. Ниже нумералов Черча сложно что-то придумать, даже ординалы фон Неймана - это то же яйцо, вид сбоку. Впрочем, можешь и предложить, думаю медаль филдса за таконе точно не пожалеют.
>>22088 Теория, предложенная Бурбаки. Если не вводить теорию множеств во всей полноте, то арифметические построения можно описать знакосочетаниями вида пикрелейтед длиной не более чем в несколько миллионов символов (грубая оценка сверху, на самом деле меньше). Вполне реальный объём для современных компьютеров.
>>22089 Эпсилоны Гильберта считать со всеми квинтиллионами знаков? Вот ты спрашивал, что есть канонический объект. Вот этот хулиардквадриллионный терм для единицы - это как раз канонический элемент множества N по бурбакам, который ниже уже ни во что не считается. Это можно, конечно. Но грустно, когда ферма из асиков размером с взлетную полосу, будет считать 1+1 пару дней. Самое обидное, что итоговый результат будет тот же, что с нумералами Черча, т.е. натуральное число 2, которое, конечно можно представить еще какими-то квадриллионными термами, но остается вопрос - нижестоящая ли это теория или таки вышестоящая, т.к. использует более сложный алфавит, чем н-р натуральное число как слово в алфавите | по Маркову?
>>22091 >То есть канонический элемент - это всего лишь терм в формальном языке, который выбран для аксиоматической теории? Точнее терм, который в данной теории нельзя свести ни к чему нижележащему. Но тут уже встает вопрос математического релятивизма (не путать с физикой), согласно которому, любую теорию можно выразить через любую другую, точнее между теорией А и В существует конечное количество теорий А1-Ан, причем теория А выразима в теории А1, а теория Ан - в теории В. В таком случае без разницы, какую теорию считать первичной, т.к. мы все равно можем придти к любой из них из любой другой. Чисто прагматически, более первичной удобнее считать более простую теорию, т.е. уж точно не стоит считать эпсилон-исчисление Гильберта основанием арифметики, потому что полнейший аутизм сначала учить детей в школе эпсилон-исчислению, а затем решать примеры 1+1. Конструктивно всю математику можно вывести из арифметики, прагматически это самый простой путь, гораздо проще и естественнее чем теория множеств, тем более в виде бурбакизма. Естественнее, потому что доказано, что понятие натурального числа врожденно и предшествует даже языковым способностям (такие нейрофизиологические модели как ATOM Уолша и теория метафор), если с более философской стороны, то Кант и Брауэр.
Бывает разная простота. Есть простота для решения задач, причем для разных классов задач простотой окажется разное - например, для решения уравнений вида x+a=b бурбаки очевидно не будут самым простым выбором. Есть простота для доказательства теорем, и вот здесь уже может оказаться наиболее простым выбором, скажем, определять дроби с помощью деления в столбик (анекдотический пример от Арнольда). Универсальной простоты не бывает.
>>22103 > Правильно, зачем чукче думать, пусть пекарня думает А чем твои думы в области математики, чукча, отличаются от дум пекарни в этой же области? Я просил привести примеры вычислимости, не сводящиеся у механическим преобразованиям выражений. Пока примеров не поступало.
>>22108 > Не вся математика сводится к вычислимости. Старые песни о главном. Если что-то невычислимо, с какой стати это вообще математика? И да, что в математике не сводится к вычислимости? Исключенное третье, актуальная бесконечность и прочая религия?
>>22110 > Это ты сужаешь математику на computer science, ограничевая его её алгоритмами. Примеры, примеры в студию. Что в математике не сводится к алгоритмам, где математика, не являющаяся преобразованием знакосочетаний и термов по заданным правилам? Формализм без формализма, давай примеры.
>>22118 Ясно. Вчера по бурбакам пояснил за все эти сокращения, соглашения итд, остальное по аналогии. Не считая того, что в mltt аксиома выбора это не аксиома, а теорема и ее можно доказать. Тоже сто раз уже писал, давал ссылкуи постил скрины.
>>22125 > там нет алгоритмов Есть правила работы с этим. Есть то, откуда это вывели, есть следствия, к которым это приводит. Если у тебя от слова 'алгоритм' бампельштильцхен, это не ко мне. И обяснять вещи, которые уже 3хлетний бы понял, мне так же неинтересно. Ты даже не можешь объяснить о чем речь вообще, мне это и темболее не нужно.
>>22092 А есть идеи как учить школьников конструктивной математике? В смысле, наверное, большей работы со средствами доказательства теорем или что-то такое. Или может еще что?
>>22137 Лямбда исчисления вполне можно изложить так, чтобы понял школьник. Тем более, что всю домашку можно сразу писать и проверять в коке. Другой вопрос, зачем.
>>22136 > С аксиомой выбора так же. Есть следствия, к которым она приводит. И что дальше? Ты хочешь сказать, что это не укладывается в понятия формализма, нотации или допустимых преобразований выражений, термов или знакосочетаний? Или что ты доказать-то пытаешься?
>>22151 Я ради стипухи взял одно недоказанное (оставим читателю в качестве упражнения) утверждение из маклейна и тиснул статью с его доказательством. Стипуху дали.
>>22170 Алгоритмами её точно не решить. Но это не значит, что без алгоритмов её решить нельзя. Ты же сам вроде должен быть против исключённого третьего?
>>22170 Да и вообще по твоей логике должен существовать единый алгоритм доказательства теорем. Даже конструктивные доказательства предполагают некоторый рывок во вне и этот рывок в каждом случае уникален. Так что если с вычислимостью и построением ещё можно понять и согласиться, то вот аппелировать к алгоритмической разрешимости уже полная ересь даже с точки зрения конструктивизма. Ты сам, похоже, до конца не понимаешь что такое конструктивность.
>>22170 То есть у тебя есть правила языка, ты можешь переводить на другой язык с помощью алгоритмов и тд, но ты не сможешь написать осмысленный текст, можно перебрать все варианты из существующих и тем самым доказать, что других вариантов нет, но сами эти варианты алгоритмически не найти, для этого нужен некий критерий закономерности, когда машина решает, является ли что-то закономерным, определяет что, обобщает и затем уже подтверждает или опровергает это конструктивно. Именно поиск закономерностей, обобщение и > не сводится к алгоритмам, где математика, не являющаяся преобразованием знакосочетаний и термов по заданным правилам
>>22159 Математика - это как игра в шахматы. Если не знаешь как ходят фигуры, то и играешь неадекватно. Строгие формальные доказательства обучают простейшим ходам.
>>22171 >Алгоритмами её точно не решить. Но это не значит, что без алгоритмов её решить нельзя. Демагогия. >>22172 Я уже просил не нести хуйни. Алгоритмически неразрешимые задачи никто не отменял. >>22173 >Именно поиск закономерностей, обобщение и не сводится к алгоритмам, где математика, не являющаяся преобразованием знакосочетаний и термов по заданным правилам И еще раз прошу не нести хуйни. То, что ты описал, называется идентификацией систем и реализуется очень большим количеством алгоритмов. Итого, ты не в теме абсолютно, а разжевывать такие азы мне неинтересно вообще никак.
>>22181 Ну так я сколько раз уже просил показать неалгоритмическое решение любой алгоритмически неразрешимой проблемы. Примеров нет. Их и не будет, поскольку например, из нас двоих кто-то не знаком с работами Тьюринга и Поста. И кто бы это мог быть, как думаешь?
>>22179 >Демагогия. Лол что? Ты пишешь , мол, раз алгоритмически задача неразрешима, то она неразрешима впринципе. Я говорю, что одно из другого не следует. Где тут демагогия? >То, что ты описал, называется идентификацией систем и реализуется очень большим количеством алгоритмов Например? >Я уже просил не нести хуйни >И еще раз прошу не нести хуйни. >Итого, ты не в теме абсолютно, а разжевывать такие азы мне неинтересно вообще никак. Демагогия.
>>22189 >Ты пишешь , мол, раз алгоритмически задача неразрешима, то она неразрешима впринципе. Я говорю, что одно из другого не следует. Где тут демагогия? Давай так, пока не принесешь примера решения неалгоритмическими методами алгоритмически неразрешимой математической проблемы, можешь мне вообще не писать. У меня нет никакого желания даже пытаться объяснить человеку, не слышавшему про тезис Черча, из чего конкретно следует общая неразрешимость алгоритмически неразрешимых задач.
>>22189 >То, что ты описал, называется идентификацией систем Ну и да, это не то, что я описал. Я о том, что, например, нет такого алгоритма, который бы, например, получая на вход последовательность чисел 2 5 12 27 58 121 ... мог бы найти закономерность, "догадаться", что это 2n-n или 2*предыдущее+номер. Разве такие алгоритмы есть? Человек же такую задачу может решить, потупив в последовательность минуту.
>>22190 >пока не принесешь примера решения неалгоритмическими методами алгоритмически неразрешимой математической проблемы >>22191 Вот это, я полагаю. Ну если она алгоритмически разрешима, то давай ссылки, буду читать.
>>22190 > из чего конкретно следует Нет, не следует. Перечитай, о чём он говорит. >Алгоритмически неразрешимо Или вот ещё пример. Нужно найти натуральные корни. x5+2x3+3x2-60=0 По теореме Абеля — Руффини не существует формулы, алгоритма по которому можно найти корни этого уравнения, но подставив 2, догадавшись, мы получим решение. По твоему это уже не математика, а гадание на Аллахе?
>>22194 >не догадался Нет, вчера с корешем эксперимент проводили, он загадал вот эту последовательность и нужно было найти закономерность, правда мой ответ был, что это a(n+1)=2a(n)+n, но не суть. >обобщил Вот это тоже, в математике это повсюду, а что это вообще? Как происходит обобщение? Как это алгоритмизировать?
>>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. А вот теперь точно уебывай, потому что детский сад - это не тот уровень, на котором мне было бы интересно дискутировать.
>>22195 >гадание на Аллахе Как бы да, это и правда оно, как и доказательство от противного, ведь есть разница между построением объекта и доказательством того, что несуществование объекта противоречиво. Но решение ведь есть. И таких примеров использования Аллаха в математике сотни. >>22197 Но следующее число 248, лол. Регрессия.
>>22198 Это простая линейная регрессия на датасете из 3х значений. Естественно, что это не самый лучший метод из существующих. Дело не в этом, а в том, что ты своеим неопниманием пытаешься что-то доказать. Буду репортить троллинг тупостью, в общем.
>>22217 Тем что ты не почитаешь их все. На основании аксиомы о непрерывности числового ряда ты можешь бесконечно делить числа и получать новые и новые числа, конца края этому не будет из за того, что исходя из аксиомы о непрерывности...
>>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)
>>22222 Короче, это же числовой ряд, из которого я сделал матрицу Ганкеля. Линейная регрессия недостаточно точно аппроксимирует такие нелинейные значения, да еше и датасет из 3х пар, но мой результат почти такой же как у этого шизика, а твой в 2 раза неправильный.
>>22235 >Там пары значений Так y от x должно зависеть,а ты просто взял значения y и поделил их на две части, лол. >х - просто последовательность натуральных чисел от 1 до 6 Ну правильно, y=2x-x, > твой в 2 раза неправильный. Да он и не должен быть правильным, как ты вообще умудрился применять линейную регрессию, когда очевидна эксп зависимость. То, что у тебя получилось "почти такой же" простое совпадение.
>>22241 >То, что у тебя получилось "почти такой же" простое совпадение. Это не совпадение, а аппроксимация. Точной она и не могла быть, т.к. зависимость нелинейная, а я использовал линейную регрессию + датасет никакой. Еще раз: из датасета была сделана матрица Ганкеля, что соответствует NARX-модели а потом линейной регрессией была проведена идентификация системы y = f(x). Регрессией т.о. была получена аппроксимация функции f, но т.к. в реальной системе эта функция нелинейна и датасет размером близок к 0, то вышла некоторая, согласись, довольно небольшая ошибочка для данных условий. Похоже, кроме меня про такое никто не слышал? Страшно вы живете, а.
>>22242 Лол, согласись, что аппроксимация рекуррентного соотношения это всё равно, что сказать "нуу каждый следующий член больше предыдущего примерно в два раза". Это не решение проблемы.
>>22243 Линейная регрессия - не решение нелинейной проблемы. В остальном идентификация систем как раз для нахождения неизвестных зависимостей выходов от входов. Даже кусочно-линейная аппроксимация (скажем, моделью Такаги-Сугено) функции выхода от входа на таком датасете была бы точнее. Ну и про теоремы об универсальной аппроксимации тут тоже не слышали, эх, африка.
>>22244 Аппроксимация вообще не решение, понятно, что аппроксимировать много чего можно, речь шла о том, как алгоритмически получить из данных точную формулу, породившую их. Неалгоритмически это сделать можно.
>>22245 >речь шла о том, как алгоритмически получить из данных точную формулу, породившую их. Неалгоритмически это сделать можно. Во-первых, идентификацией системы это сделать можно. Конкретных примеров полно. Во-вторых, то, что ты называешь "неалгоритмически" на самом деле алгоритм. >>22250 Я понял твой уровень знаний в этой теме, дальше меня на эту тему можешь не смешить.
>>22251 >полно примеров Хватит нести чушь и заниматься демагогией, примеров полно так неси хотя бы один. > "неалгоритмически" на самом деле алгоритм Ага, всё алгоритм, просто мы ещё не поняли этого. Сектант. >уровень знаний >в любой непонятной ситуации lm(y~x,data=a)
>>22253 >примеров полно так неси хотя бы один. Одна из многих монографий в тему http://b-ok.org/book/448591/9b866b Просвещаем темное африканской быдло, прямо на мейлру!
>>22254 Берёшь и копипастишь оттуда сюда пример > как алгоритмически получить из данных точную формулу, породившую их. Я не собираюсь искать на тысяче страниц то, чего там нет. >применяет демагогию >называет кого-то быдлом Пока быдло тут только ты.
>>22265 благодаря соответствию карри-говарда можно сказать, что математика — computer science. >Computer science не математика В таком случае математика не математика
Спрошу тут,, вроде тред по теме :^) Есть одно задание "доказать ¬(p ↔ ¬p) не используя исключённое третье" Внизу код на lean с доказательством, но мне интересно - нет ли у меня лишних шагов и можно ли это доказать попроще? Я не знаю насколько сильно lean отличается от более популярного coq, т.ч. на всякий случай некоторые пояснения: mp - выделяет левую импликацию из iff, mpr - соответственно, правую implies.trans - естественно, транзитивность импликации Всё остальное думаю в приведённом фрагменте по идее должно быть понятно
мимокрок: Давайте переведём разговор в конструктивное русло. Мне кажется, что Lean - это продукт без бущущего, поддерживаемый исключительно Майкрософтовским пиаром.
Coq же - нечто интересное, но адекватно и продуктивно применимое только после получения кандидатской по математике...
>>22283 Лично я учу lean, потому что в его изучение проще заход, он написан на плюсах которые, в отличие от окамла, я знаю и кодобаза достаточно компактна и организована чтобы лазить по исходникам когда хочется понять как всё устроено, плюс мне неважна дропнутая поддержка HoTT А будущее его лично мне пофигу
>>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 всем спасибо
>>22299 >>22285 Поясните, как код прувера на крестах облегчает понимание лямбда-калькулюса, исчисления конструкций и т.д? Ведь для этого достаточно кода на том же коке или лине + понимания самих формализмов.
>>22302 я (>>22285) по сорцам собирался лазить не чтобы т.о. учить лямба-калькулюс и CoC а чисто из программерского интереса как оно написано, ну и плюс в лине наличествуют тактики частично/полностью на плюсах - можно будет разбираться как они работают.
Пони маете, ваша проблема в том, что вы не видите полной картины. Вы даже внятно не сможете объяснить зачем вообще нужны основания и аксиоматика и для чего там исчисление предикатов, например. С конструктивными основаниями в этом смысле все для вас еще хуже, все эти изоморфизмы карри'говарда, ВНК интерпретации, вычислимость, суждения, натуральная дедукция итд итп сами по себе требуют неких усилий для понимания, но еще хуже, что даже если отдаленное понимание присутствует, то все эти вещи не складываются в целую картинку, тому що мозгов у вас як у хлебушка где все естественно вытекает одно из другого, как итог, конструктивная математика, а уж тем более MLTT для вас выглядит как какая'то лютая оккультная ебулда, бессмысленная и беспощадная, хотя по факту все там просто и понятно.
>>22514 >все эти изоморфизмы карри'говарда, ВНК интерпретации, вычислимость, суждения, натуральная дедукция итд итп сами по себе требуют неких усилий для понимания Только если ты совсем отбитый.
>>22903 Прочитал у Максимки статью про MLTT, заинтересовало, почитал Мартин-Лёфа и с удивлением обнаружил, что нихуя не понимаю, о чем вообще речь, хотя изложено стройно и логично. Более пристально взглянув на эту тему, понял что причина в том, что за MLTT стоит нечто мне неведомое, из принципов чего и исходит Мартин-Лёф. Это и оказалось конструктивной математикой. Ну а там на каком-то этапе нагуглил Брауэра и понеслось.
Отрицание бесконечности и конструктивный подход гут. Отрицание закона исключённого третьего бэд. Есть ли где-то система оснований с первым без второго?
>>22902 Вернее 2013-го. http://arhivach.org/thread/5822/ Он здесь уже забивал последний гвоздь в крышку гроба формализма. Потом последовала череда подобных тредов, навроде теперешних, а затем он пропал.
>>22913 Не знаю конструктивных оснований в которых отрицается исключённое третье. Недоказуемость и отрицание это разные вещи. ¬¬(P ∨ ¬ P) теорема в большинстве "видов" конструктивной математики.
>>22925 Зачем для школьников, если скоро людям в математике вообще места не будет? Сделают поисковик по доказанным компом теоремам, только нужно будет научиться запросы правильные формировать и вся "человеческая" математика будет прикладной.
>>22925 >"конструктивизм и конструктивные доказательства интерактивно и в картинках для школьников" Для школьников смысла нет, в картинках тем более. Если не лезть в философскую сторону вопроса, во что тут все равно никто не может, то самый простой путь - осваивать кок. Возможно, самый простой учебник по коку - software foundations Пирса https://softwarefoundations.cis.upenn.edu/current/index.html
>>22988 Чем получше? Там с одной установкой пердолинга не оберешься https://hackage.haskell.org/package/Agda-2.5.2/readme + я не знаю внятных IDE под нее, емакс тот еще аутизм от аутистов для аутистов, как ни крути. Кок хотя бы в установке и использовании не сложнее блокнота.
Конструктивист - это умственно отсталый человек, для которого из истинности А не следует ложность не-А. О чём вы тут спорите с умственно отсталыми 4 треда подряд?
>>23436 Да мне похуй что ты там можешь доказать, бумага всё стерпит. Другое дело, что в реальности А либо истина, либо ложь, но даунам не достаточно доказательства того что А - истинна для того чтобы убедится что не-А - ложь, им нужно всё доказывать дважды, как будто бывает третье состояние когда А и истинна и ложь одновременно блять.
(Автор этого поста был забанен. Помянем.)
>>23451 >но даунам не достаточно доказательства того что А - истинна для того чтобы убедится что не-А - ложь Что ты несёшь, ебанутый? P => ¬¬P теорема даже в минимальной логике. >как будто бывает третье состояние когда А и истинна и ложь одновременно блять ¬¬(P ∨ ¬P) теорема в конструктивной логике.
>>23452 >состояние когда А и истинна и ложь одновременно блять Я тебя не так прочитал, ты оказывается ещё более тупой чем я думал. Это ничего общего с исключённым третьим не имеет, ¬ (P ∧ ¬ P) спокойно доказывается в конструктивных основаниях.
Шел уже десятый тред, если считать со /сци, а кое-кто так до сих пор и не понял, что конструктивное доказательство - это построение, а построение - это конструктивное доказательство. И кроме как их построений конструктивным доказательствам взяться неоткуда, а в особенности из каких-то априорных аксиом, в которые нужно веровать вместо собственно процесса построения или задания правил для построения, если уж касаться потенциальной осуществимости или lazy evaluation. Как так могло случиться, что в 21 веке кому-то греет попу необъодимость непосредственно доказать хотя бы один дизъюнкт для доказательства истинности дизъюнкции? Откуда такие хуйлопаны вообще берутся? Я не понимаю.
>>23518 >интересует вопрос удобства реального использования. С этим, как я понимаю, пока довольно печально. Потому что у большинства "врети" случилось еще во времена работ Поста, Тьюринга и Черча, который все это подытожил, написав, что найдены границы математических способностей человека. Хотя так и оказалось, и выше вычислимости все равно не прыгнешь, верунов и сейчас полно. Благо, прогресс не стоит на месте, и хотя реальной математикой занимаются единицы типа Мартин-Лёфа и Воеводского, уже сейчас видно, что все идет к полной автоматизации математики.
>>23519 Ну, в восьмидесятых тоже все бодренько так шло к полной автоматизации вообще любой интеллектуальной деятельности - чем все закончилось мы знаем. Так что я бы не был столь оптимистичен на твоем месте.
>>23520 >восьмидесятых тоже все бодренько так шло к полной автоматизации вообще любой интеллектуальной деятельности - чем все закончилось мы знаем. Ты о чем?
>>23530 Под верунами я подразумеваю верующих в то, что математика не равнообъемна вычислимости и существует математика, к вычислимости не сводящаяся (точнее, верующих в то, что нечто, не сводимое к вычислимости, вообще можно называть математикой). Под вычислимостью подразумевается вычислимость на машине тьюринга и др. равнообъемным уточнениям понятия алгоритма (лямбда-определимость, нормальный алгорифм Маркова и т.д.).
>>23519 >который все это подытожил, написав, что найдены границы математических способностей человека. Заскринил твой пост. Это пиздец.
>>23531 Это не математика, а комьютер саенс, и к математике отношение не имеет. Ты даже того же Энгелькинга не осилил. Прямо пропаганда Рыбников стайл.
>>23533 >Ты даже того же Энгелькинга не осилил Ты сам не осилил даже пояснить, зачем те скрины притащил. >Это не математика, а комьютер саенс, и к математике отношение не имеет. Ты ж сам писал, что в математике не понимаешь, что и так заметно, сейчас бы еще принимать во внимание непойми кого с мейлру, который непонятно с какого диагноза решил, что может опровергнуть Черча с Тьюрингом.
>>23535 >Ты сам не осилил даже пояснить, зачем те скрины притащил. Ты говорил, что никто не пользуется мощностями больше, чес счетно. На тех скринах было показано использование таких мощностей, хватит троллить тупостью.
>>23537 Ты никак не сможешь воспользоваться тем, что несчетно. Но ты всегда можешь написать значок бесконечности, алеф0,1,...,1488 и т.д. и думать, что пользуешься. Хотя по факту пользуешься значками, не несущими в себе ничего, т.к. содержимое, которое за ними предполагается, нельзя ни во что вычислить. Это и есть религия натуральная, поскольку у них там тоже есть значки, символ Аллаха, например. Суть примерно одна.
>>23540 Опять сотый раз по кругу обсуждать одно и то же не вижу смысла. Вещественные числа обсуждали, более того, Тьюринг в своей работе "On computable numbers" машину Тьюринга представлял как имитацию действий человека, вычисляющего такие числа. Отсюда проблема останова, бла-бла и т.д., что уже сто раз обсуждалось.
>>23544 Я уже сто раз говорил, что нет. Нет, нет, оно несчетно, т.к. это мощность континуума, а еще Брауэр показал, почему континуум невычислим. Итд итп.. Скушно, короче.
>>23553 Ну так я о том же не первый тред толкую. В случае вещественных чисел речь может идти только об аппроксимации его конечным количеством знаков после запятой.
>>23539 >Ты никак не сможешь воспользоваться тем, что несчетно. А скрины с Энгелькинга? Раз ими никто не пользуется, то почему практически в каждом учебнике анализа вводят множество R, мощность которого больше, чем Q. >Это и есть религия натуральная, поскольку у них там тоже есть значки, символ Аллаха, например. Суть примерно одна. Вопрос в том, что считать существующим. Почему, если множества вещественных чисел счетно, об этом не говорят в тех же учебниках матана, но вводят в заблуждение, говоря, что есть и другие мощности?
>>23558 И в чем проблема в бесконечном процессе вычисления?
>>23557 >Только когда нам нужно вычислить результат Естественно. Когда результат не нужон, можно и Аллахов подсчитывать. >>23559 >Пользоваться одним экономнее. Вот только это не пользование, а вера в пользование. Потому что настоящее пользование - это вычисление. И опять же, все это я уже не помню сколько раз писал.
>>23561 >Потому что настоящее пользование - это вычисление ТЫСКОЗАЛ? Вот это как раз сектанство. Напиши ты pi или 3,141592653589793238462643 что принципиально поменяется?
>>23560 >И в чем проблема в бесконечном процессе вычисления? В том, что оно не закончится никогда и сл-но, не может считаться вычислимостью. >>23562 >Что плохого в вере в пользование? В вере нет ничего плохого, веруй на здоровье. Вот только математикой свою веру называть не нужно.
>>23563 >Напиши ты pi или 3,141592653589793238462643 что принципиально поменяется? Сто раз писал, что. Даже в этом треде. Вы ж читать не умеете, какая вам математика.
>>23564 >В том, что оно не закончится никогда Ну например с рациональными числами там всегда будет период, да, будет повторяться бесконечно, но детерминированно, что плохого то?
>>23575 Вычисление может производиться по самым разным правилам. Вера в одно конкретное не делает его чем-то особенным. А вот связи между объектами остаются всегда, неважно, как ты их запишешь.
>>23576 >Поклоняетесь значкам без фактического содержания. Скорее это ты поклоняешься значкам, забивая на смысл, который они несут. Мельница-вычислитель перемалывает циферки, уаааууу.
>>23576 Ты так и не ответил на вопрос >Ты никак не сможешь воспользоваться тем, что несчетно. >А скрины с Энгелькинга? Раз ими никто не пользуется, то почему практически в каждом учебнике анализа вводят множество R, мощность которого больше, чем Q.
>>23587 >Я про вычисления в целом. Вот в том и проблема. Стоит разобрать любой конкретный пример и видно все содержание твоего "целого". >>23588 В этом треде пару раз.
>>23590 Обсуждалось в последнем десятке-другом постов. Вы просто эталон необучаемости, я думал, что необучаемее хохлозависимых в крымтреде не бывает, а вот нашел.
>>23593 Так ты ещё и /по/рашник, лол. Ну так давай ссылку или проследуй нахуй. Нихуя ты не ответил, я следил, спустил на тормозах свой обосрамс, думая, что никто не заметит.
>>23596 Сто раз писалось про канонические и неканонические элементы и выражения и т.д. Мне реально лениво каждую сотню постов переписывать все, мною уже сто раз писанное. Ну необучаемые вы тута, бывает. Для мейлру это норма, как и для рашки в целом.
Я писал даже, в чем тут проблема у большинства >>22514 вы никогда ничего не поймете, поскольку либо ничего для этого не делаете, либо делаете, но тема не ваша.
>>23628 Рамануджан очень кстати. Заниматься математикой без математического образования и культуры, не имея понятия о формализме как о методе вообще, можно только одним способом - манипуляцией с ментальными построениями.
>>23629 Есть книжка, мол, как стать как Сринивас из позиций конструктивной математики? Да и вообще "конструктивная математика и психология", "конструктивная математика и сознание", "конструктивная математика и эмоции" да прочее?
>>21361 (OP) Слышал про HoTT, разобрался в нём. Он, вроде какой-то в прямом смысле недоделанный. В чём его проблема? (Пишите смело факты) Вроде есть какая-то недоказанная гипотеза. Что она за зверь?
>>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.
>>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. Полностью конструктивной модели пока нет. >Есть более простые примеры, показывающие суть понятия? Машина Тьюринга.
Аноны, поясните за вычислимость утверждений формальной теории. Вот есть некая аксиоматическая теория и есть некое утверждение. Можно ли вычислить истино оно или ложно?
>>24026 Ты путаешь вычислимость и выводимость в формальной системе. Второе вообще никак не подразумевает первого. Возьмем например истинность формулы в исчислении пропозишенов. Поскольку классически, по закону исключенного третьего, пропозишен может быть истинный или ложный, то мы можем по методу Тарского нарисовать Аллаха таблицу с этой формулой пикрелейтед, из которой выводима ложность или истинность этой формулы исходя из ложности или истинности входящих в нее пропозишенов. В данном примере, классически эта формула истинна в любом случае. Прикол же в том, что конструктивно (исходя из интерпретации логических констант, в частности, свойств импликации, по Гейтингу) эта формула (известная как формула Пирса) невычислима.
>>24057 Формула F выводима, если существует хотя бы одна конечная последовательность формул, в которой последняя формула - это F, а любая предшествующая формула есть либо аксиома, либо получается применением модус поненс. Понятие "выводимость" не зависит от понятий "истинно" и "ложно".
>>24071 Такая-то самоуверенность. >пикрелейтед, из которой выводима ложность или истинность Как это понимать? При чем тут таблицы истинности? Понятно, что полнота исчисления высказываний и бла-бла-бла. Но речь о выводимости. Ты какие книжки по математической логике читал?
>>24054 А вот вы тоже напутали: формула Пирса невыводима в интуиционисткой логике, поскольку существует модель Крипке, где она не истинна.
Вычислимость функции - это про другое: существует такая машина Тьюринга, которая по заданным аргументам некоторой функции за конечное число ходов предъявит значение этой функции.
Так вот иногда доказательством импликации A->B является вычислимая функция f:A-->B, преобразующая доказательство утверждения А в доказательство утверждения B.
В силу неизвестных мне чудес(т.е. изоморфизму Карри-Ховарда) оказалось, что всё, что выведено из интуиционистских аксиом - может быть собрано из таких вычислимых функций.
То есть уже не надо заново строить машины Тьюринга - просто бери и пользуйся интуиционисткой логикой как конструктором. Оттуда и "конструктивизм", он же - "интуиционизм".
Невычислимо же - доказательство формулы Пирса, если его воспринимать как функцию.
---------------
Я это всё написал, но мне хотелось бы дополнительного контроля - всё же верно я рассказал?
>>24077 >Так вот иногда доказательством импликации A->B является вычислимая функция f:A-->B, преобразующая доказательство утверждения А в доказательство утверждения B. И именно в таких случаях мы можем говорить об истинности в конструктивном смысле слова. Поскольку суть конструктивной выводимости - вычислимость. А не общие недоказуемые заявления. >В силу неизвестных мне чудес(т.е. изоморфизму Карри-Ховарда) оказалось, что всё, что выведено из интуиционистских аксиом - может быть собрано из таких вычислимых функций. Интерпретация логических констант по Брауэру-Гейтингу-Колмогорову это называется. Конкретно чаще всего речь о конструктивной логике Гейтинга.
Давайте теперь представим, что некая теория легко описывается в классической логике и очень-очень трудно в интуиционисткой.
Зачем нам тогда вычислимый вариант?
Ав едь ещё он может и вообще не существовать... Тогда получается, что отказываясь от веры в одни формальные системы, вы впадаете в другую крайность, веря, что существует именно вычислимая формальная система, подходящая для любых стоящих перед вами задач.
Получается, что на стороне ваших оппонентов - проверенная годами практика, а на вашей стороне - только ваши, демонстрируемые на дваче, идеалы.
Это похоже на мечты, которые разрушил Гёдель, только в новой обложке.
>>24086 >Тогда получается, что отказываясь от веры в одни формальные системы, вы впадаете в другую крайность, веря, что существует именно вычислимая формальная система, подходящая для любых стоящих перед вами задач. Обсуждали уже. Да еще Тьюринг показал, что даже если к его машине приколхозить боженьку, могущего в решение алгоритмически неразрешимых задач, это ничего не решит, т.к. не снимает вопроса о проблеме останова уже прокачанной таким образом машины Тьюринга. Отличие веры от вычислимости тоже сто раз уже обсуждали. Границы математических способностей хоть человека хоть роботов - это вычислимость, как ни крути, выше не прыгнешь. Это тоже с 40-х годов прошлого века известно.
>>24087 >Границы математических способностей хоть человека хоть роботов - это вычислимость Эта фраза лишена смысла. Не отличается от фразы "направление лингвистических одаренностей арийцев - это гладиолус".
>>24115 Давай я тебе объясгю, почему это не так. Вот ты написал в своем посте то, что написал. Но почему ты так написал? Потому что тебе свербит, и обязательно нужно что-то мне ответить? Или потому что ты можешь доказать эти свои слова, например, конкретным примером, начисто опровергающим тезис Черча тут стоит заметить, что сама эта фраза принадлежит как раз Черчу? Я уверен, что опровергнуть тезис Черча ты не можешь, это если предположить, что его опровержение вообще возможно, хотя в настоящее время человечеству ничего такого неизвестно. Тогда о чем твоя батрушка вообще? Не пони маю.
>>24090 >веруны Во что веруны-то? Вычислимость - это непосредственный конструктивный объект, а не объект веры как всякие не считающиеся ни во что значки алефов и бесконечностей.
>>24120 Будь добр, приведи пример "конструктивного объекта". А то непонятно, что ты под этим подразумеваешь. (Объекты какие-то... Функция - понятно что такое, а объект - уже непонятно)
>>24123 >приведи пример "конструктивного объекта" Да я уже и не помню сколько раз приводил. Толку все равно 0. >Функция - понятно что такое, а объект - уже непонятно) И что по-твоему есть функция?
>>24118 >>24119 Начнем с того, что "границы математических способностей" - это вообще непонятно что такое. Утверждать, что некая неопределенная вещь является тем-то и тем-то, - безумие.
>>24155 >"границы математических способностей" - это вообще непонятно что такое. Я подозреваю, тебе вообще очень многое непонятно. И не только в математике. Причем тут определенность или неопределенность некоторых утверждений, а тем более их "безумность" не очень ясно. В данной фразе речь о предположительной равнообъемности математики и вычислимости. В пользу такой точки зрения можно привести тезис Черча. Говоря проще, до тех пор пока не получены примеры, опровергающие этот тезис, упомянутое утверждение можно считать истинным. На настоящий момент любой пример, известный человечеству подтверждает тезис Черча. Так что со своим школоцентризмом, основанным на твоем школомнении обо всем на свете, дул бы ты в школку, а не лез в вопросы, до которых тебе сильно дальше чем до луны пешком.
>>21361 (OP) Вычислимость - это действительно очень интересная тема.
Будем надеяться, что местный её фанат направит большую часть своей энергии в продуктивное русло вроде обсуждения с высокой строгостью необходимых теорем.
Если предлагать тему, то вопрос:"чем надозаниматься?" Где открыт фронт работ, доступный для студентоты с двачей?
>>24424 >Будем надеяться, что местный её фанат направит большую часть своей энергии в продуктивное русло вроде обсуждения с высокой строгостью необходимых теорем. Пробовал, не заходит. Закатывания глаз и кукареканья бесноватых начинаются примерно на фразе "изоморфизм Карри-Говарда". А без этого уже не объяснить, почему лямбдаР (AUTOMATH де Брауна, например) это то же самое, что исчисление предикатов. Про что-то более сложное (Кок тот же) и говорить нечего.
>>21602 >Просто пренебрегаем последним членом >И, чем больше n, тем смелее можно пренебречь последним членом суммы. Гармонический ряд обоссывает эту логику.
>>22030 >Проблема только в том, что за всем этим стоит не пустой синтаксис ни о чем, как в формализме, а вычислимая конструктивная математика, где даже понятие равенства имеет вычислительное содержание. Вот в чём твоя проблема. Ты приравниваешь синтаксические конструкции к смысловым, и из этого выводишь, будто твой конструктивизм чем-то отличается от формализма. Проснись, ты обосрался!
>>22079 >Считающаяся в термы из квинтиллионов знаков. Это проблема, пони маешь? Потому что если мы захотим это на самом деле посчитать, то... Ты с ума сошёл? Зачем каждый раз заново выводить всю предшествующую математику, если теорема - это и есть ёбанный квинтиллион знаков, полностью доказанный? Аксиомы-то остались неизменны, зачем каждый раз перепроверять вывод?
>>24449 >Тебе задают вопросы, а ты их игнорируешь. Мне начинают нести такую ахинею, что уши вянут. Вот типичный пример >>24454 какой-то школотрон думает, что опроверг интуиционизм в 2017 году. И что отвечать в таком случае? Я, разумеется, мог бы процитировать Брауэра https://projecteuclid.org/euclid.bams/1183422499 Гейтинга или Маннури по поводу разницы между интуиционизмом и формализмом, а она есть, и существенная. Но кто здесь хотя бы поймет о чем вообще речь? Никто, очевидно же. Тут чуть выше никто так и не въехал в разницу между классической и конструктивной логикой для формулы Пирса какие же вы деграданты, пиздец просто. Как итог, получу еще больше неинтересного мне кукареканья и истерик.
>>22514 >Вы даже внятно не сможете объяснить зачем вообще нужны основания и аксиоматика и для чего там исчисление предикатов, например. Чтобы не обосраться, как на пике - т.е. всегда применять методы, адекватные данным и задачам. Основания нужны потому что, как показывает практика, обосраться можно даже в элементарных вещах.
>>24456 >разницы между интуиционизмом и формализмом Всего-навсего другой набор аксиом, вот и всё. Но маняучёным не дают покоя лавры Пуанкаре, Римана и Гильберта, поэтому очень уж хочется сделать что-нибудь "особенное" поэтому они придумывают никому ненужные системы с крайне геморроидальным выводом даже простейших теорем и эпатажно отрицают то, что успешно применяется на практике годами.
>>24464 >Всего-навсего другой набор аксиом, вот и всё. Я тебя услышал, ага. А ничего, что у Брауэра вообще аксиом не было? А про логические отрицания ты что знаешь? По Маннури, конструктивное отрицание - это choice negation, отрицание в классической логике - exclusion negation. Из чего следует 4 разновидности только двойного отрицания, из которых только 2 эквивалентны утверждению (двойные choice и exclusion negation). Если их миксануть, интереснее получается. Но логика никому не интересна, проще ж веровать в аксиомы полученные Гильбертом в виде скрижалей на горе сион.
>>24465 Ты, похоже, плохо представляешь себе, что такое аксиома. Если у Брауэра аксиом не было, то не было и определений. А без определений не о чем и размышлять. То, что в работах этого господина аксиомы присутствуют неявно, без огромной надписи АКСИОМЫ и пронумерованного списка может и рвёт шаблон, но сущности не меняет.
>>24466 >Ты, похоже, плохо представляешь себе, что такое аксиома. И что же это такое? В натуральной дедукции аксиома - это логическое заключение без посылок, т.е. нечто, принимаемое без предшествующего контекста, из которого это нечто можно вывести, т.е. нечто, ниоткуда не выводимое, а принимаемое "как есть". С такой позиции даже в MLTT аксиом нет, т.к. там 4 правила вывода и все они начинаются с контекста. Про Брауэра и говорить нечего, он даже конструктивную логику Гейтинга назвал "любопытным, но бесплодным примером", сам Гейтинг тоже явно оговаривал, почему конструктивная логика не формализует брауэровского интуиционизма.
>>24467 >это логическое заключение без посылок >логическое заключение без посылок Уже сама эта фраза полностью демаскирует полное незнание тобой терминологии, которой ты так презрительно разбрасываешься. Аксиома - это утверждение о свойствах, элементарная часть определения. Связка аксиом и образует полное определение. >принимаемое без предшествующего контекста Аксиомы не являются выросшей на пустом месте игрой ума. Они были сформированы с учётом опыта обращения человечества с числами. Они строго очертили неясные до той поры понятия и позволили прежде всего без опасений выводить новые и новые следствия. Они показали границы применимости методов, с их помощью можно всегда ответить на вопрос "А правильно ли я поступаю? Не пытаюсь ли я сложить красное с длинным?" Они позволили, наконец прояснить собственно пути математики, сделав рассуждения кристально прозрачными. Интуиционизм же является не более, чем оголтелым скептицизмом, который сомневается даже в собственном здравомыслии. И странное дело: интуиционизм яростно отрицает одно и столь же яростно отстаивает другое совершенно не желая признавать за собой место обычной формальной системы. >там 4 правила вывода и все они начинаются с контекста. А контекст-то с чего начинается? А правила на чём основываются?
>>24470 >Уже сама эта фраза полностью демаскирует полное незнание тобой терминологии, которой ты так презрительно разбрасываешься. Вообще-то я привел вполне официальное определение аксиомы, пикрелейтед http://www.cs.cornell.edu/courses/cs3110/2013sp/lectures/lec15-logic-contd/lec15.html >Аксиомы не являются выросшей на пустом месте игрой ума. Они были сформированы с учётом опыта обращения человечества с числами. Они строго очертили неясные до той поры понятия и позволили прежде всего без опасений выводить новые и новые следствия. Они показали границы применимости методов, с их помощью можно всегда ответить на вопрос "А правильно ли я поступаю? Не пытаюсь ли я сложить красное с длинным?" Они позволили, наконец прояснить собственно пути математики, сделав рассуждения кристально прозрачными. Я чуть выше ссылался на статью Брауэра, он там как раз поясняет за необоснованность таких методов, когда нечто, выведенное из конечного априори и бездоказательно обобщается на бесконечное. Как исключенное третье, например. >Интуиционизм же является не более, чем оголтелым скептицизмом, который сомневается даже в собственном здравомыслии. Требование построения доказательства - это не оголтелый скептицизм, а вполне резонное условие для математики, которая вообще-то является самым точным знанием, известным человечеству. Верования там неуместны вообще никак. И где в интуиционизме сомнения в собственном здравомыслии? >А контекст-то с чего начинается? С конструктивных объектов. >А правила на чём основываются? На возможных манипуляциях с элементами контекста.
>>24471 >Вообще-то я привел вполне официальное определение аксиомы, пикрелейтед Ты понимаешь что у тебя "логический вывод" из ничего? >Я чуть выше ссылался на статью Брауэра, он там как раз поясняет за необоснованность таких методов, когда нечто, выведенное из конечного априори и бездоказательно обобщается на бесконечное. Да, некоторые вещи приходиться принимать без доказательств. Правда в том, что если мы вот прям счас откатимся в каменный век интуиционизма и забудем большую часть теорем существования - нам придётся лишиться очень, очень многого. Оно того не стоит. >Требование построения доказательства - это не оголтелый скептицизм, а вполне резонное условие для математики, которая вообще-то является самым точным знанием, известным человечеству. В "формализме" доказательства строятся настолько замечательно, что их можно проверить исключительно основываясь на синтаксисе. >И где в интуиционизме сомнения в собственном здравомыслии? В том, что интуиционисты начинали с классики. Затем они зачем-то её кастрировали, переформулировали и вуаля - новая теория. Правда, она оказалась не то чтобы очень нужной. Но всё же, новую теорию придумать - это не хухры мухры. >С конструктивных объектов. И как же они определяются? >На возможных манипуляциях с элементами контекста. Почему это они возможны?
>>24472 >Ты понимаешь что у тебя "логический вывод" из ничего? Я-то пони маю. Теперь и ты вроде начинаешь. Аксиома - это логический вывод из ничего, в противном случае это бы не аксиомой называлось. >Да, некоторые вещи приходиться принимать без доказательств. В церкви - сколько угодно. Но не в математике. >Правда в том, что если мы вот прям счас откатимся в каменный век интуиционизма и забудем большую часть теорем существования - нам придётся лишиться очень, очень многого. Например? Чего многого-то? Полторы все равно невычислимые фофудьи типа исключенного третьего - это немного. И раз они все равно невычислимы, считай, что мы их и так лишены, использовать-то все равно нельзя, только рисовать. >В "формализме" доказательства строятся настолько замечательно, что их можно проверить исключительно основываясь на синтаксисе. Из которого нельзя вывести ничего кроме этого синтаксиса. Самый простейший пример - формулу Пирса и таблицы тарского я уже упоминал. >В том, что интуиционисты начинали с классики. Затем они зачем-то её кастрировали, переформулировали и вуаля - новая теория. Ой, всё... В каком месте Брауэр начинал с классики? Ты же его даже не читал, но осуждаешь, как совки Пастернака. Даже ту картинку с Брауэром на дачке и 1 и 2 актами интуиционизма, которую я сто раз постил, не читал. >И как же они определяются? >Почему это они возможны? А вот тут опять надо писать страшные слова, с которых бесноватых корежит - интрерпретация логических констант по Брауэру-Гейтингу-Колмогорову.
>>24473 > Аксиома - это логический вывод из ничего Это не логический вывод, потому что предпосылок нет. >В церкви - сколько угодно. Но не в математике. Ты хочешь сказать, что можешь доказать непротиворечивость кокструктивистской хуйни средствами самой теории? Она только кажется тебе убедительной, в основном из-за своей радикальности, но на имеет под собой ровно столько же оснований, что и любые другие непротиворечивые основания математики. Интуиционистский неуместный аскетизм предлагает резать всё циркулярной пилой и ножом - ну а хули, режет же, чего ещё надо? >Полторы все равно невычислимые фофудьи типа исключенного третьего - это немного. И раз они все равно невычислимы, считай, что мы их и так лишены Теоремы существования кокструктивизмом не признаются, однако часто, чтобы рассчитать то, существование чего доказывает теорема, необходимо провести над этим чем-то определённые манипуляции. Прямо как здесь: >>24459 допустимость операций определяется сходимостью ряда, что определяется существованием предела. Более того, поскольку сам придел - понятие неарифмитическое, он впринципе выпадает из рассмотрения конструктивистской секты. И что же конструктивисту делать, если его инженер попросит рассчитать работу? >Из которого нельзя вывести ничего кроме этого синтаксиса. Ты сравниваешь тёплое с мягким. Синтаксис позволяет проверить правильность умозаключений, но отнюдь не призван заменить работающую голову. >В каком месте Брауэр начинал с классики? Он начал с изучения классической математики. Он не сделал свои выводы, сидя на дачке с полной изоляцией от внешнего мира. >интрерпретация логических констант по Брауэру-Гейтингу-Колмогорову. Эти константы были положены, постулированы, как постулируется существование множества натуральных чисел. Кстати об N - оно ж бесконечно, а значит необходима очень ловкая логическая конструкция, которая позволяет манипулировать натуральными числами, не так ли?
>>24477 >Это не логический вывод, потому что предпосылок нет. Я же даже скрин логического вывода аксиомы дал. Врети?.. >Он начал с изучения классической математики. Он с нее не начал, а просто изучал в школке и в универе, как и все остальные. Это разные вещи. >Эти константы были положены, постулированы, как постулируется существование множества натуральных чисел. Множество натуральных чисел задано правилами его построения, там нечего постулировать. >Кстати об N - оно ж бесконечно, а значит необходима очень ловкая логическая конструкция, которая позволяет манипулировать натуральными числами, не так ли? Не так. Опять же, обсуждали уже все это. В том числе и отличие актуальных бесконечностей от абстракции потенциальной осуществимости.
>>24482 >логического вывода аксиомы дал Мне непонятно, из чего выводится аксиома. Я отказываюсь выводить из ничего чего-либо. Я лучше спокойно признаю произвольность аксиом. >Он с нее не начал, а просто изучал в школке и в универе, как и все остальные. Это разные вещи. Он её изучал, она была его первой дверью в математику. Классическая математика - это необходимый этап в эволюции его взглядов. Я даже рискну предположить, что до определённого момента он верил в классическую математику. >Множество натуральных чисел задано правилами его построения, там нечего постулировать. Нечего постулировать, кроме правил построения и канонического элемента, ты хотел сказать. >отличие актуальных бесконечностей от абстракции потенциальной осуществимости Какие проблемы устраняет отказ от актуальной бесконечности и принятие потенциальной, вот что интересует меня в первую очередь.
>>24483 > Какие проблемы устраняет отказ от актуальной бесконечности и принятие потенциальной, вот что интересует меня в первую очередь. Актуальная бесконечность невычислима.
>>24498 >кажется, Крестись. Разве я виноват, что про натуральную дедукцию ты от меня позавчера услышал? Подумой, ты ж даже аргументы не воспринимаешь. Я тебе даю ссылку и даже конкретный скрин, ты глаза закатил и пытаешься доказать мне, что это я что-то не знаю.
>>24503 Ээ... Прочитай, кому был адресован мой пост. Ты, кажется, просто триггеришься на определенные слова своей вечной мантрой про "я дал скрин, прочитайте, вы ничего не понимаете, уже тысячу раз объяснял". Ты точно не бот?
>>24483 >Какие проблемы устраняет отказ от актуальной бесконечности и принятие потенциальной, вот что интересует меня в первую очередь. А что вообще актуальная бесконечность делает в математике? Это даже не математический объект. Проблема как раз в этом. В математику за тысячи лет понатащили всякой хуйни, никакого отношения к ней не имеющей. В основном из третьесортной философии типа платонизма. Причем, в самые основания понатащили. А потом вжух и кризис оснований.
>>24611 Похоже на хуйню какую-то, даже скорее всего выдуманную и несуществующую. Зачем мне время тратить на поиски её в гугле? Тем более если я гос. веб сайтам не совсем доверяю в таких вопросах.
>>24612 >Похоже на хуйню какую-то, даже скорее всего выдуманную и несуществующую. Актуальная бесконечность хуйня и есть, как и любые другие попытки использовать платонизм в математике. Но с этой хуйней проще, ей можно заткнуть открытую проблему и кукарекать, что математика к вычислимости не сводится.
>>24624 Местами. В оригинальном своем виде это невычислимая аксиоматика, в качестве оснований непригодная как минимум из-за исключенного третьего. Если даже довести до ума, все равно не идет дальше лямбда-Р в кубе Барендрегта, а в 2017 это несерьезно.
>>24627 А неконструктивисты когда? Все-то вас тянет ко всякой бесконечной комбинаторной хуйне из прошлого тысячелетия типа ферзей да римановых ноликов.
>>24629 >А неконструктивисты когда? Оставляем эту почетную проблему вам, а то у вас совсем как-то плохо. Почти никаких задач не решаете, всё дрочите на свою вычислимость.
>>24629 >бесконечной комбинаторной хуйне из прошлого тысячелетия типа ферзей да римановых ноликов А вот если бы ты не был необразованным селюком, ты бы знал что почти вся эта наука о "вычислимости" сводится к задаче о ферзях.
>>24638 >Окей, а каков порядок ℤ? У ℤ нет конечного порядка. >Или у вас не существует бесконечных групп? Существуют группы, которые не являются конечными.
>>24672 А меня вот бесит аксиома пары. Каждый раз, как о ней думаю, аж зубы сводит, так сильно эту аксиому ненавижу. Блядские веруны в пару, так бы и запретил.
>>24668 >Любая NP-полная задача сводится к любой NP-полной. И что? Класс задач, разрешимость которых можно проверить на машине Тьюринга за не более чем полиномиальное от размера входных данных время - это далеко не вся "наука о вычислимости". И это чудо капустное кого-то будет селюком называть.
>>21361 (OP) Какова природа математической истины? Вот 1+1=2 это вроде как истина, но истина не такая как "Расстояние от моей лобковой кости до конца головки моего члена в эрегированном стоянии составляет 13см, что является средним и нормальным значением". Знаю людей утверждающих что математика это вообще не про истину и не про объективность, а просто маняфантазёрство.
>>24801 >Какова природа математической истины? Классически в математике истинно то, что непротиворечиво. Конструктивно - истинно то, что построимо, т.е. конструктивные объекты и доказуемве / выводимые / наблюдаемые их свойства. >Вот 1+1=2 это вроде как истина, но истина не такая как "Расстояние от моей лобковой кости до конца головки моего члена в эрегированном стоянии составляет 13см, что является средним и нормальным значением". Есть мнение, что точно такая же. Пикрелейтед, выделенное. Математический релятивизм Маннури - утверждение о сводимости любого концепта к любому другому, т.е. если есть концепт A и другой концепт В, то первый можно свести ко второму через конечное число промежуточных концептов A1,...,An таких, что концепт А представим в форме концепта А1, а концепт An представим в виде концепта В. Концепты, например, могут быть любыми математическими объектами, принадлежащими любой аксиоматике, теории и т.д. В твоем примере даже этого не требуется, поскольку в обоих случаях речь о натуральных числах, к которым напрямую сводятся оба твои примера.
>>24806 >если есть концепт A и другой концепт В, то первый можно свести ко второму через конечное число промежуточных концептов A1,...,An таких, что концепт А представим в форме концепта А1, а концепт An представим в виде концепта В. Давай конструктивное доказательство.
>>24807 Типизированная лямбда же. К ней легко свести даже естественный язык,как пример - семантика Монтегю, есть еще целая монография Ранте, где естественный язык анализируется с позиции MLTT и наоборот. А на естественном языке можно описать хоть твою мамку. Опять же, по Маннури, есть 5 уровней языка, от естественного разговорного до полностью формального, н-р матлогика, и разница между этими уровнями относительная, а не абсолютная. Так что доказать можно и конструктивно, через типизированную лямбду, т.к. любой концепт так или иначе можно представить лямбда-термом.
>>24810 Можно, причем элементарно - через обобщение номинальной дефиниции и редукций (дельта, бета, иота, дзета) до кое-чего интересного. Когда-нибудь допилю свой мега-гитлер прувер, будет конструктивное доказательство.
>>24814 Подробнее долго. Когда-нибудь руки дойдут, запилю нормальный пейпер. >>24847 >планируешь прувер сделать онлайновым? Полноценная реализация изначально планируется онлайновой, т.к. все нужное проще всего реализовать средствами гугловской облачной платформы https://cloud.google.com/ и не привязанной ни к какой конкретной операционке. Кто бы еще все это сделал, т.к. я в гуглооблако не могу. Локально почти все нужное (кроме OCR для математической нотации (LaTeX и AMS-TeX) реализуемо в R, это уже посильно для меня, было бы еще свободного времени побольше а быдлопроблем поменьше.
>>25383 >Очередная победа теоретико-множественного подхода. Единственная, я бы сказал. Других не подвозили, начиная с того самого 11-го симпозиума в Палермо в 1897 году, когда Бурали-Форти торжественно помочился Кантору за шиворот, уничтожив его как математика.
Брауэр, к слову, не только задолго до Геделя и обсера Гильберта с его изначальной программой, показал несостоятельность формализма как оснований математики. И даже не только вывел суть математики как ментальных построений, что подтвердилось уже в нулевых годах 21 века (модели ATOM, MT, о чем уже писалось). Его взгляды на природу и физику как науку очень похожи на то, что сейчас известно как квантово-волновой дуализм и эффект наблюдателя (во II части его диссертации и немного в самом начале III части есть некоторое количество цитат на эту тему), он же был профессором кафедры математики и физики. К сожалению, я в квантмехе практически нихуя не понимаю давно забытый материал из учебников не считается, чтобы сделать более грамотное сравнение. Даже его определение дискретного и непрерывного в интуиции времени как основе математики можно было бы рассмотреть с точки зрения квантово-волнового дуализма.
>>25396 Всецело поддерживаю это начинание. Чем больше вы будете пиздеть о квантовой механике, тем большему количеству людей будет видно, что вы сумасшедшие.
>>25397 Кто "мы"-то? Я один тута. Разве то, что из некоей теории можно вывести нечто такое, до чего остальная наука дошла десятилетия спустя, не говорит в пользу правильности этой теории7
>>25408 Ну зачем же сразу расстройство. У нас свобода вероисповедания. Кто-то в Аллаха верует, кто-то в платоновский мир идей. Другой вопрос, что ни то ни другое - это не математика.
>>25415 Чем же ты объясняешь очевидную популярность теории множеств? Видимо ты просто не умеешь ей правильно пользоваться, поэтому в отрицание скатываешься.
>>25415 Тут даже не про веру в Аллаха, хотя и она конечно даёт о себе знать. >>25423 Скорее всего это объясняется пока ещё неизвестным вирусом. Другого объяснения не вижу.
>>25423 >Чем же ты объясняешь очевидную популярность ислама? Видимо ты просто не умеешь правильно веровать, поэтому в куфр скатываешься. Я тебя услышал.
Когда доказываешь кому-то теорему можно сделать двумя способами: либо доказать уже известными всем методами, простыми, быстрыми.
Либо выдумывать свою конструктивную науку и в ней болтаться без конца.
Я тебя спрашиваю: где результат? Какую реальную проблему помогла решить вычислимость теорем?
Сможешь хотя бы 3 примера реальных задач привести. За которые тебе заплатят деньги. Классическая логика и обычные основания математики - дают рабочий инструмент. Нахрена из кувалды делать микроскоп?
>>25456 Действительно, согласен. Вот ещё что думаю: У них контринтуитивное отрицание закона исключенного третьего. Утверждение: Конструктивист петух или конструктивист не петух. Но зная, что конструктивист петух, мы не можем определить истинность этого утверждения!
>>25486 Хороший вопрос! Хотелось бы чёткое обоснование, без всяких отсылок к изоморфизмам гарри-ховарда, тезиса чёрча и прочих сложныхштук. По-нашему, кратко, по-простому, но по делу.
>>25552 сагласен! я вот ещё кстате вычислил что канструктивные основания пративоречивы!! ведь в них отрицается исключённае третье и доказывается двойное отрицание исключённого третьего!! другими словами просто фууу....
так... я даказал в гаматапической теории типав что исключённое третье неверно. из этого следует пративоречивость канструктивной математики.
теорема: канструктивная математика противоречива.
доказательство:
исключённая третье говорит нам, что верно - для всех типав X и для всех точак x и y в X наличие пути из x в y разрешимо. то есть у нас есть терм назавём его الله. الله : Π (X : U) . Π (x, y : X) . x = y ∐ x ≠ y الله X x y := "тут применяем наше исключённае третье" читаем как "الله имеет тип "для всех термав принадлежащих универсуму U (типав) и для любых термав x и y типа Х наличие пути из х в у разрешимо"" из этого следует что все типы являются 0-типами! теперь подставляем x вместо у и палучаем что все гаматопические группы (любого типа!!!) тривиальны!