Кризис оснований закончился, когда теория множеств была аксиоматизирована.
И сразу все бесконечности и исключенное третье сами посчитались. А Гильберту делать было нехуй, что он решил обосновывать арифметику финитарными методами, потому что чисто аксиоматически это оказалось сделать невозможно. Финитарными, Карл! До такого даже Брауэр не докатился, хотя и описал то, что Гильберт назвал "метаматематикой" задолго до Гильберта т.к. признавал потенциальную осуществимость, как абстракцию от действия над ментальными построениями "and so forth". Суть-то в чем? Невычислимые основания нельзя использовать на практике, н-р для доказательства непротиворечивости арифметики, на чем Гильберт и прогорел, скатившись в итоге к финитизму. Подобные же причины сделали необходимым создание вычислимых оснований - MLTT и HoTT. Если бы все можно было доказать в ZFC, никто бы не ебался с конструктивными основаниями.
>никто бы не ебался с конструктивными основаниями.
С ними никто не ебётся, кроме двух психов.
Ну я тебе пример с непротиворечивостью арифметики привел. Нахуя нужны основания, пользуясь которыми нельзя обосновать что 1+1 будет 2? Это не то что не основания, это не математика даже.
>кроме двух психов.
Манямир, ты ж и сам это прекрасно знаешь. Пишешь просто чтобы возразить.
Арифметика Пеано непротиворечива, и это доказано. В любой формальной арифметике со сложением можно доказать, что 1+1=2. В чем проблема-то?
>Арифметика Пеано непротиворечива, и это доказано.
Теоремой Гудстейна? Ты формально докажи непротиворечивость арифметики, а не правилами построения типа аксиом Пеано.
Это доказал трансфинитной индукцией Генцен, чем окончательно выполнил программу-минимум Гильберта. Как бе известнейший факт.
Доказательство Генцена еще зимой разбирали (тащи свою пасту).
Давай устроим полноценный диспут? Ты за свой интуиционизм, я за обычную математику.
Го пвп? Сейчас бы в 2017 намейлру опровергать интуиционизм. Ну что вы тут за аутисты? Вот ты ж даже не читаешь, что тебе пишут, не говоря о том чтобы попытаться понять. Помимо невычислимых нематематических верований вся используемая математика конструктивна и даже выразима в лямбда Р исчислении, что показал де Браун. Я это не писал уже сто раз? Писал. Так что ты опровергать собрался?
Ну, вначале ведь нужно уточнить позиции. Первым делом я бы хотел выяснить объём и границы того, что ты называешь "всей используемой математикой". От общих вопросов - не отсекается ли тобой, скажем, вся теория множеств и вся современная алгебра, и до таких частностей, как возможно ли определить топологию Зоргенфрея на числовой прямой. Согласись, вполне справедливая хотелка.
> Ну, вначале ведь нужно уточнить позиции.
Я их уже 4ый тред уточняю + до этого тредов 5 как минимум в сци. Математика это все, что вычислимо, все что невычислимо это не математика. Именно поэтому всю математику можно изложить уже в лямбда Р исчислении (Automath де Брауна), да даже на машине Тьюринга, хотя это дальше от практики. Т.к конструктивный объект это обобщение натурального числа, любую математическую структуру можно свести к натуральному числу, геделевской нумерацией например, а вся математика точно так же сводится к арифметике. А все, что не сводится - это не математика, с этим только в церковь покемонов ловить. Не писал я этого сто раз? Писал ведь. И если после всего этого моя позиция остается гепонятной кому'то, я даже не знаю.
Это слишком общие слова. Хотелось бы (и, похоже, не мне одному) узнать, что же конкретно ты относишь к области покемонов. Понятно, что ты запрещаешь изучать большие кардиналы и нестандартный анализ, но как далеко простираются запреты и не попадает ли вдруг под них вообще вся общая топология? Вот скажи, как в твоем учении выглядит введение разнообразных топологий на множестве вещественных чисел? Как, к примеру, топологию Зоргенфрея следует определять? Это конкретные вопросы, и я рассчитываю на конкретные ответы.
Это не общие слова, а вполне конкретная конкретика. Математика = вычислимость, для определенности, пусть будет вычислимость на машине Тьюринга, хотя сойдет и любое другое уточнение понятия алгоритма. Невычислимое невычислимо, поэтому его нельзя вычислить, можно только верить. Потенциальная осуществимость осуществима потенциально, отличие от актуальной бесконечности - наличие правил построения.
> Как, к примеру, топологию Зоргенфрея следует определять?
Дался тебе этот Зоргенфрей. Еще Брауэр показал, что континуум невычислим и уж точно не сводится к множеству вещественных чисел.
> Как, к примеру, топологию Зоргенфрея следует определять?
Дался тебе этот Зоргенфрей. Еще Брауэр показал, что континуум невычислим и уж точно не сводится к множеству вещественных чисел.
Верно ли я понял, что ты запрещаешь вводить различные топологии на множестве вещественных чисел?
Я думаю тут еще хуже, смотри он пишет
>Математика = вычислимость
И при этом следом
>континуум невычислим
Отсюда по его манялогике: вещественные числа эта манявера и четко твердо НИНУЖНО. Я тут подумал, а этого сумасшедшего легко косплеить.
> Верно ли я понял, что ты запрещаешь вводить различные топологии на множестве вещественных чисел?
Ты ведь и сам понимаешь, даже без всякого конструктивизма, что это в любом случае будет аппроксимация с конкретным количеством знаков после запятой. Именно их ты и будешь вычислять. Нет никакого запрета, есть трезвый взгляд на тему. Брауэр, к слову, топологией занимался еще до интуиционизма.
О какой аппроксимации речь? В какой процедуре? Топология стрелки - это классический пример топологического пространства с неинтуитивными свойствами, и работает этот пример именно как цельное пространство.
Все эти ваши "цельные пространства" на самом деле дискретизация. Самый простой пример - интегральчики. Веровается, что с помощью предельного перехода размера интервалов dx к бесконечно малому получается нечто отличное от просто интервалов, хотя ни для кого не секрет, что любые численные методы интегрирования - это чистая дискретка. Т.о. имеем практически возможную аппроксимацию конечным числом интервалов dx, а предельный переход существует только на бамаге, ничего построимого и вычислимого за ним не стоит. Т.е. на самом деле вычисления не идут за пределы реально вычислимого. И опять же, я приводил конкретный пример - теория статистического обучения. Таких примеров можно привести еще сколько угодно, те же функции принадлежности в нечетких множествах. Т.е. на самом деле работает все так, как показал еще Брауэр - континуум невычислим, реально можно работать только с его дискретизацией.
>Веровается, что с помощью предельного перехода размера интервалов dx к бесконечно малому получается нечто отличное от просто интервалов, хотя ни для кого не секрет, что любые численные методы интегрирования - это чистая дискретка.
Какая разница, что там в реальности считают инженеры?
>Т.е. на самом деле вычисления не идут за пределы реально вычислимого.
А число Грэма?
>Какая разница, что там в реальности считают инженеры?
Типа ты можешь посчитать больше, чем инженер, причем в какой-то своей реальности? Вычислимость это вычислимость, машину Тьюринга, Поста и другие подобные вещи ты не перевычисляешь, это факт.
>А число Грэма?
Обсуждали уже. Тебе в слове "вычислимое" что непонятно? Опять сказка про белого бычка из-за непонимания разницы между фактически построимым и абстракции потенциальной осуществимости? Извини, не интересно.
>разницы между фактически построимым и абстракции потенциальной осуществимости
Тогда почему ты говоришь про какие-то там дискретные величины в интегралах? Там бесконечность, континуум! УХ!
Я понял, что тебе непонятно слово "потенциально", еще в прошлом году. Поэтому, давай так - ты разбираешься с этим понятием, потом приходишь сюда спрашивать. До этого не вижу ни одной причины повторять миллион раз одно и то же, причем тому, кто принципиально не способен воспринимать объяснения на эту тему.
Если ты говоришь про потенциальность то зачем тогда упоминаешь интегральчики?
>Самый простой пример - интегральчики. Веровается, что с помощью предельного перехода размера интервалов dx к бесконечно малому получается нечто отличное от просто интервалов, хотя ни для кого не секрет, что любые численные методы интегрирования - это чистая дискретка.
У нас есть аналитический метод вычисления, без дискретки с континуумом!
"Математика = вычислимость".
То есть математика - это один из разделов Computer Science?
>математика - это один из разделов Computer Science?
Да, конструктивное доказательство чему - изоморфизм Карри-Говарда. Хотя так-то это всем умным людям из тех, кого Брауэр не разбудил это стало ясно уже после работ Тьюринга с Постом. Самое смешное, что с тех пор кроме кривляний разной степени толстоты возражений пока не поступало.
Но ведь ты веришь, в то, что например, доказательство на компьютере коком верно, поскольку человек не может его проверить. Ту же проблему четырёх красок взять!
А что лемму вложенных отрезков думаешь? Можно же пересекать бесконечное число отрезков.
Я еще раз прошу не нести хуйни, т.к. в теме ты не понимаешь совсем, что видно за километр. Автоматическое доказательство коком ничем не отличается от автоматического доказательства человеком. Машину Тьюринга можно сделать из бумажной ленты и все нужное делать руками, это ничем не будет отличаться от неручной машины Тьюринга. Другой вопрос, что это займет гораздо больше времени. Я еще раз скажу - вычислимость это вычислимость, она одна, других не бывает.
>Автоматическое доказательство коком ничем не отличается от автоматического доказательства человеком.
Во первых, тогда почему твой кок не может оперировать исключающим третьим, аксиомой выбора, и актульными бесконечностями, а человек может? Почему я например могу работать с вещественными числами(бесконечными последовательностями десятичных дробей), а твой кок нет?
Во вторых, доказательство коком сомниетльные, поскольку человек их не может увидеть. А раз мы не можем увидеть доказательство, то веруем в него. Как и веруем в доказательство проблемы черытёх красок, от которого плювался Гротендик.
Я вижу, что во-первых, вопросы по конструктивной математике тут таки возникают, во-вторых, с матчастью тут совсем все плохо, настолько плохо, что хуже уже не бывает. Поэтому, вниманию самых маленьких предлагается такая книшка:
http://gen.lib.rus.ec/book/index.php?md5=2BBE15747B57CDB3BAF9F25BDFEC280B да, в совке издавали годные материалы по конструктивной математики даже для дошкольников и младших школьников. Все поясняется буквально на пальцах.
>почему твой кок не может оперировать исключающим третьим, аксиомой выбора, и актульными бесконечностями, а человек может?
Во-первых, ты не можешь, ты вероваешь, что можешь. Во-вторых, в коке можно задать и исколюченное третье и даже Аллаха. Но, поскольку это неконструктивные сущности, за которыми не стоит никаких вычислимых в канонические элементы конструкций, это бесполезно.
>Почему я например могу работать с вещественными числами(бесконечными последовательностями десятичных дробей), а твой кок нет?
Давай, покажи. Тащи сюда полностью свои бесконечности.
>доказательство коком сомниетльные, поскольку человек их не может увидеть.
В третий раз тебе говорят, хватит писать мне хуйню, реально надоело. Если ты кок в глаза видел, то видел и доказательства, которые он выдает. А если бы еще слышал про лямбда-куб, исчисление конструкций итд, то даже и понял бы их.
http://gen.lib.rus.ec/book/index.php?md5=2BBE15747B57CDB3BAF9F25BDFEC280B да, в совке издавали годные материалы по конструктивной математики даже для дошкольников и младших школьников. Все поясняется буквально на пальцах.
>почему твой кок не может оперировать исключающим третьим, аксиомой выбора, и актульными бесконечностями, а человек может?
Во-первых, ты не можешь, ты вероваешь, что можешь. Во-вторых, в коке можно задать и исколюченное третье и даже Аллаха. Но, поскольку это неконструктивные сущности, за которыми не стоит никаких вычислимых в канонические элементы конструкций, это бесполезно.
>Почему я например могу работать с вещественными числами(бесконечными последовательностями десятичных дробей), а твой кок нет?
Давай, покажи. Тащи сюда полностью свои бесконечности.
>доказательство коком сомниетльные, поскольку человек их не может увидеть.
В третий раз тебе говорят, хватит писать мне хуйню, реально надоело. Если ты кок в глаза видел, то видел и доказательства, которые он выдает. А если бы еще слышал про лямбда-куб, исчисление конструкций итд, то даже и понял бы их.
Ты можешь с помощью кока доказать формулу, что сумма 1+2+3+...+n равна n(n-1)/2?
Зачем мне читать твою конструктивную литературу? Почему вместо нормального объяснения ты всё время крепишь скриншоты и отсылаешь к книжкам? Хочешь меня так в свою секту завербовать?
Один раз нормально распиши, а потом копипасть на однотипные ответы, довен.
>Во-первых, ты не можешь, ты вероваешь, что можешь.
Смотри, у нас есть множество действительных числе R.
Я беру и выбираю из него такое число x, что оно будет меньше 3 и больше 2.
>Смотри, у нас есть множество действительных числе R. Я беру и выбираю из него такое число x, что оно будет меньше 3 и больше 2.
И что дальше? Получаем дискретизацию континуума вещественными числами. Континуум не сводится к множеству R, т.к. между двумя вещественными числами всегда можно вставить еще. Даже если применим абстракцию потенциальной осуществимости и предположим, что такое деление можно вести сколько угодно далеко, все равно итогом будут вещественные числа, но не континуум.
>Почему вместо нормального объяснения
Я не виноват, что вместо того, чтобы вникать в объяснения, ты закатываешь глаза и начинаешь кукарекать.
>Один раз нормально распиши
Я каждый раз нормально пишу. Нужно пытаться понять, а не кукарекать.
>Хочешь меня так в свою секту завербовать?
Деревянные по пояс тут точно не нужны. Правильно Максимка говорил, что в рашке никто не может в зависимые типы.
>абстракции потенциальной осуществимости
Да у нас тут ВЕРА
>Я каждый раз нормально пишу.
И да, когда ты там мне все простые числа перечислишь? Их же конечное число не так ли?
>Я не виноват, что вместо того, чтобы вникать в объяснения, ты закатываешь глаза и начинаешь кукарекать.
Посылание читать Брауэера это не объеснения.
>Я каждый раз нормально пишу.
Ты даже сейчас не можешь нормально писать и скатываешься до оскорблений. Давай ссылку на пост с нормальными объяснениями, раз писал.
>Деревянные по пояс тут точно не нужны.
>— Ты издеваешься. Ты не можешь писать это всерьёз.
>— Я не виноват, что ты такой тупой.
>Посылание читать Брауэера это не объеснения.
Да ну, какой тебе Брауэр, ты вышеупомянутую книжку для дошкольников не осилишь. Хотя если бы осилил, много откровенно тупых вопросов бы отпало, там реально хорошо объясняют, лучше чем я. При всем неуважении к совку, научпоп там был мирового уровня. Но тебе не нужны объяснения (да, я сто раз объяснял, можешь опять вспомнить свою пасту), ты изначально исходишь из предположения, что я неправ, и уже с этой позиции рассматриваешь все остальное, безотносительно к его содержанию. Мне-то похуй, одно непонятно, зачем тогда тебе вообще сюда писать и пытаться что-то кому-то доказать.
Вот как пример, что можно доказать тому, для которого абстракция и вера это одно и то же? Тут вообще говорить не о чем.
>Да ну, какой тебе Брауэр, ты вышеупомянутую книжку для дошкольников не осилишь
Я не собираюсь читать какие-то книжки для того, чтобы доказать свою правоту анону с двачей. Это лишнее.
>ты изначально исходишь из предположения, что я неправ,
А я должен был считать изначально, что ты прав? У тебя не получилось доказать свою провату, и каждый раз ты только и делаешь, что уходишь от ответа:
Ну ты типа тупой, не поймёшь)))
Иди Брауэра читать)))
Да я уже сто раз объяснял)))
Это вера а не математика)))
Хватит уходить от вопросов, нам нужны ответы!
>да, я сто раз объяснял
Тогда дай ссылки на посты с объяснениями. А то только можешь отсылать читать свои книжки, да скиншоты лепить. Ты сам видно не до конца понимаешь всю эту мутотень с основаниями и поэтому нормально объяснить не можешь.
>Вот как пример, что можно доказать тому, для которого абстракция и вера это одно и то же?
Континуум или трансфитная индукция тоже абстрактная вещь, но ты называешь его верой.
>Я не собираюсь читать какие-то книжки для того, чтобы доказать свою правоту анону с двачей.
А что ты мне можешь доказать, если не понимаешь разницу между верой и абстракцией и между трансфинитной индукцией и континуумом? Смешно даже читать такое. А книжки нужны не для того, чтобы что-то кому-то доказать и самоутвердиться, а чтобы в вопросе разобраться. Для этого читать книжки - норма. К слову, это не ты тот деятель, который еще зимой обещал меня разгромить, доказав мне неправильность MLTT?
Вот бы сейчас использовать Успенского для борьбы с этими гадкими бесконечностями.
>Успенского
Ну раз Брауэра и Мартин-Лёфа тута не осилили, может быть хоть Успенский зайдет.
Который сам почему-то отзывается об интуиционизме неприязненно.
>Который сам почему-то отзывается об интуиционизме неприязненно.
Называя Брауэра "замечательным математиком"? Но допустим, в целом это возможно, ведь в совочке брауэровский интуиционизм считали буржуазным идеалистическим учением, в отличие от конструктивизма, который с вычислительной точки зрения то же самое. Опять же, если ты этого не можешь понять, почему это должны были понимать выжившие из ума старперы из КПСС? Они и логицизм Рассела считали тем же самым и даже заявляли, что это причина того, что Рассел призывал разбомбить совок ядерным оружием.
Есть вещи, которые невозможно вычислить или узнать через машЫну. Есть истины, которым нет объяснения. Исходя из этого, именно в этот момент в сознании людей появляется вера во что-то сверхъестественное (и это не плохо). Об этом еще Гедель писал. Кончайте уже со своим конструктивизмом выебываться. Машина не может дать истинные ответы на все вопросы.
/thread
/thread
Недавняя книжка, появившаяся сильно после кпсс. Первое попавшееся место.
Зависимые типы я осилил, а вот исчисление конструкций пока нет. Чем примечательны, полезны, красивы исчисления конструкций, если объяснять для чайника?
Хорошая книжка, автору сразу можно помочиться за шиворот и отправить доучиваться. Классическая матлогика не рассматривает смысл (т.е. семантику) выражений вообще, от слова никак. Там только синтаксис, о чем писал и Гильберт и Бурбаки.
> исчисление конструкций пока нет.
С Барендрегта начни. Исчисление конструкций - просто наиболее полное лямбда-исчисление по Черчу, т.е. в кубе Барендрегта.
На пикрелейтед месте можно окропить автора уриной еще раз. Он даже конструктивное отрицание не осилил. "Недоказанный" и "неверный" конструктивно абсолютно разные понятия.
Эй, конструктивист, ты упорот? Автор этого текста - твой собственный Успенский.
Ну я рад, дальше что? Написанного мной про конструктивное отрицание и семантику матлогики это не отменяет. Что за книжка-то?
Ссылаешься на него как на большого авторитета и тут же пишешь, что ему нужно ссать за воротник. Ни единого разрыва, нормалёк полный вообще.
"Предисловие к математике".
Где книшку-то взял? На либгене нету.
>Ссылаешься на него как на большого авторитета
На конкретную книгу, которую читал лично и в которой ошибок не обнаружил.
Да понятно уже всё с твоими ссылками. Небось если достаточно покопаться, то ты и Брауэра с Мартин-Лёфом обвинишь в непонимании великих идей Брауэра и Мартин-Лёфа.
Вопрос к конструктивистам. В конструктивизме 0.(9)=1?
В принципе, конструктивно, как мне кажется, это можно доказать. Если я хорошо понимаю суть конструктивизма(а я узнал о нем из этого треда), то конструктивное доказательство будет выглядеть так:
У нас есть сумма (сложнее сумму возьмем): 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
Просто пренебрегаем последним членом.
Впрочем, да. Но тут несколько новых понятий придется ввести.
Все же, я не понимаю, чем конструктивистов не устраивает бесконечность. С ней ведь размышлять удобнее. Но, на самом деле, можно сформулировать бесконечность таким образом, чтобы ее смогла юзать и машина. Однако самого смысла она не поймет, очевидно.
Чем одно и то же спрашивать сотый раз, послушайте лучше умного человека.
https://www.youtube.com/watch?v=VDreWuWDUu0&t=1269s
https://www.youtube.com/watch?v=VDreWuWDUu0&t=1269s
А как с мнимой единицей у конструктивистов дела обстоят? Мы же просто верим в её существание, она имеет отличную природу от натуральных чисел.
Как я и говорю, основная проблема местных поциентов - категорическое неумение пользовпться головой. В нее не только кушать можно, прикинь. Вот твой вопрос, объясни, к чему он вообще? Ты ни разу не слышал, что даже некоторые калькуляторы могут считать комплексные числа, не говоря о любом нормальном языке программтрования? А если комплексные числа построимы, т.е вычислимы, что можно сказать об их конструктивности, сам догадаешься, или это слишком сложно?
Некоторые калькдяторы и бесконечность считают, мнимания единица имеет другию прировуд. Вот число один -это число. Но мнимая единица не имеет алгоритма построения.
Комплюктор не ПОНИмает сути производимых операий. Он просто следует алгоритму который в него вбили.
>Комплюктор не ПОНИмает сути производимых операий. Он просто следует алгоритму который в него вбили.
Прямо как конструктивисты, лол.
> Некоторые калькдяторы и бесконечность считают, мнимания единица имеет другию прировуд. Вот число один -это число. Но мнимая единица не имеет алгоритма построения.
Ты читать не умеешь? Вычисление это построение.
Как можно построить мнимую единицу?
> Комплюктор не ПОНИмает сути производимых операий.
Суть, семантика производимых операций в MLTT это вычисление, т.е получение канонических элементов. Комплюктер понимает вычисление иак же как и не комплюктер, ты никогда и не при каких обстоятельствах не сведешь вычисление к тому, к чему его не сведет компьютер, следовательно твое понимание вычисления равнообъемно с компьютерным. И это сто раз уже писано, просто вы все иута деревянные по пояс.
А computer science - это чистая математика?
> Как можно построить мнимую единицу?
А как нельзя? Ее даже нарисовать можно, погугли. Суть построений в вычислимости, еще раз говорю. Построение это вычисление, ферштейн, нихт?
> А computer science - это чистая математика?
В рамках изоморфизма Карри- Говарда, если тебе эти слова о чем'то говорят.
Можно и бесконечность нарисовать, а ты мне найди число, которое в квадрате будет -1.
Нет, я плох в программировании.
> Можно и бесконечность нарисовать,
Бесконечность невычислима, комплексные числа вычислимы. Спать идите, аутисты.
> Нет, я плох в программировании.
Это математика в том же объеме, что и програмиирование. Если слово 'изоморфизм' тебе о чем'то говорит.
Откуда взялось i? Мы просто верим, что существует число, равно в квадрате -1?
> Откуда взялось i? Мы просто верим, что существует число, равно в квадрате -1?
Верования невычислимы, конструктивные объекты вычислимы. Комплексные числа вычислииы. Так ясно?
Чему равно пи мы знаем, но чему равно i?
>Бесконечность невычислима
Арифметика кардиналов вычислима.
i = (0,1)
Это семантика. Всё равно, что сказать бесконечность = /inf.
Я хочу знать, чем оно равняется.
> Это семантика. Всё равно, что сказать бесконечность = /inf.
Тебе тролить тупостью не надоело? Конструктивно семантика это вычисление. Эта твоя запись /inf не вычислима ни во что, т.к не является каноническим элементом, не является она и неканоническтм элементом, поскольку не имеет правил вычисления в канонический элемент. Аллаха опять же в этой связи уже обсуждали. И открой для себя гугл, разберись с любым алгоритмом вычисления комплексных чисел, а не пиши одно и тоже сюда сто раз.
Повторяю, можно дать тебе алгоритм, с помощью которого ты сможешь работать с ординальной арифметикой.
Вычисли мне i.
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
Это лишь формальные операции над символами.
Как и любое вычисление? Давай, покажи вычисление комплексного числа, не сводящееся к вычислению, ебани духовненько, а не как бездушный кудахтер.
Чем тогда это отличается от Аллаh'а?
Я уже очень, очень много раз говорил чем. Последний раз в этом посте но ты не вертись, а показывай свой вариант вычисления комплексных чисел
Определи канонический элемент, будь любезен.
Тоже много раз обсуждалось уже, со скринами и примерами. Все определения тута есть http://www.cse.chalmers.se/research/group/logic/book/book.pdf в первой части.
Хватит кидать ссылки на книги. Я так же могу обсуждать работу мочидзуки, а когда у меня что-то спросить, то дать ссылки на статьи, и сказать сто раз обсуждалось, там же написано. Берёшь и объясняешь всё с нуля.
>Я так же могу обсуждать работу мочидзуки
Какой тебе Мочидзука, ты ж элементарное понятие вычислимости осилить не можешь. Ты даже понятие равенства по этой лекции не осилишь.
Вместо ответа давать ссылку на талмуд? Всё по методичке, лол. http://lurkmore.to/Правила_демагога
>вместо аргумента тащит на мейлру ссылку с лурки
>обвиняет кого-то в использовании методичек
Ясно.
Неужели для того, чтобы понять твою аргументацию, нужно читать все эти жуткие сотни страниц и смотреть многие часы лекций? Классическую теорию множеств можно изложить за несколько минут, аксиоматическую вплоть до форсинга - за вечер.
В MLTT 4 суждения, 4 правила вывода, 4 основных типа и 4 правила построения выражений. Все это можно уместить на половину тетрадного листа. Тетраграмматон рабби Лёфа прост как 4 шекеля. Проблема только в том, что за всем этим стоит не пустой синтаксис ни о чем, как в формализме, а вычислимая конструктивная математика, где даже понятие равенства имеет вычислительное содержание. Это вам не невычислимые ни во что кардиналы и прочих Аллахов рисовать, тут уже не глиняная голова нужна, чтобы въехать.
Если это так просто, то объясни же это. Зачем ссылки непонятно на что кидать.
>Зачем ссылки непонятно на что кидать.
Не "непонятно на что", а как раз на объяснения.
На многие сотни страниц. Совсем не половина тетрадного листа, как ты говоришь.
Аксиомы исчисления предикатов тоже немного места занимают. А книг с нормальным изложением меньше чем на сотню страниц так же нет. Поэтому возражение не принимается.
Бурбаки. Вся лежащая под математикой логика, включая исчисление предикатов, занимает страницы 31-65. Из них на собственно исчисление предикатов отводится четырнадцать страниц.
>Бурбаки
Пикрелейтед.
>Вся лежащая под математикой логика,
Не вся, ZFC не может в типы, а за что-нибудь уровня NBG у бурбаков нет ничего.
>занимает страницы 31-65. Из них на собственно исчисление предикатов отводится четырнадцать страниц.
Вся книжка Мартин-Лёфа 50 с небольшим страниц, собственно изложение самой теории даже не половина https://github.com/michaelt/martin-lof/blob/master/pdfs/Bibliopolis-Book-retypeset-1984.pdf
На твоём пике математика в объёме, превышающем кандидатский курс (гомологическую алгебру не изучают даже в магистратуре, например). Речь шла о предикатах онли. Короче, показывай листок.
>за что-нибудь уровня NBG
Аксиоматика Бурбаки строго сильнее ZFC. Не слабее чем NBG+аксиома глобального выбора.
Аксиома S8 - обобщенный replacement, если непонятно.
К этой картинке пояснений как раз под сотню страниц и нужно. Из самой картинки не выведешь тау (или эпсилон Гильберта) и т.д. Ну и главная претензия - вычислимость, конечно. Даже не исключенное третье, с этой хуиткой все ясно, вот самая последняя строка, А5. "Существует бесконечное множество", вот и Аллаха подвезли. В каком смысле оно существует? впрочем, все это опять же уже сто раз обсуждалось, сейчас пойдут аргументы про чернильную дыру и про то что актуальная бесконечность не хуже потенциальной осуществимости, бла-бла... К MLTT так не доебешься, пример - лекция выше, там даже равенство сводится к вычислимым построениям, а не просто к значку "=".
>Аксиоматика Бурбаки строго сильнее ZFC. Не слабее чем NBG+аксиома глобального выбора.
До двух считать научиться по их книгам можно?
>До двух считать научиться по их книгам можно?
Нет, на единице застрянешь.
>получаем, что полная запись обыкновенной единицы состоит из 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 связей, то есть полная запись терма, обозначающего единицу, заняла бы сто миллиардов квинтиллионов квинтиллионов книг
УРЕТЕ!!!! АДИН ЕТА СЕРЫЙ КОРДЕНАЛ ПУСТОВА МНОЖЕСТВА!!!! ДЖВА ЕТА КАРДЕНАЛ МНОЖАСТВА АДЫН!!! И ТАК ДАЛЕЕ!!!
Мне такой ответ встречался.
Зачем тебе с ординалов фон Неймана так бомбануло? И чем они хуже аутизма уровня гильбертовского эпсилона, при использовании которого получаются термы размером в квинтиллионы знаков?
До двух досчитать нельзя
>В каком смысле оно существует?
Бессмысленная строка символов, которая в естественный язык транслируется как "существует бесконечное множество", является аксиомой.
>MLTT так не доебешься
Либо ты постишь листочек, либо ты - всего лишь ещё один сосачеребенок.
Да.
Это, конечно же, вздор.
Неверно. Кардинал пустого множества - это 0. Число 1 - это кардинал множества {0}. Число 2 - это кардинал множества {0,1}.
>Это, конечно же, вздор
Сильное заявление...
Обсирают бурбакистов, конечно же, бетежки которые не смогли их осилить, а не из за того что книги переусложненная хуйня.
В книгах Бурбаки нет ничего "переусложненного", они очень легко читаются (пикрелейтед). Вообще, это такой детектор очень хороший: кто считает Бурбаки чем-то сложным, тот некомпетентный лапоть с шерстью на ушах.
>Либо ты постишь листочек, либо ты - всего лишь ещё один сосачеребенок
Что ты разнервничался? Вон же у Максимки все есть http://groupoid.space/mltt/semantics/ с нескучным оформлением. Педивикия опять же.
>Это, конечно же, вздор.
Это эпсилон Гильберта, формализм курильщика.
>Вообще, это такой детектор очень хороший: кто считает Бурбаки чем-то сложным, тот некомпетентный лапоть с шерстью на ушах.
Школьца-максималиста в тебе вижу я.
Иначе говоря, то что первый параграф ссылается на вторую главу, параграф шесть, пункт номер один, это признак хорошего, годного легко читающегося учебника.
Это ты так двачи тролируешь тупость или реально такой дурачек?
Хорошо, теперь давай по порядку. Что по Мартин-Лёфу есть proposition и что есть judgement? В предложенных тобой книгах эти термины используются, но определений им не дано.
>ссылается
Впервые математическую книжку увидел, да?
У бурбаков проблема не в этом. Я даже соглашусь, что это хорошая литература. А в том, что при попытке полной формализации того, о чем они пишут, мы очень быстро упремся в квинтиллионнобуквенные термы. Там же они с самого начала пишут, что для удобочитаемости текста он почти полностью состоит из соглашений, вольностей речи и т.д., откуда и столько отсылок к ранее определенным вещам. В MLTT такой хуйни нет, там все можно свести к вычислениям и вычислить полностью.
>Что по Мартин-Лёфу есть 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
Если откопаете полную версию то сможете узнать что даже макаки-резусы умеют считать до трех.
Тобишь буракисты это даже не уровень человеческой личинки. Они хуже макак.
В то время как обычные пятимесячные младенцы УЖЕ умеют считать до двух.
Вот пруф
https://books.google.com.ua/books?id=s5KqmjDyxTMC&printsec=frontcover&hl=ru#v=onepage&q&f=false
Если откопаете полную версию то сможете узнать что даже макаки-резусы умеют считать до трех.
Тобишь буракисты это даже не уровень человеческой личинки. Они хуже макак.
Я видел этот текст, и он мне непонятен. Прошу объяснить. Я прочитал столько книжек, что слово "формула" для меня не имеет само по себе никакого смысла, увы.
>из соглашений, вольностей речи и т.д.
Из сокращений; это другое. Это не неформальность, а лишь инкапсуляция и абстракция. Любую главу трактата можно рассмотреть как набор аксиом некой новой формальной теории, а все предыдущие главы забыть. В этой новой теории букв в знакосочетаниях будет гораздо меньше. Кроме того, трактат можно дополнить минус первой, минус второй и сколь угодно более низкоуровневыми главами - общность при этом будет повышаться, сложность грамматики - падать, количество букв в знакосочетаниях - увеличиваться. Например, язык начальной главы можно транслировать в морзянку. Математика окажется в таком случае теорией о громадных совокупностях точек и тире.
>тролируешь тупость
Это конструктивисты траллируют тупостью, когда говорят, что бесконечности нет и аксиома исключающего третьего вера.
>а лишь инкапсуляция и абстракция
Считающаяся в термы из квинтиллионов знаков. Это проблема, пони маешь? Потому что если мы захотим это на самом деле посчитать, то...
>Я прочитал столько книжек, что слово "формула" для меня не имеет само по себе никакого смысла, увы.
Значит, неправильные книжки читал. Я ж уточнил, что "формула" там имеет значение, обычное именно для матлогики. Ну и также можно считать пропозишен множеством.
>когда говорят, что бесконечности нет
Ты для начала пойми о чем вообще тут говорят, потом в разговор лезь.
>в термы из квинтиллионов знаков
Только если считающему угодно настолько сильно углубиться в абстракцию. Он вполне может остаться на одном из более высоких уровней, на них символов будет заметно меньше. Например, можно отказаться от трансляции кванторов и импликации, приняв их в синтаксис, тогда квинтиллионы мгновенно исчезнут. Алсо, не в термы, в знакосочетания.
>обычное именно для матлогики
Произвольная формула? Правильно построенная формула (элемент наименьшего класса формул, замкнутого относительно логических связок и содержащего все атомы)? Выводимая формула? Меня "hold to be true" смущает, это вообще о чем.
>Меня "hold to be true" смущает, это вообще о чем.
Изоморфизм Карри-Говарда же. И интерпретация логических констант по Брауэру-Гейтингу-Колмогорову. Общеизвестно, что логические операции это то же самое, что операции над множествами. Истина - это 1, ложь = 0. Классически пропозишен - это функция принадлежности или характеристическая функция, принимающая значение 0 или 1 (не считая многозначных логик). Логическое "и" это пересечение множеств, "или" - объединение, импликация - отношение подмножества. Конструктивно же пропозишен - это множество пруф-объектов, т.е. построений, доказывающих, что данное множество не пусто. Т.о. по упомянутому изоморфизму Карри-Говарда, истинность пропозишена А - это ненулевое количество элементов х принадлежащих А, х:А. Доказательство "не А" - это построенное пустое множество. Отсюда уже видно, почему исключенное третье в общем случае не работает. Классически верно правило "А или не А", конструктивно мы должны доказать конкретно, А или не А, т.е. пусто множество А или нет. Это можно сделать только построив его. Конкретные методы построений получаются интерпретацией логических констант по Колмогорову, т.е. в простейшем случае это могут быть лямбда-термы, а все вышесказанное в таком случае можно свести к типизированной лямбде, откуда вычисление это есть лямбда-определимость. Итд итп.
>Только если считающему угодно настолько сильно углубиться в абстракцию. Он вполне может остаться на одном из более высоких уровней, на них символов будет заметно меньше.
Классически и так сойдет, конечно. тяп-ляп и готов кризис оснований Конструктивно нам нужна полная вычислимость, чего с бурбаками не выйдет вообще никак.
>Конструктивно нам нужно уметь считать ящик и сдачу в магазине
Поправил тебя чутка
>логические операции
А как быть, если нужны нелогические операции? От голого исчисления предикатов мало пользы, пользу приносят первопорядковые теории (исчисление предикатов плюс нелогические формулы).
>операции над множествами
Для корректности такого подхода нужно зафиксировать метатеорию множеств и внятно определить предметную область. Неоправданно сложный подход, чисто синтаксический подход гораздо яснее (а всё семантическое надстраивается на него в теории моделей).
>построений
Что считается построением?
>полная вычислимость
Вычислимость бесконечна вниз, если можно так выразиться. Всегда можно заменить атомарное действие фиксированного исполнителя подпрограммой для более низкоуровневого исполнителя. Полной вычислимости не бывает.
Собственно, на все вопросы в твоем посте ответ один - типизированная лямбда.
>Вычислимость бесконечна вниз, если можно так выразиться.
Только до канонических элементов, которые дальше невычислимы ни во что.
>канонических элементов
А что это такое?
По определению - замкнутые, насыщенные лямбда-термы нулевой арности. Ну или категоремы. Элементы, которые нельзя вычислить во что-то нижележащее, т.к. они сами по себе есть итоговые значение вычислений. Пример - натуральные числа, как элементы множества N они не сводятся к чему-либо более простому.
>категоремы
Я не знаю, что это такое. Но ведь, гм. Для натуральных чисел можно предложить много нижележащих теорий, разве нет?
>Для натуральных чисел можно предложить много нижележащих теорий, разве нет?
Вычислимых-то? Думаю, строго 0. Ниже нумералов Черча сложно что-то придумать, даже ординалы фон Неймана - это то же яйцо, вид сбоку. Впрочем, можешь и предложить, думаю медаль филдса за таконе точно не пожалеют.
Теория, предложенная Бурбаки. Если не вводить теорию множеств во всей полноте, то арифметические построения можно описать знакосочетаниями вида пикрелейтед длиной не более чем в несколько миллионов символов (грубая оценка сверху, на самом деле меньше). Вполне реальный объём для современных компьютеров.
Эпсилоны Гильберта считать со всеми квинтиллионами знаков? Вот ты спрашивал, что есть канонический объект. Вот этот хулиардквадриллионный терм для единицы - это как раз канонический элемент множества N по бурбакам, который ниже уже ни во что не считается. Это можно, конечно. Но грустно, когда ферма из асиков размером с взлетную полосу, будет считать 1+1 пару дней. Самое обидное, что итоговый результат будет тот же, что с нумералами Черча, т.е. натуральное число 2, которое, конечно можно представить еще какими-то квадриллионными термами, но остается вопрос - нижестоящая ли это теория или таки вышестоящая, т.к. использует более сложный алфавит, чем н-р натуральное число как слово в алфавите | по Маркову?
Миллионами.
То есть канонический элемент - это всего лишь терм в формальном языке, который выбран для аксиоматической теории?
>То есть канонический элемент - это всего лишь терм в формальном языке, который выбран для аксиоматической теории?
Точнее терм, который в данной теории нельзя свести ни к чему нижележащему. Но тут уже встает вопрос математического релятивизма (не путать с физикой), согласно которому, любую теорию можно выразить через любую другую, точнее между теорией А и В существует конечное количество теорий А1-Ан, причем теория А выразима в теории А1, а теория Ан - в теории В. В таком случае без разницы, какую теорию считать первичной, т.к. мы все равно можем придти к любой из них из любой другой. Чисто прагматически, более первичной удобнее считать более простую теорию, т.е. уж точно не стоит считать эпсилон-исчисление Гильберта основанием арифметики, потому что полнейший аутизм сначала учить детей в школе эпсилон-исчислению, а затем решать примеры 1+1. Конструктивно всю математику можно вывести из арифметики, прагматически это самый простой путь, гораздо проще и естественнее чем теория множеств, тем более в виде бурбакизма. Естественнее, потому что доказано, что понятие натурального числа врожденно и предшествует даже языковым способностям (такие нейрофизиологические модели как ATOM Уолша и теория метафор), если с более философской стороны, то Кант и Брауэр.
Спасибо за ответы.
Бывает разная простота. Есть простота для решения задач, причем для разных классов задач простотой окажется разное - например, для решения уравнений вида x+a=b бурбаки очевидно не будут самым простым выбором. Есть простота для доказательства теорем, и вот здесь уже может оказаться наиболее простым выбором, скажем, определять дроби с помощью деления в столбик (анекдотический пример от Арнольда). Универсальной простоты не бывает.
>компьютеров
Правильно, зачем чукче думать, пусть пекарня думает
> Правильно, зачем чукче думать, пусть пекарня думает
А чем твои думы в области математики, чукча, отличаются от дум пекарни в этой же области? Я просил привести примеры вычислимости, не сводящиеся у механическим преобразованиям выражений. Пока примеров не поступало.
Не вся математика сводится к вычислимости.
> Не вся математика сводится к вычислимости.
Старые песни о главном. Если что-то невычислимо, с какой стати это вообще математика? И да, что в математике не сводится к вычислимости? Исключенное третье, актуальная бесконечность и прочая религия?
Это ты сужаешь математику на computer science, ограничевая его её алгоритмами.
> Это ты сужаешь математику на computer science, ограничевая его её алгоритмами.
Примеры, примеры в студию. Что в математике не сводится к алгоритмам, где математика, не являющаяся преобразованием знакосочетаний и термов по заданным правилам? Формализм без формализма, давай примеры.
А как же алгоритмически неразрешимые проблемы?
> А как же алгоритмически неразрешимые проблемы?
Ты можешь как-то решить алгоритмически неразрешимые проблемы? И как?
Той же аксиомой выбора люди успешно пользуются.
И что это? Ты хочешь сказать, что это неразрешимо алгоритмически, но разрешимо как-то иначе?
> Той же аксиомой выбора люди успешно пользуются.
Как пользуются?
Успешно. Сюда кидали скрины Энгелькинга, посмотри.
Ясно. Вчера по бурбакам пояснил за все эти сокращения, соглашения итд, остальное по аналогии. Не считая того, что в mltt аксиома выбора это не аксиома, а теорема и ее можно доказать. Тоже сто раз уже писал, давал ссылкуи постил скрины.
Я про скрины с Энгелькингом, прочитай его и посмотри.
> Я про скрины с Энгелькингом, прочитай его и посмотри.
Зачем? Там в любом случае нотация, формализмы и правила преобразований, т.е алгоритмы.
Где? Укажи на скринах?
Как в случае с комплексными числами, ты опять притащил сам не понимаешь что, и теперь пытаешься троллить тупостью. Мне это не интересно.
Тебе не надоело уходить от ответов?
>это неразрешимо алгоритмически
this
там нет алгоритмов
> там нет алгоритмов
Есть правила работы с этим. Есть то, откуда это вывели, есть следствия, к которым это приводит. Если у тебя от слова 'алгоритм' бампельштильцхен, это не ко мне. И обяснять вещи, которые уже 3хлетний бы понял, мне так же неинтересно. Ты даже не можешь объяснить о чем речь вообще, мне это и темболее не нужно.
С аксиомой выбора так же. Есть следствия, к которым она приводит.
А есть идеи как учить школьников конструктивной математике? В смысле, наверное, большей работы со средствами доказательства теорем или что-то такое. Или может еще что?
Лямбда исчисления вполне можно изложить так, чтобы понял школьник. Тем более, что всю домашку можно сразу писать и проверять в коке. Другой вопрос, зачем.
> С аксиомой выбора так же. Есть следствия, к которым она приводит.
И что дальше? Ты хочешь сказать, что это не укладывается в понятия формализма, нотации или допустимых преобразований выражений, термов или знакосочетаний? Или что ты доказать-то пытаешься?
Тогда почему она - аллах, а другие аксиомы - не аллах?
Разницу между вычислимым и невычислимым обсуждали неоднократно даже в этом треде.
Она укладывается "в понятия формализма, нотации и допустимых преобразований выражений".
Господа, а хоть один человек в этом треде занимается вопросом оснований ПРОФЕССИОНАЛЬНО?
Сколько уже теорем доказали?
Или трёп сплошной?
Если есть хоть один - деанонься, публикацию свою покажи, будем на тебя ровняться.
На самом деле нет таких, какие-то глупые, бессодержательные разговоры ни о чём.
Я ради стипухи взял одно недоказанное (оставим читателю в качестве упражнения) утверждение из маклейна и тиснул статью с его доказательством. Стипуху дали.
Погоди, а в какие журналы такую статью могли принять? А то я тут на хлебе и воде, а доказывать люблю.
Вестник МухГУ.
Как ты полюбил доказательства?
> Что в математике не сводится к алгоритмам
Десятая проблема Гильберта.
> Десятая проблема Гильберта.
Покажи как решить ее без алгоритмов.
Алгоритмами её точно не решить. Но это не значит, что без алгоритмов её решить нельзя. Ты же сам вроде должен быть против исключённого третьего?
Да и вообще по твоей логике должен существовать единый алгоритм доказательства теорем. Даже конструктивные доказательства предполагают некоторый рывок во вне и этот рывок в каждом случае уникален. Так что если с вычислимостью и построением ещё можно понять и согласиться, то вот аппелировать к алгоритмической разрешимости уже полная ересь даже с точки зрения конструктивизма. Ты сам, похоже, до конца не понимаешь что такое конструктивность.
То есть у тебя есть правила языка, ты можешь переводить на другой язык с помощью алгоритмов и тд, но ты не сможешь написать осмысленный текст, можно перебрать все варианты из существующих и тем самым доказать, что других вариантов нет, но сами эти варианты алгоритмически не найти, для этого нужен некий критерий закономерности, когда машина решает, является ли что-то закономерным, определяет что, обобщает и затем уже подтверждает или опровергает это конструктивно. Именно поиск закономерностей, обобщение и
> не сводится к алгоритмам, где математика, не являющаяся преобразованием знакосочетаний и термов по заданным правилам
Математика - это как игра в шахматы.
Если не знаешь как ходят фигуры, то и играешь неадекватно.
Строгие формальные доказательства обучают простейшим ходам.
>Алгоритмами её точно не решить. Но это не значит, что без алгоритмов её решить нельзя.
Демагогия.
Я уже просил не нести хуйни. Алгоритмически неразрешимые задачи никто не отменял.
>Именно поиск закономерностей, обобщение и не сводится к алгоритмам, где математика, не являющаяся преобразованием знакосочетаний и термов по заданным правилам
И еще раз прошу не нести хуйни. То, что ты описал, называется идентификацией систем и реализуется очень большим количеством алгоритмов. Итого, ты не в теме абсолютно, а разжевывать такие азы мне неинтересно вообще никак.
>Демагогия.
Разве?
Надо научиться играть в шахматы тогда хотя бы, дабы понять аналогию.
Ну так я сколько раз уже просил показать неалгоритмическое решение любой алгоритмически неразрешимой проблемы. Примеров нет. Их и не будет, поскольку например, из нас двоих кто-то не знаком с работами Тьюринга и Поста. И кто бы это мог быть, как думаешь?
>Демагогия.
Лол что? Ты пишешь , мол, раз алгоритмически задача неразрешима, то она неразрешима впринципе. Я говорю, что одно из другого не следует. Где тут демагогия?
>То, что ты описал, называется идентификацией систем и реализуется очень большим количеством алгоритмов
Например?
>Я уже просил не нести хуйни
>И еще раз прошу не нести хуйни.
>Итого, ты не в теме абсолютно, а разжевывать такие азы мне неинтересно вообще никак.
Демагогия.
>Ты пишешь , мол, раз алгоритмически задача неразрешима, то она неразрешима впринципе. Я говорю, что одно из другого не следует. Где тут демагогия?
Давай так, пока не принесешь примера решения неалгоритмическими методами алгоритмически неразрешимой математической проблемы, можешь мне вообще не писать. У меня нет никакого желания даже пытаться объяснить человеку, не слышавшему про тезис Черча, из чего конкретно следует общая неразрешимость алгоритмически неразрешимых задач.
>То, что ты описал, называется идентификацией систем
Ну и да, это не то, что я описал. Я о том, что, например, нет такого алгоритма, который бы, например, получая на вход последовательность чисел 2 5 12 27 58 121 ... мог бы найти закономерность, "догадаться", что это 2n-n или 2*предыдущее+номер. Разве такие алгоритмы есть? Человек же такую задачу может решить, потупив в последовательность минуту.
>пока не принесешь примера решения неалгоритмическими методами алгоритмически неразрешимой математической проблемы
Вот это, я полагаю. Ну если она алгоритмически разрешима, то давай ссылки, буду читать.
Ящитаю, что ты не догадался, а просто запомнил, может чуток обобщив.
> из чего конкретно следует
Нет, не следует. Перечитай, о чём он говорит.
>Алгоритмически неразрешимо
Или вот ещё пример. Нужно найти натуральные корни.
x5+2x3+3x2-60=0
По теореме Абеля — Руффини не существует формулы, алгоритма по которому можно найти корни этого уравнения, но подставив 2, догадавшись, мы получим решение. По твоему это уже не математика, а гадание на Аллахе?
>не догадался
Нет, вчера с корешем эксперимент проводили, он загадал вот эту последовательность и нужно было найти закономерность, правда мой ответ был, что это
a(n+1)=2a(n)+n, но не суть.
>обобщил
Вот это тоже, в математике это повсюду, а что это вообще? Как происходит обобщение? Как это алгоритмизировать?
>Разве такие алгоритмы есть?
Деточка, дуй в школку, ну. Ты про идентификацию систем не слышал, зачем ты свою тупость используешь как доказательство чего-то? Это же настолько элементарная задача идентификации, что даже объяснять как ее решить алгоритмически, смешно. Простая регрессия на калькуляторе с этой задачей справится, достаточно расположить эти числа парами
> 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. А вот теперь точно уебывай, потому что детский сад - это не тот уровень, на котором мне было бы интересно дискутировать.
>гадание на Аллахе
Как бы да, это и правда оно, как и доказательство от противного, ведь есть разница между построением объекта и доказательством того, что несуществование объекта противоречиво. Но решение ведь есть. И таких примеров использования Аллаха в математике сотни.
Но следующее число 248, лол. Регрессия.
Доказательство седьмой проблеммы Гилберта неконструктивно и использует не алгоритмические методы.
>R
>регрессия
>алгоритмы
>НИЙРАСЕЕТИ))00)00
А, так ты из этих. Теперь всё ясно. Уёбывай к себе в загон.
Это простая линейная регрессия на датасете из 3х значений. Естественно, что это не самый лучший метод из существующих. Дело не в этом, а в том, что ты своеим неопниманием пытаешься что-то доказать. Буду репортить троллинг тупостью, в общем.
>линейная регрессия
Это не просто не самый лучший метод, это неверный метод, ты ведь даже не понял, зачем её тут использовал, даун.
Даун твой папа, так ему и передай. А регрессия - это простейший пример идентификации системы, в данном случае - системы из пар значений с неизвестной зависимостью выхода от входа.
Ты идиот, регрессия предполагает линейную, сука, зависимость, ахаха, какой нахуй идентификация системы, какие блядь основания ХАХХАХАХХА, ТЫ ЖЕ ДОЛБОЁБ СУКА АХАХАХХАХХАХА УХАХХАХАХХАХАХА
https://www.youtube.com/watch?v=qYodWEKCuGg
Почему актуальной бесконечности не существует?
Потому что ты дебил и она существует.
Пересчитай мне все числа между нулем и единицей. И когда я говорю все, я имю ввиду ВСЕ*
Зачем мне их пересчитовать? Как это докажет её существование?
Тем что ты не почитаешь их все.
На основании аксиомы о непрерывности числового ряда ты можешь бесконечно делить числа и получать новые и новые числа, конца края этому не будет из за того, что исходя из аксиомы о непрерывности...
То есть актуальная бесконечность существует?
Ну и да, там надо тогда уж
#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 это номер члена потому что.
И скажи, конструктивизм всегда алгоритм предполагает разве? Построить значит предоставить алгоритм построения?
Существует.
Ты гет упустил, глупец.
Опять цирк попер. Все-таки пидорашки унтерменши, как ни крути.
Ну и че ты сделал, сам-то понял? Там пары значений (х у), а у тебя х - просто последовательность натуральных чисел от 1 до 6
Короче, это же числовой ряд, из которого я сделал матрицу Ганкеля. Линейная регрессия недостаточно точно аппроксимирует такие нелинейные значения, да еше и датасет из 3х пар, но мой результат почти такой же как у этого шизика, а твой в 2 раза неправильный.
>Там пары значений
Так y от x должно зависеть,а ты просто взял значения y и поделил их на две части, лол.
>х - просто последовательность натуральных чисел от 1 до 6
Ну правильно, y=2x-x,
> твой в 2 раза неправильный.
Да он и не должен быть правильным, как ты вообще умудрился применять линейную регрессию, когда очевидна эксп зависимость. То, что у тебя получилось "почти такой же" простое совпадение.
>То, что у тебя получилось "почти такой же" простое совпадение.
Это не совпадение, а аппроксимация. Точной она и не могла быть, т.к. зависимость нелинейная, а я использовал линейную регрессию + датасет никакой. Еще раз: из датасета была сделана матрица Ганкеля, что соответствует NARX-модели а потом линейной регрессией была проведена идентификация системы y = f(x). Регрессией т.о. была получена аппроксимация функции f, но т.к. в реальной системе эта функция нелинейна и датасет размером близок к 0, то вышла некоторая, согласись, довольно небольшая ошибочка для данных условий. Похоже, кроме меня про такое никто не слышал? Страшно вы живете, а.
Лол, согласись, что аппроксимация рекуррентного соотношения это всё равно, что сказать "нуу каждый следующий член больше предыдущего примерно в два раза". Это не решение проблемы.
Линейная регрессия - не решение нелинейной проблемы. В остальном идентификация систем как раз для нахождения неизвестных зависимостей выходов от входов. Даже кусочно-линейная аппроксимация (скажем, моделью Такаги-Сугено) функции выхода от входа на таком датасете была бы точнее. Ну и про теоремы об универсальной аппроксимации тут тоже не слышали, эх, африка.
Аппроксимация вообще не решение, понятно, что аппроксимировать много чего можно, речь шла о том, как алгоритмически получить из данных точную формулу, породившую их. Неалгоритмически это сделать можно.
>сделать можно
Иногда.
Ну и применять линейную регрессию можно только в предположении линейности зависости. Иначе смысла в такой "аппроксимации" нет никакого.
>речь шла о том, как алгоритмически получить из данных точную формулу, породившую их. Неалгоритмически это сделать можно.
Во-первых, идентификацией системы это сделать можно. Конкретных примеров полно. Во-вторых, то, что ты называешь "неалгоритмически" на самом деле алгоритм.
Я понял твой уровень знаний в этой теме, дальше меня на эту тему можешь не смешить.
>полно примеров
Хватит нести чушь и заниматься демагогией, примеров полно так неси хотя бы один.
> "неалгоритмически" на самом деле алгоритм
Ага, всё алгоритм, просто мы ещё не поняли этого. Сектант.
>уровень знаний
>в любой непонятной ситуации lm(y~x,data=a)
>примеров полно так неси хотя бы один.
Одна из многих монографий в тему http://b-ok.org/book/448591/9b866b Просвещаем темное африканской быдло, прямо на мейлру!
Берёшь и копипастишь оттуда сюда пример
> как алгоритмически получить из данных точную формулу, породившую их.
Я не собираюсь искать на тысяче страниц то, чего там нет.
>применяет демагогию
>называет кого-то быдлом
Пока быдло тут только ты.
> темное африканской быдло
>R макака
Обосрался с этого просветителя.
Ты думаешь, мне это надо? Я на вопрос ответил, разжевывать какому-то чучелу то, что он в силу своей дебильности не поймет с вероятностью 100% я не собираюсь.
>Ты думаешь, мне это надо?
То есть ты не можешь подтвердить свои слова, пиздабол? Ожидаемо.
Т.е. теперь тебя можно всегда ткнуть носом в твоё говно, косяк теперь за тобой имеется, фуфел.
Я не вижу обсуждения оснований. Кукарекающее чучело - это не обсуждение в любом случае.
Конструктивизм — computer science. Computer science не математика.
Ты просто тупой слишком, чтобы понять почему не прав, поэтому и объяснять бесполезно.
Все математики такие тупые, почему они ещё все разом не перешли на конструктивизм? Идиоты.
благодаря соответствию карри-говарда можно сказать, что математика — computer science.
>Computer science не математика
В таком случае математика не математика
Спрошу тут,, вроде тред по теме :^)
Есть одно задание "доказать ¬(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)
Есть одно задание "доказать ¬(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)
Лень объяснять что-то африканскому быдлу, которое не может в coq.
вполне возможно
только coq от этого нужнее не становится
выходит что у меня с coq'ом общего больше чем у тебя, т.к. ты, очевидно, ни coq ни lean не знаешь
не стыдно?
мимокрок: Давайте переведём разговор в конструктивное русло.
Мне кажется, что Lean - это продукт без бущущего, поддерживаемый исключительно Майкрософтовским пиаром.
Coq же - нечто интересное, но адекватно и продуктивно применимое только после получения кандидатской по математике...
Лично я учу lean, потому что в его изучение проще заход, он написан на плюсах которые, в отличие от окамла, я знаю и кодобаза достаточно компактна и организована чтобы лазить по исходникам когда хочется понять как всё устроено, плюс мне неважна дропнутая поддержка HoTT
А будущее его лично мне пофигу
>Самое глупое из человеческих чувств
для тебя в самый раз
додумался до менее ебанутого решения
lemma Ex₂ {p : Prop} : ¬(p ↔ ¬p) :=
λ (h : p ↔ p → false),
let hp := h.mpr (λ hpₗ, h.mp hpₗ hpₗ)
in h.mp hp hp
всем спасибо
Справедливое утверждение. Написание на С существенно облегчает понимание. Вы всё правильно делаете, я в ближайшие пару месяцев тоже вкачусь.
Поясните, как код прувера на крестах облегчает понимание лямбда-калькулюса, исчисления конструкций и т.д? Ведь для этого достаточно кода на том же коке или лине + понимания самих формализмов.
я () по сорцам собирался лазить не чтобы т.о. учить лямба-калькулюс и CoC а чисто из программерского интереса как оно написано, ну и плюс в лине наличествуют тактики частично/полностью на плюсах - можно будет разбираться как они работают.
Чет нашел какой-то вероятностный метод и википедия дает прямо в определении, что это неконструктивный метод доказательства. И че?
А конструктивная математика и конечная математика — это одно и тоже?
Нет.
Конструктивная математика - это конченная математика.
А как это проверить?
Очевидно с помощью Сuсk.
Пони маете, ваша проблема в том, что вы не видите полной картины. Вы даже внятно не сможете объяснить зачем вообще нужны основания и аксиоматика и для чего там исчисление предикатов, например. С конструктивными основаниями в этом смысле все для вас еще хуже, все эти изоморфизмы карри'говарда, ВНК интерпретации, вычислимость, суждения, натуральная дедукция итд итп сами по себе требуют неких усилий для понимания, но еще хуже, что даже если отдаленное понимание присутствует, то все эти вещи не складываются в целую картинку, тому що мозгов у вас як у хлебушка где все естественно вытекает одно из другого, как итог, конструктивная математика, а уж тем более MLTT для вас выглядит как какая'то лютая оккультная ебулда, бессмысленная и беспощадная, хотя по факту все там просто и понятно.
>все эти изоморфизмы карри'говарда, ВНК интерпретации, вычислимость, суждения, натуральная дедукция итд итп сами по себе требуют неких усилий для понимания
Только если ты совсем отбитый.
А вещественные числа существуют?
Нет, кончено! Раз их нельзя запрограмировать на компуктере, то не существует!
Запрограммировать то можно, но я в любом случае сомневаюсь в их существовании.
Дяденьки, научите меня евклидовой геометрии.
Конструктивисто-петух опять разгулялся. Не видел его с 2012-го года - с тредов про китайца.
>с 2012-го года
Про что несет. Я про интуиционизм и конструктивную математику узнал в августе 2016го.
Как ты про неё узнал?
Прочитал у Максимки статью про MLTT, заинтересовало, почитал Мартин-Лёфа и с удивлением обнаружил, что нихуя не понимаю, о чем вообще речь, хотя изложено стройно и логично. Более пристально взглянув на эту тему, понял что причина в том, что за MLTT стоит нечто мне неведомое, из принципов чего и исходит Мартин-Лёф. Это и оказалось конструктивной математикой. Ну а там на каком-то этапе нагуглил Брауэра и понеслось.
Отрицание бесконечности и конструктивный подход гут. Отрицание закона исключённого третьего бэд. Есть ли где-то система оснований с первым без второго?
>Отрицание бесконечности
>Отрицание закона исключённого третьего бэд.
О какой системе идёт речь?
Вернее 2013-го.
http://arhivach.org/thread/5822/
Он здесь уже забивал последний гвоздь в крышку гроба формализма. Потом последовала череда подобных тредов, навроде теперешних, а затем он пропал.
В плане из второго следует первое?Или наоборот?
Не знаю конструктивных оснований в которых отрицается исключённое третье. Недоказуемость и отрицание это разные вещи.
¬¬(P ∨ ¬ P) теорема в большинстве "видов" конструктивной математики.
Ультрафинитизм Пахома Есенина-Вольпина ж. Поскольку все там конечно, исключенное третье доказывается напрямую простым перебором.
>Ультрафинитизм
> все там конечно
>исключенное третье доказывается напрямую простым перебором.
Во, вот это. Спасибо.
Сделайте что-то вроде "конструктивизм и конструктивные доказательства интерактивно и в
картинках для школьников".
картинках для школьников".
Зачем для школьников, если скоро людям в математике вообще места не будет? Сделают поисковик по доказанным компом теоремам, только нужно будет научиться запросы правильные формировать и вся "человеческая" математика будет прикладной.
Скоро очень скоро
youtu.be/ZxrP3MA2Iwo?t=29
Хотите смешную шутку? Приготовились? В ультрафинитизме все конечные! Ахаха!
>"конструктивизм и конструктивные доказательства интерактивно и в картинках для школьников"
Для школьников смысла нет, в картинках тем более. Если не лезть в философскую сторону вопроса, во что тут все равно никто не может, то самый простой путь - осваивать кок. Возможно, самый простой учебник по коку - software foundations Пирса https://softwarefoundations.cis.upenn.edu/current/index.html
Agda получше будет, разве нет? Тем более для начинающего.
Чем получше? Там с одной установкой пердолинга не оберешься https://hackage.haskell.org/package/Agda-2.5.2/readme + я не знаю внятных IDE под нее, емакс тот еще аутизм от аутистов для аутистов, как ни крути. Кок хотя бы в установке и использовании не сложнее блокнота.
Конструктивист - это умственно отсталый человек, для которого из истинности А не следует ложность не-А. О чём вы тут спорите с умственно отсталыми 4 треда подряд?
>для которого из истинности А не следует ложность не-А
Если бы ты не был конченным, ты бы очень быстро понял, что это доказывается тривиально.
Да мне похуй что ты там можешь доказать, бумага всё стерпит. Другое дело, что в реальности А либо истина, либо ложь, но даунам не достаточно доказательства того что А - истинна для того чтобы убедится что не-А - ложь, им нужно всё доказывать дважды, как будто бывает третье состояние когда А и истинна и ложь одновременно блять.
>но даунам не достаточно доказательства того что А - истинна для того чтобы убедится что не-А - ложь
Что ты несёшь, ебанутый?
P => ¬¬P теорема даже в минимальной логике.
>как будто бывает третье состояние когда А и истинна и ложь одновременно блять
¬¬(P ∨ ¬P) теорема в конструктивной логике.
>состояние когда А и истинна и ложь одновременно блять
Я тебя не так прочитал, ты оказывается ещё более тупой чем я думал.
Это ничего общего с исключённым третьим не имеет, ¬ (P ∧ ¬ P) спокойно доказывается в конструктивных основаниях.
Как искать в поисковике теорем?
Шел уже десятый тред, если считать со /сци, а кое-кто так до сих пор и не понял, что конструктивное доказательство - это построение, а построение - это конструктивное доказательство. И кроме как их построений конструктивным доказательствам взяться неоткуда, а в особенности из каких-то априорных аксиом, в которые нужно веровать вместо собственно процесса построения или задания правил для построения, если уж касаться потенциальной осуществимости или lazy evaluation. Как так могло случиться, что в 21 веке кому-то греет попу необъодимость непосредственно доказать хотя бы один дизъюнкт для доказательства истинности дизъюнкции? Откуда такие хуйлопаны вообще берутся? Я не понимаю.
О чём ты? Не понимаю твой пост, извини.
Я вот понял, например. Меня больше интересует вопрос удобства реального использования. С этим, как я понимаю, пока довольно печально.
>интересует вопрос удобства реального использования. С этим, как я понимаю, пока довольно печально.
Потому что у большинства "врети" случилось еще во времена работ Поста, Тьюринга и Черча, который все это подытожил, написав, что найдены границы математических способностей человека. Хотя так и оказалось, и выше вычислимости все равно не прыгнешь, верунов и сейчас полно. Благо, прогресс не стоит на месте, и хотя реальной математикой занимаются единицы типа Мартин-Лёфа и Воеводского, уже сейчас видно, что все идет к полной автоматизации математики.
Ну, в восьмидесятых тоже все бодренько так шло к полной автоматизации вообще любой интеллектуальной деятельности - чем все закончилось мы знаем. Так что я бы не был столь оптимистичен на твоем месте.
>восьмидесятых тоже все бодренько так шло к полной автоматизации вообще любой интеллектуальной деятельности - чем все закончилось мы знаем.
Ты о чем?
Ээ... AI Winter, все дела?
Для этого даже сейчас техническое развитие никакое, какие уж тут 80-е.
>реального использования
Реального использования чего?
Что ты подразумеваешь под "верунами"?
Под верунами я подразумеваю верующих в то, что математика не равнообъемна вычислимости и существует математика, к вычислимости не сводящаяся (точнее, верующих в то, что нечто, не сводимое к вычислимости, вообще можно называть математикой). Под вычислимостью подразумевается вычислимость на машине тьюринга и др. равнообъемным уточнениям понятия алгоритма (лямбда-определимость, нормальный алгорифм Маркова и т.д.).
>который все это подытожил, написав, что найдены границы математических способностей человека.
Заскринил твой пост. Это пиздец.
Это не математика, а комьютер саенс, и к математике отношение не имеет. Ты даже того же Энгелькинга не осилил. Прямо пропаганда Рыбников стайл.
>к математике отношение не имеет
Почему подмножество математики не имеет отношения к математике?
>Ты даже того же Энгелькинга не осилил
Ты сам не осилил даже пояснить, зачем те скрины притащил.
>Это не математика, а комьютер саенс, и к математике отношение не имеет.
Ты ж сам писал, что в математике не понимаешь, что и так заметно, сейчас бы еще принимать во внимание непойми кого с мейлру, который непонятно с какого диагноза решил, что может опровергнуть Черча с Тьюрингом.
Никто не спорит с Чёрчем и Тьюрингом. Чёрч и Тьюринг не сводили всю математику к вычислимости.
>Ты сам не осилил даже пояснить, зачем те скрины притащил.
Ты говорил, что никто не пользуется мощностями больше, чес счетно. На тех скринах было показано использование таких мощностей, хватит троллить тупостью.
*чем
-быстрофикс
Ты никак не сможешь воспользоваться тем, что несчетно. Но ты всегда можешь написать значок бесконечности, алеф0,1,...,1488 и т.д. и думать, что пользуешься. Хотя по факту пользуешься значками, не несущими в себе ничего, т.к. содержимое, которое за ними предполагается, нельзя ни во что вычислить. Это и есть религия натуральная, поскольку у них там тоже есть значки, символ Аллаха, например. Суть примерно одна.
>Ты никак не сможешь воспользоваться тем, что несчетно
А как же действительные числа?
Все существующие вычислимы, их множество счётно.
>их множество счётно
Множество действительных чисел?
Опять сотый раз по кругу обсуждать одно и то же не вижу смысла. Вещественные числа обсуждали, более того, Тьюринг в своей работе "On computable numbers" машину Тьюринга представлял как имитацию действий человека, вычисляющего такие числа. Отсюда проблема останова, бла-бла и т.д., что уже сто раз обсуждалось.
По твоему множество действительных чисел счётно?
Множество всех существующих вещественных чисел. То есть множество всех чисел, которые ты когда-либо использовал.
А есть несуществующие действительные числа?
>есть несуществующие
Хм...
Я уже сто раз говорил, что нет. Нет, нет, оно несчетно, т.к. это мощность континуума, а еще Брауэр показал, почему континуум невычислим. Итд итп.. Скушно, короче.
>нет, оно несчетно
>Ты никак не сможешь воспользоваться тем, что несчетно
А как же действительные числа?
Ты пользуешься числом с конечным количеством знаков после запятой. И это уже сто раз обсуждалось.
Я пользуюсь не числом, а R, множеством действительных чисел.
Я тут недавно читаю это треды. Похоже, что они реально ебанутые или необучаемые.
> числом с конечным количеством знаков после запятой
Это не число, а приближение числа.
МИМО. ЛОЛШТО?
Ну так я о том же не первый тред толкую. В случае вещественных чисел речь может идти только об аппроксимации его конечным количеством знаков после запятой.
pi,e например. Вычислены только до какого-то знака, приблизительно значит.
Только когда нам нужно вычислить результат. Мы вполне можем работать с тем же pi или e чисто алгебраически. И это уже будет точное значение.
Ты им не пользуешься, а рисуешь его значок. Попытка воспользоваться приведет к бесконечному процессу вычисления.
Попытка вычисления приведёт к бесконечному процессу рисования значков, что дальше? Пользоваться одним экономнее.
>Ты никак не сможешь воспользоваться тем, что несчетно.
А скрины с Энгелькинга? Раз ими никто не пользуется, то почему практически в каждом учебнике анализа вводят множество R, мощность которого больше, чем Q.
>Это и есть религия натуральная, поскольку у них там тоже есть значки, символ Аллаха, например. Суть примерно одна.
Вопрос в том, что считать существующим. Почему, если множества вещественных чисел счетно, об этом не говорят в тех же учебниках матана, но вводят в заблуждение, говоря, что есть и другие мощности?
И в чем проблема в бесконечном процессе вычисления?
>Только когда нам нужно вычислить результат
Естественно. Когда результат не нужон, можно и Аллахов подсчитывать.
>Пользоваться одним экономнее.
Вот только это не пользование, а вера в пользование. Потому что настоящее пользование - это вычисление. И опять же, все это я уже не помню сколько раз писал.
Что плохого в вере в пользование?
>Потому что настоящее пользование - это вычисление
ТЫСКОЗАЛ? Вот это как раз сектанство. Напиши ты pi или 3,141592653589793238462643 что принципиально поменяется?
>И в чем проблема в бесконечном процессе вычисления?
В том, что оно не закончится никогда и сл-но, не может считаться вычислимостью.
>Что плохого в вере в пользование?
В вере нет ничего плохого, веруй на здоровье. Вот только математикой свою веру называть не нужно.
Причём заметь первое абсолютно точное значение, а второе лишь аппроксимация.
>В том, что оно не закончится никогда и сл-но, не может считаться вычислимостью.
А оно должно закончится?
>Напиши ты pi или 3,141592653589793238462643 что принципиально поменяется?
Сто раз писал, что. Даже в этом треде. Вы ж читать не умеете, какая вам математика.
>В том, что оно не закончится никогда
Ну например с рациональными числами там всегда будет период, да, будет повторяться бесконечно, но детерминированно, что плохого то?
Я сам не уверен что верую, просто интересуюсь.
Я по твоему должен все твои посты перечитывать?
>Вот только математикой свою веру называть не нужно.
Как её называть тогда?
Веру? Верой и называй, очевидно же.
Вот только не надо свою веру в калькуляторы называть математикой.
Нужно более подробное название, вера разная бывает.
Вычислимость - это вычислимость, а не вера. Вычислимое можно вычислить, в невычислимое можно только веровать.
"Математикопоклонничество" пусть будет. Поклоняетесь значкам без фактического содержания.
>"Математикопоклонничество" пусть будет.
Слишком длинно.
Какие разделы математики ты считаешь верой в Аллаха?
Вычисление может производиться по самым разным правилам. Вера в одно конкретное не делает его чем-то особенным. А вот связи между объектами остаются всегда, неважно, как ты их запишешь.
Неконструктивные основания. Просто концентрированная вера.
>Поклоняетесь значкам без фактического содержания.
Скорее это ты поклоняешься значкам, забивая на смысл, который они несут. Мельница-вычислитель перемалывает циферки, уаааууу.
99% математики - вера?
То есть любая математика невозможная в конструктивных основаниях?
Далеко не 99%.
Пример с вещественными числами разобрали буквально десяток постов назад. У тебя ж память как у хлебушка.
Ты так и не ответил на вопрос
>Ты никак не сможешь воспользоваться тем, что несчетно.
>А скрины с Энгелькинга? Раз ими никто не пользуется, то почему практически в каждом учебнике анализа вводят множество R, мощность которого больше, чем Q.
Ответил.
Причём тут вещественные числа? Я про вычисления в целом.
В своём манямирке?
>Я про вычисления в целом.
Вот в том и проблема. Стоит разобрать любой конкретный пример и видно все содержание твоего "целого".
В этом треде пару раз.
>Ты никак не сможешь воспользоваться тем, что несчетно.
Все пользуются, как же так? Еретики?
>В этом треде пару раз.
Номер поста?
>Вот в том и проблема
В чём? Ты будешь спорить, что вычисления это правила перемалывания значков?
Обсуждалось в последнем десятке-другом постов. Вы просто эталон необучаемости, я думал, что необучаемее хохлозависимых в крымтреде не бывает, а вот нашел.
Так ты ещё и /по/рашник, лол. Ну так давай ссылку или проследуй нахуй. Нихуя ты не ответил, я следил, спустил на тормозах свой обосрамс, думая, что никто не заметит.
Не все значки одинаково полезны, опять же, разница обсуждалась.
Вера в полезность достаточный критерий для тебя?
Сто раз писалось про канонические и неканонические элементы и выражения и т.д. Мне реально лениво каждую сотню постов переписывать все, мною уже сто раз писанное. Ну необучаемые вы тута, бывает. Для мейлру это норма, как и для рашки в целом.
>Сто раз писалось
>не может скопипастить
Просто пукнул в лужу, ясно.
Ты можешь один раз написать, заскринить, а после кидать скрины со своим ответом. Ты просто тупой и троллишь тупостью.
Одно из двух. Третьего не дано
>Ты просто тупой и троллишь тупостью.
Я писал даже, в чем тут проблема у большинства вы никогда ничего не поймете, поскольку либо ничего для этого не делаете, либо делаете, но тема не ваша.
Он троллит тупостью неосознано, как ребёнок, нагадивший в штаны, и радующейся, что прохожие шарахаются от него из-за вони.
Просто тут 3.5 математика на всю борду, да и те на первом курсе мухгу обучаются.
Нет, осознанно. Если неосознанно, значит просто тупой. Третьего не дано. Нельзя быть тупым и троллить тупостью одновременно.
Как скажешь.
Лол.
>Третьего не дано
А если в моих основаниях дано?
Какие есть основания где можно доказать, что аксиома Аллаха (выбора) не верна?
Тогда у тебя нет оснований для беспокойства.
Твоя вера в неё не делает её верной в любой формальной системе.
А твоя вера не делает её неверной в любой формальной системе.
Проблема только в том, что любая неконструктивная формальная система, в которой даже нет требования доказать аксиоматику, сама по себе чистая вера. Тот же закон исключенного третьего. Как можно веровать в дизъюнкцию, если нет условия построения/доказательства одного из дизъюнктов? Это же нечто уровня веры в то, что когда ты идешь поссать в сортир, вероятность встретить там бэтмена верхом на динозавре 50%, т.к. по закону исключенного третьего - либо встретишь, либо нет. Шизофрения натуральная, да? А вот на такой шизе пытаются построить основания математики - самого точного знания, что вообще есть у человечества. Больные, епту...
>Чего?
Того. Аксиомы вам боженька дал на горе синай? С какой стати ты веруешь в дизъюнкцию без доказательства одного из дизъюнктов, а? А потом кто-то удивляется кризису оснований.
Ну я об этом и толкую. Когда ты общаешься с богом - это молитва. А вот когда бог общается с тобой - это уже шиза.
Рамануджан очень кстати. Заниматься математикой без математического образования и культуры, не имея понятия о формализме как о методе вообще, можно только одним способом - манипуляцией с ментальными построениями.
>Заниматься математикой без математического образования и культуры, не имея понятия о формализме как о методе вообще, можно
Ну раз двощи разрешили...
Есть книжка, мол, как стать как Сринивас из позиций конструктивной математики? Да и вообще "конструктивная математика и психология", "конструктивная математика и сознание", "конструктивная математика и эмоции" да прочее?
>Я и не говорил про любую систему, еблан.
>Твоя вера в неё не делает её верной в любой формальной системе.
>еблан
>Какие есть основания где можно доказать, что аксиома Аллаха (выбора) не верна?
>Но она верна
Ты говоришь, что твоя вера верна в любой формальной системе, еблан.
Я говорил, что в любой? Нет. Просто ты чсвшный долбаёб.
Я спрашиваю, есть ли основания где она доказуемо неверна. Ты говоришь, что она верна. Следовательно таких оснований нет, то есть она верна в любой системе (что уже не правда, даже если без доказуемости).
>Следовательно таких оснований нет
??? Совсем не следовательно.
мимо
Если она верна во всех основаниях, то нет оснований где можно доказать, что она неверна. Противоречивое дерьмо наподобие ZF я не рассматриваю.
>Противоречивое дерьмо наподобие ZF
А оно противоречивое?
>конструктивистов
В каком посте я называл себя "конструктивистом"?
Доказательство действительно тривиально. Подумай над этим немножко.
Одна хуйня. Где я называл себя "ко-ко-конструктивистом"?
Пример противоречивости, раз так тривиально. Я жду. И прекращай демагогию, мань.
>Пример противоречивости
Доказательство не конструктивно. Но из него следует, что ZF противоречива.
А почему мы должны верить только в конструктивные доказательства?
О доказательстве того, что ZF противоречива. Где оно?
>А почему мы должны верить только в конструктивные доказательства
О чём ты?
Я ничего не говорил про веру в правила построения. Доказательство не конструктивно, следовательно оно не даёт конкретного примера.
Доказательство есть, но оно не конструктивно. И поэтому нет примера.
Ты вообще отбитый? Есть доказательство противоречивости ZF. Следовательно ZF противоречива.
Оно на самом деле тривиально. Нужно всего лишь доказать непротиворечивость ZF в самой ZF.
>Если она верна во всех основаниях, то нет оснований где можно доказать, что она неверна.
Да, но ты заявлял другое.
> Ты говоришь, что она верна. Следовательно таких оснований нет
Ты вообще еблан видимо. Или просто читать не умеешь. Или просто в математику самую простую не можешь. Понятно всё с тобой.
Слышал про HoTT, разобрался в нём. Он, вроде какой-то в прямом смысле недоделанный.
В чём его проблема? (Пишите смело факты)
Вроде есть какая-то недоказанная гипотеза. Что она за зверь?
>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.
>как стать как Сринивас
Он же с детства свои умения развивал. Вся его жизнь как одно доказательство тезиса Черча. А вообще, http://gen.lib.rus.ec/book/index.php?md5=74ED3244789E3A66301750212342D470 1ая глава.
> HoTT,
Я в ней не разбирался, как по мне - какая-то странная надстройка над MLTT.
Ух, прояснил, спасибо.
Единственное, что непонятно : "Computational interpretation of homotopy type theory is an open problem."
Что это такое, "вычислительная интерпретация"?
Есть более простые примеры, показывающие суть понятия?
>Единственное, что непонятно : "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.
Полностью конструктивной модели пока нет.
>Есть более простые примеры, показывающие суть понятия?
Машина Тьюринга.
А где конкретно в тексте аксиома выбора существенно используется? Про это что-нибудь знаете?
Что можно почитать в качестве введения в формальную теорию типов? С "неформальной" уже более менее знаком.
Конкретнее не знаю, я НоТТ не читал.
Барендрехт, не? http://ttic.uchicago.edu/~dreyer/course/papers/barendregt.pdf
очень годное чтиво, спасибо.
мимоанон
Аноны, поясните за вычислимость утверждений формальной теории. Вот есть некая аксиоматическая теория и есть некое утверждение. Можно ли вычислить истино оно или ложно?
>вычислимость утверждений формальной теории
Я думаю ты имеешь ввиду разрешимость верности утверждений в этих теориях.
Почитай про арифметику Пресбургера, всё что намного сильнее неё неразрешимо (то есть не существует алгоритма, который вычисляет истинно или ложно какое-либо утверждение). Например арифметика Пеано уже неразрешима.
Но ведь проект компьютеров пятого поколения не удался.
Ты путаешь вычислимость и выводимость в формальной системе. Второе вообще никак не подразумевает первого. Возьмем например истинность формулы в исчислении пропозишенов. Поскольку классически, по закону исключенного третьего, пропозишен может быть истинный или ложный, то мы можем по методу Тарского нарисовать Аллаха таблицу с этой формулой пикрелейтед, из которой выводима ложность или истинность этой формулы исходя из ложности или истинности входящих в нее пропозишенов. В данном примере, классически эта формула истинна в любом случае. Прикол же в том, что конструктивно (исходя из интерпретации логических констант, в частности, свойств импликации, по Гейтингу) эта формула (известная как формула Пирса) невычислима.
Вы ничего не понимаете в выводимости. Она не связана с интерпретацией.
Читать не умеем? Я не утверждал, что выводимость связана с интерпретацией.
Формула F выводима, если существует хотя бы одна конечная последовательность формул, в которой последняя формула - это F, а любая предшествующая формула есть либо аксиома, либо получается применением модус поненс. Понятие "выводимость" не зависит от понятий "истинно" и "ложно".
Ну и? Из выводимости формулы никак не следует ее вычислимость, пример я привел - это формула Пирса.
В огороде бузина, а в Киеве дядька. Ты зачем таблицу истинности нарисовал?
А ты пост почитай, там написано.
Такая-то самоуверенность.
>пикрелейтед, из которой выводима ложность или истинность
Как это понимать? При чем тут таблицы истинности? Понятно, что полнота исчисления высказываний и бла-бла-бла. Но речь о выводимости. Ты какие книжки по математической логике читал?
А вот вы тоже напутали: формула Пирса невыводима в интуиционисткой логике, поскольку существует модель Крипке, где она не истинна.
Вычислимость функции - это про другое: существует такая машина Тьюринга, которая по заданным аргументам некоторой функции за конечное число ходов предъявит значение этой функции.
Так вот иногда доказательством импликации A->B является вычислимая функция f:A-->B, преобразующая доказательство утверждения А в доказательство утверждения B.
В силу неизвестных мне чудес(т.е. изоморфизму Карри-Ховарда) оказалось, что всё, что выведено из интуиционистских аксиом - может быть собрано из таких вычислимых функций.
То есть уже не надо заново строить машины Тьюринга - просто бери и пользуйся интуиционисткой логикой как конструктором. Оттуда и "конструктивизм", он же - "интуиционизм".
Невычислимо же - доказательство формулы Пирса, если его воспринимать как функцию.
---------------
Я это всё написал, но мне хотелось бы дополнительного контроля - всё же верно я рассказал?
>Так вот иногда доказательством импликации A->B является вычислимая функция f:A-->B, преобразующая доказательство утверждения А в доказательство утверждения B.
И именно в таких случаях мы можем говорить об истинности в конструктивном смысле слова. Поскольку суть конструктивной выводимости - вычислимость. А не общие недоказуемые заявления.
>В силу неизвестных мне чудес(т.е. изоморфизму Карри-Ховарда) оказалось, что всё, что выведено из интуиционистских аксиом - может быть собрано из таких вычислимых функций.
Интерпретация логических констант по Брауэру-Гейтингу-Колмогорову это называется. Конкретно чаще всего речь о конструктивной логике Гейтинга.
Окей, мы согласны.
Давайте теперь представим, что некая теория легко описывается в классической логике и очень-очень трудно в интуиционисткой.
Зачем нам тогда вычислимый вариант?
Ав едь ещё он может и вообще не существовать... Тогда получается, что отказываясь от веры в одни формальные системы, вы впадаете в другую крайность, веря, что существует именно вычислимая формальная система, подходящая для любых стоящих перед вами задач.
Получается, что на стороне ваших оппонентов - проверенная годами практика, а на вашей стороне - только ваши, демонстрируемые на дваче, идеалы.
Это похоже на мечты, которые разрушил Гёдель, только в новой обложке.
как вам такой вброс?
>Тогда получается, что отказываясь от веры в одни формальные системы, вы впадаете в другую крайность, веря, что существует именно вычислимая формальная система, подходящая для любых стоящих перед вами задач.
Обсуждали уже. Да еще Тьюринг показал, что даже если к его машине приколхозить боженьку, могущего в решение алгоритмически неразрешимых задач, это ничего не решит, т.к. не снимает вопроса о проблеме останова уже прокачанной таким образом машины Тьюринга. Отличие веры от вычислимости тоже сто раз уже обсуждали. Границы математических способностей хоть человека хоть роботов - это вычислимость, как ни крути, выше не прыгнешь. Это тоже с 40-х годов прошлого века известно.
>веря, что существует именно вычислимая формальная система, подходящая для любых стоящих перед вами задач
О чём ты вообще?
>это вычислимость, как ни крути
веруны неисправимы.
>Границы математических способностей хоть человека хоть роботов - это вычислимость
Эта фраза лишена смысла. Не отличается от фразы "направление лингвистических одаренностей арийцев - это гладиолус".
Нет.
Давай я тебе объясгю, почему это не так. Вот ты написал в своем посте то, что написал. Но почему ты так написал? Потому что тебе свербит, и обязательно нужно что-то мне ответить? Или потому что ты можешь доказать эти свои слова, например, конкретным примером, начисто опровергающим тезис Черча тут стоит заметить, что сама эта фраза принадлежит как раз Черчу? Я уверен, что опровергнуть тезис Черча ты не можешь, это если предположить, что его опровержение вообще возможно, хотя в настоящее время человечеству ничего такого неизвестно. Тогда о чем твоя батрушка вообще? Не пони маю.
>веруны
Во что веруны-то? Вычислимость - это непосредственный конструктивный объект, а не объект веры как всякие не считающиеся ни во что значки алефов и бесконечностей.
Будь добр, приведи пример "конструктивного объекта". А то непонятно, что ты под этим подразумеваешь. (Объекты какие-то... Функция - понятно что такое, а объект - уже непонятно)
>приведи пример "конструктивного объекта"
Да я уже и не помню сколько раз приводил. Толку все равно 0.
>Функция - понятно что такое, а объект - уже непонятно)
И что по-твоему есть функция?
Ещё раз, какую пользу работающему математику проиносит отказ от
1) исключённого третьего,
2) аксиомы выбора.
1) исключённого третьего,
2) аксиомы выбора.
Определение функции:
(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 ) )
*exactly
я понимаю твою усталость, но всё-таки интересно об этом поговорить
>работающему математику
Если в твоей области не видно какой-то пользы от этого, то ты и не математик. Анализ и прочее дерьмо не является математикой.
Как ты сам себе оправдываешь глупость и низость твоего падения? Уровень этих ответов - ниже плинтуса же.
>низость твоего падения
Низость какого падения? Это мой первый пост в треде.
>Уровень этих ответов - ниже плинтуса же.
Примерно как аксиома выбора.
Ты обосновать свою позицию не сможешь, иди учись, не мешай взрослым дядям обсуждать интересные вещи.
Моя позиция очевидная (для математиков) и не нуждается в обоснованиях.
Все "взрослые дядьки" уже давно поняли, что аксиому выбора использовать не нужно.
Начнем с того, что "границы математических способностей" - это вообще непонятно что такое. Утверждать, что некая неопределенная вещь является тем-то и тем-то, - безумие.
>"границы математических способностей" - это вообще непонятно что такое.
Я подозреваю, тебе вообще очень многое непонятно. И не только в математике. Причем тут определенность или неопределенность некоторых утверждений, а тем более их "безумность" не очень ясно. В данной фразе речь о предположительной равнообъемности математики и вычислимости. В пользу такой точки зрения можно привести тезис Черча. Говоря проще, до тех пор пока не получены примеры, опровергающие этот тезис, упомянутое утверждение можно считать истинным. На настоящий момент любой пример, известный человечеству подтверждает тезис Черча. Так что со своим школоцентризмом, основанным на твоем школомнении обо всем на свете, дул бы ты в школку, а не лез в вопросы, до которых тебе сильно дальше чем до луны пешком.
Галиматья.
Жалко, что мод удаляет посты - все бы видели, что с тобой бесполезно говорить, так как ты делаешь безосновательные, громкие, а главное - бессмысленные заявления, и никак не обосновываешь их.
Ты прёшься от того, что тебя не понимаю, но это не от того, что ты умён. Ты жалок.
мимоанон
>ты делаешь безосновательные, громкие, а главное - бессмысленные заявления, и никак не обосновываешь их.
Пример подобных из предыдущего поста можно? Если ты тупее моих тапочек, это не значит, что все тебе непонятное - галиматья. Если бы ты это понял, но ты не поймешь.
Думаешь ты охуеть какой тролль? Засунь себе твои гнилые недоидеи в жопу.
>Думаешь ты охуеть какой тролль?
Думаю, что ты пидорашка тупая. Более того, уверен, что не ошибаюсь.
Там же анон сказал, что он мимопроходил был, а не конструктивист-кун.
этот пост не соответствует теме треда и тоже должен быть удален
Алсо,
> Галиматья.
Аргументировал как бог просто. Тебе с такими аргументами в деградации тред.
Конструктивистопетуха в его категоричности я, кстати, не поддерживаю. С этим постом согласен. Но от этого "Галиматья" аргументом не становится.
этот пост тоже является частью мета-дискуссии и должен быть удален
Ты меня учишь аргументировать? Тут явно, что какой-то мудак просто выёбывается и портит дискуссию на нормальную тему.
Нет ты, и похоже ты этого не понимаешь из-за неоправдано большого самомнения.
Матач, что происходит на http://www.mi.ras.ru/?c=noc? Где расписание на новый семестр? Они будут работать в этом семестре? Может быть, они уже начали, но простым смертным не сообщили? Кто-нибудь знает?
ЗАРЕПОРТИЛ!!!! ЧТО ЗА БАЗАР УСТРОИЛИ В ПРАВОСЛАВНОМ ТРЕДЖЕ??!
я выбрал самый бессмысленный тред, чтобы спросить
а где надо было?
вопрос вообще-то важный
Вычислимость - это действительно очень интересная тема.
Будем надеяться, что местный её фанат направит большую часть своей энергии в продуктивное русло вроде обсуждения с высокой строгостью необходимых теорем.
Если предлагать тему, то вопрос:"чем надозаниматься?" Где открыт фронт работ, доступный для студентоты с двачей?
>Будем надеяться, что местный её фанат направит большую часть своей энергии в продуктивное русло вроде обсуждения с высокой строгостью необходимых теорем.
Пробовал, не заходит. Закатывания глаз и кукареканья бесноватых начинаются примерно на фразе "изоморфизм Карри-Говарда". А без этого уже не объяснить, почему лямбдаР (AUTOMATH де Брауна, например) это то же самое, что исчисление предикатов. Про что-то более сложное (Кок тот же) и говорить нечего.
Тебе задают вопросы, а ты их игнорируешь.
>Просто пренебрегаем последним членом
>И, чем больше n, тем смелее можно пренебречь последним членом суммы.
Гармонический ряд обоссывает эту логику.
>Проблема только в том, что за всем этим стоит не пустой синтаксис ни о чем, как в формализме, а вычислимая конструктивная математика, где даже понятие равенства имеет вычислительное содержание.
Вот в чём твоя проблема. Ты приравниваешь синтаксические конструкции к смысловым, и из этого выводишь, будто твой конструктивизм чем-то отличается от формализма. Проснись, ты обосрался!
>Считающаяся в термы из квинтиллионов знаков. Это проблема, пони маешь? Потому что если мы захотим это на самом деле посчитать, то...
Ты с ума сошёл? Зачем каждый раз заново выводить всю предшествующую математику, если теорема - это и есть ёбанный квинтиллион знаков, полностью доказанный? Аксиомы-то остались неизменны, зачем каждый раз перепроверять вывод?
>Тебе задают вопросы, а ты их игнорируешь.
Мне начинают нести такую ахинею, что уши вянут. Вот типичный пример какой-то школотрон думает, что опроверг интуиционизм в 2017 году. И что отвечать в таком случае? Я, разумеется, мог бы процитировать Брауэра https://projecteuclid.org/euclid.bams/1183422499 Гейтинга или Маннури по поводу разницы между интуиционизмом и формализмом, а она есть, и существенная. Но кто здесь хотя бы поймет о чем вообще речь? Никто, очевидно же. Тут чуть выше никто так и не въехал в разницу между классической и конструктивной логикой для формулы Пирса какие же вы деграданты, пиздец просто. Как итог, получу еще больше неинтересного мне кукареканья и истерик.
>Вы даже внятно не сможете объяснить зачем вообще нужны основания и аксиоматика и для чего там исчисление предикатов, например.
Чтобы не обосраться, как на пике - т.е. всегда применять методы, адекватные данным и задачам. Основания нужны потому что, как показывает практика, обосраться можно даже в элементарных вещах.
Существуют объекты, достаточно точно описываемые вещественнозначными функциями вещественного же аргумента.
>Отрицание бесконечности и конструктивный подход гут.
И чем же он гут?
Жак Адамар, "Исследование психологии процесса изобретения в математике"
>разницы между интуиционизмом и формализмом
Всего-навсего другой набор аксиом, вот и всё. Но маняучёным не дают покоя лавры Пуанкаре, Римана и Гильберта, поэтому очень уж хочется сделать что-нибудь "особенное" поэтому они придумывают никому ненужные системы с крайне геморроидальным выводом даже простейших теорем и эпатажно отрицают то, что успешно применяется на практике годами.
>Всего-навсего другой набор аксиом, вот и всё.
Я тебя услышал, ага. А ничего, что у Брауэра вообще аксиом не было? А про логические отрицания ты что знаешь? По Маннури, конструктивное отрицание - это choice negation, отрицание в классической логике - exclusion negation. Из чего следует 4 разновидности только двойного отрицания, из которых только 2 эквивалентны утверждению (двойные choice и exclusion negation). Если их миксануть, интереснее получается. Но логика никому не интересна, проще ж веровать в аксиомы полученные Гильбертом в виде скрижалей на горе сион.
Ты, похоже, плохо представляешь себе, что такое аксиома. Если у Брауэра аксиом не было, то не было и определений. А без определений не о чем и размышлять. То, что в работах этого господина аксиомы присутствуют неявно, без огромной надписи АКСИОМЫ и пронумерованного списка может и рвёт шаблон, но сущности не меняет.
>Ты, похоже, плохо представляешь себе, что такое аксиома.
И что же это такое? В натуральной дедукции аксиома - это логическое заключение без посылок, т.е. нечто, принимаемое без предшествующего контекста, из которого это нечто можно вывести, т.е. нечто, ниоткуда не выводимое, а принимаемое "как есть". С такой позиции даже в MLTT аксиом нет, т.к. там 4 правила вывода и все они начинаются с контекста. Про Брауэра и говорить нечего, он даже конструктивную логику Гейтинга назвал "любопытным, но бесплодным примером", сам Гейтинг тоже явно оговаривал, почему конструктивная логика не формализует брауэровского интуиционизма.
>это логическое заключение без посылок
>логическое заключение без посылок
Уже сама эта фраза полностью демаскирует полное незнание тобой терминологии, которой ты так презрительно разбрасываешься. Аксиома - это утверждение о свойствах, элементарная часть определения. Связка аксиом и образует полное определение.
>принимаемое без предшествующего контекста
Аксиомы не являются выросшей на пустом месте игрой ума. Они были сформированы с учётом опыта обращения человечества с числами. Они строго очертили неясные до той поры понятия и позволили прежде всего без опасений выводить новые и новые следствия. Они показали границы применимости методов, с их помощью можно всегда ответить на вопрос "А правильно ли я поступаю? Не пытаюсь ли я сложить красное с длинным?" Они позволили, наконец прояснить собственно пути математики, сделав рассуждения кристально прозрачными.
Интуиционизм же является не более, чем оголтелым скептицизмом, который сомневается даже в собственном здравомыслии. И странное дело: интуиционизм яростно отрицает одно и столь же яростно отстаивает другое совершенно не желая признавать за собой место обычной формальной системы.
>там 4 правила вывода и все они начинаются с контекста.
А контекст-то с чего начинается? А правила на чём основываются?
>Уже сама эта фраза полностью демаскирует полное незнание тобой терминологии, которой ты так презрительно разбрасываешься.
Вообще-то я привел вполне официальное определение аксиомы, пикрелейтед http://www.cs.cornell.edu/courses/cs3110/2013sp/lectures/lec15-logic-contd/lec15.html
>Аксиомы не являются выросшей на пустом месте игрой ума. Они были сформированы с учётом опыта обращения человечества с числами. Они строго очертили неясные до той поры понятия и позволили прежде всего без опасений выводить новые и новые следствия. Они показали границы применимости методов, с их помощью можно всегда ответить на вопрос "А правильно ли я поступаю? Не пытаюсь ли я сложить красное с длинным?" Они позволили, наконец прояснить собственно пути математики, сделав рассуждения кристально прозрачными.
Я чуть выше ссылался на статью Брауэра, он там как раз поясняет за необоснованность таких методов, когда нечто, выведенное из конечного априори и бездоказательно обобщается на бесконечное. Как исключенное третье, например.
>Интуиционизм же является не более, чем оголтелым скептицизмом, который сомневается даже в собственном здравомыслии.
Требование построения доказательства - это не оголтелый скептицизм, а вполне резонное условие для математики, которая вообще-то является самым точным знанием, известным человечеству. Верования там неуместны вообще никак. И где в интуиционизме сомнения в собственном здравомыслии?
>А контекст-то с чего начинается?
С конструктивных объектов.
>А правила на чём основываются?
На возможных манипуляциях с элементами контекста.
>Вообще-то я привел вполне официальное определение аксиомы, пикрелейтед
Ты понимаешь что у тебя "логический вывод" из ничего?
>Я чуть выше ссылался на статью Брауэра, он там как раз поясняет за необоснованность таких методов, когда нечто, выведенное из конечного априори и бездоказательно обобщается на бесконечное.
Да, некоторые вещи приходиться принимать без доказательств. Правда в том, что если мы вот прям счас откатимся в каменный век интуиционизма и забудем большую часть теорем существования - нам придётся лишиться очень, очень многого. Оно того не стоит.
>Требование построения доказательства - это не оголтелый скептицизм, а вполне резонное условие для математики, которая вообще-то является самым точным знанием, известным человечеству.
В "формализме" доказательства строятся настолько замечательно, что их можно проверить исключительно основываясь на синтаксисе.
>И где в интуиционизме сомнения в собственном здравомыслии?
В том, что интуиционисты начинали с классики. Затем они зачем-то её кастрировали, переформулировали и вуаля - новая теория. Правда, она оказалась не то чтобы очень нужной. Но всё же, новую теорию придумать - это не хухры мухры.
>С конструктивных объектов.
И как же они определяются?
>На возможных манипуляциях с элементами контекста.
Почему это они возможны?
>Ты понимаешь что у тебя "логический вывод" из ничего?
Я-то пони маю. Теперь и ты вроде начинаешь. Аксиома - это логический вывод из ничего, в противном случае это бы не аксиомой называлось.
>Да, некоторые вещи приходиться принимать без доказательств.
В церкви - сколько угодно. Но не в математике.
>Правда в том, что если мы вот прям счас откатимся в каменный век интуиционизма и забудем большую часть теорем существования - нам придётся лишиться очень, очень многого.
Например? Чего многого-то? Полторы все равно невычислимые фофудьи типа исключенного третьего - это немного. И раз они все равно невычислимы, считай, что мы их и так лишены, использовать-то все равно нельзя, только рисовать.
>В "формализме" доказательства строятся настолько замечательно, что их можно проверить исключительно основываясь на синтаксисе.
Из которого нельзя вывести ничего кроме этого синтаксиса. Самый простейший пример - формулу Пирса и таблицы тарского я уже упоминал.
>В том, что интуиционисты начинали с классики. Затем они зачем-то её кастрировали, переформулировали и вуаля - новая теория.
Ой, всё... В каком месте Брауэр начинал с классики? Ты же его даже не читал, но осуждаешь, как совки Пастернака. Даже ту картинку с Брауэром на дачке и 1 и 2 актами интуиционизма, которую я сто раз постил, не читал.
>И как же они определяются?
>Почему это они возможны?
А вот тут опять надо писать страшные слова, с которых бесноватых корежит - интрерпретация логических констант по Брауэру-Гейтингу-Колмогорову.
> Аксиома - это логический вывод из ничего
Это не логический вывод, потому что предпосылок нет.
>В церкви - сколько угодно. Но не в математике.
Ты хочешь сказать, что можешь доказать непротиворечивость кокструктивистской хуйни средствами самой теории? Она только кажется тебе убедительной, в основном из-за своей радикальности, но на имеет под собой ровно столько же оснований, что и любые другие непротиворечивые основания математики. Интуиционистский неуместный аскетизм предлагает резать всё циркулярной пилой и ножом - ну а хули, режет же, чего ещё надо?
>Полторы все равно невычислимые фофудьи типа исключенного третьего - это немного. И раз они все равно невычислимы, считай, что мы их и так лишены
Теоремы существования кокструктивизмом не признаются, однако часто, чтобы рассчитать то, существование чего доказывает теорема, необходимо провести над этим чем-то определённые манипуляции. Прямо как здесь:
допустимость операций определяется сходимостью ряда, что определяется существованием предела. Более того, поскольку сам придел - понятие неарифмитическое, он впринципе выпадает из рассмотрения конструктивистской секты. И что же конструктивисту делать, если его инженер попросит рассчитать работу?
>Из которого нельзя вывести ничего кроме этого синтаксиса.
Ты сравниваешь тёплое с мягким. Синтаксис позволяет проверить правильность умозаключений, но отнюдь не призван заменить работающую голову.
>В каком месте Брауэр начинал с классики?
Он начал с изучения классической математики. Он не сделал свои выводы, сидя на дачке с полной изоляцией от внешнего мира.
>интрерпретация логических констант по Брауэру-Гейтингу-Колмогорову.
Эти константы были положены, постулированы, как постулируется существование множества натуральных чисел. Кстати об N - оно ж бесконечно, а значит необходима очень ловкая логическая конструкция, которая позволяет манипулировать натуральными числами, не так ли?
>Это не логический вывод, потому что предпосылок нет.
Я же даже скрин логического вывода аксиомы дал. Врети?..
>Он начал с изучения классической математики.
Он с нее не начал, а просто изучал в школке и в универе, как и все остальные. Это разные вещи.
>Эти константы были положены, постулированы, как постулируется существование множества натуральных чисел.
Множество натуральных чисел задано правилами его построения, там нечего постулировать.
>Кстати об N - оно ж бесконечно, а значит необходима очень ловкая логическая конструкция, которая позволяет манипулировать натуральными числами, не так ли?
Не так. Опять же, обсуждали уже все это. В том числе и отличие актуальных бесконечностей от абстракции потенциальной осуществимости.
>логического вывода аксиомы дал
Мне непонятно, из чего выводится аксиома. Я отказываюсь выводить из ничего чего-либо. Я лучше спокойно признаю произвольность аксиом.
>Он с нее не начал, а просто изучал в школке и в универе, как и все остальные. Это разные вещи.
Он её изучал, она была его первой дверью в математику. Классическая математика - это необходимый этап в эволюции его взглядов. Я даже рискну предположить, что до определённого момента он верил в классическую математику.
>Множество натуральных чисел задано правилами его построения, там нечего постулировать.
Нечего постулировать, кроме правил построения и канонического элемента, ты хотел сказать.
>отличие актуальных бесконечностей от абстракции потенциальной осуществимости
Какие проблемы устраняет отказ от актуальной бесконечности и принятие потенциальной, вот что интересует меня в первую очередь.
> Какие проблемы устраняет отказ от актуальной бесконечности и принятие потенциальной, вот что интересует меня в первую очередь.
Актуальная бесконечность невычислима.
>невычислима
И что?
Невычислимое может быть принято только на веру. Математика - это не верунство.
Вычислимость сама по себе -верунство.
Докажи.
Ты, кажется, не отличаешь аксиомы и правила вывода. Прочитай какой-нибудь учебник по мат.логике, первый курс мехмата.
>кажется,
Крестись. Разве я виноват, что про натуральную дедукцию ты от меня позавчера услышал? Подумой, ты ж даже аргументы не воспринимаешь. Я тебе даю ссылку и даже конкретный скрин, ты глаза закатил и пытаешься доказать мне, что это я что-то не знаю.
Ээ... Шта? Это мой первый пост в этом треде. Креститься надо, да.
Я вот об этом если что.
Ээ... Прочитай, кому был адресован мой пост. Ты, кажется, просто триггеришься на определенные слова своей вечной мантрой про "я дал скрин, прочитайте, вы ничего не понимаете, уже тысячу раз объяснял". Ты точно не бот?
>Какие проблемы устраняет отказ от актуальной бесконечности и принятие потенциальной, вот что интересует меня в первую очередь.
А что вообще актуальная бесконечность делает в математике? Это даже не математический объект. Проблема как раз в этом. В математику за тысячи лет понатащили всякой хуйни, никакого отношения к ней не имеющей. В основном из третьесортной философии типа платонизма. Причем, в самые основания понатащили. А потом вжух и кризис оснований.
Что такое "актуальная бесконечность"?
У тебя еще есть время научиться пользоваться гуглом. В чебурнете такой возможности уже не будет, поторопись.
Похоже на хуйню какую-то, даже скорее всего выдуманную и несуществующую.
Зачем мне время тратить на поиски её в гугле? Тем более если я гос. веб сайтам не совсем доверяю в таких вопросах.
>Похоже на хуйню какую-то, даже скорее всего выдуманную и несуществующую.
Актуальная бесконечность хуйня и есть, как и любые другие попытки использовать платонизм в математике. Но с этой хуйней проще, ей можно заткнуть открытую проблему и кукарекать, что математика к вычислимости не сводится.
Но математика действительно к вычислимости не сводится.
Примеры будут?
Теория множеств - это математика?
Местами. В оригинальном своем виде это невычислимая аксиоматика, в качестве оснований непригодная как минимум из-за исключенного третьего. Если даже довести до ума, все равно не идет дальше лямбда-Р в кубе Барендрегта, а в 2017 это несерьезно.
Когда там конструктивисты гипотезу Римана докажут? А то в 2017 как то не серьезно.
А неконструктивисты когда? Все-то вас тянет ко всякой бесконечной комбинаторной хуйне из прошлого тысячелетия типа ферзей да римановых ноликов.
>А неконструктивисты когда?
Оставляем эту почетную проблему вам, а то у вас совсем как-то плохо. Почти никаких задач не решаете, всё дрочите на свою вычислимость.
Окей, а каков порядок ℤ? Или у вас не существует бесконечных групп?
>бесконечной комбинаторной хуйне из прошлого тысячелетия типа ферзей да римановых ноликов
А вот если бы ты не был необразованным селюком, ты бы знал что почти вся эта наука о "вычислимости" сводится к задаче о ферзях.
Каким образом?
Любая NP-полная задача сводится к любой NP-полной.
>Окей, а каков порядок ℤ?
У ℤ нет конечного порядка.
>Или у вас не существует бесконечных групп?
Существуют группы, которые не являются конечными.
А это нормально, что меня от использования аксиомы выбора и исключённого третьего подташнивать начинает?
А меня вот бесит аксиома пары. Каждый раз, как о ней думаю, аж зубы сводит, так сильно эту аксиому ненавижу. Блядские веруны в пару, так бы и запретил.
Я не использую теорию множеств, я же не совсем конченный.
>Любая NP-полная задача сводится к любой NP-полной.
И что? Класс задач, разрешимость которых можно проверить на машине Тьюринга за не более чем полиномиальное от размера входных данных время - это далеко не вся "наука о вычислимости". И это чудо капустное кого-то будет селюком называть.
Какова природа математической истины? Вот 1+1=2 это вроде как истина, но истина не такая как "Расстояние от моей лобковой кости до конца головки моего члена в эрегированном стоянии составляет 13см, что является средним и нормальным значением". Знаю людей утверждающих что математика это вообще не про истину и не про объективность, а просто маняфантазёрство.
-> /ph
>Какова природа математической истины?
Классически в математике истинно то, что непротиворечиво. Конструктивно - истинно то, что построимо, т.е. конструктивные объекты и доказуемве / выводимые / наблюдаемые их свойства.
>Вот 1+1=2 это вроде как истина, но истина не такая как "Расстояние от моей лобковой кости до конца головки моего члена в эрегированном стоянии составляет 13см, что является средним и нормальным значением".
Есть мнение, что точно такая же. Пикрелейтед, выделенное. Математический релятивизм Маннури - утверждение о сводимости любого концепта к любому другому, т.е. если есть концепт A и другой концепт В, то первый можно свести ко второму через конечное число промежуточных концептов A1,...,An таких, что концепт А представим в форме концепта А1, а концепт An представим в виде концепта В. Концепты, например, могут быть любыми математическими объектами, принадлежащими любой аксиоматике, теории и т.д. В твоем примере даже этого не требуется, поскольку в обоих случаях речь о натуральных числах, к которым напрямую сводятся оба твои примера.
>если есть концепт A и другой концепт В, то первый можно свести ко второму через конечное число промежуточных концептов A1,...,An таких, что концепт А представим в форме концепта А1, а концепт An представим в виде концепта В.
Давай конструктивное доказательство.
Типизированная лямбда же. К ней легко свести даже естественный язык,как пример - семантика Монтегю, есть еще целая монография Ранте, где естественный язык анализируется с позиции MLTT и наоборот. А на естественном языке можно описать хоть твою мамку. Опять же, по Маннури, есть 5 уровней языка, от естественного разговорного до полностью формального, н-р матлогика, и разница между этими уровнями относительная, а не абсолютная. Так что доказать можно и конструктивно, через типизированную лямбду, т.к. любой концепт так или иначе можно представить лямбда-термом.
>любой концепт так или иначе можно представить лямбда-термом.
Сомневаюсь, что это можно конструктивно доказать.
Можно, причем элементарно - через обобщение номинальной дефиниции и редукций (дельта, бета, иота, дзета) до кое-чего интересного. Когда-нибудь допилю свой мега-гитлер прувер, будет конструктивное доказательство.
>до кое-чего интересного
Можно подробнее?
А планируешь прувер сделать онлайновым? Сейчас типа все современные пруверы имеют онлайн морду.
Подробнее долго. Когда-нибудь руки дойдут, запилю нормальный пейпер.
>планируешь прувер сделать онлайновым?
Полноценная реализация изначально планируется онлайновой, т.к. все нужное проще всего реализовать средствами гугловской облачной платформы https://cloud.google.com/ и не привязанной ни к какой конкретной операционке. Кто бы еще все это сделал, т.к. я в гуглооблако не могу. Локально почти все нужное (кроме OCR для математической нотации (LaTeX и AMS-TeX) реализуемо в R, это уже посильно для меня, было бы еще свободного времени побольше а быдлопроблем поменьше.
Что такое пейпер, как на английском пишется?
Был тут рукастый анон, который сайт создавал, может он поможет. Как тебе его сайт был?
Отличное видео. У него как я понимаю вообще мало записанных лекций?
Ты же понимаешь, что в тебе борются два волка?
Один - волк-программист, другой волк-математик.
Хорен что ли?))
Надо ли перестать использовать классическую логику?
Не нужно вообще начинать даже. Это как вирус.
Хорошо, а тогда как с помощью киинтуиционисткой логики доказать, например, неразрешимость проблемы останвки?
там же явным образом используется исключение третьего.
Я и говорю как вирус, уже везде видишь невозможность доказать что-либо без его использования.
Хорошо, порекомендуй тогда, пожалуйста, монографии по конструктивной математике.
Ну то есть уважаемые труды, где много теорем.
Посоны, лисп учить или нет?
Он милый
А скема?
Да одно и тоже
Посоны, микроядра кто нибудь доказывал? Че там жопа или реал вкатится и бабосы рубить под пивасик?
Посоны, я тут короче кнута решаю. Всё правильно делаю?
Посоны, емакс учить или таблеток лучше?
Воеводский умер, я в шоке :((
Пиздец, ужасная новость. Вроде как-то фиолетово, когда слышишь подобные известия, ну не друг и не родственник умер, но тут не по себе.
Очередная победа теоретико-множественного подхода.
Проиграл на весь театр.
Синъити, верни мне мой театр! Заебал.
Ходж
Не верну, я обиделся на всех.
>Очередная победа теоретико-множественного подхода.
Единственная, я бы сказал. Других не подвозили, начиная с того самого 11-го симпозиума в Палермо в 1897 году, когда Бурали-Форти торжественно помочился Кантору за шиворот, уничтожив его как математика.
У Кантора хотябы есть что критиковать.
У любого найдется, что критиковать. Одно дело критика, другое - доказательство противоречивости и т.о. бесполезности всей теории.
Брауэр, к слову, не только задолго до Геделя и обсера Гильберта с его изначальной программой, показал несостоятельность формализма как оснований математики. И даже не только вывел суть математики как ментальных построений, что подтвердилось уже в нулевых годах 21 века (модели ATOM, MT, о чем уже писалось). Его взгляды на природу и физику как науку очень похожи на то, что сейчас известно как квантово-волновой дуализм и эффект наблюдателя (во II части его диссертации и немного в самом начале III части есть некоторое количество цитат на эту тему), он же был профессором кафедры математики и физики. К сожалению, я в квантмехе практически нихуя не понимаю давно забытый материал из учебников не считается, чтобы сделать более грамотное сравнение. Даже его определение дискретного и непрерывного в интуиции времени как основе математики можно было бы рассмотреть с точки зрения квантово-волнового дуализма.
Всецело поддерживаю это начинание. Чем больше вы будете пиздеть о квантовой механике, тем большему количеству людей будет видно, что вы сумасшедшие.
Кто "мы"-то? Я один тута. Разве то, что из некоей теории можно вывести нечто такое, до чего остальная наука дошла десятилетия спустя, не говорит в пользу правильности этой теории7
Да-да, конечно. Если Кузанский о множественности миров кукарекал, то это он на самом деле теорию струн открыл.
>множественности миров
Это одна из возможных интерпретаций же. А корпускулярно-волновой дуализм - медицинский факт.
Да-да. И вот так, легким движением ушей, Кузанский записывается в отцы-основатели квантовой механики.
Можно ли считать любовь к теории мн*жеств психическим расстройством?
Ну зачем же сразу расстройство. У нас свобода вероисповедания. Кто-то в Аллаха верует, кто-то в платоновский мир идей. Другой вопрос, что ни то ни другое - это не математика.
Чем же ты объясняешь очевидную популярность теории множеств? Видимо ты просто не умеешь ей правильно пользоваться, поэтому в отрицание скатываешься.
Тут даже не про веру в Аллаха, хотя и она конечно даёт о себе знать.
Скорее всего это объясняется пока ещё неизвестным вирусом. Другого объяснения не вижу.
>Чем же ты объясняешь очевидную популярность ислама? Видимо ты просто не умеешь правильно веровать, поэтому в куфр скатываешься.
Я тебя услышал.
Ок, ты мечтаешь о вычслимости.
Когда доказываешь кому-то теорему можно сделать двумя способами: либо доказать уже известными всем методами, простыми, быстрыми.
Либо выдумывать свою конструктивную науку и в ней болтаться без конца.
Я тебя спрашиваю: где результат?
Какую реальную проблему помогла решить вычислимость теорем?
Сможешь хотя бы 3 примера реальных задач привести.
За которые тебе заплатят деньги. Классическая логика и обычные основания математики - дают рабочий инструмент.
Нахрена из кувалды делать микроскоп?
Ваша анальная фиксация на исламе поражает, вас в детстве насиловал отчим дагестанец?
ℵ_∞
Действительно, согласен. Вот ещё что думаю:
У них контринтуитивное отрицание закона исключенного третьего.
Утверждение: Конструктивист петух или конструктивист не петух. Но зная, что конструктивист петух, мы не можем определить истинность этого утверждения!
почитай по теме чуть больше, ты пока не разобрался
Пришёл ты в /матх/
о вычислимости мечтаешь ты
сосни-ка хуйца
Навеяло
А пачиму в канструктивных оснонваниях отрцицается исключённае третье????????
Хороший вопрос! Хотелось бы чёткое обоснование, без всяких отсылок к изоморфизмам гарри-ховарда, тезиса чёрча и прочих сложныхштук. По-нашему, кратко, по-простому, но по делу.
сагласен! я вот ещё кстате вычислил что канструктивные основания пративоречивы!!
ведь в них отрицается исключённае третье и доказывается двойное отрицание исключённого третьего!!
другими словами просто фууу....
так... я даказал в гаматапической теории типав что исключённое третье неверно. из этого следует пративоречивость канструктивной
математики.
теорема: канструктивная математика противоречива.
доказательство:
исключённая третье говорит нам, что верно - для всех типав X и для всех точак x и y в X наличие пути из x в y разрешимо.
то есть у нас есть терм назавём его الله.
الله : Π (X : U) . Π (x, y : X) . x = y ∐ x ≠ y
الله X x y := "тут применяем наше исключённае третье"
читаем как "الله имеет тип "для всех термав принадлежащих универсуму U (типав) и для любых термав x и y типа Х наличие пути из х в у разрешимо""
из этого следует что все типы являются 0-типами!
теперь подставляем x вместо у и палучаем что все гаматопические группы (любого типа!!!) тривиальны!
куда можно это опубликовать?
математики.
теорема: канструктивная математика противоречива.
доказательство:
исключённая третье говорит нам, что верно - для всех типав X и для всех точак x и y в X наличие пути из x в y разрешимо.
то есть у нас есть терм назавём его الله.
الله : Π (X : U) . Π (x, y : X) . x = y ∐ x ≠ y
الله X x y := "тут применяем наше исключённае третье"
читаем как "الله имеет тип "для всех термав принадлежащих универсуму U (типав) и для любых термав x и y типа Х наличие пути из х в у разрешимо""
из этого следует что все типы являются 0-типами!
теперь подставляем x вместо у и палучаем что все гаматопические группы (любого типа!!!) тривиальны!
куда можно это опубликовать?
извените...
там в конце доказательство должен был быть знак как на скриншоте.
там в конце доказательство должен был быть знак как на скриншоте.
улыбнул, но лучше бы ты по теме что-нибудь писал про вычислимость. Очень кайфовая тема.
тут дажы вычислимасть не нужна чтобы доказать пративаречивость вычислимасти.
Предыдущий - https://2ch.hk/math/res/17772.html
Архив тредов