Помимо трех основных направлений в основаниях - формализм, логицизм и интуиционизм, иногда возникали идеи построить математику на кардинально отличных от общепринятых принципах. Одно из таких направлений - Сигнифика, Significs. Попытка основать математику на основе естественного языка (т.к. язык и математика - это деятельность человека) принадлежит учителю Брауэра, голландскому математику и философу Герриту Маннури. Согласно его теории уровней языка (таких уровней 5), чисто формальный язык математики (5ый уровень) отличается от языка общения детей (1ый уровень) только степенью связи между словами и их сочетаниями (языковыми конструкциями). Идеи Маннури более чем на столетие опередили свое время, т.к. при его жизни не было методов автоматизированной работы с текстом (NLP, Natural Language Processing). В наше время такие методы развиты достаточно, чтобы поставить вопрос о построении вычислительной сигнифики (Computational Significs) для нужд математики, в т.ч. автоматизированного доказательства теорем и т.о. реализации на этих основах прувера, отличающегося принципом функционирования от всех остальных чуть менее чем полностью.
Предыдущий - https://2ch.hk/math/res/17772.html (
М)
Архив тредов
Предыдущий - https://2ch.hk/math/res/17772.html (
М) Архив тредов
>>1361 (OP)
Кризис оснований закончился, когда теория множеств была аксиоматизирована.
Кризис оснований закончился, когда теория множеств была аксиоматизирована.
167 Кб, 782x543>>1363
И сразу все бесконечности и исключенное третье сами посчитались. А Гильберту делать было нехуй, что он решил обосновывать арифметику финитарными методами, потому что чисто аксиоматически это оказалось сделать невозможно. Финитарными, Карл! До такого даже Брауэр не докатился, хотя и описал то, что Гильберт назвал "метаматематикой" задолго до Гильберта т.к. признавал потенциальную осуществимость, как абстракцию от действия над ментальными построениями "and so forth". Суть-то в чем? Невычислимые основания нельзя использовать на практике, н-р для доказательства непротиворечивости арифметики, на чем Гильберт и прогорел, скатившись в итоге к финитизму. Подобные же причины сделали необходимым создание вычислимых оснований - MLTT и HoTT. Если бы все можно было доказать в ZFC, никто бы не ебался с конструктивными основаниями.
И сразу все бесконечности и исключенное третье сами посчитались. А Гильберту делать было нехуй, что он решил обосновывать арифметику финитарными методами, потому что чисто аксиоматически это оказалось сделать невозможно. Финитарными, Карл! До такого даже Брауэр не докатился, хотя и описал то, что Гильберт назвал "метаматематикой" задолго до Гильберта т.к. признавал потенциальную осуществимость, как абстракцию от действия над ментальными построениями "and so forth". Суть-то в чем? Невычислимые основания нельзя использовать на практике, н-р для доказательства непротиворечивости арифметики, на чем Гильберт и прогорел, скатившись в итоге к финитизму. Подобные же причины сделали необходимым создание вычислимых оснований - MLTT и HoTT. Если бы все можно было доказать в ZFC, никто бы не ебался с конструктивными основаниями.
>>1365
Ну я тебе пример с непротиворечивостью арифметики привел. Нахуя нужны основания, пользуясь которыми нельзя обосновать что 1+1 будет 2? Это не то что не основания, это не математика даже.
Ну я тебе пример с непротиворечивостью арифметики привел. Нахуя нужны основания, пользуясь которыми нельзя обосновать что 1+1 будет 2? Это не то что не основания, это не математика даже.
>>1366
Арифметика Пеано непротиворечива, и это доказано. В любой формальной арифметике со сложением можно доказать, что 1+1=2. В чем проблема-то?
Арифметика Пеано непротиворечива, и это доказано. В любой формальной арифметике со сложением можно доказать, что 1+1=2. В чем проблема-то?
>>1368
Теоремой Гудстейна? Ты формально докажи непротиворечивость арифметики, а не правилами построения типа аксиом Пеано.
>Арифметика Пеано непротиворечива, и это доказано.
Теоремой Гудстейна? Ты формально докажи непротиворечивость арифметики, а не правилами построения типа аксиом Пеано.
>>1369
Это доказал трансфинитной индукцией Генцен, чем окончательно выполнил программу-минимум Гильберта. Как бе известнейший факт.
Это доказал трансфинитной индукцией Генцен, чем окончательно выполнил программу-минимум Гильберта. Как бе известнейший факт.
>>1373
Го пвп? Сейчас бы в 2017 намейлру опровергать интуиционизм. Ну что вы тут за аутисты? Вот ты ж даже не читаешь, что тебе пишут, не говоря о том чтобы попытаться понять. Помимо невычислимых нематематических верований вся используемая математика конструктивна и даже выразима в лямбда Р исчислении, что показал де Браун. Я это не писал уже сто раз? Писал. Так что ты опровергать собрался?
Го пвп? Сейчас бы в 2017 намейлру опровергать интуиционизм. Ну что вы тут за аутисты? Вот ты ж даже не читаешь, что тебе пишут, не говоря о том чтобы попытаться понять. Помимо невычислимых нематематических верований вся используемая математика конструктивна и даже выразима в лямбда Р исчислении, что показал де Браун. Я это не писал уже сто раз? Писал. Так что ты опровергать собрался?
>>1391
Ну, вначале ведь нужно уточнить позиции. Первым делом я бы хотел выяснить объём и границы того, что ты называешь "всей используемой математикой". От общих вопросов - не отсекается ли тобой, скажем, вся теория множеств и вся современная алгебра, и до таких частностей, как возможно ли определить топологию Зоргенфрея на числовой прямой. Согласись, вполне справедливая хотелка.
Ну, вначале ведь нужно уточнить позиции. Первым делом я бы хотел выяснить объём и границы того, что ты называешь "всей используемой математикой". От общих вопросов - не отсекается ли тобой, скажем, вся теория множеств и вся современная алгебра, и до таких частностей, как возможно ли определить топологию Зоргенфрея на числовой прямой. Согласись, вполне справедливая хотелка.
64 Кб, 715x1013>>1398
Я их уже 4ый тред уточняю + до этого тредов 5 как минимум в сци. Математика это все, что вычислимо, все что невычислимо это не математика. Именно поэтому всю математику можно изложить уже в лямбда Р исчислении (Automath де Брауна), да даже на машине Тьюринга, хотя это дальше от практики. Т.к конструктивный объект это обобщение натурального числа, любую математическую структуру можно свести к натуральному числу, геделевской нумерацией например, а вся математика точно так же сводится к арифметике. А все, что не сводится - это не математика, с этим только в церковь покемонов ловить. Не писал я этого сто раз? Писал ведь. И если после всего этого моя позиция остается гепонятной кому'то, я даже не знаю.
> Ну, вначале ведь нужно уточнить позиции.
Я их уже 4ый тред уточняю + до этого тредов 5 как минимум в сци. Математика это все, что вычислимо, все что невычислимо это не математика. Именно поэтому всю математику можно изложить уже в лямбда Р исчислении (Automath де Брауна), да даже на машине Тьюринга, хотя это дальше от практики. Т.к конструктивный объект это обобщение натурального числа, любую математическую структуру можно свести к натуральному числу, геделевской нумерацией например, а вся математика точно так же сводится к арифметике. А все, что не сводится - это не математика, с этим только в церковь покемонов ловить. Не писал я этого сто раз? Писал ведь. И если после всего этого моя позиция остается гепонятной кому'то, я даже не знаю.
>>1400
Это слишком общие слова. Хотелось бы (и, похоже, не мне одному) узнать, что же конкретно ты относишь к области покемонов. Понятно, что ты запрещаешь изучать большие кардиналы и нестандартный анализ, но как далеко простираются запреты и не попадает ли вдруг под них вообще вся общая топология? Вот скажи, как в твоем учении выглядит введение разнообразных топологий на множестве вещественных чисел? Как, к примеру, топологию Зоргенфрея следует определять? Это конкретные вопросы, и я рассчитываю на конкретные ответы.
Это слишком общие слова. Хотелось бы (и, похоже, не мне одному) узнать, что же конкретно ты относишь к области покемонов. Понятно, что ты запрещаешь изучать большие кардиналы и нестандартный анализ, но как далеко простираются запреты и не попадает ли вдруг под них вообще вся общая топология? Вот скажи, как в твоем учении выглядит введение разнообразных топологий на множестве вещественных чисел? Как, к примеру, топологию Зоргенфрея следует определять? Это конкретные вопросы, и я рассчитываю на конкретные ответы.
Это не общие слова, а вполне конкретная конкретика. Математика = вычислимость, для определенности, пусть будет вычислимость на машине Тьюринга, хотя сойдет и любое другое уточнение понятия алгоритма. Невычислимое невычислимо, поэтому его нельзя вычислить, можно только верить. Потенциальная осуществимость осуществима потенциально, отличие от актуальной бесконечности - наличие правил построения.
>>1401
Дался тебе этот Зоргенфрей. Еще Брауэр показал, что континуум невычислим и уж точно не сводится к множеству вещественных чисел.
>>1401
> Как, к примеру, топологию Зоргенфрея следует определять?
Дался тебе этот Зоргенфрей. Еще Брауэр показал, что континуум невычислим и уж точно не сводится к множеству вещественных чисел.
>>1410
Верно ли я понял, что ты запрещаешь вводить различные топологии на множестве вещественных чисел?
Верно ли я понял, что ты запрещаешь вводить различные топологии на множестве вещественных чисел?
>>1411
Я думаю тут еще хуже, смотри он пишет
И при этом следом
Отсюда по его манялогике: вещественные числа эта манявера и четко твердо НИНУЖНО. Я тут подумал, а этого сумасшедшего легко косплеить.
Я думаю тут еще хуже, смотри он пишет
>Математика = вычислимость
И при этом следом
>континуум невычислим
Отсюда по его манялогике: вещественные числа эта манявера и четко твердо НИНУЖНО. Я тут подумал, а этого сумасшедшего легко косплеить.
>>1411
Ты ведь и сам понимаешь, даже без всякого конструктивизма, что это в любом случае будет аппроксимация с конкретным количеством знаков после запятой. Именно их ты и будешь вычислять. Нет никакого запрета, есть трезвый взгляд на тему. Брауэр, к слову, топологией занимался еще до интуиционизма.
> Верно ли я понял, что ты запрещаешь вводить различные топологии на множестве вещественных чисел?
Ты ведь и сам понимаешь, даже без всякого конструктивизма, что это в любом случае будет аппроксимация с конкретным количеством знаков после запятой. Именно их ты и будешь вычислять. Нет никакого запрета, есть трезвый взгляд на тему. Брауэр, к слову, топологией занимался еще до интуиционизма.
>>1414
О какой аппроксимации речь? В какой процедуре? Топология стрелки - это классический пример топологического пространства с неинтуитивными свойствами, и работает этот пример именно как цельное пространство.
О какой аппроксимации речь? В какой процедуре? Топология стрелки - это классический пример топологического пространства с неинтуитивными свойствами, и работает этот пример именно как цельное пространство.
>>1417
Все эти ваши "цельные пространства" на самом деле дискретизация. Самый простой пример - интегральчики. Веровается, что с помощью предельного перехода размера интервалов dx к бесконечно малому получается нечто отличное от просто интервалов, хотя ни для кого не секрет, что любые численные методы интегрирования - это чистая дискретка. Т.о. имеем практически возможную аппроксимацию конечным числом интервалов dx, а предельный переход существует только на бамаге, ничего построимого и вычислимого за ним не стоит. Т.е. на самом деле вычисления не идут за пределы реально вычислимого. И опять же, я приводил конкретный пример - теория статистического обучения. Таких примеров можно привести еще сколько угодно, те же функции принадлежности в нечетких множествах. Т.е. на самом деле работает все так, как показал еще Брауэр - континуум невычислим, реально можно работать только с его дискретизацией.
Все эти ваши "цельные пространства" на самом деле дискретизация. Самый простой пример - интегральчики. Веровается, что с помощью предельного перехода размера интервалов dx к бесконечно малому получается нечто отличное от просто интервалов, хотя ни для кого не секрет, что любые численные методы интегрирования - это чистая дискретка. Т.о. имеем практически возможную аппроксимацию конечным числом интервалов dx, а предельный переход существует только на бамаге, ничего построимого и вычислимого за ним не стоит. Т.е. на самом деле вычисления не идут за пределы реально вычислимого. И опять же, я приводил конкретный пример - теория статистического обучения. Таких примеров можно привести еще сколько угодно, те же функции принадлежности в нечетких множествах. Т.е. на самом деле работает все так, как показал еще Брауэр - континуум невычислим, реально можно работать только с его дискретизацией.
>>1430
Какая разница, что там в реальности считают инженеры?
А число Грэма?
>Веровается, что с помощью предельного перехода размера интервалов dx к бесконечно малому получается нечто отличное от просто интервалов, хотя ни для кого не секрет, что любые численные методы интегрирования - это чистая дискретка.
Какая разница, что там в реальности считают инженеры?
>Т.е. на самом деле вычисления не идут за пределы реально вычислимого.
А число Грэма?
>>1431
Типа ты можешь посчитать больше, чем инженер, причем в какой-то своей реальности? Вычислимость это вычислимость, машину Тьюринга, Поста и другие подобные вещи ты не перевычисляешь, это факт.
Обсуждали уже. Тебе в слове "вычислимое" что непонятно? Опять сказка про белого бычка из-за непонимания разницы между фактически построимым и абстракции потенциальной осуществимости? Извини, не интересно.
>Какая разница, что там в реальности считают инженеры?
Типа ты можешь посчитать больше, чем инженер, причем в какой-то своей реальности? Вычислимость это вычислимость, машину Тьюринга, Поста и другие подобные вещи ты не перевычисляешь, это факт.
>А число Грэма?
Обсуждали уже. Тебе в слове "вычислимое" что непонятно? Опять сказка про белого бычка из-за непонимания разницы между фактически построимым и абстракции потенциальной осуществимости? Извини, не интересно.
>>1432
Тогда почему ты говоришь про какие-то там дискретные величины в интегралах? Там бесконечность, континуум! УХ!
>разницы между фактически построимым и абстракции потенциальной осуществимости
Тогда почему ты говоришь про какие-то там дискретные величины в интегралах? Там бесконечность, континуум! УХ!
>>1434
Я понял, что тебе непонятно слово "потенциально", еще в прошлом году. Поэтому, давай так - ты разбираешься с этим понятием, потом приходишь сюда спрашивать. До этого не вижу ни одной причины повторять миллион раз одно и то же, причем тому, кто принципиально не способен воспринимать объяснения на эту тему.
Я понял, что тебе непонятно слово "потенциально", еще в прошлом году. Поэтому, давай так - ты разбираешься с этим понятием, потом приходишь сюда спрашивать. До этого не вижу ни одной причины повторять миллион раз одно и то же, причем тому, кто принципиально не способен воспринимать объяснения на эту тему.
>>1435
Если ты говоришь про потенциальность то зачем тогда упоминаешь интегральчики?
У нас есть аналитический метод вычисления, без дискретки с континуумом!
Если ты говоришь про потенциальность то зачем тогда упоминаешь интегральчики?
>Самый простой пример - интегральчики. Веровается, что с помощью предельного перехода размера интервалов dx к бесконечно малому получается нечто отличное от просто интервалов, хотя ни для кого не секрет, что любые численные методы интегрирования - это чистая дискретка.
У нас есть аналитический метод вычисления, без дискретки с континуумом!
34 Кб, 600x823>>1437
Да, конструктивное доказательство чему - изоморфизм Карри-Говарда. Хотя так-то это всем умным людям из тех, кого Брауэр не разбудил это стало ясно уже после работ Тьюринга с Постом. Самое смешное, что с тех пор кроме кривляний разной степени толстоты возражений пока не поступало.
>математика - это один из разделов Computer Science?
Да, конструктивное доказательство чему - изоморфизм Карри-Говарда. Хотя так-то это всем умным людям из тех, кого Брауэр не разбудил это стало ясно уже после работ Тьюринга с Постом. Самое смешное, что с тех пор кроме кривляний разной степени толстоты возражений пока не поступало.
>>1439
Но ведь ты веришь, в то, что например, доказательство на компьютере коком верно, поскольку человек не может его проверить. Ту же проблему четырёх красок взять!
Но ведь ты веришь, в то, что например, доказательство на компьютере коком верно, поскольку человек не может его проверить. Ту же проблему четырёх красок взять!
А что лемму вложенных отрезков думаешь? Можно же пересекать бесконечное число отрезков.
>>1440
Я еще раз прошу не нести хуйни, т.к. в теме ты не понимаешь совсем, что видно за километр. Автоматическое доказательство коком ничем не отличается от автоматического доказательства человеком. Машину Тьюринга можно сделать из бумажной ленты и все нужное делать руками, это ничем не будет отличаться от неручной машины Тьюринга. Другой вопрос, что это займет гораздо больше времени. Я еще раз скажу - вычислимость это вычислимость, она одна, других не бывает.
Я еще раз прошу не нести хуйни, т.к. в теме ты не понимаешь совсем, что видно за километр. Автоматическое доказательство коком ничем не отличается от автоматического доказательства человеком. Машину Тьюринга можно сделать из бумажной ленты и все нужное делать руками, это ничем не будет отличаться от неручной машины Тьюринга. Другой вопрос, что это займет гораздо больше времени. Я еще раз скажу - вычислимость это вычислимость, она одна, других не бывает.
>>1442
Во первых, тогда почему твой кок не может оперировать исключающим третьим, аксиомой выбора, и актульными бесконечностями, а человек может? Почему я например могу работать с вещественными числами(бесконечными последовательностями десятичных дробей), а твой кок нет?
Во вторых, доказательство коком сомниетльные, поскольку человек их не может увидеть. А раз мы не можем увидеть доказательство, то веруем в него. Как и веруем в доказательство проблемы черытёх красок, от которого плювался Гротендик.
>Автоматическое доказательство коком ничем не отличается от автоматического доказательства человеком.
Во первых, тогда почему твой кок не может оперировать исключающим третьим, аксиомой выбора, и актульными бесконечностями, а человек может? Почему я например могу работать с вещественными числами(бесконечными последовательностями десятичных дробей), а твой кок нет?
Во вторых, доказательство коком сомниетльные, поскольку человек их не может увидеть. А раз мы не можем увидеть доказательство, то веруем в него. Как и веруем в доказательство проблемы черытёх красок, от которого плювался Гротендик.
65 Кб, 310x350Я вижу, что во-первых, вопросы по конструктивной математике тут таки возникают, во-вторых, с матчастью тут совсем все плохо, настолько плохо, что хуже уже не бывает. Поэтому, вниманию самых маленьких предлагается такая книшка:
http://gen.lib.rus.ec/book/index.php?md5=2BBE15747B57CDB3BAF9F25BDFEC280B да, в совке издавали годные материалы по конструктивной математики даже для дошкольников и младших школьников. Все поясняется буквально на пальцах.
>>1443
Во-первых, ты не можешь, ты вероваешь, что можешь. Во-вторых, в коке можно задать и исколюченное третье и даже Аллаха. Но, поскольку это неконструктивные сущности, за которыми не стоит никаких вычислимых в канонические элементы конструкций, это бесполезно.
Давай, покажи. Тащи сюда полностью свои бесконечности.
В третий раз тебе говорят, хватит писать мне хуйню, реально надоело. Если ты кок в глаза видел, то видел и доказательства, которые он выдает. А если бы еще слышал про лямбда-куб, исчисление конструкций итд, то даже и понял бы их.
http://gen.lib.rus.ec/book/index.php?md5=2BBE15747B57CDB3BAF9F25BDFEC280B да, в совке издавали годные материалы по конструктивной математики даже для дошкольников и младших школьников. Все поясняется буквально на пальцах.
>>1443
>почему твой кок не может оперировать исключающим третьим, аксиомой выбора, и актульными бесконечностями, а человек может?
Во-первых, ты не можешь, ты вероваешь, что можешь. Во-вторых, в коке можно задать и исколюченное третье и даже Аллаха. Но, поскольку это неконструктивные сущности, за которыми не стоит никаких вычислимых в канонические элементы конструкций, это бесполезно.
>Почему я например могу работать с вещественными числами(бесконечными последовательностями десятичных дробей), а твой кок нет?
Давай, покажи. Тащи сюда полностью свои бесконечности.
>доказательство коком сомниетльные, поскольку человек их не может увидеть.
В третий раз тебе говорят, хватит писать мне хуйню, реально надоело. Если ты кок в глаза видел, то видел и доказательства, которые он выдает. А если бы еще слышал про лямбда-куб, исчисление конструкций итд, то даже и понял бы их.
>>1444
Зачем мне читать твою конструктивную литературу? Почему вместо нормального объяснения ты всё время крепишь скриншоты и отсылаешь к книжкам? Хочешь меня так в свою секту завербовать?
Один раз нормально распиши, а потом копипасть на однотипные ответы, довен.
Зачем мне читать твою конструктивную литературу? Почему вместо нормального объяснения ты всё время крепишь скриншоты и отсылаешь к книжкам? Хочешь меня так в свою секту завербовать?
Один раз нормально распиши, а потом копипасть на однотипные ответы, довен.
>>1444
Смотри, у нас есть множество действительных числе R.
Я беру и выбираю из него такое число x, что оно будет меньше 3 и больше 2.
>Во-первых, ты не можешь, ты вероваешь, что можешь.
Смотри, у нас есть множество действительных числе R.
Я беру и выбираю из него такое число x, что оно будет меньше 3 и больше 2.
>>1447
И что дальше? Получаем дискретизацию континуума вещественными числами. Континуум не сводится к множеству R, т.к. между двумя вещественными числами всегда можно вставить еще. Даже если применим абстракцию потенциальной осуществимости и предположим, что такое деление можно вести сколько угодно далеко, все равно итогом будут вещественные числа, но не континуум.
>>1446
Я не виноват, что вместо того, чтобы вникать в объяснения, ты закатываешь глаза и начинаешь кукарекать.
Я каждый раз нормально пишу. Нужно пытаться понять, а не кукарекать.
Деревянные по пояс тут точно не нужны. Правильно Максимка говорил, что в рашке никто не может в зависимые типы.
>Смотри, у нас есть множество действительных числе R. Я беру и выбираю из него такое число x, что оно будет меньше 3 и больше 2.
И что дальше? Получаем дискретизацию континуума вещественными числами. Континуум не сводится к множеству R, т.к. между двумя вещественными числами всегда можно вставить еще. Даже если применим абстракцию потенциальной осуществимости и предположим, что такое деление можно вести сколько угодно далеко, все равно итогом будут вещественные числа, но не континуум.
>>1446
>Почему вместо нормального объяснения
Я не виноват, что вместо того, чтобы вникать в объяснения, ты закатываешь глаза и начинаешь кукарекать.
>Один раз нормально распиши
Я каждый раз нормально пишу. Нужно пытаться понять, а не кукарекать.
>Хочешь меня так в свою секту завербовать?
Деревянные по пояс тут точно не нужны. Правильно Максимка говорил, что в рашке никто не может в зависимые типы.
>>1451
Посылание читать Брауэера это не объеснения.
Ты даже сейчас не можешь нормально писать и скатываешься до оскорблений. Давай ссылку на пост с нормальными объяснениями, раз писал.
>Я не виноват, что вместо того, чтобы вникать в объяснения, ты закатываешь глаза и начинаешь кукарекать.
Посылание читать Брауэера это не объеснения.
>Я каждый раз нормально пишу.
Ты даже сейчас не можешь нормально писать и скатываешься до оскорблений. Давай ссылку на пост с нормальными объяснениями, раз писал.
>Деревянные по пояс тут точно не нужны.
>— Ты издеваешься. Ты не можешь писать это всерьёз.
>— Я не виноват, что ты такой тупой.
>>1462
Да ну, какой тебе Брауэр, ты вышеупомянутую книжку для дошкольников не осилишь. Хотя если бы осилил, много откровенно тупых вопросов бы отпало, там реально хорошо объясняют, лучше чем я. При всем неуважении к совку, научпоп там был мирового уровня. Но тебе не нужны объяснения (да, я сто раз объяснял, можешь опять вспомнить свою пасту), ты изначально исходишь из предположения, что я неправ, и уже с этой позиции рассматриваешь все остальное, безотносительно к его содержанию. Мне-то похуй, одно непонятно, зачем тогда тебе вообще сюда писать и пытаться что-то кому-то доказать.
>>1456
Вот как пример, что можно доказать тому, для которого абстракция и вера это одно и то же? Тут вообще говорить не о чем.
>Посылание читать Брауэера это не объеснения.
Да ну, какой тебе Брауэр, ты вышеупомянутую книжку для дошкольников не осилишь. Хотя если бы осилил, много откровенно тупых вопросов бы отпало, там реально хорошо объясняют, лучше чем я. При всем неуважении к совку, научпоп там был мирового уровня. Но тебе не нужны объяснения (да, я сто раз объяснял, можешь опять вспомнить свою пасту), ты изначально исходишь из предположения, что я неправ, и уже с этой позиции рассматриваешь все остальное, безотносительно к его содержанию. Мне-то похуй, одно непонятно, зачем тогда тебе вообще сюда писать и пытаться что-то кому-то доказать.
>>1456
Вот как пример, что можно доказать тому, для которого абстракция и вера это одно и то же? Тут вообще говорить не о чем.
>>1467
Я не собираюсь читать какие-то книжки для того, чтобы доказать свою правоту анону с двачей. Это лишнее.
А я должен был считать изначально, что ты прав? У тебя не получилось доказать свою провату, и каждый раз ты только и делаешь, что уходишь от ответа:
Ну ты типа тупой, не поймёшь)))
Иди Брауэра читать)))
Да я уже сто раз объяснял)))
Это вера а не математика)))
Хватит уходить от вопросов, нам нужны ответы!
Тогда дай ссылки на посты с объяснениями. А то только можешь отсылать читать свои книжки, да скиншоты лепить. Ты сам видно не до конца понимаешь всю эту мутотень с основаниями и поэтому нормально объяснить не можешь.
Континуум или трансфитная индукция тоже абстрактная вещь, но ты называешь его верой.
>Да ну, какой тебе Брауэр, ты вышеупомянутую книжку для дошкольников не осилишь
Я не собираюсь читать какие-то книжки для того, чтобы доказать свою правоту анону с двачей. Это лишнее.
>ты изначально исходишь из предположения, что я неправ,
А я должен был считать изначально, что ты прав? У тебя не получилось доказать свою провату, и каждый раз ты только и делаешь, что уходишь от ответа:
Ну ты типа тупой, не поймёшь)))
Иди Брауэра читать)))
Да я уже сто раз объяснял)))
Это вера а не математика)))
Хватит уходить от вопросов, нам нужны ответы!
>да, я сто раз объяснял
Тогда дай ссылки на посты с объяснениями. А то только можешь отсылать читать свои книжки, да скиншоты лепить. Ты сам видно не до конца понимаешь всю эту мутотень с основаниями и поэтому нормально объяснить не можешь.
>Вот как пример, что можно доказать тому, для которого абстракция и вера это одно и то же?
Континуум или трансфитная индукция тоже абстрактная вещь, но ты называешь его верой.
1,3 Мб, webm,552x512
>>1468
А что ты мне можешь доказать, если не понимаешь разницу между верой и абстракцией и между трансфинитной индукцией и континуумом? Смешно даже читать такое. А книжки нужны не для того, чтобы что-то кому-то доказать и самоутвердиться, а чтобы в вопросе разобраться. Для этого читать книжки - норма. К слову, это не ты тот деятель, который еще зимой обещал меня разгромить, доказав мне неправильность MLTT?
>Я не собираюсь читать какие-то книжки для того, чтобы доказать свою правоту анону с двачей.
А что ты мне можешь доказать, если не понимаешь разницу между верой и абстракцией и между трансфинитной индукцией и континуумом? Смешно даже читать такое. А книжки нужны не для того, чтобы что-то кому-то доказать и самоутвердиться, а чтобы в вопросе разобраться. Для этого читать книжки - норма. К слову, это не ты тот деятель, который еще зимой обещал меня разгромить, доказав мне неправильность MLTT?
>>1505
Называя Брауэра "замечательным математиком"? Но допустим, в целом это возможно, ведь в совочке брауэровский интуиционизм считали буржуазным идеалистическим учением, в отличие от конструктивизма, который с вычислительной точки зрения то же самое. Опять же, если ты этого не можешь понять, почему это должны были понимать выжившие из ума старперы из КПСС? Они и логицизм Рассела считали тем же самым и даже заявляли, что это причина того, что Рассел призывал разбомбить совок ядерным оружием.
>Который сам почему-то отзывается об интуиционизме неприязненно.
Называя Брауэра "замечательным математиком"? Но допустим, в целом это возможно, ведь в совочке брауэровский интуиционизм считали буржуазным идеалистическим учением, в отличие от конструктивизма, который с вычислительной точки зрения то же самое. Опять же, если ты этого не можешь понять, почему это должны были понимать выжившие из ума старперы из КПСС? Они и логицизм Рассела считали тем же самым и даже заявляли, что это причина того, что Рассел призывал разбомбить совок ядерным оружием.
Есть вещи, которые невозможно вычислить или узнать через машЫну. Есть истины, которым нет объяснения. Исходя из этого, именно в этот момент в сознании людей появляется вера во что-то сверхъестественное (и это не плохо). Об этом еще Гедель писал. Кончайте уже со своим конструктивизмом выебываться. Машина не может дать истинные ответы на все вопросы.
/thread
/thread
184 Кб, 672x511>>1507
Недавняя книжка, появившаяся сильно после кпсс. Первое попавшееся место.
Недавняя книжка, появившаяся сильно после кпсс. Первое попавшееся место.
Зависимые типы я осилил, а вот исчисление конструкций пока нет. Чем примечательны, полезны, красивы исчисления конструкций, если объяснять для чайника?
111 Кб, 819x227>>1509
Хорошая книжка, автору сразу можно помочиться за шиворот и отправить доучиваться. Классическая матлогика не рассматривает смысл (т.е. семантику) выражений вообще, от слова никак. Там только синтаксис, о чем писал и Гильберт и Бурбаки.
>>1534
С Барендрегта начни. Исчисление конструкций - просто наиболее полное лямбда-исчисление по Черчу, т.е. в кубе Барендрегта.
Хорошая книжка, автору сразу можно помочиться за шиворот и отправить доучиваться. Классическая матлогика не рассматривает смысл (т.е. семантику) выражений вообще, от слова никак. Там только синтаксис, о чем писал и Гильберт и Бурбаки.
>>1534
> исчисление конструкций пока нет.
С Барендрегта начни. Исчисление конструкций - просто наиболее полное лямбда-исчисление по Черчу, т.е. в кубе Барендрегта.
83 Кб, 1015x140>>1509
На пикрелейтед месте можно окропить автора уриной еще раз. Он даже конструктивное отрицание не осилил. "Недоказанный" и "неверный" конструктивно абсолютно разные понятия.
На пикрелейтед месте можно окропить автора уриной еще раз. Он даже конструктивное отрицание не осилил. "Недоказанный" и "неверный" конструктивно абсолютно разные понятия.
>>1564
Ну я рад, дальше что? Написанного мной про конструктивное отрицание и семантику матлогики это не отменяет. Что за книжка-то?
Ну я рад, дальше что? Написанного мной про конструктивное отрицание и семантику матлогики это не отменяет. Что за книжка-то?
>>1565
Ссылаешься на него как на большого авторитета и тут же пишешь, что ему нужно ссать за воротник. Ни единого разрыва, нормалёк полный вообще.
"Предисловие к математике".
Ссылаешься на него как на большого авторитета и тут же пишешь, что ему нужно ссать за воротник. Ни единого разрыва, нормалёк полный вообще.
"Предисловие к математике".
29 Кб, 1438x227>>1566
Где книшку-то взял? На либгене нету.
На конкретную книгу, которую читал лично и в которой ошибок не обнаружил.
Где книшку-то взял? На либгене нету.
>Ссылаешься на него как на большого авторитета
На конкретную книгу, которую читал лично и в которой ошибок не обнаружил.
>>1361 (OP)
Вопрос к конструктивистам. В конструктивизме 0.(9)=1?
Вопрос к конструктивистам. В конструктивизме 0.(9)=1?
>>1445
В принципе, конструктивно, как мне кажется, это можно доказать. Если я хорошо понимаю суть конструктивизма(а я узнал о нем из этого треда), то конструктивное доказательство будет выглядеть так:
У нас есть сумма (сложнее сумму возьмем): 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
Просто пренебрегаем последним членом.
В принципе, конструктивно, как мне кажется, это можно доказать. Если я хорошо понимаю суть конструктивизма(а я узнал о нем из этого треда), то конструктивное доказательство будет выглядеть так:
У нас есть сумма (сложнее сумму возьмем): 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
Просто пренебрегаем последним членом.
Чем одно и то же >>1604 >>1597 спрашивать сотый раз, послушайте лучше умного человека.
https://www.youtube.com/watch?v=VDreWuWDUu0&t=1269s
https://www.youtube.com/watch?v=VDreWuWDUu0&t=1269s
А как с мнимой единицей у конструктивистов дела обстоят? Мы же просто верим в её существание, она имеет отличную природу от натуральных чисел.
>>1956
Как я и говорю, основная проблема местных поциентов - категорическое неумение пользовпться головой. В нее не только кушать можно, прикинь. Вот твой вопрос, объясни, к чему он вообще? Ты ни разу не слышал, что даже некоторые калькуляторы могут считать комплексные числа, не говоря о любом нормальном языке программтрования? А если комплексные числа построимы, т.е вычислимы, что можно сказать об их конструктивности, сам догадаешься, или это слишком сложно?
Как я и говорю, основная проблема местных поциентов - категорическое неумение пользовпться головой. В нее не только кушать можно, прикинь. Вот твой вопрос, объясни, к чему он вообще? Ты ни разу не слышал, что даже некоторые калькуляторы могут считать комплексные числа, не говоря о любом нормальном языке программтрования? А если комплексные числа построимы, т.е вычислимы, что можно сказать об их конструктивности, сам догадаешься, или это слишком сложно?
>>1960
Некоторые калькдяторы и бесконечность считают, мнимания единица имеет другию прировуд. Вот число один -это число. Но мнимая единица не имеет алгоритма построения.
Некоторые калькдяторы и бесконечность считают, мнимания единица имеет другию прировуд. Вот число один -это число. Но мнимая единица не имеет алгоритма построения.
>>1960
Комплюктор не ПОНИмает сути производимых операий. Он просто следует алгоритму который в него вбили.
Комплюктор не ПОНИмает сути производимых операий. Он просто следует алгоритму который в него вбили.
>>1993
Прямо как конструктивисты, лол.
>Комплюктор не ПОНИмает сути производимых операий. Он просто следует алгоритму который в него вбили.
Прямо как конструктивисты, лол.
>>1991
Ты читать не умеешь? Вычисление это построение.
> Некоторые калькдяторы и бесконечность считают, мнимания единица имеет другию прировуд. Вот число один -это число. Но мнимая единица не имеет алгоритма построения.
Ты читать не умеешь? Вычисление это построение.
64 Кб, 460x500>>1993
Суть, семантика производимых операций в MLTT это вычисление, т.е получение канонических элементов. Комплюктер понимает вычисление иак же как и не комплюктер, ты никогда и не при каких обстоятельствах не сведешь вычисление к тому, к чему его не сведет компьютер, следовательно твое понимание вычисления равнообъемно с компьютерным. И это сто раз уже писано, просто вы все иута деревянные по пояс.
> Комплюктор не ПОНИмает сути производимых операий.
Суть, семантика производимых операций в MLTT это вычисление, т.е получение канонических элементов. Комплюктер понимает вычисление иак же как и не комплюктер, ты никогда и не при каких обстоятельствах не сведешь вычисление к тому, к чему его не сведет компьютер, следовательно твое понимание вычисления равнообъемно с компьютерным. И это сто раз уже писано, просто вы все иута деревянные по пояс.
>>1996
А как нельзя? Ее даже нарисовать можно, погугли. Суть построений в вычислимости, еще раз говорю. Построение это вычисление, ферштейн, нихт?
> Как можно построить мнимую единицу?
А как нельзя? Ее даже нарисовать можно, погугли. Суть построений в вычислимости, еще раз говорю. Построение это вычисление, ферштейн, нихт?
>>1998
В рамках изоморфизма Карри- Говарда, если тебе эти слова о чем'то говорят.
> А computer science - это чистая математика?
В рамках изоморфизма Карри- Говарда, если тебе эти слова о чем'то говорят.
>>1999
Можно и бесконечность нарисовать, а ты мне найди число, которое в квадрате будет -1.
Можно и бесконечность нарисовать, а ты мне найди число, которое в квадрате будет -1.
>>2001
Бесконечность невычислима, комплексные числа вычислимы. Спать идите, аутисты.
> Можно и бесконечность нарисовать,
Бесконечность невычислима, комплексные числа вычислимы. Спать идите, аутисты.
>>2002
Это математика в том же объеме, что и програмиирование. Если слово 'изоморфизм' тебе о чем'то говорит.
> Нет, я плох в программировании.
Это математика в том же объеме, что и програмиирование. Если слово 'изоморфизм' тебе о чем'то говорит.
>>2005
Верования невычислимы, конструктивные объекты вычислимы. Комплексные числа вычислииы. Так ясно?
> Откуда взялось i? Мы просто верим, что существует число, равно в квадрате -1?
Верования невычислимы, конструктивные объекты вычислимы. Комплексные числа вычислииы. Так ясно?
>>2011
Тебе тролить тупостью не надоело? Конструктивно семантика это вычисление. Эта твоя запись /inf не вычислима ни во что, т.к не является каноническим элементом, не является она и неканоническтм элементом, поскольку не имеет правил вычисления в канонический элемент. Аллаха опять же в этой связи уже обсуждали. И открой для себя гугл, разберись с любым алгоритмом вычисления комплексных чисел, а не пиши одно и тоже сюда сто раз.
> Это семантика. Всё равно, что сказать бесконечность = /inf.
Тебе тролить тупостью не надоело? Конструктивно семантика это вычисление. Эта твоя запись /inf не вычислима ни во что, т.к не является каноническим элементом, не является она и неканоническтм элементом, поскольку не имеет правил вычисления в канонический элемент. Аллаха опять же в этой связи уже обсуждали. И открой для себя гугл, разберись с любым алгоритмом вычисления комплексных чисел, а не пиши одно и тоже сюда сто раз.
>>2012
Повторяю, можно дать тебе алгоритм, с помощью которого ты сможешь работать с ординальной арифметикой.
Повторяю, можно дать тебе алгоритм, с помощью которого ты сможешь работать с ординальной арифметикой.
>>2014
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
x <- 1
y <- 1
z <- complex(real = x, imaginary = y)
z
[1] 1+1i
as.complex(-1)
[1] -1+0i
is.complex(as.complex(-1))
[1] TRUE
z <- complex(real = 2, imaginary = 1)
Re(z)
[1] 2
Im(z)
[1] 1
>>2019
Как и любое вычисление? Давай, покажи вычисление комплексного числа, не сводящееся к вычислению, ебани духовненько, а не как бездушный кудахтер.
Как и любое вычисление? Давай, покажи вычисление комплексного числа, не сводящееся к вычислению, ебани духовненько, а не как бездушный кудахтер.
>>2023
Тоже много раз обсуждалось уже, со скринами и примерами. Все определения тута есть http://www.cse.chalmers.se/research/group/logic/book/book.pdf в первой части.
Тоже много раз обсуждалось уже, со скринами и примерами. Все определения тута есть http://www.cse.chalmers.se/research/group/logic/book/book.pdf в первой части.
>>2024
Хватит кидать ссылки на книги. Я так же могу обсуждать работу мочидзуки, а когда у меня что-то спросить, то дать ссылки на статьи, и сказать сто раз обсуждалось, там же написано. Берёшь и объясняешь всё с нуля.
Хватит кидать ссылки на книги. Я так же могу обсуждать работу мочидзуки, а когда у меня что-то спросить, то дать ссылки на статьи, и сказать сто раз обсуждалось, там же написано. Берёшь и объясняешь всё с нуля.
>>2024
Вместо ответа давать ссылку на талмуд? Всё по методичке, лол. http://lurkmore.to/Правила_демагога
Вместо ответа давать ссылку на талмуд? Всё по методичке, лол. http://lurkmore.to/Правила_демагога
>>2027
Ясно.
>вместо аргумента тащит на мейлру ссылку с лурки
>обвиняет кого-то в использовании методичек
Ясно.
>>2028
Неужели для того, чтобы понять твою аргументацию, нужно читать все эти жуткие сотни страниц и смотреть многие часы лекций? Классическую теорию множеств можно изложить за несколько минут, аксиоматическую вплоть до форсинга - за вечер.
Неужели для того, чтобы понять твою аргументацию, нужно читать все эти жуткие сотни страниц и смотреть многие часы лекций? Классическую теорию множеств можно изложить за несколько минут, аксиоматическую вплоть до форсинга - за вечер.
62 Кб, 274x477>>2029
В MLTT 4 суждения, 4 правила вывода, 4 основных типа и 4 правила построения выражений. Все это можно уместить на половину тетрадного листа. Тетраграмматон рабби Лёфа прост как 4 шекеля. Проблема только в том, что за всем этим стоит не пустой синтаксис ни о чем, как в формализме, а вычислимая конструктивная математика, где даже понятие равенства имеет вычислительное содержание. Это вам не невычислимые ни во что кардиналы и прочих Аллахов рисовать, тут уже не глиняная голова нужна, чтобы въехать.
В MLTT 4 суждения, 4 правила вывода, 4 основных типа и 4 правила построения выражений. Все это можно уместить на половину тетрадного листа. Тетраграмматон рабби Лёфа прост как 4 шекеля. Проблема только в том, что за всем этим стоит не пустой синтаксис ни о чем, как в формализме, а вычислимая конструктивная математика, где даже понятие равенства имеет вычислительное содержание. Это вам не невычислимые ни во что кардиналы и прочих Аллахов рисовать, тут уже не глиняная голова нужна, чтобы въехать.
>>2033
Аксиомы исчисления предикатов тоже немного места занимают. А книг с нормальным изложением меньше чем на сотню страниц так же нет. Поэтому возражение не принимается.
Аксиомы исчисления предикатов тоже немного места занимают. А книг с нормальным изложением меньше чем на сотню страниц так же нет. Поэтому возражение не принимается.
>>2034
Бурбаки. Вся лежащая под математикой логика, включая исчисление предикатов, занимает страницы 31-65. Из них на собственно исчисление предикатов отводится четырнадцать страниц.
Бурбаки. Вся лежащая под математикой логика, включая исчисление предикатов, занимает страницы 31-65. Из них на собственно исчисление предикатов отводится четырнадцать страниц.
456 Кб, 726x1084>>2037
Пикрелейтед.
Не вся, ZFC не может в типы, а за что-нибудь уровня NBG у бурбаков нет ничего.
Вся книжка Мартин-Лёфа 50 с небольшим страниц, собственно изложение самой теории даже не половина https://github.com/michaelt/martin-lof/blob/master/pdfs/Bibliopolis-Book-retypeset-1984.pdf
>Бурбаки
Пикрелейтед.
>Вся лежащая под математикой логика,
Не вся, ZFC не может в типы, а за что-нибудь уровня NBG у бурбаков нет ничего.
>занимает страницы 31-65. Из них на собственно исчисление предикатов отводится четырнадцать страниц.
Вся книжка Мартин-Лёфа 50 с небольшим страниц, собственно изложение самой теории даже не половина https://github.com/michaelt/martin-lof/blob/master/pdfs/Bibliopolis-Book-retypeset-1984.pdf
124 Кб, 635x868>>2038
На твоём пике математика в объёме, превышающем кандидатский курс (гомологическую алгебру не изучают даже в магистратуре, например). Речь шла о предикатах онли. Короче, показывай листок.
Аксиоматика Бурбаки строго сильнее ZFC. Не слабее чем NBG+аксиома глобального выбора.
На твоём пике математика в объёме, превышающем кандидатский курс (гомологическую алгебру не изучают даже в магистратуре, например). Речь шла о предикатах онли. Короче, показывай листок.
>за что-нибудь уровня NBG
Аксиоматика Бурбаки строго сильнее ZFC. Не слабее чем NBG+аксиома глобального выбора.
>>2039
Аксиома S8 - обобщенный replacement, если непонятно.
Аксиома S8 - обобщенный replacement, если непонятно.
>>2039
К этой картинке пояснений как раз под сотню страниц и нужно. Из самой картинки не выведешь тау (или эпсилон Гильберта) и т.д. Ну и главная претензия - вычислимость, конечно. Даже не исключенное третье, с этой хуиткой все ясно, вот самая последняя строка, А5. "Существует бесконечное множество", вот и Аллаха подвезли. В каком смысле оно существует? впрочем, все это опять же уже сто раз обсуждалось, сейчас пойдут аргументы про чернильную дыру и про то что актуальная бесконечность не хуже потенциальной осуществимости, бла-бла... К MLTT так не доебешься, пример - лекция выше, там даже равенство сводится к вычислимым построениям, а не просто к значку "=".
К этой картинке пояснений как раз под сотню страниц и нужно. Из самой картинки не выведешь тау (или эпсилон Гильберта) и т.д. Ну и главная претензия - вычислимость, конечно. Даже не исключенное третье, с этой хуиткой все ясно, вот самая последняя строка, А5. "Существует бесконечное множество", вот и Аллаха подвезли. В каком смысле оно существует? впрочем, все это опять же уже сто раз обсуждалось, сейчас пойдут аргументы про чернильную дыру и про то что актуальная бесконечность не хуже потенциальной осуществимости, бла-бла... К MLTT так не доебешься, пример - лекция выше, там даже равенство сводится к вычислимым построениям, а не просто к значку "=".
>>2039
До двух считать научиться по их книгам можно?
>Аксиоматика Бурбаки строго сильнее ZFC. Не слабее чем NBG+аксиома глобального выбора.
До двух считать научиться по их книгам можно?
>>2044
Нет, на единице застрянешь.
>До двух считать научиться по их книгам можно?
Нет, на единице застрянешь.
>получаем, что полная запись обыкновенной единицы состоит из 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 связей, то есть полная запись терма, обозначающего единицу, заняла бы сто миллиардов квинтиллионов квинтиллионов книг
22 Кб, 333x249>>2046
УРЕТЕ!!!! АДИН ЕТА СЕРЫЙ КОРДЕНАЛ ПУСТОВА МНОЖЕСТВА!!!! ДЖВА ЕТА КАРДЕНАЛ МНОЖАСТВА АДЫН!!! И ТАК ДАЛЕЕ!!!
Мне такой ответ встречался.
УРЕТЕ!!!! АДИН ЕТА СЕРЫЙ КОРДЕНАЛ ПУСТОВА МНОЖЕСТВА!!!! ДЖВА ЕТА КАРДЕНАЛ МНОЖАСТВА АДЫН!!! И ТАК ДАЛЕЕ!!!
Мне такой ответ встречался.
>>2053
Зачем тебе с ординалов фон Неймана так бомбануло? И чем они хуже аутизма уровня гильбертовского эпсилона, при использовании которого получаются термы размером в квинтиллионы знаков?
Зачем тебе с ординалов фон Неймана так бомбануло? И чем они хуже аутизма уровня гильбертовского эпсилона, при использовании которого получаются термы размером в квинтиллионы знаков?
>>2055
До двух досчитать нельзя
До двух досчитать нельзя
24 Кб, 632x198>>2042
Бессмысленная строка символов, которая в естественный язык транслируется как "существует бесконечное множество", является аксиомой.
Либо ты постишь листочек, либо ты - всего лишь ещё один сосачеребенок.
>>2044
Да.
>>2046
Это, конечно же, вздор.
>>2053
Неверно. Кардинал пустого множества - это 0. Число 1 - это кардинал множества {0}. Число 2 - это кардинал множества {0,1}.
>В каком смысле оно существует?
Бессмысленная строка символов, которая в естественный язык транслируется как "существует бесконечное множество", является аксиомой.
>MLTT так не доебешься
Либо ты постишь листочек, либо ты - всего лишь ещё один сосачеребенок.
>>2044
Да.
>>2046
Это, конечно же, вздор.
>>2053
Неверно. Кардинал пустого множества - это 0. Число 1 - это кардинал множества {0}. Число 2 - это кардинал множества {0,1}.
>>2059
Сильное заявление...
Обсирают бурбакистов, конечно же, бетежки которые не смогли их осилить, а не из за того что книги переусложненная хуйня.
>Это, конечно же, вздор
Сильное заявление...
Обсирают бурбакистов, конечно же, бетежки которые не смогли их осилить, а не из за того что книги переусложненная хуйня.
128 Кб, 639x613>>2067
В книгах Бурбаки нет ничего "переусложненного", они очень легко читаются (пикрелейтед). Вообще, это такой детектор очень хороший: кто считает Бурбаки чем-то сложным, тот некомпетентный лапоть с шерстью на ушах.
В книгах Бурбаки нет ничего "переусложненного", они очень легко читаются (пикрелейтед). Вообще, это такой детектор очень хороший: кто считает Бурбаки чем-то сложным, тот некомпетентный лапоть с шерстью на ушах.
>>2059
Что ты разнервничался? Вон же у Максимки все есть http://groupoid.space/mltt/semantics/ с нескучным оформлением. Педивикия опять же.
Это эпсилон Гильберта, формализм курильщика.
>>2069
Школьца-максималиста в тебе вижу я.
>Либо ты постишь листочек, либо ты - всего лишь ещё один сосачеребенок
Что ты разнервничался? Вон же у Максимки все есть http://groupoid.space/mltt/semantics/ с нескучным оформлением. Педивикия опять же.
>Это, конечно же, вздор.
Это эпсилон Гильберта, формализм курильщика.
>>2069
>Вообще, это такой детектор очень хороший: кто считает Бурбаки чем-то сложным, тот некомпетентный лапоть с шерстью на ушах.
Школьца-максималиста в тебе вижу я.
>>2069
Иначе говоря, то что первый параграф ссылается на вторую главу, параграф шесть, пункт номер один, это признак хорошего, годного легко читающегося учебника.
Это ты так двачи тролируешь тупость или реально такой дурачек?
Иначе говоря, то что первый параграф ссылается на вторую главу, параграф шесть, пункт номер один, это признак хорошего, годного легко читающегося учебника.
Это ты так двачи тролируешь тупость или реально такой дурачек?
95 Кб, 815x428>>2072
У бурбаков проблема не в этом. Я даже соглашусь, что это хорошая литература. А в том, что при попытке полной формализации того, о чем они пишут, мы очень быстро упремся в квинтиллионнобуквенные термы. Там же они с самого начала пишут, что для удобочитаемости текста он почти полностью состоит из соглашений, вольностей речи и т.д., откуда и столько отсылок к ранее определенным вещам. В MLTT такой хуйни нет, там все можно свести к вычислениям и вычислить полностью.
>>2073
Попочтец, плиз. Самая первая страница. Пропозишен = формула в матлогике (и множество, согласно изоморфизму Карри-Говарда), суждение = теорема. Совсем подробно - 4ая глава в programming in martin-löf's type theory.
У бурбаков проблема не в этом. Я даже соглашусь, что это хорошая литература. А в том, что при попытке полной формализации того, о чем они пишут, мы очень быстро упремся в квинтиллионнобуквенные термы. Там же они с самого начала пишут, что для удобочитаемости текста он почти полностью состоит из соглашений, вольностей речи и т.д., откуда и столько отсылок к ранее определенным вещам. В MLTT такой хуйни нет, там все можно свести к вычислениям и вычислить полностью.
>>2073
>Что по Мартин-Лёфу есть 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
Если откопаете полную версию то сможете узнать что даже макаки-резусы умеют считать до трех.
Тобишь буракисты это даже не уровень человеческой личинки. Они хуже макак.
>>2075
Я видел этот текст, и он мне непонятен. Прошу объяснить. Я прочитал столько книжек, что слово "формула" для меня не имеет само по себе никакого смысла, увы.
Из сокращений; это другое. Это не неформальность, а лишь инкапсуляция и абстракция. Любую главу трактата можно рассмотреть как набор аксиом некой новой формальной теории, а все предыдущие главы забыть. В этой новой теории букв в знакосочетаниях будет гораздо меньше. Кроме того, трактат можно дополнить минус первой, минус второй и сколь угодно более низкоуровневыми главами - общность при этом будет повышаться, сложность грамматики - падать, количество букв в знакосочетаниях - увеличиваться. Например, язык начальной главы можно транслировать в морзянку. Математика окажется в таком случае теорией о громадных совокупностях точек и тире.
Я видел этот текст, и он мне непонятен. Прошу объяснить. Я прочитал столько книжек, что слово "формула" для меня не имеет само по себе никакого смысла, увы.
>из соглашений, вольностей речи и т.д.
Из сокращений; это другое. Это не неформальность, а лишь инкапсуляция и абстракция. Любую главу трактата можно рассмотреть как набор аксиом некой новой формальной теории, а все предыдущие главы забыть. В этой новой теории букв в знакосочетаниях будет гораздо меньше. Кроме того, трактат можно дополнить минус первой, минус второй и сколь угодно более низкоуровневыми главами - общность при этом будет повышаться, сложность грамматики - падать, количество букв в знакосочетаниях - увеличиваться. Например, язык начальной главы можно транслировать в морзянку. Математика окажется в таком случае теорией о громадных совокупностях точек и тире.
>>2072
Это конструктивисты траллируют тупостью, когда говорят, что бесконечности нет и аксиома исключающего третьего вера.
>тролируешь тупость
Это конструктивисты траллируют тупостью, когда говорят, что бесконечности нет и аксиома исключающего третьего вера.
>>2077
Считающаяся в термы из квинтиллионов знаков. Это проблема, пони маешь? Потому что если мы захотим это на самом деле посчитать, то...
Значит, неправильные книжки читал. Я ж уточнил, что "формула" там имеет значение, обычное именно для матлогики. Ну и также можно считать пропозишен множеством.
>>2078
Ты для начала пойми о чем вообще тут говорят, потом в разговор лезь.
>а лишь инкапсуляция и абстракция
Считающаяся в термы из квинтиллионов знаков. Это проблема, пони маешь? Потому что если мы захотим это на самом деле посчитать, то...
>Я прочитал столько книжек, что слово "формула" для меня не имеет само по себе никакого смысла, увы.
Значит, неправильные книжки читал. Я ж уточнил, что "формула" там имеет значение, обычное именно для матлогики. Ну и также можно считать пропозишен множеством.
>>2078
>когда говорят, что бесконечности нет
Ты для начала пойми о чем вообще тут говорят, потом в разговор лезь.
>>2079
Только если считающему угодно настолько сильно углубиться в абстракцию. Он вполне может остаться на одном из более высоких уровней, на них символов будет заметно меньше. Например, можно отказаться от трансляции кванторов и импликации, приняв их в синтаксис, тогда квинтиллионы мгновенно исчезнут. Алсо, не в термы, в знакосочетания.
Произвольная формула? Правильно построенная формула (элемент наименьшего класса формул, замкнутого относительно логических связок и содержащего все атомы)? Выводимая формула? Меня "hold to be true" смущает, это вообще о чем.
>в термы из квинтиллионов знаков
Только если считающему угодно настолько сильно углубиться в абстракцию. Он вполне может остаться на одном из более высоких уровней, на них символов будет заметно меньше. Например, можно отказаться от трансляции кванторов и импликации, приняв их в синтаксис, тогда квинтиллионы мгновенно исчезнут. Алсо, не в термы, в знакосочетания.
>обычное именно для матлогики
Произвольная формула? Правильно построенная формула (элемент наименьшего класса формул, замкнутого относительно логических связок и содержащего все атомы)? Выводимая формула? Меня "hold to be true" смущает, это вообще о чем.
64 Кб, 818x381>>2080
Изоморфизм Карри-Говарда же. И интерпретация логических констант по Брауэру-Гейтингу-Колмогорову. Общеизвестно, что логические операции это то же самое, что операции над множествами. Истина - это 1, ложь = 0. Классически пропозишен - это функция принадлежности или характеристическая функция, принимающая значение 0 или 1 (не считая многозначных логик). Логическое "и" это пересечение множеств, "или" - объединение, импликация - отношение подмножества. Конструктивно же пропозишен - это множество пруф-объектов, т.е. построений, доказывающих, что данное множество не пусто. Т.о. по упомянутому изоморфизму Карри-Говарда, истинность пропозишена А - это ненулевое количество элементов х принадлежащих А, х:А. Доказательство "не А" - это построенное пустое множество. Отсюда уже видно, почему исключенное третье в общем случае не работает. Классически верно правило "А или не А", конструктивно мы должны доказать конкретно, А или не А, т.е. пусто множество А или нет. Это можно сделать только построив его. Конкретные методы построений получаются интерпретацией логических констант по Колмогорову, т.е. в простейшем случае это могут быть лямбда-термы, а все вышесказанное в таком случае можно свести к типизированной лямбде, откуда вычисление это есть лямбда-определимость. Итд итп.
Классически и так сойдет, конечно. тяп-ляп и готов кризис оснований Конструктивно нам нужна полная вычислимость, чего с бурбаками не выйдет вообще никак.
>Меня "hold to be true" смущает, это вообще о чем.
Изоморфизм Карри-Говарда же. И интерпретация логических констант по Брауэру-Гейтингу-Колмогорову. Общеизвестно, что логические операции это то же самое, что операции над множествами. Истина - это 1, ложь = 0. Классически пропозишен - это функция принадлежности или характеристическая функция, принимающая значение 0 или 1 (не считая многозначных логик). Логическое "и" это пересечение множеств, "или" - объединение, импликация - отношение подмножества. Конструктивно же пропозишен - это множество пруф-объектов, т.е. построений, доказывающих, что данное множество не пусто. Т.о. по упомянутому изоморфизму Карри-Говарда, истинность пропозишена А - это ненулевое количество элементов х принадлежащих А, х:А. Доказательство "не А" - это построенное пустое множество. Отсюда уже видно, почему исключенное третье в общем случае не работает. Классически верно правило "А или не А", конструктивно мы должны доказать конкретно, А или не А, т.е. пусто множество А или нет. Это можно сделать только построив его. Конкретные методы построений получаются интерпретацией логических констант по Колмогорову, т.е. в простейшем случае это могут быть лямбда-термы, а все вышесказанное в таком случае можно свести к типизированной лямбде, откуда вычисление это есть лямбда-определимость. Итд итп.
>Только если считающему угодно настолько сильно углубиться в абстракцию. Он вполне может остаться на одном из более высоких уровней, на них символов будет заметно меньше.
Классически и так сойдет, конечно. тяп-ляп и готов кризис оснований Конструктивно нам нужна полная вычислимость, чего с бурбаками не выйдет вообще никак.
>>2081
А как быть, если нужны нелогические операции? От голого исчисления предикатов мало пользы, пользу приносят первопорядковые теории (исчисление предикатов плюс нелогические формулы).
Для корректности такого подхода нужно зафиксировать метатеорию множеств и внятно определить предметную область. Неоправданно сложный подход, чисто синтаксический подход гораздо яснее (а всё семантическое надстраивается на него в теории моделей).
Что считается построением?
Вычислимость бесконечна вниз, если можно так выразиться. Всегда можно заменить атомарное действие фиксированного исполнителя подпрограммой для более низкоуровневого исполнителя. Полной вычислимости не бывает.
>логические операции
А как быть, если нужны нелогические операции? От голого исчисления предикатов мало пользы, пользу приносят первопорядковые теории (исчисление предикатов плюс нелогические формулы).
>операции над множествами
Для корректности такого подхода нужно зафиксировать метатеорию множеств и внятно определить предметную область. Неоправданно сложный подход, чисто синтаксический подход гораздо яснее (а всё семантическое надстраивается на него в теории моделей).
>построений
Что считается построением?
>полная вычислимость
Вычислимость бесконечна вниз, если можно так выразиться. Всегда можно заменить атомарное действие фиксированного исполнителя подпрограммой для более низкоуровневого исполнителя. Полной вычислимости не бывает.
>>2083
Собственно, на все вопросы в твоем посте ответ один - типизированная лямбда.
Только до канонических элементов, которые дальше невычислимы ни во что.
Собственно, на все вопросы в твоем посте ответ один - типизированная лямбда.
>Вычислимость бесконечна вниз, если можно так выразиться.
Только до канонических элементов, которые дальше невычислимы ни во что.
>>2085
По определению - замкнутые, насыщенные лямбда-термы нулевой арности. Ну или категоремы. Элементы, которые нельзя вычислить во что-то нижележащее, т.к. они сами по себе есть итоговые значение вычислений. Пример - натуральные числа, как элементы множества N они не сводятся к чему-либо более простому.
По определению - замкнутые, насыщенные лямбда-термы нулевой арности. Ну или категоремы. Элементы, которые нельзя вычислить во что-то нижележащее, т.к. они сами по себе есть итоговые значение вычислений. Пример - натуральные числа, как элементы множества N они не сводятся к чему-либо более простому.
>>2086
Я не знаю, что это такое. Но ведь, гм. Для натуральных чисел можно предложить много нижележащих теорий, разве нет?
>категоремы
Я не знаю, что это такое. Но ведь, гм. Для натуральных чисел можно предложить много нижележащих теорий, разве нет?
>>2087
Вычислимых-то? Думаю, строго 0. Ниже нумералов Черча сложно что-то придумать, даже ординалы фон Неймана - это то же яйцо, вид сбоку. Впрочем, можешь и предложить, думаю медаль филдса за таконе точно не пожалеют.
>Для натуральных чисел можно предложить много нижележащих теорий, разве нет?
Вычислимых-то? Думаю, строго 0. Ниже нумералов Черча сложно что-то придумать, даже ординалы фон Неймана - это то же яйцо, вид сбоку. Впрочем, можешь и предложить, думаю медаль филдса за таконе точно не пожалеют.
3 Кб, 217x78>>2088
Теория, предложенная Бурбаки. Если не вводить теорию множеств во всей полноте, то арифметические построения можно описать знакосочетаниями вида пикрелейтед длиной не более чем в несколько миллионов символов (грубая оценка сверху, на самом деле меньше). Вполне реальный объём для современных компьютеров.
Теория, предложенная Бурбаки. Если не вводить теорию множеств во всей полноте, то арифметические построения можно описать знакосочетаниями вида пикрелейтед длиной не более чем в несколько миллионов символов (грубая оценка сверху, на самом деле меньше). Вполне реальный объём для современных компьютеров.
>>2089
Эпсилоны Гильберта считать со всеми квинтиллионами знаков? Вот ты спрашивал, что есть канонический объект. Вот этот хулиардквадриллионный терм для единицы - это как раз канонический элемент множества N по бурбакам, который ниже уже ни во что не считается. Это можно, конечно. Но грустно, когда ферма из асиков размером с взлетную полосу, будет считать 1+1 пару дней. Самое обидное, что итоговый результат будет тот же, что с нумералами Черча, т.е. натуральное число 2, которое, конечно можно представить еще какими-то квадриллионными термами, но остается вопрос - нижестоящая ли это теория или таки вышестоящая, т.к. использует более сложный алфавит, чем н-р натуральное число как слово в алфавите | по Маркову?
Эпсилоны Гильберта считать со всеми квинтиллионами знаков? Вот ты спрашивал, что есть канонический объект. Вот этот хулиардквадриллионный терм для единицы - это как раз канонический элемент множества N по бурбакам, который ниже уже ни во что не считается. Это можно, конечно. Но грустно, когда ферма из асиков размером с взлетную полосу, будет считать 1+1 пару дней. Самое обидное, что итоговый результат будет тот же, что с нумералами Черча, т.е. натуральное число 2, которое, конечно можно представить еще какими-то квадриллионными термами, но остается вопрос - нижестоящая ли это теория или таки вышестоящая, т.к. использует более сложный алфавит, чем н-р натуральное число как слово в алфавите | по Маркову?
>>2090
Миллионами.
То есть канонический элемент - это всего лишь терм в формальном языке, который выбран для аксиоматической теории?
Миллионами.
То есть канонический элемент - это всего лишь терм в формальном языке, который выбран для аксиоматической теории?
>>2091
Точнее терм, который в данной теории нельзя свести ни к чему нижележащему. Но тут уже встает вопрос математического релятивизма (не путать с физикой), согласно которому, любую теорию можно выразить через любую другую, точнее между теорией А и В существует конечное количество теорий А1-Ан, причем теория А выразима в теории А1, а теория Ан - в теории В. В таком случае без разницы, какую теорию считать первичной, т.к. мы все равно можем придти к любой из них из любой другой. Чисто прагматически, более первичной удобнее считать более простую теорию, т.е. уж точно не стоит считать эпсилон-исчисление Гильберта основанием арифметики, потому что полнейший аутизм сначала учить детей в школе эпсилон-исчислению, а затем решать примеры 1+1. Конструктивно всю математику можно вывести из арифметики, прагматически это самый простой путь, гораздо проще и естественнее чем теория множеств, тем более в виде бурбакизма. Естественнее, потому что доказано, что понятие натурального числа врожденно и предшествует даже языковым способностям (такие нейрофизиологические модели как ATOM Уолша и теория метафор), если с более философской стороны, то Кант и Брауэр.
>То есть канонический элемент - это всего лишь терм в формальном языке, который выбран для аксиоматической теории?
Точнее терм, который в данной теории нельзя свести ни к чему нижележащему. Но тут уже встает вопрос математического релятивизма (не путать с физикой), согласно которому, любую теорию можно выразить через любую другую, точнее между теорией А и В существует конечное количество теорий А1-Ан, причем теория А выразима в теории А1, а теория Ан - в теории В. В таком случае без разницы, какую теорию считать первичной, т.к. мы все равно можем придти к любой из них из любой другой. Чисто прагматически, более первичной удобнее считать более простую теорию, т.е. уж точно не стоит считать эпсилон-исчисление Гильберта основанием арифметики, потому что полнейший аутизм сначала учить детей в школе эпсилон-исчислению, а затем решать примеры 1+1. Конструктивно всю математику можно вывести из арифметики, прагматически это самый простой путь, гораздо проще и естественнее чем теория множеств, тем более в виде бурбакизма. Естественнее, потому что доказано, что понятие натурального числа врожденно и предшествует даже языковым способностям (такие нейрофизиологические модели как ATOM Уолша и теория метафор), если с более философской стороны, то Кант и Брауэр.
>>2092
Спасибо за ответы.
Бывает разная простота. Есть простота для решения задач, причем для разных классов задач простотой окажется разное - например, для решения уравнений вида x+a=b бурбаки очевидно не будут самым простым выбором. Есть простота для доказательства теорем, и вот здесь уже может оказаться наиболее простым выбором, скажем, определять дроби с помощью деления в столбик (анекдотический пример от Арнольда). Универсальной простоты не бывает.
Спасибо за ответы.
Бывает разная простота. Есть простота для решения задач, причем для разных классов задач простотой окажется разное - например, для решения уравнений вида x+a=b бурбаки очевидно не будут самым простым выбором. Есть простота для доказательства теорем, и вот здесь уже может оказаться наиболее простым выбором, скажем, определять дроби с помощью деления в столбик (анекдотический пример от Арнольда). Универсальной простоты не бывает.
>>2103
А чем твои думы в области математики, чукча, отличаются от дум пекарни в этой же области? Я просил привести примеры вычислимости, не сводящиеся у механическим преобразованиям выражений. Пока примеров не поступало.
> Правильно, зачем чукче думать, пусть пекарня думает
А чем твои думы в области математики, чукча, отличаются от дум пекарни в этой же области? Я просил привести примеры вычислимости, не сводящиеся у механическим преобразованиям выражений. Пока примеров не поступало.
>>2108
Старые песни о главном. Если что-то невычислимо, с какой стати это вообще математика? И да, что в математике не сводится к вычислимости? Исключенное третье, актуальная бесконечность и прочая религия?
> Не вся математика сводится к вычислимости.
Старые песни о главном. Если что-то невычислимо, с какой стати это вообще математика? И да, что в математике не сводится к вычислимости? Исключенное третье, актуальная бесконечность и прочая религия?
>>2110
Примеры, примеры в студию. Что в математике не сводится к алгоритмам, где математика, не являющаяся преобразованием знакосочетаний и термов по заданным правилам? Формализм без формализма, давай примеры.
> Это ты сужаешь математику на computer science, ограничевая его её алгоритмами.
Примеры, примеры в студию. Что в математике не сводится к алгоритмам, где математика, не являющаяся преобразованием знакосочетаний и термов по заданным правилам? Формализм без формализма, давай примеры.
>>2112
Ты можешь как-то решить алгоритмически неразрешимые проблемы? И как?
> А как же алгоритмически неразрешимые проблемы?
Ты можешь как-то решить алгоритмически неразрешимые проблемы? И как?
>>2113
И что это? Ты хочешь сказать, что это неразрешимо алгоритмически, но разрешимо как-то иначе?
И что это? Ты хочешь сказать, что это неразрешимо алгоритмически, но разрешимо как-то иначе?
>>2118
Ясно. Вчера по бурбакам пояснил за все эти сокращения, соглашения итд, остальное по аналогии. Не считая того, что в mltt аксиома выбора это не аксиома, а теорема и ее можно доказать. Тоже сто раз уже писал, давал ссылкуи постил скрины.
Ясно. Вчера по бурбакам пояснил за все эти сокращения, соглашения итд, остальное по аналогии. Не считая того, что в mltt аксиома выбора это не аксиома, а теорема и ее можно доказать. Тоже сто раз уже писал, давал ссылкуи постил скрины.
>>2120
Зачем? Там в любом случае нотация, формализмы и правила преобразований, т.е алгоритмы.
> Я про скрины с Энгелькингом, прочитай его и посмотри.
Зачем? Там в любом случае нотация, формализмы и правила преобразований, т.е алгоритмы.
>>2122
Как в случае с комплексными числами, ты опять притащил сам не понимаешь что, и теперь пытаешься троллить тупостью. Мне это не интересно.
Как в случае с комплексными числами, ты опять притащил сам не понимаешь что, и теперь пытаешься троллить тупостью. Мне это не интересно.
>>2123
Тебе не надоело уходить от ответов?
Тебе не надоело уходить от ответов?
>>2125
Есть правила работы с этим. Есть то, откуда это вывели, есть следствия, к которым это приводит. Если у тебя от слова 'алгоритм' бампельштильцхен, это не ко мне. И обяснять вещи, которые уже 3хлетний бы понял, мне так же неинтересно. Ты даже не можешь объяснить о чем речь вообще, мне это и темболее не нужно.
> там нет алгоритмов
Есть правила работы с этим. Есть то, откуда это вывели, есть следствия, к которым это приводит. Если у тебя от слова 'алгоритм' бампельштильцхен, это не ко мне. И обяснять вещи, которые уже 3хлетний бы понял, мне так же неинтересно. Ты даже не можешь объяснить о чем речь вообще, мне это и темболее не нужно.
>>2092
А есть идеи как учить школьников конструктивной математике? В смысле, наверное, большей работы со средствами доказательства теорем или что-то такое. Или может еще что?
А есть идеи как учить школьников конструктивной математике? В смысле, наверное, большей работы со средствами доказательства теорем или что-то такое. Или может еще что?
>>2137
Лямбда исчисления вполне можно изложить так, чтобы понял школьник. Тем более, что всю домашку можно сразу писать и проверять в коке. Другой вопрос, зачем.
Лямбда исчисления вполне можно изложить так, чтобы понял школьник. Тем более, что всю домашку можно сразу писать и проверять в коке. Другой вопрос, зачем.
>>2136
И что дальше? Ты хочешь сказать, что это не укладывается в понятия формализма, нотации или допустимых преобразований выражений, термов или знакосочетаний? Или что ты доказать-то пытаешься?
> С аксиомой выбора так же. Есть следствия, к которым она приводит.
И что дальше? Ты хочешь сказать, что это не укладывается в понятия формализма, нотации или допустимых преобразований выражений, термов или знакосочетаний? Или что ты доказать-то пытаешься?
>>2141
Она укладывается "в понятия формализма, нотации и допустимых преобразований выражений".
Она укладывается "в понятия формализма, нотации и допустимых преобразований выражений".
>>1361 (OP)
Господа, а хоть один человек в этом треде занимается вопросом оснований ПРОФЕССИОНАЛЬНО?
Сколько уже теорем доказали?
Или трёп сплошной?
Если есть хоть один - деанонься, публикацию свою покажи, будем на тебя ровняться.
На самом деле нет таких, какие-то глупые, бессодержательные разговоры ни о чём.
Господа, а хоть один человек в этом треде занимается вопросом оснований ПРОФЕССИОНАЛЬНО?
Сколько уже теорем доказали?
Или трёп сплошной?
Если есть хоть один - деанонься, публикацию свою покажи, будем на тебя ровняться.
На самом деле нет таких, какие-то глупые, бессодержательные разговоры ни о чём.
>>2151
Я ради стипухи взял одно недоказанное (оставим читателю в качестве упражнения) утверждение из маклейна и тиснул статью с его доказательством. Стипуху дали.
Я ради стипухи взял одно недоказанное (оставим читателю в качестве упражнения) утверждение из маклейна и тиснул статью с его доказательством. Стипуху дали.
>>2152
Погоди, а в какие журналы такую статью могли принять? А то я тут на хлебе и воде, а доказывать люблю.
Погоди, а в какие журналы такую статью могли принять? А то я тут на хлебе и воде, а доказывать люблю.
>>2153
Вестник МухГУ.
Вестник МухГУ.
>>2170
Алгоритмами её точно не решить. Но это не значит, что без алгоритмов её решить нельзя. Ты же сам вроде должен быть против исключённого третьего?
Алгоритмами её точно не решить. Но это не значит, что без алгоритмов её решить нельзя. Ты же сам вроде должен быть против исключённого третьего?
>>2170
Да и вообще по твоей логике должен существовать единый алгоритм доказательства теорем. Даже конструктивные доказательства предполагают некоторый рывок во вне и этот рывок в каждом случае уникален. Так что если с вычислимостью и построением ещё можно понять и согласиться, то вот аппелировать к алгоритмической разрешимости уже полная ересь даже с точки зрения конструктивизма. Ты сам, похоже, до конца не понимаешь что такое конструктивность.
Да и вообще по твоей логике должен существовать единый алгоритм доказательства теорем. Даже конструктивные доказательства предполагают некоторый рывок во вне и этот рывок в каждом случае уникален. Так что если с вычислимостью и построением ещё можно понять и согласиться, то вот аппелировать к алгоритмической разрешимости уже полная ересь даже с точки зрения конструктивизма. Ты сам, похоже, до конца не понимаешь что такое конструктивность.
>>2170
То есть у тебя есть правила языка, ты можешь переводить на другой язык с помощью алгоритмов и тд, но ты не сможешь написать осмысленный текст, можно перебрать все варианты из существующих и тем самым доказать, что других вариантов нет, но сами эти варианты алгоритмически не найти, для этого нужен некий критерий закономерности, когда машина решает, является ли что-то закономерным, определяет что, обобщает и затем уже подтверждает или опровергает это конструктивно. Именно поиск закономерностей, обобщение и
То есть у тебя есть правила языка, ты можешь переводить на другой язык с помощью алгоритмов и тд, но ты не сможешь написать осмысленный текст, можно перебрать все варианты из существующих и тем самым доказать, что других вариантов нет, но сами эти варианты алгоритмически не найти, для этого нужен некий критерий закономерности, когда машина решает, является ли что-то закономерным, определяет что, обобщает и затем уже подтверждает или опровергает это конструктивно. Именно поиск закономерностей, обобщение и
> не сводится к алгоритмам, где математика, не являющаяся преобразованием знакосочетаний и термов по заданным правилам
>>2159
Математика - это как игра в шахматы.
Если не знаешь как ходят фигуры, то и играешь неадекватно.
Строгие формальные доказательства обучают простейшим ходам.
Математика - это как игра в шахматы.
Если не знаешь как ходят фигуры, то и играешь неадекватно.
Строгие формальные доказательства обучают простейшим ходам.
>>2171
Демагогия.
>>2172
Я уже просил не нести хуйни. Алгоритмически неразрешимые задачи никто не отменял.
>>2173
И еще раз прошу не нести хуйни. То, что ты описал, называется идентификацией систем и реализуется очень большим количеством алгоритмов. Итого, ты не в теме абсолютно, а разжевывать такие азы мне неинтересно вообще никак.
>Алгоритмами её точно не решить. Но это не значит, что без алгоритмов её решить нельзя.
Демагогия.
>>2172
Я уже просил не нести хуйни. Алгоритмически неразрешимые задачи никто не отменял.
>>2173
>Именно поиск закономерностей, обобщение и не сводится к алгоритмам, где математика, не являющаяся преобразованием знакосочетаний и термов по заданным правилам
И еще раз прошу не нести хуйни. То, что ты описал, называется идентификацией систем и реализуется очень большим количеством алгоритмов. Итого, ты не в теме абсолютно, а разжевывать такие азы мне неинтересно вообще никак.
>>2177
Надо научиться играть в шахматы тогда хотя бы, дабы понять аналогию.
Надо научиться играть в шахматы тогда хотя бы, дабы понять аналогию.
>>2181
Ну так я сколько раз уже просил показать неалгоритмическое решение любой алгоритмически неразрешимой проблемы. Примеров нет. Их и не будет, поскольку например, из нас двоих кто-то не знаком с работами Тьюринга и Поста. И кто бы это мог быть, как думаешь?
Ну так я сколько раз уже просил показать неалгоритмическое решение любой алгоритмически неразрешимой проблемы. Примеров нет. Их и не будет, поскольку например, из нас двоих кто-то не знаком с работами Тьюринга и Поста. И кто бы это мог быть, как думаешь?
>>2179
Лол что? Ты пишешь , мол, раз алгоритмически задача неразрешима, то она неразрешима впринципе. Я говорю, что одно из другого не следует. Где тут демагогия?
Например?
Демагогия.
>Демагогия.
Лол что? Ты пишешь , мол, раз алгоритмически задача неразрешима, то она неразрешима впринципе. Я говорю, что одно из другого не следует. Где тут демагогия?
>То, что ты описал, называется идентификацией систем и реализуется очень большим количеством алгоритмов
Например?
>Я уже просил не нести хуйни
>И еще раз прошу не нести хуйни.
>Итого, ты не в теме абсолютно, а разжевывать такие азы мне неинтересно вообще никак.
Демагогия.
>>2189
Давай так, пока не принесешь примера решения неалгоритмическими методами алгоритмически неразрешимой математической проблемы, можешь мне вообще не писать. У меня нет никакого желания даже пытаться объяснить человеку, не слышавшему про тезис Черча, из чего конкретно следует общая неразрешимость алгоритмически неразрешимых задач.
>Ты пишешь , мол, раз алгоритмически задача неразрешима, то она неразрешима впринципе. Я говорю, что одно из другого не следует. Где тут демагогия?
Давай так, пока не принесешь примера решения неалгоритмическими методами алгоритмически неразрешимой математической проблемы, можешь мне вообще не писать. У меня нет никакого желания даже пытаться объяснить человеку, не слышавшему про тезис Черча, из чего конкретно следует общая неразрешимость алгоритмически неразрешимых задач.
>>2189
Ну и да, это не то, что я описал. Я о том, что, например, нет такого алгоритма, который бы, например, получая на вход последовательность чисел 2 5 12 27 58 121 ... мог бы найти закономерность, "догадаться", что это 2n-n или 2*предыдущее+номер. Разве такие алгоритмы есть? Человек же такую задачу может решить, потупив в последовательность минуту.
>То, что ты описал, называется идентификацией систем
Ну и да, это не то, что я описал. Я о том, что, например, нет такого алгоритма, который бы, например, получая на вход последовательность чисел 2 5 12 27 58 121 ... мог бы найти закономерность, "догадаться", что это 2n-n или 2*предыдущее+номер. Разве такие алгоритмы есть? Человек же такую задачу может решить, потупив в последовательность минуту.
>>2190
Нет, не следует. Перечитай, о чём он говорит.
Или вот ещё пример. Нужно найти натуральные корни.
x5+2x3+3x2-60=0
По теореме Абеля — Руффини не существует формулы, алгоритма по которому можно найти корни этого уравнения, но подставив 2, догадавшись, мы получим решение. По твоему это уже не математика, а гадание на Аллахе?
> из чего конкретно следует
Нет, не следует. Перечитай, о чём он говорит.
>Алгоритмически неразрешимо
Или вот ещё пример. Нужно найти натуральные корни.
x5+2x3+3x2-60=0
По теореме Абеля — Руффини не существует формулы, алгоритма по которому можно найти корни этого уравнения, но подставив 2, догадавшись, мы получим решение. По твоему это уже не математика, а гадание на Аллахе?
>>2194
Нет, вчера с корешем эксперимент проводили, он загадал вот эту последовательность и нужно было найти закономерность, правда мой ответ был, что это
a(n+1)=2a(n)+n, но не суть.
Вот это тоже, в математике это повсюду, а что это вообще? Как происходит обобщение? Как это алгоритмизировать?
>не догадался
Нет, вчера с корешем эксперимент проводили, он загадал вот эту последовательность и нужно было найти закономерность, правда мой ответ был, что это
a(n+1)=2a(n)+n, но не суть.
>обобщил
Вот это тоже, в математике это повсюду, а что это вообще? Как происходит обобщение? Как это алгоритмизировать?
>>2191
Деточка, дуй в школку, ну. Ты про идентификацию систем не слышал, зачем ты свою тупость используешь как доказательство чего-то? Это же настолько элементарная задача идентификации, что даже объяснять как ее решить алгоритмически, смешно. Простая регрессия на калькуляторе с этой задачей справится, достаточно расположить эти числа парами
+ x = c(2,12,58),
+ y = c(5,27,121)
+ )
x y
1 2 5
2 12 27
3 58 121
и применить регрессию:
1
251.0897
Следующее значение твоего ряда 251. А вот теперь точно уебывай, потому что детский сад - это не тот уровень, на котором мне было бы интересно дискутировать.
>Разве такие алгоритмы есть?
Деточка, дуй в школку, ну. Ты про идентификацию систем не слышал, зачем ты свою тупость используешь как доказательство чего-то? Это же настолько элементарная задача идентификации, что даже объяснять как ее решить алгоритмически, смешно. Простая регрессия на калькуляторе с этой задачей справится, достаточно расположить эти числа парами
> 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. А вот теперь точно уебывай, потому что детский сад - это не тот уровень, на котором мне было бы интересно дискутировать.
>>2195
Как бы да, это и правда оно, как и доказательство от противного, ведь есть разница между построением объекта и доказательством того, что несуществование объекта противоречиво. Но решение ведь есть. И таких примеров использования Аллаха в математике сотни.
>>2197
Но следующее число 248, лол. Регрессия.
>гадание на Аллахе
Как бы да, это и правда оно, как и доказательство от противного, ведь есть разница между построением объекта и доказательством того, что несуществование объекта противоречиво. Но решение ведь есть. И таких примеров использования Аллаха в математике сотни.
>>2197
Но следующее число 248, лол. Регрессия.
Доказательство седьмой проблеммы Гилберта неконструктивно и использует не алгоритмические методы.
>>2198
Это простая линейная регрессия на датасете из 3х значений. Естественно, что это не самый лучший метод из существующих. Дело не в этом, а в том, что ты своеим неопниманием пытаешься что-то доказать. Буду репортить троллинг тупостью, в общем.
Это простая линейная регрессия на датасете из 3х значений. Естественно, что это не самый лучший метод из существующих. Дело не в этом, а в том, что ты своеим неопниманием пытаешься что-то доказать. Буду репортить троллинг тупостью, в общем.
>>2215
Потому что ты дебил и она существует.
Пересчитай мне все числа между нулем и единицей. И когда я говорю все, я имю ввиду ВСЕ*
Потому что ты дебил и она существует.
Пересчитай мне все числа между нулем и единицей. И когда я говорю все, я имю ввиду ВСЕ*
>>2217
Тем что ты не почитаешь их все.
На основании аксиомы о непрерывности числового ряда ты можешь бесконечно делить числа и получать новые и новые числа, конца края этому не будет из за того, что исходя из аксиомы о непрерывности...
Тем что ты не почитаешь их все.
На основании аксиомы о непрерывности числового ряда ты можешь бесконечно делить числа и получать новые и новые числа, конца края этому не будет из за того, что исходя из аксиомы о непрерывности...
>>2197
>>2212 (Del)
Ну и да, там надо тогда уж
#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 это номер члена потому что.
>>2212 (Del)
Ну и да, там надо тогда уж
#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 это номер члена потому что.
>>2197
И скажи, конструктивизм всегда алгоритм предполагает разве? Построить значит предоставить алгоритм построения?
И скажи, конструктивизм всегда алгоритм предполагает разве? Построить значит предоставить алгоритм построения?
>>2219
Существует.
Существует.
>>2222
Ты гет упустил, глупец.
Ты гет упустил, глупец.
>>2222
Ну и че ты сделал, сам-то понял? Там пары значений (х у), а у тебя х - просто последовательность натуральных чисел от 1 до 6
Ну и че ты сделал, сам-то понял? Там пары значений (х у), а у тебя х - просто последовательность натуральных чисел от 1 до 6
>>2222
Короче, это же числовой ряд, из которого я сделал матрицу Ганкеля. Линейная регрессия недостаточно точно аппроксимирует такие нелинейные значения, да еше и датасет из 3х пар, но мой результат почти такой же как у этого шизика, а твой в 2 раза неправильный.
Короче, это же числовой ряд, из которого я сделал матрицу Ганкеля. Линейная регрессия недостаточно точно аппроксимирует такие нелинейные значения, да еше и датасет из 3х пар, но мой результат почти такой же как у этого шизика, а твой в 2 раза неправильный.
>>2235
Так y от x должно зависеть,а ты просто взял значения y и поделил их на две части, лол.
Ну правильно, y=2x-x,
Да он и не должен быть правильным, как ты вообще умудрился применять линейную регрессию, когда очевидна эксп зависимость. То, что у тебя получилось "почти такой же" простое совпадение.
>Там пары значений
Так y от x должно зависеть,а ты просто взял значения y и поделил их на две части, лол.
>х - просто последовательность натуральных чисел от 1 до 6
Ну правильно, y=2x-x,
> твой в 2 раза неправильный.
Да он и не должен быть правильным, как ты вообще умудрился применять линейную регрессию, когда очевидна эксп зависимость. То, что у тебя получилось "почти такой же" простое совпадение.
>>2241
Это не совпадение, а аппроксимация. Точной она и не могла быть, т.к. зависимость нелинейная, а я использовал линейную регрессию + датасет никакой. Еще раз: из датасета была сделана матрица Ганкеля, что соответствует NARX-модели а потом линейной регрессией была проведена идентификация системы y = f(x). Регрессией т.о. была получена аппроксимация функции f, но т.к. в реальной системе эта функция нелинейна и датасет размером близок к 0, то вышла некоторая, согласись, довольно небольшая ошибочка для данных условий. Похоже, кроме меня про такое никто не слышал? Страшно вы живете, а.
>То, что у тебя получилось "почти такой же" простое совпадение.
Это не совпадение, а аппроксимация. Точной она и не могла быть, т.к. зависимость нелинейная, а я использовал линейную регрессию + датасет никакой. Еще раз: из датасета была сделана матрица Ганкеля, что соответствует NARX-модели а потом линейной регрессией была проведена идентификация системы y = f(x). Регрессией т.о. была получена аппроксимация функции f, но т.к. в реальной системе эта функция нелинейна и датасет размером близок к 0, то вышла некоторая, согласись, довольно небольшая ошибочка для данных условий. Похоже, кроме меня про такое никто не слышал? Страшно вы живете, а.
>>2242
Лол, согласись, что аппроксимация рекуррентного соотношения это всё равно, что сказать "нуу каждый следующий член больше предыдущего примерно в два раза". Это не решение проблемы.
Лол, согласись, что аппроксимация рекуррентного соотношения это всё равно, что сказать "нуу каждый следующий член больше предыдущего примерно в два раза". Это не решение проблемы.
>>2243
Линейная регрессия - не решение нелинейной проблемы. В остальном идентификация систем как раз для нахождения неизвестных зависимостей выходов от входов. Даже кусочно-линейная аппроксимация (скажем, моделью Такаги-Сугено) функции выхода от входа на таком датасете была бы точнее. Ну и про теоремы об универсальной аппроксимации тут тоже не слышали, эх, африка.
Линейная регрессия - не решение нелинейной проблемы. В остальном идентификация систем как раз для нахождения неизвестных зависимостей выходов от входов. Даже кусочно-линейная аппроксимация (скажем, моделью Такаги-Сугено) функции выхода от входа на таком датасете была бы точнее. Ну и про теоремы об универсальной аппроксимации тут тоже не слышали, эх, африка.
>>2244
Аппроксимация вообще не решение, понятно, что аппроксимировать много чего можно, речь шла о том, как алгоритмически получить из данных точную формулу, породившую их. Неалгоритмически это сделать можно.
Аппроксимация вообще не решение, понятно, что аппроксимировать много чего можно, речь шла о том, как алгоритмически получить из данных точную формулу, породившую их. Неалгоритмически это сделать можно.
>>2244
Ну и применять линейную регрессию можно только в предположении линейности зависости. Иначе смысла в такой "аппроксимации" нет никакого.
Ну и применять линейную регрессию можно только в предположении линейности зависости. Иначе смысла в такой "аппроксимации" нет никакого.
>>2245
Во-первых, идентификацией системы это сделать можно. Конкретных примеров полно. Во-вторых, то, что ты называешь "неалгоритмически" на самом деле алгоритм.
>>2250
Я понял твой уровень знаний в этой теме, дальше меня на эту тему можешь не смешить.
>речь шла о том, как алгоритмически получить из данных точную формулу, породившую их. Неалгоритмически это сделать можно.
Во-первых, идентификацией системы это сделать можно. Конкретных примеров полно. Во-вторых, то, что ты называешь "неалгоритмически" на самом деле алгоритм.
>>2250
Я понял твой уровень знаний в этой теме, дальше меня на эту тему можешь не смешить.
>>2251
Хватит нести чушь и заниматься демагогией, примеров полно так неси хотя бы один.
Ага, всё алгоритм, просто мы ещё не поняли этого. Сектант.
>полно примеров
Хватит нести чушь и заниматься демагогией, примеров полно так неси хотя бы один.
> "неалгоритмически" на самом деле алгоритм
Ага, всё алгоритм, просто мы ещё не поняли этого. Сектант.
>уровень знаний
>в любой непонятной ситуации lm(y~x,data=a)
>>2253
Одна из многих монографий в тему http://b-ok.org/book/448591/9b866b Просвещаем темное африканской быдло, прямо на мейлру!
>примеров полно так неси хотя бы один.
Одна из многих монографий в тему http://b-ok.org/book/448591/9b866b Просвещаем темное африканской быдло, прямо на мейлру!
>>2254
Берёшь и копипастишь оттуда сюда пример
Я не собираюсь искать на тысяче страниц то, чего там нет.
Пока быдло тут только ты.
Берёшь и копипастишь оттуда сюда пример
> как алгоритмически получить из данных точную формулу, породившую их.
Я не собираюсь искать на тысяче страниц то, чего там нет.
>применяет демагогию
>называет кого-то быдлом
Пока быдло тут только ты.
>>1361 (OP)
Конструктивизм — computer science. Computer science не математика.
Конструктивизм — computer science. Computer science не математика.
>>2265
благодаря соответствию карри-говарда можно сказать, что математика — 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)
>>2282 (Del)
мимокрок: Давайте переведём разговор в конструктивное русло.
Мне кажется, что Lean - это продукт без бущущего, поддерживаемый исключительно Майкрософтовским пиаром.
Coq же - нечто интересное, но адекватно и продуктивно применимое только после получения кандидатской по математике...
мимокрок: Давайте переведём разговор в конструктивное русло.
Мне кажется, что Lean - это продукт без бущущего, поддерживаемый исключительно Майкрософтовским пиаром.
Coq же - нечто интересное, но адекватно и продуктивно применимое только после получения кандидатской по математике...
>>2283
Лично я учу lean, потому что в его изучение проще заход, он написан на плюсах которые, в отличие от окамла, я знаю и кодобаза достаточно компактна и организована чтобы лазить по исходникам когда хочется понять как всё устроено, плюс мне неважна дропнутая поддержка HoTT
А будущее его лично мне пофигу
Лично я учу lean, потому что в его изучение проще заход, он написан на плюсах которые, в отличие от окамла, я знаю и кодобаза достаточно компактна и организована чтобы лазить по исходникам когда хочется понять как всё устроено, плюс мне неважна дропнутая поддержка HoTT
А будущее его лично мне пофигу
>>2274
додумался до менее ебанутого решения
lemma Ex₂ {p : Prop} : ¬(p ↔ ¬p) :=
λ (h : p ↔ p → false),
let hp := h.mpr (λ hpₗ, h.mp hpₗ hpₗ)
in h.mp hp hp
всем спасибо
додумался до менее ебанутого решения
lemma Ex₂ {p : Prop} : ¬(p ↔ ¬p) :=
λ (h : p ↔ p → false),
let hp := h.mpr (λ hpₗ, h.mp hpₗ hpₗ)
in h.mp hp hp
всем спасибо
>>2285
Справедливое утверждение. Написание на С существенно облегчает понимание. Вы всё правильно делаете, я в ближайшие пару месяцев тоже вкачусь.
Справедливое утверждение. Написание на С существенно облегчает понимание. Вы всё правильно делаете, я в ближайшие пару месяцев тоже вкачусь.
Чет нашел какой-то вероятностный метод и википедия дает прямо в определении, что это неконструктивный метод доказательства. И че?
>>2481
Нет.
Нет.
>>2481
Конструктивная математика - это конченная математика.
Конструктивная математика - это конченная математика.
>>2496
Очевидно с помощью Сuсk.
Очевидно с помощью Сuсk.
552 Кб, 770x522Пони маете, ваша проблема в том, что вы не видите полной картины. Вы даже внятно не сможете объяснить зачем вообще нужны основания и аксиоматика и для чего там исчисление предикатов, например. С конструктивными основаниями в этом смысле все для вас еще хуже, все эти изоморфизмы карри'говарда, ВНК интерпретации, вычислимость, суждения, натуральная дедукция итд итп сами по себе требуют неких усилий для понимания, но еще хуже, что даже если отдаленное понимание присутствует, то все эти вещи не складываются в целую картинку, тому що мозгов у вас як у хлебушка где все естественно вытекает одно из другого, как итог, конструктивная математика, а уж тем более MLTT для вас выглядит как какая'то лютая оккультная ебулда, бессмысленная и беспощадная, хотя по факту все там просто и понятно.
>>2514
Только если ты совсем отбитый.
>все эти изоморфизмы карри'говарда, ВНК интерпретации, вычислимость, суждения, натуральная дедукция итд итп сами по себе требуют неких усилий для понимания
Только если ты совсем отбитый.
>>2554
Запрограммировать то можно, но я в любом случае сомневаюсь в их существовании.
Запрограммировать то можно, но я в любом случае сомневаюсь в их существовании.
1,7 Мб, webm,450x360, 0:18
>>1361 (OP)
Конструктивисто-петух опять разгулялся. Не видел его с 2012-го года - с тредов про китайца.
Конструктивисто-петух опять разгулялся. Не видел его с 2012-го года - с тредов про китайца.
>>2889
Про что несет. Я про интуиционизм и конструктивную математику узнал в августе 2016го.
>с 2012-го года
Про что несет. Я про интуиционизм и конструктивную математику узнал в августе 2016го.
>>2903
Прочитал у Максимки статью про MLTT, заинтересовало, почитал Мартин-Лёфа и с удивлением обнаружил, что нихуя не понимаю, о чем вообще речь, хотя изложено стройно и логично. Более пристально взглянув на эту тему, понял что причина в том, что за MLTT стоит нечто мне неведомое, из принципов чего и исходит Мартин-Лёф. Это и оказалось конструктивной математикой. Ну а там на каком-то этапе нагуглил Брауэра и понеслось.
Прочитал у Максимки статью про MLTT, заинтересовало, почитал Мартин-Лёфа и с удивлением обнаружил, что нихуя не понимаю, о чем вообще речь, хотя изложено стройно и логично. Более пристально взглянув на эту тему, понял что причина в том, что за MLTT стоит нечто мне неведомое, из принципов чего и исходит Мартин-Лёф. Это и оказалось конструктивной математикой. Ну а там на каком-то этапе нагуглил Брауэра и понеслось.
Отрицание бесконечности и конструктивный подход гут. Отрицание закона исключённого третьего бэд. Есть ли где-то система оснований с первым без второго?
>>2910
О какой системе идёт речь?
>Отрицание бесконечности
>Отрицание закона исключённого третьего бэд.
О какой системе идёт речь?
>>2902
Вернее 2013-го.
http://arhivach.org/thread/5822/
Он здесь уже забивал последний гвоздь в крышку гроба формализма. Потом последовала череда подобных тредов, навроде теперешних, а затем он пропал.
Вернее 2013-го.
http://arhivach.org/thread/5822/
Он здесь уже забивал последний гвоздь в крышку гроба формализма. Потом последовала череда подобных тредов, навроде теперешних, а затем он пропал.
>>2913
Не знаю конструктивных оснований в которых отрицается исключённое третье. Недоказуемость и отрицание это разные вещи.
¬¬(P ∨ ¬ P) теорема в большинстве "видов" конструктивной математики.
Не знаю конструктивных оснований в которых отрицается исключённое третье. Недоказуемость и отрицание это разные вещи.
¬¬(P ∨ ¬ P) теорема в большинстве "видов" конструктивной математики.
212 Кб, 400x321>>2910
Ультрафинитизм Пахома Есенина-Вольпина ж. Поскольку все там конечно, исключенное третье доказывается напрямую простым перебором.
Ультрафинитизм Пахома Есенина-Вольпина ж. Поскольку все там конечно, исключенное третье доказывается напрямую простым перебором.
Сделайте что-то вроде "конструктивизм и конструктивные доказательства интерактивно и в
картинках для школьников".
картинках для школьников".
>>2925
Зачем для школьников, если скоро людям в математике вообще места не будет? Сделают поисковик по доказанным компом теоремам, только нужно будет научиться запросы правильные формировать и вся "человеческая" математика будет прикладной.
Зачем для школьников, если скоро людям в математике вообще места не будет? Сделают поисковик по доказанным компом теоремам, только нужно будет научиться запросы правильные формировать и вся "человеческая" математика будет прикладной.
>>2916
Хотите смешную шутку? Приготовились? В ультрафинитизме все конечные! Ахаха!
Хотите смешную шутку? Приготовились? В ультрафинитизме все конечные! Ахаха!
>>2925
Для школьников смысла нет, в картинках тем более. Если не лезть в философскую сторону вопроса, во что тут все равно никто не может, то самый простой путь - осваивать кок. Возможно, самый простой учебник по коку - software foundations Пирса https://softwarefoundations.cis.upenn.edu/current/index.html
>"конструктивизм и конструктивные доказательства интерактивно и в картинках для школьников"
Для школьников смысла нет, в картинках тем более. Если не лезть в философскую сторону вопроса, во что тут все равно никто не может, то самый простой путь - осваивать кок. Возможно, самый простой учебник по коку - software foundations Пирса https://softwarefoundations.cis.upenn.edu/current/index.html
>>2988
Чем получше? Там с одной установкой пердолинга не оберешься https://hackage.haskell.org/package/Agda-2.5.2/readme + я не знаю внятных IDE под нее, емакс тот еще аутизм от аутистов для аутистов, как ни крути. Кок хотя бы в установке и использовании не сложнее блокнота.
Чем получше? Там с одной установкой пердолинга не оберешься https://hackage.haskell.org/package/Agda-2.5.2/readme + я не знаю внятных IDE под нее, емакс тот еще аутизм от аутистов для аутистов, как ни крути. Кок хотя бы в установке и использовании не сложнее блокнота.
Конструктивист - это умственно отсталый человек, для которого из истинности А не следует ложность не-А. О чём вы тут спорите с умственно отсталыми 4 треда подряд?
>>3435
Если бы ты не был конченным, ты бы очень быстро понял, что это доказывается тривиально.
>для которого из истинности А не следует ложность не-А
Если бы ты не был конченным, ты бы очень быстро понял, что это доказывается тривиально.
>>3436
Да мне похуй что ты там можешь доказать, бумага всё стерпит. Другое дело, что в реальности А либо истина, либо ложь, но даунам не достаточно доказательства того что А - истинна для того чтобы убедится что не-А - ложь, им нужно всё доказывать дважды, как будто бывает третье состояние когда А и истинна и ложь одновременно блять.
(Автор этого поста был забанен. Помянем.)
Да мне похуй что ты там можешь доказать, бумага всё стерпит. Другое дело, что в реальности А либо истина, либо ложь, но даунам не достаточно доказательства того что А - истинна для того чтобы убедится что не-А - ложь, им нужно всё доказывать дважды, как будто бывает третье состояние когда А и истинна и ложь одновременно блять.
(Автор этого поста был забанен. Помянем.)
>>3451
Что ты несёшь, ебанутый?
P => ¬¬P теорема даже в минимальной логике.
¬¬(P ∨ ¬P) теорема в конструктивной логике.
>но даунам не достаточно доказательства того что А - истинна для того чтобы убедится что не-А - ложь
Что ты несёшь, ебанутый?
P => ¬¬P теорема даже в минимальной логике.
>как будто бывает третье состояние когда А и истинна и ложь одновременно блять
¬¬(P ∨ ¬P) теорема в конструктивной логике.
>>3452
Я тебя не так прочитал, ты оказывается ещё более тупой чем я думал.
Это ничего общего с исключённым третьим не имеет, ¬ (P ∧ ¬ P) спокойно доказывается в конструктивных основаниях.
>состояние когда А и истинна и ложь одновременно блять
Я тебя не так прочитал, ты оказывается ещё более тупой чем я думал.
Это ничего общего с исключённым третьим не имеет, ¬ (P ∧ ¬ P) спокойно доказывается в конструктивных основаниях.
Как искать в поисковике теорем?
Шел уже десятый тред, если считать со /сци, а кое-кто так до сих пор и не понял, что конструктивное доказательство - это построение, а построение - это конструктивное доказательство. И кроме как их построений конструктивным доказательствам взяться неоткуда, а в особенности из каких-то априорных аксиом, в которые нужно веровать вместо собственно процесса построения или задания правил для построения, если уж касаться потенциальной осуществимости или lazy evaluation. Как так могло случиться, что в 21 веке кому-то греет попу необъодимость непосредственно доказать хотя бы один дизъюнкт для доказательства истинности дизъюнкции? Откуда такие хуйлопаны вообще берутся? Я не понимаю.
>>3515
О чём ты? Не понимаю твой пост, извини.
О чём ты? Не понимаю твой пост, извини.
>>3515
Я вот понял, например. Меня больше интересует вопрос удобства реального использования. С этим, как я понимаю, пока довольно печально.
Я вот понял, например. Меня больше интересует вопрос удобства реального использования. С этим, как я понимаю, пока довольно печально.
82 Кб, 720x990>>3518
Потому что у большинства "врети" случилось еще во времена работ Поста, Тьюринга и Черча, который все это подытожил, написав, что найдены границы математических способностей человека. Хотя так и оказалось, и выше вычислимости все равно не прыгнешь, верунов и сейчас полно. Благо, прогресс не стоит на месте, и хотя реальной математикой занимаются единицы типа Мартин-Лёфа и Воеводского, уже сейчас видно, что все идет к полной автоматизации математики.
>интересует вопрос удобства реального использования. С этим, как я понимаю, пока довольно печально.
Потому что у большинства "врети" случилось еще во времена работ Поста, Тьюринга и Черча, который все это подытожил, написав, что найдены границы математических способностей человека. Хотя так и оказалось, и выше вычислимости все равно не прыгнешь, верунов и сейчас полно. Благо, прогресс не стоит на месте, и хотя реальной математикой занимаются единицы типа Мартин-Лёфа и Воеводского, уже сейчас видно, что все идет к полной автоматизации математики.
>>3519
Ну, в восьмидесятых тоже все бодренько так шло к полной автоматизации вообще любой интеллектуальной деятельности - чем все закончилось мы знаем. Так что я бы не был столь оптимистичен на твоем месте.
Ну, в восьмидесятых тоже все бодренько так шло к полной автоматизации вообще любой интеллектуальной деятельности - чем все закончилось мы знаем. Так что я бы не был столь оптимистичен на твоем месте.
>>3520
Ты о чем?
>восьмидесятых тоже все бодренько так шло к полной автоматизации вообще любой интеллектуальной деятельности - чем все закончилось мы знаем.
Ты о чем?
>>3522
Для этого даже сейчас техническое развитие никакое, какие уж тут 80-е.
Для этого даже сейчас техническое развитие никакое, какие уж тут 80-е.
>>3530
Под верунами я подразумеваю верующих в то, что математика не равнообъемна вычислимости и существует математика, к вычислимости не сводящаяся (точнее, верующих в то, что нечто, не сводимое к вычислимости, вообще можно называть математикой). Под вычислимостью подразумевается вычислимость на машине тьюринга и др. равнообъемным уточнениям понятия алгоритма (лямбда-определимость, нормальный алгорифм Маркова и т.д.).
Под верунами я подразумеваю верующих в то, что математика не равнообъемна вычислимости и существует математика, к вычислимости не сводящаяся (точнее, верующих в то, что нечто, не сводимое к вычислимости, вообще можно называть математикой). Под вычислимостью подразумевается вычислимость на машине тьюринга и др. равнообъемным уточнениям понятия алгоритма (лямбда-определимость, нормальный алгорифм Маркова и т.д.).
>>3533
Почему подмножество математики не имеет отношения к математике?
>к математике отношение не имеет
Почему подмножество математики не имеет отношения к математике?
>>3533
Ты сам не осилил даже пояснить, зачем те скрины притащил.
Ты ж сам писал, что в математике не понимаешь, что и так заметно, сейчас бы еще принимать во внимание непойми кого с мейлру, который непонятно с какого диагноза решил, что может опровергнуть Черча с Тьюрингом.
>Ты даже того же Энгелькинга не осилил
Ты сам не осилил даже пояснить, зачем те скрины притащил.
>Это не математика, а комьютер саенс, и к математике отношение не имеет.
Ты ж сам писал, что в математике не понимаешь, что и так заметно, сейчас бы еще принимать во внимание непойми кого с мейлру, который непонятно с какого диагноза решил, что может опровергнуть Черча с Тьюрингом.
>>3535
Никто не спорит с Чёрчем и Тьюрингом. Чёрч и Тьюринг не сводили всю математику к вычислимости.
Никто не спорит с Чёрчем и Тьюрингом. Чёрч и Тьюринг не сводили всю математику к вычислимости.
>>3535
Ты говорил, что никто не пользуется мощностями больше, чес счетно. На тех скринах было показано использование таких мощностей, хватит троллить тупостью.
>Ты сам не осилил даже пояснить, зачем те скрины притащил.
Ты говорил, что никто не пользуется мощностями больше, чес счетно. На тех скринах было показано использование таких мощностей, хватит троллить тупостью.
>>3537
Ты никак не сможешь воспользоваться тем, что несчетно. Но ты всегда можешь написать значок бесконечности, алеф0,1,...,1488 и т.д. и думать, что пользуешься. Хотя по факту пользуешься значками, не несущими в себе ничего, т.к. содержимое, которое за ними предполагается, нельзя ни во что вычислить. Это и есть религия натуральная, поскольку у них там тоже есть значки, символ Аллаха, например. Суть примерно одна.
Ты никак не сможешь воспользоваться тем, что несчетно. Но ты всегда можешь написать значок бесконечности, алеф0,1,...,1488 и т.д. и думать, что пользуешься. Хотя по факту пользуешься значками, не несущими в себе ничего, т.к. содержимое, которое за ними предполагается, нельзя ни во что вычислить. Это и есть религия натуральная, поскольку у них там тоже есть значки, символ Аллаха, например. Суть примерно одна.
>>3540
Опять сотый раз по кругу обсуждать одно и то же не вижу смысла. Вещественные числа обсуждали, более того, Тьюринг в своей работе "On computable numbers" машину Тьюринга представлял как имитацию действий человека, вычисляющего такие числа. Отсюда проблема останова, бла-бла и т.д., что уже сто раз обсуждалось.
Опять сотый раз по кругу обсуждать одно и то же не вижу смысла. Вещественные числа обсуждали, более того, Тьюринг в своей работе "On computable numbers" машину Тьюринга представлял как имитацию действий человека, вычисляющего такие числа. Отсюда проблема останова, бла-бла и т.д., что уже сто раз обсуждалось.
>>3542
Множество всех существующих вещественных чисел. То есть множество всех чисел, которые ты когда-либо использовал.
Множество всех существующих вещественных чисел. То есть множество всех чисел, которые ты когда-либо использовал.
>>3544
Я уже сто раз говорил, что нет. Нет, нет, оно несчетно, т.к. это мощность континуума, а еще Брауэр показал, почему континуум невычислим. Итд итп.. Скушно, короче.
Я уже сто раз говорил, что нет. Нет, нет, оно несчетно, т.к. это мощность континуума, а еще Брауэр показал, почему континуум невычислим. Итд итп.. Скушно, короче.
>>3548
А как же действительные числа?
>нет, оно несчетно
>Ты никак не сможешь воспользоваться тем, что несчетно
А как же действительные числа?
>>3549
Ты пользуешься числом с конечным количеством знаков после запятой. И это уже сто раз обсуждалось.
Ты пользуешься числом с конечным количеством знаков после запятой. И это уже сто раз обсуждалось.
>>3548
Я тут недавно читаю это треды. Похоже, что они реально ебанутые или необучаемые.
Я тут недавно читаю это треды. Похоже, что они реально ебанутые или необучаемые.
>>3553
Ну так я о том же не первый тред толкую. В случае вещественных чисел речь может идти только об аппроксимации его конечным количеством знаков после запятой.
Ну так я о том же не первый тред толкую. В случае вещественных чисел речь может идти только об аппроксимации его конечным количеством знаков после запятой.
>>3554
pi,e например. Вычислены только до какого-то знака, приблизительно значит.
pi,e например. Вычислены только до какого-то знака, приблизительно значит.
>>3555
Только когда нам нужно вычислить результат. Мы вполне можем работать с тем же pi или e чисто алгебраически. И это уже будет точное значение.
Только когда нам нужно вычислить результат. Мы вполне можем работать с тем же pi или e чисто алгебраически. И это уже будет точное значение.
>>3551
Ты им не пользуешься, а рисуешь его значок. Попытка воспользоваться приведет к бесконечному процессу вычисления.
Ты им не пользуешься, а рисуешь его значок. Попытка воспользоваться приведет к бесконечному процессу вычисления.
>>3558
Попытка вычисления приведёт к бесконечному процессу рисования значков, что дальше? Пользоваться одним экономнее.
Попытка вычисления приведёт к бесконечному процессу рисования значков, что дальше? Пользоваться одним экономнее.
>>3539
А скрины с Энгелькинга? Раз ими никто не пользуется, то почему практически в каждом учебнике анализа вводят множество R, мощность которого больше, чем Q.
Вопрос в том, что считать существующим. Почему, если множества вещественных чисел счетно, об этом не говорят в тех же учебниках матана, но вводят в заблуждение, говоря, что есть и другие мощности?
>>3558
И в чем проблема в бесконечном процессе вычисления?
>Ты никак не сможешь воспользоваться тем, что несчетно.
А скрины с Энгелькинга? Раз ими никто не пользуется, то почему практически в каждом учебнике анализа вводят множество R, мощность которого больше, чем Q.
>Это и есть религия натуральная, поскольку у них там тоже есть значки, символ Аллаха, например. Суть примерно одна.
Вопрос в том, что считать существующим. Почему, если множества вещественных чисел счетно, об этом не говорят в тех же учебниках матана, но вводят в заблуждение, говоря, что есть и другие мощности?
>>3558
И в чем проблема в бесконечном процессе вычисления?
>>3557
Естественно. Когда результат не нужон, можно и Аллахов подсчитывать.
>>3559
Вот только это не пользование, а вера в пользование. Потому что настоящее пользование - это вычисление. И опять же, все это я уже не помню сколько раз писал.
>Только когда нам нужно вычислить результат
Естественно. Когда результат не нужон, можно и Аллахов подсчитывать.
>>3559
>Пользоваться одним экономнее.
Вот только это не пользование, а вера в пользование. Потому что настоящее пользование - это вычисление. И опять же, все это я уже не помню сколько раз писал.
>>3561
ТЫСКОЗАЛ? Вот это как раз сектанство. Напиши ты pi или 3,141592653589793238462643 что принципиально поменяется?
>Потому что настоящее пользование - это вычисление
ТЫСКОЗАЛ? Вот это как раз сектанство. Напиши ты pi или 3,141592653589793238462643 что принципиально поменяется?
>>3563
Причём заметь первое абсолютно точное значение, а второе лишь аппроксимация.
Причём заметь первое абсолютно точное значение, а второе лишь аппроксимация.
>>3564
А оно должно закончится?
>В том, что оно не закончится никогда и сл-но, не может считаться вычислимостью.
А оно должно закончится?
>>3563
Сто раз писал, что. Даже в этом треде. Вы ж читать не умеете, какая вам математика.
>Напиши ты pi или 3,141592653589793238462643 что принципиально поменяется?
Сто раз писал, что. Даже в этом треде. Вы ж читать не умеете, какая вам математика.
>>3564
Ну например с рациональными числами там всегда будет период, да, будет повторяться бесконечно, но детерминированно, что плохого то?
>В том, что оно не закончится никогда
Ну например с рациональными числами там всегда будет период, да, будет повторяться бесконечно, но детерминированно, что плохого то?
>>3564
Я сам не уверен что верую, просто интересуюсь.
Я сам не уверен что верую, просто интересуюсь.
>>3567
Я по твоему должен все твои посты перечитывать?
Я по твоему должен все твои посты перечитывать?
>>3573
Вычислимость - это вычислимость, а не вера. Вычислимое можно вычислить, в невычислимое можно только веровать.
Вычислимость - это вычислимость, а не вера. Вычислимое можно вычислить, в невычислимое можно только веровать.
>>3574
"Математикопоклонничество" пусть будет. Поклоняетесь значкам без фактического содержания.
"Математикопоклонничество" пусть будет. Поклоняетесь значкам без фактического содержания.
>>3575
Вычисление может производиться по самым разным правилам. Вера в одно конкретное не делает его чем-то особенным. А вот связи между объектами остаются всегда, неважно, как ты их запишешь.
Вычисление может производиться по самым разным правилам. Вера в одно конкретное не делает его чем-то особенным. А вот связи между объектами остаются всегда, неважно, как ты их запишешь.
>>3576
Скорее это ты поклоняешься значкам, забивая на смысл, который они несут. Мельница-вычислитель перемалывает циферки, уаааууу.
>Поклоняетесь значкам без фактического содержания.
Скорее это ты поклоняешься значкам, забивая на смысл, который они несут. Мельница-вычислитель перемалывает циферки, уаааууу.
>>3581
Пример с вещественными числами разобрали буквально десяток постов назад. У тебя ж память как у хлебушка.
Пример с вещественными числами разобрали буквально десяток постов назад. У тебя ж память как у хлебушка.
>>3576
Ты так и не ответил на вопрос
Ты так и не ответил на вопрос
>Ты никак не сможешь воспользоваться тем, что несчетно.
>А скрины с Энгелькинга? Раз ими никто не пользуется, то почему практически в каждом учебнике анализа вводят множество R, мощность которого больше, чем Q.
>>3589
В чём? Ты будешь спорить, что вычисления это правила перемалывания значков?
>Вот в том и проблема
В чём? Ты будешь спорить, что вычисления это правила перемалывания значков?
>>3590
Обсуждалось в последнем десятке-другом постов. Вы просто эталон необучаемости, я думал, что необучаемее хохлозависимых в крымтреде не бывает, а вот нашел.
Обсуждалось в последнем десятке-другом постов. Вы просто эталон необучаемости, я думал, что необучаемее хохлозависимых в крымтреде не бывает, а вот нашел.
>>3593
Так ты ещё и /по/рашник, лол. Ну так давай ссылку или проследуй нахуй. Нихуя ты не ответил, я следил, спустил на тормозах свой обосрамс, думая, что никто не заметит.
Так ты ещё и /по/рашник, лол. Ну так давай ссылку или проследуй нахуй. Нихуя ты не ответил, я следил, спустил на тормозах свой обосрамс, думая, что никто не заметит.
>>3596
Сто раз писалось про канонические и неканонические элементы и выражения и т.д. Мне реально лениво каждую сотню постов переписывать все, мною уже сто раз писанное. Ну необучаемые вы тута, бывает. Для мейлру это норма, как и для рашки в целом.
Сто раз писалось про канонические и неканонические элементы и выражения и т.д. Мне реально лениво каждую сотню постов переписывать все, мною уже сто раз писанное. Ну необучаемые вы тута, бывает. Для мейлру это норма, как и для рашки в целом.
>>3597
Ты можешь один раз написать, заскринить, а после кидать скрины со своим ответом. Ты просто тупой и троллишь тупостью.
Ты можешь один раз написать, заскринить, а после кидать скрины со своим ответом. Ты просто тупой и троллишь тупостью.
Я писал даже, в чем тут проблема у большинства >>2514 вы никогда ничего не поймете, поскольку либо ничего для этого не делаете, либо делаете, но тема не ваша.
>>3600
Он троллит тупостью неосознано, как ребёнок, нагадивший в штаны, и радующейся, что прохожие шарахаются от него из-за вони.
Он троллит тупостью неосознано, как ребёнок, нагадивший в штаны, и радующейся, что прохожие шарахаются от него из-за вони.
>>3601
Просто тут 3.5 математика на всю борду, да и те на первом курсе мухгу обучаются.
Просто тут 3.5 математика на всю борду, да и те на первом курсе мухгу обучаются.
>>3602
Нет, осознанно. Если неосознанно, значит просто тупой. Третьего не дано. Нельзя быть тупым и троллить тупостью одновременно.
Нет, осознанно. Если неосознанно, значит просто тупой. Третьего не дано. Нельзя быть тупым и троллить тупостью одновременно.
>>3606
Лол.
Лол.
Какие есть основания где можно доказать, что аксиома Аллаха (выбора) не верна?
>>3614
Тогда у тебя нет оснований для беспокойства.
Тогда у тебя нет оснований для беспокойства.
>>3628
Рамануджан очень кстати. Заниматься математикой без математического образования и культуры, не имея понятия о формализме как о методе вообще, можно только одним способом - манипуляцией с ментальными построениями.
Рамануджан очень кстати. Заниматься математикой без математического образования и культуры, не имея понятия о формализме как о методе вообще, можно только одним способом - манипуляцией с ментальными построениями.
>>3629
Есть книжка, мол, как стать как Сринивас из позиций конструктивной математики? Да и вообще "конструктивная математика и психология", "конструктивная математика и сознание", "конструктивная математика и эмоции" да прочее?
Есть книжка, мол, как стать как Сринивас из позиций конструктивной математики? Да и вообще "конструктивная математика и психология", "конструктивная математика и сознание", "конструктивная математика и эмоции" да прочее?
>>1361 (OP)
Слышал про HoTT, разобрался в нём. Он, вроде какой-то в прямом смысле недоделанный.
В чём его проблема? (Пишите смело факты)
Вроде есть какая-то недоказанная гипотеза. Что она за зверь?
Слышал про HoTT, разобрался в нём. Он, вроде какой-то в прямом смысле недоделанный.
В чём его проблема? (Пишите смело факты)
Вроде есть какая-то недоказанная гипотеза. Что она за зверь?
>>3706
>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.
>>3637
Он же с детства свои умения развивал. Вся его жизнь как одно доказательство тезиса Черча. А вообще, http://gen.lib.rus.ec/book/index.php?md5=74ED3244789E3A66301750212342D470 1ая глава.
>>3706
Я в ней не разбирался, как по мне - какая-то странная надстройка над MLTT.
>как стать как Сринивас
Он же с детства свои умения развивал. Вся его жизнь как одно доказательство тезиса Черча. А вообще, http://gen.lib.rus.ec/book/index.php?md5=74ED3244789E3A66301750212342D470 1ая глава.
>>3706
> HoTT,
Я в ней не разбирался, как по мне - какая-то странная надстройка над MLTT.
>>3712
Ух, прояснил, спасибо.
Единственное, что непонятно : "Computational interpretation of homotopy type theory is an open problem."
Что это такое, "вычислительная интерпретация"?
Есть более простые примеры, показывающие суть понятия?
Ух, прояснил, спасибо.
Единственное, что непонятно : "Computational interpretation of homotopy type theory is an open problem."
Что это такое, "вычислительная интерпретация"?
Есть более простые примеры, показывающие суть понятия?
>>3730
Ну так все ж треды об этом. Суть конструктивной математики в том, что она вычислима. Что-то у них с этими гомотопиями пока не вычисляется, причем там жи и написано, что именно:
Полностью конструктивной модели пока нет.
Машина Тьюринга.
>Единственное, что непонятно : "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.
Полностью конструктивной модели пока нет.
>Есть более простые примеры, показывающие суть понятия?
Машина Тьюринга.
>>3731
А где конкретно в тексте аксиома выбора существенно используется? Про это что-нибудь знаете?
А где конкретно в тексте аксиома выбора существенно используется? Про это что-нибудь знаете?
Что можно почитать в качестве введения в формальную теорию типов? С "неформальной" уже более менее знаком.
>>3928
Конкретнее не знаю, я НоТТ не читал.
>>3979
Барендрехт, не? http://ttic.uchicago.edu/~dreyer/course/papers/barendregt.pdf
Конкретнее не знаю, я НоТТ не читал.
>>3979
Барендрехт, не? http://ttic.uchicago.edu/~dreyer/course/papers/barendregt.pdf
Аноны, поясните за вычислимость утверждений формальной теории. Вот есть некая аксиоматическая теория и есть некое утверждение. Можно ли вычислить истино оно или ложно?
Но ведь проект компьютеров пятого поколения не удался.
23 Кб, 712x254>>4026
Ты путаешь вычислимость и выводимость в формальной системе. Второе вообще никак не подразумевает первого. Возьмем например истинность формулы в исчислении пропозишенов. Поскольку классически, по закону исключенного третьего, пропозишен может быть истинный или ложный, то мы можем по методу Тарского нарисовать Аллаха таблицу с этой формулой пикрелейтед, из которой выводима ложность или истинность этой формулы исходя из ложности или истинности входящих в нее пропозишенов. В данном примере, классически эта формула истинна в любом случае. Прикол же в том, что конструктивно (исходя из интерпретации логических констант, в частности, свойств импликации, по Гейтингу) эта формула (известная как формула Пирса) невычислима.
Ты путаешь вычислимость и выводимость в формальной системе. Второе вообще никак не подразумевает первого. Возьмем например истинность формулы в исчислении пропозишенов. Поскольку классически, по закону исключенного третьего, пропозишен может быть истинный или ложный, то мы можем по методу Тарского нарисовать Аллаха таблицу с этой формулой пикрелейтед, из которой выводима ложность или истинность этой формулы исходя из ложности или истинности входящих в нее пропозишенов. В данном примере, классически эта формула истинна в любом случае. Прикол же в том, что конструктивно (исходя из интерпретации логических констант, в частности, свойств импликации, по Гейтингу) эта формула (известная как формула Пирса) невычислима.
>>4057
Формула F выводима, если существует хотя бы одна конечная последовательность формул, в которой последняя формула - это F, а любая предшествующая формула есть либо аксиома, либо получается применением модус поненс. Понятие "выводимость" не зависит от понятий "истинно" и "ложно".
Формула F выводима, если существует хотя бы одна конечная последовательность формул, в которой последняя формула - это F, а любая предшествующая формула есть либо аксиома, либо получается применением модус поненс. Понятие "выводимость" не зависит от понятий "истинно" и "ложно".
>>4062
Ну и? Из выводимости формулы никак не следует ее вычислимость, пример я привел - это формула Пирса.
Ну и? Из выводимости формулы никак не следует ее вычислимость, пример я привел - это формула Пирса.
>>4071
Такая-то самоуверенность.
Как это понимать? При чем тут таблицы истинности? Понятно, что полнота исчисления высказываний и бла-бла-бла. Но речь о выводимости. Ты какие книжки по математической логике читал?
Такая-то самоуверенность.
>пикрелейтед, из которой выводима ложность или истинность
Как это понимать? При чем тут таблицы истинности? Понятно, что полнота исчисления высказываний и бла-бла-бла. Но речь о выводимости. Ты какие книжки по математической логике читал?
>>4054
А вот вы тоже напутали: формула Пирса невыводима в интуиционисткой логике, поскольку существует модель Крипке, где она не истинна.
Вычислимость функции - это про другое: существует такая машина Тьюринга, которая по заданным аргументам некоторой функции за конечное число ходов предъявит значение этой функции.
Так вот иногда доказательством импликации A->B является вычислимая функция f:A-->B, преобразующая доказательство утверждения А в доказательство утверждения B.
В силу неизвестных мне чудес(т.е. изоморфизму Карри-Ховарда) оказалось, что всё, что выведено из интуиционистских аксиом - может быть собрано из таких вычислимых функций.
То есть уже не надо заново строить машины Тьюринга - просто бери и пользуйся интуиционисткой логикой как конструктором. Оттуда и "конструктивизм", он же - "интуиционизм".
Невычислимо же - доказательство формулы Пирса, если его воспринимать как функцию.
---------------
Я это всё написал, но мне хотелось бы дополнительного контроля - всё же верно я рассказал?
А вот вы тоже напутали: формула Пирса невыводима в интуиционисткой логике, поскольку существует модель Крипке, где она не истинна.
Вычислимость функции - это про другое: существует такая машина Тьюринга, которая по заданным аргументам некоторой функции за конечное число ходов предъявит значение этой функции.
Так вот иногда доказательством импликации A->B является вычислимая функция f:A-->B, преобразующая доказательство утверждения А в доказательство утверждения B.
В силу неизвестных мне чудес(т.е. изоморфизму Карри-Ховарда) оказалось, что всё, что выведено из интуиционистских аксиом - может быть собрано из таких вычислимых функций.
То есть уже не надо заново строить машины Тьюринга - просто бери и пользуйся интуиционисткой логикой как конструктором. Оттуда и "конструктивизм", он же - "интуиционизм".
Невычислимо же - доказательство формулы Пирса, если его воспринимать как функцию.
---------------
Я это всё написал, но мне хотелось бы дополнительного контроля - всё же верно я рассказал?
>>4077
И именно в таких случаях мы можем говорить об истинности в конструктивном смысле слова. Поскольку суть конструктивной выводимости - вычислимость. А не общие недоказуемые заявления.
Интерпретация логических констант по Брауэру-Гейтингу-Колмогорову это называется. Конкретно чаще всего речь о конструктивной логике Гейтинга.
>Так вот иногда доказательством импликации A->B является вычислимая функция f:A-->B, преобразующая доказательство утверждения А в доказательство утверждения B.
И именно в таких случаях мы можем говорить об истинности в конструктивном смысле слова. Поскольку суть конструктивной выводимости - вычислимость. А не общие недоказуемые заявления.
>В силу неизвестных мне чудес(т.е. изоморфизму Карри-Ховарда) оказалось, что всё, что выведено из интуиционистских аксиом - может быть собрано из таких вычислимых функций.
Интерпретация логических констант по Брауэру-Гейтингу-Колмогорову это называется. Конкретно чаще всего речь о конструктивной логике Гейтинга.
>>4083
Окей, мы согласны.
Давайте теперь представим, что некая теория легко описывается в классической логике и очень-очень трудно в интуиционисткой.
Зачем нам тогда вычислимый вариант?
Ав едь ещё он может и вообще не существовать... Тогда получается, что отказываясь от веры в одни формальные системы, вы впадаете в другую крайность, веря, что существует именно вычислимая формальная система, подходящая для любых стоящих перед вами задач.
Получается, что на стороне ваших оппонентов - проверенная годами практика, а на вашей стороне - только ваши, демонстрируемые на дваче, идеалы.
Это похоже на мечты, которые разрушил Гёдель, только в новой обложке.
как вам такой вброс?
Окей, мы согласны.
Давайте теперь представим, что некая теория легко описывается в классической логике и очень-очень трудно в интуиционисткой.
Зачем нам тогда вычислимый вариант?
Ав едь ещё он может и вообще не существовать... Тогда получается, что отказываясь от веры в одни формальные системы, вы впадаете в другую крайность, веря, что существует именно вычислимая формальная система, подходящая для любых стоящих перед вами задач.
Получается, что на стороне ваших оппонентов - проверенная годами практика, а на вашей стороне - только ваши, демонстрируемые на дваче, идеалы.
Это похоже на мечты, которые разрушил Гёдель, только в новой обложке.
как вам такой вброс?
55 Кб, 707x919>>4086
Обсуждали уже. Да еще Тьюринг показал, что даже если к его машине приколхозить боженьку, могущего в решение алгоритмически неразрешимых задач, это ничего не решит, т.к. не снимает вопроса о проблеме останова уже прокачанной таким образом машины Тьюринга. Отличие веры от вычислимости тоже сто раз уже обсуждали. Границы математических способностей хоть человека хоть роботов - это вычислимость, как ни крути, выше не прыгнешь. Это тоже с 40-х годов прошлого века известно.
>Тогда получается, что отказываясь от веры в одни формальные системы, вы впадаете в другую крайность, веря, что существует именно вычислимая формальная система, подходящая для любых стоящих перед вами задач.
Обсуждали уже. Да еще Тьюринг показал, что даже если к его машине приколхозить боженьку, могущего в решение алгоритмически неразрешимых задач, это ничего не решит, т.к. не снимает вопроса о проблеме останова уже прокачанной таким образом машины Тьюринга. Отличие веры от вычислимости тоже сто раз уже обсуждали. Границы математических способностей хоть человека хоть роботов - это вычислимость, как ни крути, выше не прыгнешь. Это тоже с 40-х годов прошлого века известно.
>>4087
Эта фраза лишена смысла. Не отличается от фразы "направление лингвистических одаренностей арийцев - это гладиолус".
>Границы математических способностей хоть человека хоть роботов - это вычислимость
Эта фраза лишена смысла. Не отличается от фразы "направление лингвистических одаренностей арийцев - это гладиолус".
>>4115
Давай я тебе объясгю, почему это не так. Вот ты написал в своем посте то, что написал. Но почему ты так написал? Потому что тебе свербит, и обязательно нужно что-то мне ответить? Или потому что ты можешь доказать эти свои слова, например, конкретным примером, начисто опровергающим тезис Черча тут стоит заметить, что сама эта фраза принадлежит как раз Черчу? Я уверен, что опровергнуть тезис Черча ты не можешь, это если предположить, что его опровержение вообще возможно, хотя в настоящее время человечеству ничего такого неизвестно. Тогда о чем твоя батрушка вообще? Не пони маю.
Давай я тебе объясгю, почему это не так. Вот ты написал в своем посте то, что написал. Но почему ты так написал? Потому что тебе свербит, и обязательно нужно что-то мне ответить? Или потому что ты можешь доказать эти свои слова, например, конкретным примером, начисто опровергающим тезис Черча тут стоит заметить, что сама эта фраза принадлежит как раз Черчу? Я уверен, что опровергнуть тезис Черча ты не можешь, это если предположить, что его опровержение вообще возможно, хотя в настоящее время человечеству ничего такого неизвестно. Тогда о чем твоя батрушка вообще? Не пони маю.
>>4090
Во что веруны-то? Вычислимость - это непосредственный конструктивный объект, а не объект веры как всякие не считающиеся ни во что значки алефов и бесконечностей.
>веруны
Во что веруны-то? Вычислимость - это непосредственный конструктивный объект, а не объект веры как всякие не считающиеся ни во что значки алефов и бесконечностей.
>>4120
Будь добр, приведи пример "конструктивного объекта". А то непонятно, что ты под этим подразумеваешь. (Объекты какие-то... Функция - понятно что такое, а объект - уже непонятно)
Будь добр, приведи пример "конструктивного объекта". А то непонятно, что ты под этим подразумеваешь. (Объекты какие-то... Функция - понятно что такое, а объект - уже непонятно)
>>4123
Да я уже и не помню сколько раз приводил. Толку все равно 0.
И что по-твоему есть функция?
>приведи пример "конструктивного объекта"
Да я уже и не помню сколько раз приводил. Толку все равно 0.
>Функция - понятно что такое, а объект - уже непонятно)
И что по-твоему есть функция?
Ещё раз, какую пользу работающему математику проиносит отказ от
1) исключённого третьего,
2) аксиомы выбора.
1) исключённого третьего,
2) аксиомы выбора.
>>4124
Определение функции:
(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 ) )
Определение функции:
(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
>>4124
я понимаю твою усталость, но всё-таки интересно об этом поговорить
я понимаю твою усталость, но всё-таки интересно об этом поговорить
>>4155
Я подозреваю, тебе вообще очень многое непонятно. И не только в математике. Причем тут определенность или неопределенность некоторых утверждений, а тем более их "безумность" не очень ясно. В данной фразе речь о предположительной равнообъемности математики и вычислимости. В пользу такой точки зрения можно привести тезис Черча. Говоря проще, до тех пор пока не получены примеры, опровергающие этот тезис, упомянутое утверждение можно считать истинным. На настоящий момент любой пример, известный человечеству подтверждает тезис Черча. Так что со своим школоцентризмом, основанным на твоем школомнении обо всем на свете, дул бы ты в школку, а не лез в вопросы, до которых тебе сильно дальше чем до луны пешком.
>"границы математических способностей" - это вообще непонятно что такое.
Я подозреваю, тебе вообще очень многое непонятно. И не только в математике. Причем тут определенность или неопределенность некоторых утверждений, а тем более их "безумность" не очень ясно. В данной фразе речь о предположительной равнообъемности математики и вычислимости. В пользу такой точки зрения можно привести тезис Черча. Говоря проще, до тех пор пока не получены примеры, опровергающие этот тезис, упомянутое утверждение можно считать истинным. На настоящий момент любой пример, известный человечеству подтверждает тезис Черча. Так что со своим школоцентризмом, основанным на твоем школомнении обо всем на свете, дул бы ты в школку, а не лез в вопросы, до которых тебе сильно дальше чем до луны пешком.
>>1361 (OP)
Вычислимость - это действительно очень интересная тема.
Будем надеяться, что местный её фанат направит большую часть своей энергии в продуктивное русло вроде обсуждения с высокой строгостью необходимых теорем.
Если предлагать тему, то вопрос:"чем надозаниматься?" Где открыт фронт работ, доступный для студентоты с двачей?
Вычислимость - это действительно очень интересная тема.
Будем надеяться, что местный её фанат направит большую часть своей энергии в продуктивное русло вроде обсуждения с высокой строгостью необходимых теорем.
Если предлагать тему, то вопрос:"чем надозаниматься?" Где открыт фронт работ, доступный для студентоты с двачей?
>>4424
Пробовал, не заходит. Закатывания глаз и кукареканья бесноватых начинаются примерно на фразе "изоморфизм Карри-Говарда". А без этого уже не объяснить, почему лямбдаР (AUTOMATH де Брауна, например) это то же самое, что исчисление предикатов. Про что-то более сложное (Кок тот же) и говорить нечего.
>Будем надеяться, что местный её фанат направит большую часть своей энергии в продуктивное русло вроде обсуждения с высокой строгостью необходимых теорем.
Пробовал, не заходит. Закатывания глаз и кукареканья бесноватых начинаются примерно на фразе "изоморфизм Карри-Говарда". А без этого уже не объяснить, почему лямбдаР (AUTOMATH де Брауна, например) это то же самое, что исчисление предикатов. Про что-то более сложное (Кок тот же) и говорить нечего.
>>1602
Гармонический ряд обоссывает эту логику.
>Просто пренебрегаем последним членом
>И, чем больше n, тем смелее можно пренебречь последним членом суммы.
Гармонический ряд обоссывает эту логику.
>>2030
Вот в чём твоя проблема. Ты приравниваешь синтаксические конструкции к смысловым, и из этого выводишь, будто твой конструктивизм чем-то отличается от формализма. Проснись, ты обосрался!
>Проблема только в том, что за всем этим стоит не пустой синтаксис ни о чем, как в формализме, а вычислимая конструктивная математика, где даже понятие равенства имеет вычислительное содержание.
Вот в чём твоя проблема. Ты приравниваешь синтаксические конструкции к смысловым, и из этого выводишь, будто твой конструктивизм чем-то отличается от формализма. Проснись, ты обосрался!
>>2079
Ты с ума сошёл? Зачем каждый раз заново выводить всю предшествующую математику, если теорема - это и есть ёбанный квинтиллион знаков, полностью доказанный? Аксиомы-то остались неизменны, зачем каждый раз перепроверять вывод?
>Считающаяся в термы из квинтиллионов знаков. Это проблема, пони маешь? Потому что если мы захотим это на самом деле посчитать, то...
Ты с ума сошёл? Зачем каждый раз заново выводить всю предшествующую математику, если теорема - это и есть ёбанный квинтиллион знаков, полностью доказанный? Аксиомы-то остались неизменны, зачем каждый раз перепроверять вывод?
>>4449
Мне начинают нести такую ахинею, что уши вянут. Вот типичный пример >>4454 какой-то школотрон думает, что опроверг интуиционизм в 2017 году. И что отвечать в таком случае? Я, разумеется, мог бы процитировать Брауэра https://projecteuclid.org/euclid.bams/1183422499 Гейтинга или Маннури по поводу разницы между интуиционизмом и формализмом, а она есть, и существенная. Но кто здесь хотя бы поймет о чем вообще речь? Никто, очевидно же. Тут чуть выше никто так и не въехал в разницу между классической и конструктивной логикой для формулы Пирса какие же вы деграданты, пиздец просто. Как итог, получу еще больше неинтересного мне кукареканья и истерик.
>Тебе задают вопросы, а ты их игнорируешь.
Мне начинают нести такую ахинею, что уши вянут. Вот типичный пример >>4454 какой-то школотрон думает, что опроверг интуиционизм в 2017 году. И что отвечать в таком случае? Я, разумеется, мог бы процитировать Брауэра https://projecteuclid.org/euclid.bams/1183422499 Гейтинга или Маннури по поводу разницы между интуиционизмом и формализмом, а она есть, и существенная. Но кто здесь хотя бы поймет о чем вообще речь? Никто, очевидно же. Тут чуть выше никто так и не въехал в разницу между классической и конструктивной логикой для формулы Пирса какие же вы деграданты, пиздец просто. Как итог, получу еще больше неинтересного мне кукареканья и истерик.
50 Кб, 809x301>>2514
Чтобы не обосраться, как на пике - т.е. всегда применять методы, адекватные данным и задачам. Основания нужны потому что, как показывает практика, обосраться можно даже в элементарных вещах.
>Вы даже внятно не сможете объяснить зачем вообще нужны основания и аксиоматика и для чего там исчисление предикатов, например.
Чтобы не обосраться, как на пике - т.е. всегда применять методы, адекватные данным и задачам. Основания нужны потому что, как показывает практика, обосраться можно даже в элементарных вещах.
>>2550
Существуют объекты, достаточно точно описываемые вещественнозначными функциями вещественного же аргумента.
Существуют объекты, достаточно точно описываемые вещественнозначными функциями вещественного же аргумента.
>>3637
Жак Адамар, "Исследование психологии процесса изобретения в математике"
Жак Адамар, "Исследование психологии процесса изобретения в математике"
>>4456
Всего-навсего другой набор аксиом, вот и всё. Но маняучёным не дают покоя лавры Пуанкаре, Римана и Гильберта, поэтому очень уж хочется сделать что-нибудь "особенное" поэтому они придумывают никому ненужные системы с крайне геморроидальным выводом даже простейших теорем и эпатажно отрицают то, что успешно применяется на практике годами.
>разницы между интуиционизмом и формализмом
Всего-навсего другой набор аксиом, вот и всё. Но маняучёным не дают покоя лавры Пуанкаре, Римана и Гильберта, поэтому очень уж хочется сделать что-нибудь "особенное" поэтому они придумывают никому ненужные системы с крайне геморроидальным выводом даже простейших теорем и эпатажно отрицают то, что успешно применяется на практике годами.
>>4464
Я тебя услышал, ага. А ничего, что у Брауэра вообще аксиом не было? А про логические отрицания ты что знаешь? По Маннури, конструктивное отрицание - это choice negation, отрицание в классической логике - exclusion negation. Из чего следует 4 разновидности только двойного отрицания, из которых только 2 эквивалентны утверждению (двойные choice и exclusion negation). Если их миксануть, интереснее получается. Но логика никому не интересна, проще ж веровать в аксиомы полученные Гильбертом в виде скрижалей на горе сион.
>Всего-навсего другой набор аксиом, вот и всё.
Я тебя услышал, ага. А ничего, что у Брауэра вообще аксиом не было? А про логические отрицания ты что знаешь? По Маннури, конструктивное отрицание - это choice negation, отрицание в классической логике - exclusion negation. Из чего следует 4 разновидности только двойного отрицания, из которых только 2 эквивалентны утверждению (двойные choice и exclusion negation). Если их миксануть, интереснее получается. Но логика никому не интересна, проще ж веровать в аксиомы полученные Гильбертом в виде скрижалей на горе сион.
>>4465
Ты, похоже, плохо представляешь себе, что такое аксиома. Если у Брауэра аксиом не было, то не было и определений. А без определений не о чем и размышлять. То, что в работах этого господина аксиомы присутствуют неявно, без огромной надписи АКСИОМЫ и пронумерованного списка может и рвёт шаблон, но сущности не меняет.
Ты, похоже, плохо представляешь себе, что такое аксиома. Если у Брауэра аксиом не было, то не было и определений. А без определений не о чем и размышлять. То, что в работах этого господина аксиомы присутствуют неявно, без огромной надписи АКСИОМЫ и пронумерованного списка может и рвёт шаблон, но сущности не меняет.
>>4466
И что же это такое? В натуральной дедукции аксиома - это логическое заключение без посылок, т.е. нечто, принимаемое без предшествующего контекста, из которого это нечто можно вывести, т.е. нечто, ниоткуда не выводимое, а принимаемое "как есть". С такой позиции даже в MLTT аксиом нет, т.к. там 4 правила вывода и все они начинаются с контекста. Про Брауэра и говорить нечего, он даже конструктивную логику Гейтинга назвал "любопытным, но бесплодным примером", сам Гейтинг тоже явно оговаривал, почему конструктивная логика не формализует брауэровского интуиционизма.
>Ты, похоже, плохо представляешь себе, что такое аксиома.
И что же это такое? В натуральной дедукции аксиома - это логическое заключение без посылок, т.е. нечто, принимаемое без предшествующего контекста, из которого это нечто можно вывести, т.е. нечто, ниоткуда не выводимое, а принимаемое "как есть". С такой позиции даже в MLTT аксиом нет, т.к. там 4 правила вывода и все они начинаются с контекста. Про Брауэра и говорить нечего, он даже конструктивную логику Гейтинга назвал "любопытным, но бесплодным примером", сам Гейтинг тоже явно оговаривал, почему конструктивная логика не формализует брауэровского интуиционизма.
>>4467
Уже сама эта фраза полностью демаскирует полное незнание тобой терминологии, которой ты так презрительно разбрасываешься. Аксиома - это утверждение о свойствах, элементарная часть определения. Связка аксиом и образует полное определение.
Аксиомы не являются выросшей на пустом месте игрой ума. Они были сформированы с учётом опыта обращения человечества с числами. Они строго очертили неясные до той поры понятия и позволили прежде всего без опасений выводить новые и новые следствия. Они показали границы применимости методов, с их помощью можно всегда ответить на вопрос "А правильно ли я поступаю? Не пытаюсь ли я сложить красное с длинным?" Они позволили, наконец прояснить собственно пути математики, сделав рассуждения кристально прозрачными.
Интуиционизм же является не более, чем оголтелым скептицизмом, который сомневается даже в собственном здравомыслии. И странное дело: интуиционизм яростно отрицает одно и столь же яростно отстаивает другое совершенно не желая признавать за собой место обычной формальной системы.
А контекст-то с чего начинается? А правила на чём основываются?
>это логическое заключение без посылок
>логическое заключение без посылок
Уже сама эта фраза полностью демаскирует полное незнание тобой терминологии, которой ты так презрительно разбрасываешься. Аксиома - это утверждение о свойствах, элементарная часть определения. Связка аксиом и образует полное определение.
>принимаемое без предшествующего контекста
Аксиомы не являются выросшей на пустом месте игрой ума. Они были сформированы с учётом опыта обращения человечества с числами. Они строго очертили неясные до той поры понятия и позволили прежде всего без опасений выводить новые и новые следствия. Они показали границы применимости методов, с их помощью можно всегда ответить на вопрос "А правильно ли я поступаю? Не пытаюсь ли я сложить красное с длинным?" Они позволили, наконец прояснить собственно пути математики, сделав рассуждения кристально прозрачными.
Интуиционизм же является не более, чем оголтелым скептицизмом, который сомневается даже в собственном здравомыслии. И странное дело: интуиционизм яростно отрицает одно и столь же яростно отстаивает другое совершенно не желая признавать за собой место обычной формальной системы.
>там 4 правила вывода и все они начинаются с контекста.
А контекст-то с чего начинается? А правила на чём основываются?
4 Кб, 562x103>>4470
Вообще-то я привел вполне официальное определение аксиомы, пикрелейтед http://www.cs.cornell.edu/courses/cs3110/2013sp/lectures/lec15-logic-contd/lec15.html
Я чуть выше ссылался на статью Брауэра, он там как раз поясняет за необоснованность таких методов, когда нечто, выведенное из конечного априори и бездоказательно обобщается на бесконечное. Как исключенное третье, например.
Требование построения доказательства - это не оголтелый скептицизм, а вполне резонное условие для математики, которая вообще-то является самым точным знанием, известным человечеству. Верования там неуместны вообще никак. И где в интуиционизме сомнения в собственном здравомыслии?
С конструктивных объектов.
На возможных манипуляциях с элементами контекста.
>Уже сама эта фраза полностью демаскирует полное незнание тобой терминологии, которой ты так презрительно разбрасываешься.
Вообще-то я привел вполне официальное определение аксиомы, пикрелейтед http://www.cs.cornell.edu/courses/cs3110/2013sp/lectures/lec15-logic-contd/lec15.html
>Аксиомы не являются выросшей на пустом месте игрой ума. Они были сформированы с учётом опыта обращения человечества с числами. Они строго очертили неясные до той поры понятия и позволили прежде всего без опасений выводить новые и новые следствия. Они показали границы применимости методов, с их помощью можно всегда ответить на вопрос "А правильно ли я поступаю? Не пытаюсь ли я сложить красное с длинным?" Они позволили, наконец прояснить собственно пути математики, сделав рассуждения кристально прозрачными.
Я чуть выше ссылался на статью Брауэра, он там как раз поясняет за необоснованность таких методов, когда нечто, выведенное из конечного априори и бездоказательно обобщается на бесконечное. Как исключенное третье, например.
>Интуиционизм же является не более, чем оголтелым скептицизмом, который сомневается даже в собственном здравомыслии.
Требование построения доказательства - это не оголтелый скептицизм, а вполне резонное условие для математики, которая вообще-то является самым точным знанием, известным человечеству. Верования там неуместны вообще никак. И где в интуиционизме сомнения в собственном здравомыслии?
>А контекст-то с чего начинается?
С конструктивных объектов.
>А правила на чём основываются?
На возможных манипуляциях с элементами контекста.
>>4471
Ты понимаешь что у тебя "логический вывод" из ничего?
Да, некоторые вещи приходиться принимать без доказательств. Правда в том, что если мы вот прям счас откатимся в каменный век интуиционизма и забудем большую часть теорем существования - нам придётся лишиться очень, очень многого. Оно того не стоит.
В "формализме" доказательства строятся настолько замечательно, что их можно проверить исключительно основываясь на синтаксисе.
В том, что интуиционисты начинали с классики. Затем они зачем-то её кастрировали, переформулировали и вуаля - новая теория. Правда, она оказалась не то чтобы очень нужной. Но всё же, новую теорию придумать - это не хухры мухры.
И как же они определяются?
Почему это они возможны?
>Вообще-то я привел вполне официальное определение аксиомы, пикрелейтед
Ты понимаешь что у тебя "логический вывод" из ничего?
>Я чуть выше ссылался на статью Брауэра, он там как раз поясняет за необоснованность таких методов, когда нечто, выведенное из конечного априори и бездоказательно обобщается на бесконечное.
Да, некоторые вещи приходиться принимать без доказательств. Правда в том, что если мы вот прям счас откатимся в каменный век интуиционизма и забудем большую часть теорем существования - нам придётся лишиться очень, очень многого. Оно того не стоит.
>Требование построения доказательства - это не оголтелый скептицизм, а вполне резонное условие для математики, которая вообще-то является самым точным знанием, известным человечеству.
В "формализме" доказательства строятся настолько замечательно, что их можно проверить исключительно основываясь на синтаксисе.
>И где в интуиционизме сомнения в собственном здравомыслии?
В том, что интуиционисты начинали с классики. Затем они зачем-то её кастрировали, переформулировали и вуаля - новая теория. Правда, она оказалась не то чтобы очень нужной. Но всё же, новую теорию придумать - это не хухры мухры.
>С конструктивных объектов.
И как же они определяются?
>На возможных манипуляциях с элементами контекста.
Почему это они возможны?
255 Кб, 660x465>>4472
Я-то пони маю. Теперь и ты вроде начинаешь. Аксиома - это логический вывод из ничего, в противном случае это бы не аксиомой называлось.
В церкви - сколько угодно. Но не в математике.
Например? Чего многого-то? Полторы все равно невычислимые фофудьи типа исключенного третьего - это немного. И раз они все равно невычислимы, считай, что мы их и так лишены, использовать-то все равно нельзя, только рисовать.
Из которого нельзя вывести ничего кроме этого синтаксиса. Самый простейший пример - формулу Пирса и таблицы тарского я уже упоминал.
Ой, всё... В каком месте Брауэр начинал с классики? Ты же его даже не читал, но осуждаешь, как совки Пастернака. Даже ту картинку с Брауэром на дачке и 1 и 2 актами интуиционизма, которую я сто раз постил, не читал.
А вот тут опять надо писать страшные слова, с которых бесноватых корежит - интрерпретация логических констант по Брауэру-Гейтингу-Колмогорову.
>Ты понимаешь что у тебя "логический вывод" из ничего?
Я-то пони маю. Теперь и ты вроде начинаешь. Аксиома - это логический вывод из ничего, в противном случае это бы не аксиомой называлось.
>Да, некоторые вещи приходиться принимать без доказательств.
В церкви - сколько угодно. Но не в математике.
>Правда в том, что если мы вот прям счас откатимся в каменный век интуиционизма и забудем большую часть теорем существования - нам придётся лишиться очень, очень многого.
Например? Чего многого-то? Полторы все равно невычислимые фофудьи типа исключенного третьего - это немного. И раз они все равно невычислимы, считай, что мы их и так лишены, использовать-то все равно нельзя, только рисовать.
>В "формализме" доказательства строятся настолько замечательно, что их можно проверить исключительно основываясь на синтаксисе.
Из которого нельзя вывести ничего кроме этого синтаксиса. Самый простейший пример - формулу Пирса и таблицы тарского я уже упоминал.
>В том, что интуиционисты начинали с классики. Затем они зачем-то её кастрировали, переформулировали и вуаля - новая теория.
Ой, всё... В каком месте Брауэр начинал с классики? Ты же его даже не читал, но осуждаешь, как совки Пастернака. Даже ту картинку с Брауэром на дачке и 1 и 2 актами интуиционизма, которую я сто раз постил, не читал.
>И как же они определяются?
>Почему это они возможны?
А вот тут опять надо писать страшные слова, с которых бесноватых корежит - интрерпретация логических констант по Брауэру-Гейтингу-Колмогорову.
>>4473
Это не логический вывод, потому что предпосылок нет.
Ты хочешь сказать, что можешь доказать непротиворечивость кокструктивистской хуйни средствами самой теории? Она только кажется тебе убедительной, в основном из-за своей радикальности, но на имеет под собой ровно столько же оснований, что и любые другие непротиворечивые основания математики. Интуиционистский неуместный аскетизм предлагает резать всё циркулярной пилой и ножом - ну а хули, режет же, чего ещё надо?
Теоремы существования кокструктивизмом не признаются, однако часто, чтобы рассчитать то, существование чего доказывает теорема, необходимо провести над этим чем-то определённые манипуляции. Прямо как здесь: >>4459
допустимость операций определяется сходимостью ряда, что определяется существованием предела. Более того, поскольку сам придел - понятие неарифмитическое, он впринципе выпадает из рассмотрения конструктивистской секты. И что же конструктивисту делать, если его инженер попросит рассчитать работу?
Ты сравниваешь тёплое с мягким. Синтаксис позволяет проверить правильность умозаключений, но отнюдь не призван заменить работающую голову.
Он начал с изучения классической математики. Он не сделал свои выводы, сидя на дачке с полной изоляцией от внешнего мира.
Эти константы были положены, постулированы, как постулируется существование множества натуральных чисел. Кстати об N - оно ж бесконечно, а значит необходима очень ловкая логическая конструкция, которая позволяет манипулировать натуральными числами, не так ли?
> Аксиома - это логический вывод из ничего
Это не логический вывод, потому что предпосылок нет.
>В церкви - сколько угодно. Но не в математике.
Ты хочешь сказать, что можешь доказать непротиворечивость кокструктивистской хуйни средствами самой теории? Она только кажется тебе убедительной, в основном из-за своей радикальности, но на имеет под собой ровно столько же оснований, что и любые другие непротиворечивые основания математики. Интуиционистский неуместный аскетизм предлагает резать всё циркулярной пилой и ножом - ну а хули, режет же, чего ещё надо?
>Полторы все равно невычислимые фофудьи типа исключенного третьего - это немного. И раз они все равно невычислимы, считай, что мы их и так лишены
Теоремы существования кокструктивизмом не признаются, однако часто, чтобы рассчитать то, существование чего доказывает теорема, необходимо провести над этим чем-то определённые манипуляции. Прямо как здесь: >>4459
допустимость операций определяется сходимостью ряда, что определяется существованием предела. Более того, поскольку сам придел - понятие неарифмитическое, он впринципе выпадает из рассмотрения конструктивистской секты. И что же конструктивисту делать, если его инженер попросит рассчитать работу?
>Из которого нельзя вывести ничего кроме этого синтаксиса.
Ты сравниваешь тёплое с мягким. Синтаксис позволяет проверить правильность умозаключений, но отнюдь не призван заменить работающую голову.
>В каком месте Брауэр начинал с классики?
Он начал с изучения классической математики. Он не сделал свои выводы, сидя на дачке с полной изоляцией от внешнего мира.
>интрерпретация логических констант по Брауэру-Гейтингу-Колмогорову.
Эти константы были положены, постулированы, как постулируется существование множества натуральных чисел. Кстати об N - оно ж бесконечно, а значит необходима очень ловкая логическая конструкция, которая позволяет манипулировать натуральными числами, не так ли?
86 Кб, 491x661>>4477
Я же даже скрин логического вывода аксиомы дал. Врети?..
Он с нее не начал, а просто изучал в школке и в универе, как и все остальные. Это разные вещи.
Множество натуральных чисел задано правилами его построения, там нечего постулировать.
Не так. Опять же, обсуждали уже все это. В том числе и отличие актуальных бесконечностей от абстракции потенциальной осуществимости.
>Это не логический вывод, потому что предпосылок нет.
Я же даже скрин логического вывода аксиомы дал. Врети?..
>Он начал с изучения классической математики.
Он с нее не начал, а просто изучал в школке и в универе, как и все остальные. Это разные вещи.
>Эти константы были положены, постулированы, как постулируется существование множества натуральных чисел.
Множество натуральных чисел задано правилами его построения, там нечего постулировать.
>Кстати об N - оно ж бесконечно, а значит необходима очень ловкая логическая конструкция, которая позволяет манипулировать натуральными числами, не так ли?
Не так. Опять же, обсуждали уже все это. В том числе и отличие актуальных бесконечностей от абстракции потенциальной осуществимости.
>>4482
Мне непонятно, из чего выводится аксиома. Я отказываюсь выводить из ничего чего-либо. Я лучше спокойно признаю произвольность аксиом.
Он её изучал, она была его первой дверью в математику. Классическая математика - это необходимый этап в эволюции его взглядов. Я даже рискну предположить, что до определённого момента он верил в классическую математику.
Нечего постулировать, кроме правил построения и канонического элемента, ты хотел сказать.
Какие проблемы устраняет отказ от актуальной бесконечности и принятие потенциальной, вот что интересует меня в первую очередь.
>логического вывода аксиомы дал
Мне непонятно, из чего выводится аксиома. Я отказываюсь выводить из ничего чего-либо. Я лучше спокойно признаю произвольность аксиом.
>Он с нее не начал, а просто изучал в школке и в универе, как и все остальные. Это разные вещи.
Он её изучал, она была его первой дверью в математику. Классическая математика - это необходимый этап в эволюции его взглядов. Я даже рискну предположить, что до определённого момента он верил в классическую математику.
>Множество натуральных чисел задано правилами его построения, там нечего постулировать.
Нечего постулировать, кроме правил построения и канонического элемента, ты хотел сказать.
>отличие актуальных бесконечностей от абстракции потенциальной осуществимости
Какие проблемы устраняет отказ от актуальной бесконечности и принятие потенциальной, вот что интересует меня в первую очередь.
>>4483
Актуальная бесконечность невычислима.
> Какие проблемы устраняет отказ от актуальной бесконечности и принятие потенциальной, вот что интересует меня в первую очередь.
Актуальная бесконечность невычислима.
>>4487
Вычислимость сама по себе -верунство.
Вычислимость сама по себе -верунство.
>>4485
Докажи.
Докажи.
>>4470
Ты, кажется, не отличаешь аксиомы и правила вывода. Прочитай какой-нибудь учебник по мат.логике, первый курс мехмата.
Ты, кажется, не отличаешь аксиомы и правила вывода. Прочитай какой-нибудь учебник по мат.логике, первый курс мехмата.
>>4498
Крестись. Разве я виноват, что про натуральную дедукцию ты от меня позавчера услышал? Подумой, ты ж даже аргументы не воспринимаешь. Я тебе даю ссылку и даже конкретный скрин, ты глаза закатил и пытаешься доказать мне, что это я что-то не знаю.
>кажется,
Крестись. Разве я виноват, что про натуральную дедукцию ты от меня позавчера услышал? Подумой, ты ж даже аргументы не воспринимаешь. Я тебе даю ссылку и даже конкретный скрин, ты глаза закатил и пытаешься доказать мне, что это я что-то не знаю.
>>4503
Ээ... Прочитай, кому был адресован мой пост. Ты, кажется, просто триггеришься на определенные слова своей вечной мантрой про "я дал скрин, прочитайте, вы ничего не понимаете, уже тысячу раз объяснял". Ты точно не бот?
Ээ... Прочитай, кому был адресован мой пост. Ты, кажется, просто триггеришься на определенные слова своей вечной мантрой про "я дал скрин, прочитайте, вы ничего не понимаете, уже тысячу раз объяснял". Ты точно не бот?
>>4483
А что вообще актуальная бесконечность делает в математике? Это даже не математический объект. Проблема как раз в этом. В математику за тысячи лет понатащили всякой хуйни, никакого отношения к ней не имеющей. В основном из третьесортной философии типа платонизма. Причем, в самые основания понатащили. А потом вжух и кризис оснований.
>Какие проблемы устраняет отказ от актуальной бесконечности и принятие потенциальной, вот что интересует меня в первую очередь.
А что вообще актуальная бесконечность делает в математике? Это даже не математический объект. Проблема как раз в этом. В математику за тысячи лет понатащили всякой хуйни, никакого отношения к ней не имеющей. В основном из третьесортной философии типа платонизма. Причем, в самые основания понатащили. А потом вжух и кризис оснований.
156 Кб, 787x830>>4607
У тебя еще есть время научиться пользоваться гуглом. В чебурнете такой возможности уже не будет, поторопись.
У тебя еще есть время научиться пользоваться гуглом. В чебурнете такой возможности уже не будет, поторопись.
34 Кб, 357x333>>4611
Похоже на хуйню какую-то, даже скорее всего выдуманную и несуществующую.
Зачем мне время тратить на поиски её в гугле? Тем более если я гос. веб сайтам не совсем доверяю в таких вопросах.
Похоже на хуйню какую-то, даже скорее всего выдуманную и несуществующую.
Зачем мне время тратить на поиски её в гугле? Тем более если я гос. веб сайтам не совсем доверяю в таких вопросах.
>>4612
Актуальная бесконечность хуйня и есть, как и любые другие попытки использовать платонизм в математике. Но с этой хуйней проще, ей можно заткнуть открытую проблему и кукарекать, что математика к вычислимости не сводится.
>Похоже на хуйню какую-то, даже скорее всего выдуманную и несуществующую.
Актуальная бесконечность хуйня и есть, как и любые другие попытки использовать платонизм в математике. Но с этой хуйней проще, ей можно заткнуть открытую проблему и кукарекать, что математика к вычислимости не сводится.
>>4624
Местами. В оригинальном своем виде это невычислимая аксиоматика, в качестве оснований непригодная как минимум из-за исключенного третьего. Если даже довести до ума, все равно не идет дальше лямбда-Р в кубе Барендрегта, а в 2017 это несерьезно.
Местами. В оригинальном своем виде это невычислимая аксиоматика, в качестве оснований непригодная как минимум из-за исключенного третьего. Если даже довести до ума, все равно не идет дальше лямбда-Р в кубе Барендрегта, а в 2017 это несерьезно.
>>4627
А неконструктивисты когда? Все-то вас тянет ко всякой бесконечной комбинаторной хуйне из прошлого тысячелетия типа ферзей да римановых ноликов.
А неконструктивисты когда? Все-то вас тянет ко всякой бесконечной комбинаторной хуйне из прошлого тысячелетия типа ферзей да римановых ноликов.
>>4629
Оставляем эту почетную проблему вам, а то у вас совсем как-то плохо. Почти никаких задач не решаете, всё дрочите на свою вычислимость.
>А неконструктивисты когда?
Оставляем эту почетную проблему вам, а то у вас совсем как-то плохо. Почти никаких задач не решаете, всё дрочите на свою вычислимость.
>>4629
А вот если бы ты не был необразованным селюком, ты бы знал что почти вся эта наука о "вычислимости" сводится к задаче о ферзях.
>бесконечной комбинаторной хуйне из прошлого тысячелетия типа ферзей да римановых ноликов
А вот если бы ты не был необразованным селюком, ты бы знал что почти вся эта наука о "вычислимости" сводится к задаче о ферзях.
>>4638
У ℤ нет конечного порядка.
Существуют группы, которые не являются конечными.
>Окей, а каков порядок ℤ?
У ℤ нет конечного порядка.
>Или у вас не существует бесконечных групп?
Существуют группы, которые не являются конечными.
А это нормально, что меня от использования аксиомы выбора и исключённого третьего подташнивать начинает?
>>4672
А меня вот бесит аксиома пары. Каждый раз, как о ней думаю, аж зубы сводит, так сильно эту аксиому ненавижу. Блядские веруны в пару, так бы и запретил.
А меня вот бесит аксиома пары. Каждый раз, как о ней думаю, аж зубы сводит, так сильно эту аксиому ненавижу. Блядские веруны в пару, так бы и запретил.
>>4673
Я не использую теорию множеств, я же не совсем конченный.
Я не использую теорию множеств, я же не совсем конченный.
>>4668
И что? Класс задач, разрешимость которых можно проверить на машине Тьюринга за не более чем полиномиальное от размера входных данных время - это далеко не вся "наука о вычислимости". И это чудо капустное кого-то будет селюком называть.
>Любая NP-полная задача сводится к любой NP-полной.
И что? Класс задач, разрешимость которых можно проверить на машине Тьюринга за не более чем полиномиальное от размера входных данных время - это далеко не вся "наука о вычислимости". И это чудо капустное кого-то будет селюком называть.
>>1361 (OP)
Какова природа математической истины? Вот 1+1=2 это вроде как истина, но истина не такая как "Расстояние от моей лобковой кости до конца головки моего члена в эрегированном стоянии составляет 13см, что является средним и нормальным значением". Знаю людей утверждающих что математика это вообще не про истину и не про объективность, а просто маняфантазёрство.
Какова природа математической истины? Вот 1+1=2 это вроде как истина, но истина не такая как "Расстояние от моей лобковой кости до конца головки моего члена в эрегированном стоянии составляет 13см, что является средним и нормальным значением". Знаю людей утверждающих что математика это вообще не про истину и не про объективность, а просто маняфантазёрство.
>>4801
-> /ph
-> /ph
309 Кб, 1902x2842>>4801
Классически в математике истинно то, что непротиворечиво. Конструктивно - истинно то, что построимо, т.е. конструктивные объекты и доказуемве / выводимые / наблюдаемые их свойства.
Есть мнение, что точно такая же. Пикрелейтед, выделенное. Математический релятивизм Маннури - утверждение о сводимости любого концепта к любому другому, т.е. если есть концепт A и другой концепт В, то первый можно свести ко второму через конечное число промежуточных концептов A1,...,An таких, что концепт А представим в форме концепта А1, а концепт An представим в виде концепта В. Концепты, например, могут быть любыми математическими объектами, принадлежащими любой аксиоматике, теории и т.д. В твоем примере даже этого не требуется, поскольку в обоих случаях речь о натуральных числах, к которым напрямую сводятся оба твои примера.
>Какова природа математической истины?
Классически в математике истинно то, что непротиворечиво. Конструктивно - истинно то, что построимо, т.е. конструктивные объекты и доказуемве / выводимые / наблюдаемые их свойства.
>Вот 1+1=2 это вроде как истина, но истина не такая как "Расстояние от моей лобковой кости до конца головки моего члена в эрегированном стоянии составляет 13см, что является средним и нормальным значением".
Есть мнение, что точно такая же. Пикрелейтед, выделенное. Математический релятивизм Маннури - утверждение о сводимости любого концепта к любому другому, т.е. если есть концепт A и другой концепт В, то первый можно свести ко второму через конечное число промежуточных концептов A1,...,An таких, что концепт А представим в форме концепта А1, а концепт An представим в виде концепта В. Концепты, например, могут быть любыми математическими объектами, принадлежащими любой аксиоматике, теории и т.д. В твоем примере даже этого не требуется, поскольку в обоих случаях речь о натуральных числах, к которым напрямую сводятся оба твои примера.
>>4806
Давай конструктивное доказательство.
>если есть концепт A и другой концепт В, то первый можно свести ко второму через конечное число промежуточных концептов A1,...,An таких, что концепт А представим в форме концепта А1, а концепт An представим в виде концепта В.
Давай конструктивное доказательство.
>>4807
Типизированная лямбда же. К ней легко свести даже естественный язык,как пример - семантика Монтегю, есть еще целая монография Ранте, где естественный язык анализируется с позиции MLTT и наоборот. А на естественном языке можно описать хоть твою мамку. Опять же, по Маннури, есть 5 уровней языка, от естественного разговорного до полностью формального, н-р матлогика, и разница между этими уровнями относительная, а не абсолютная. Так что доказать можно и конструктивно, через типизированную лямбду, т.к. любой концепт так или иначе можно представить лямбда-термом.
Типизированная лямбда же. К ней легко свести даже естественный язык,как пример - семантика Монтегю, есть еще целая монография Ранте, где естественный язык анализируется с позиции MLTT и наоборот. А на естественном языке можно описать хоть твою мамку. Опять же, по Маннури, есть 5 уровней языка, от естественного разговорного до полностью формального, н-р матлогика, и разница между этими уровнями относительная, а не абсолютная. Так что доказать можно и конструктивно, через типизированную лямбду, т.к. любой концепт так или иначе можно представить лямбда-термом.
>>4808
Сомневаюсь, что это можно конструктивно доказать.
>любой концепт так или иначе можно представить лямбда-термом.
Сомневаюсь, что это можно конструктивно доказать.
>>4810
Можно, причем элементарно - через обобщение номинальной дефиниции и редукций (дельта, бета, иота, дзета) до кое-чего интересного. Когда-нибудь допилю свой мега-гитлер прувер, будет конструктивное доказательство.
Можно, причем элементарно - через обобщение номинальной дефиниции и редукций (дельта, бета, иота, дзета) до кое-чего интересного. Когда-нибудь допилю свой мега-гитлер прувер, будет конструктивное доказательство.
>>4812
А планируешь прувер сделать онлайновым? Сейчас типа все современные пруверы имеют онлайн морду.
А планируешь прувер сделать онлайновым? Сейчас типа все современные пруверы имеют онлайн морду.
>>4814
Подробнее долго. Когда-нибудь руки дойдут, запилю нормальный пейпер.
>>4847
Полноценная реализация изначально планируется онлайновой, т.к. все нужное проще всего реализовать средствами гугловской облачной платформы https://cloud.google.com/ и не привязанной ни к какой конкретной операционке. Кто бы еще все это сделал, т.к. я в гуглооблако не могу. Локально почти все нужное (кроме OCR для математической нотации (LaTeX и AMS-TeX) реализуемо в R, это уже посильно для меня, было бы еще свободного времени побольше а быдлопроблем поменьше.
Подробнее долго. Когда-нибудь руки дойдут, запилю нормальный пейпер.
>>4847
>планируешь прувер сделать онлайновым?
Полноценная реализация изначально планируется онлайновой, т.к. все нужное проще всего реализовать средствами гугловской облачной платформы https://cloud.google.com/ и не привязанной ни к какой конкретной операционке. Кто бы еще все это сделал, т.к. я в гуглооблако не могу. Локально почти все нужное (кроме OCR для математической нотации (LaTeX и AMS-TeX) реализуемо в R, это уже посильно для меня, было бы еще свободного времени побольше а быдлопроблем поменьше.
>>4855
Был тут рукастый анон, который сайт создавал, может он поможет. Как тебе его сайт был?
Был тут рукастый анон, который сайт создавал, может он поможет. Как тебе его сайт был?
>>1607
Отличное видео. У него как я понимаю вообще мало записанных лекций?
Отличное видео. У него как я понимаю вообще мало записанных лекций?
![8652786f1024[1].jpg](https://2ch.life//math/src/21361/15062963498940.jpg)
![267px-AlexanderGrothendieck[1].jpg](https://2ch.life//math/src/21361/15063578856740.jpg)
19 Кб, 267x325>>4867
Хорен что ли?))
Хорен что ли?))
>>5211
Хорошо, а тогда как с помощью киинтуиционисткой логики доказать, например, неразрешимость проблемы останвки?
Хорошо, а тогда как с помощью киинтуиционисткой логики доказать, например, неразрешимость проблемы останвки?
>>5213
Я и говорю как вирус, уже везде видишь невозможность доказать что-либо без его использования.
Я и говорю как вирус, уже везде видишь невозможность доказать что-либо без его использования.
>>5215
Хорошо, порекомендуй тогда, пожалуйста, монографии по конструктивной математике.
Ну то есть уважаемые труды, где много теорем.
Хорошо, порекомендуй тогда, пожалуйста, монографии по конструктивной математике.
Ну то есть уважаемые труды, где много теорем.
>>5285
Да одно и тоже
Да одно и тоже
Посоны, микроядра кто нибудь доказывал? Че там жопа или реал вкатится и бабосы рубить под пивасик?
Посоны, я тут короче кнута решаю. Всё правильно делаю?
Посоны, емакс учить или таблеток лучше?
>>5375
Пиздец, ужасная новость. Вроде как-то фиолетово, когда слышишь подобные известия, ну не друг и не родственник умер, но тут не по себе.
Пиздец, ужасная новость. Вроде как-то фиолетово, когда слышишь подобные известия, ну не друг и не родственник умер, но тут не по себе.
>>5388
Не верну, я обиделся на всех.
Не верну, я обиделся на всех.
>>5383
Единственная, я бы сказал. Других не подвозили, начиная с того самого 11-го симпозиума в Палермо в 1897 году, когда Бурали-Форти торжественно помочился Кантору за шиворот, уничтожив его как математика.
>Очередная победа теоретико-множественного подхода.
Единственная, я бы сказал. Других не подвозили, начиная с того самого 11-го симпозиума в Палермо в 1897 году, когда Бурали-Форти торжественно помочился Кантору за шиворот, уничтожив его как математика.
>>5394
У любого найдется, что критиковать. Одно дело критика, другое - доказательство противоречивости и т.о. бесполезности всей теории.
У любого найдется, что критиковать. Одно дело критика, другое - доказательство противоречивости и т.о. бесполезности всей теории.
Брауэр, к слову, не только задолго до Геделя и обсера Гильберта с его изначальной программой, показал несостоятельность формализма как оснований математики. И даже не только вывел суть математики как ментальных построений, что подтвердилось уже в нулевых годах 21 века (модели ATOM, MT, о чем уже писалось). Его взгляды на природу и физику как науку очень похожи на то, что сейчас известно как квантово-волновой дуализм и эффект наблюдателя (во II части его диссертации и немного в самом начале III части есть некоторое количество цитат на эту тему), он же был профессором кафедры математики и физики. К сожалению, я в квантмехе практически нихуя не понимаю давно забытый материал из учебников не считается, чтобы сделать более грамотное сравнение. Даже его определение дискретного и непрерывного в интуиции времени как основе математики можно было бы рассмотреть с точки зрения квантово-волнового дуализма.
>>5396
Всецело поддерживаю это начинание. Чем больше вы будете пиздеть о квантовой механике, тем большему количеству людей будет видно, что вы сумасшедшие.
Всецело поддерживаю это начинание. Чем больше вы будете пиздеть о квантовой механике, тем большему количеству людей будет видно, что вы сумасшедшие.
>>5397
Кто "мы"-то? Я один тута. Разве то, что из некоей теории можно вывести нечто такое, до чего остальная наука дошла десятилетия спустя, не говорит в пользу правильности этой теории7
Кто "мы"-то? Я один тута. Разве то, что из некоей теории можно вывести нечто такое, до чего остальная наука дошла десятилетия спустя, не говорит в пользу правильности этой теории7
>>5398
Да-да, конечно. Если Кузанский о множественности миров кукарекал, то это он на самом деле теорию струн открыл.
Да-да, конечно. Если Кузанский о множественности миров кукарекал, то это он на самом деле теорию струн открыл.
>>5399
Это одна из возможных интерпретаций же. А корпускулярно-волновой дуализм - медицинский факт.
>множественности миров
Это одна из возможных интерпретаций же. А корпускулярно-волновой дуализм - медицинский факт.
>>5400
Да-да. И вот так, легким движением ушей, Кузанский записывается в отцы-основатели квантовой механики.
Да-да. И вот так, легким движением ушей, Кузанский записывается в отцы-основатели квантовой механики.
>>5408
Ну зачем же сразу расстройство. У нас свобода вероисповедания. Кто-то в Аллаха верует, кто-то в платоновский мир идей. Другой вопрос, что ни то ни другое - это не математика.
Ну зачем же сразу расстройство. У нас свобода вероисповедания. Кто-то в Аллаха верует, кто-то в платоновский мир идей. Другой вопрос, что ни то ни другое - это не математика.
>>5415
Чем же ты объясняешь очевидную популярность теории множеств? Видимо ты просто не умеешь ей правильно пользоваться, поэтому в отрицание скатываешься.
Чем же ты объясняешь очевидную популярность теории множеств? Видимо ты просто не умеешь ей правильно пользоваться, поэтому в отрицание скатываешься.
>>5423
Я тебя услышал.
>Чем же ты объясняешь очевидную популярность ислама? Видимо ты просто не умеешь правильно веровать, поэтому в куфр скатываешься.
Я тебя услышал.
>>5439
Ок, ты мечтаешь о вычслимости.
Когда доказываешь кому-то теорему можно сделать двумя способами: либо доказать уже известными всем методами, простыми, быстрыми.
Либо выдумывать свою конструктивную науку и в ней болтаться без конца.
Я тебя спрашиваю: где результат?
Какую реальную проблему помогла решить вычислимость теорем?
Сможешь хотя бы 3 примера реальных задач привести.
За которые тебе заплатят деньги. Классическая логика и обычные основания математики - дают рабочий инструмент.
Нахрена из кувалды делать микроскоп?
Ок, ты мечтаешь о вычслимости.
Когда доказываешь кому-то теорему можно сделать двумя способами: либо доказать уже известными всем методами, простыми, быстрыми.
Либо выдумывать свою конструктивную науку и в ней болтаться без конца.
Я тебя спрашиваю: где результат?
Какую реальную проблему помогла решить вычислимость теорем?
Сможешь хотя бы 3 примера реальных задач привести.
За которые тебе заплатят деньги. Классическая логика и обычные основания математики - дают рабочий инструмент.
Нахрена из кувалды делать микроскоп?
>>5439
Ваша анальная фиксация на исламе поражает, вас в детстве насиловал отчим дагестанец?
Ваша анальная фиксация на исламе поражает, вас в детстве насиловал отчим дагестанец?
ℵ_∞
>>5456
Действительно, согласен. Вот ещё что думаю:
У них контринтуитивное отрицание закона исключенного третьего.
Утверждение: Конструктивист петух или конструктивист не петух. Но зная, что конструктивист петух, мы не можем определить истинность этого утверждения!
Действительно, согласен. Вот ещё что думаю:
У них контринтуитивное отрицание закона исключенного третьего.
Утверждение: Конструктивист петух или конструктивист не петух. Но зная, что конструктивист петух, мы не можем определить истинность этого утверждения!
>>5486
Хороший вопрос! Хотелось бы чёткое обоснование, без всяких отсылок к изоморфизмам гарри-ховарда, тезиса чёрча и прочих сложныхштук. По-нашему, кратко, по-простому, но по делу.
Хороший вопрос! Хотелось бы чёткое обоснование, без всяких отсылок к изоморфизмам гарри-ховарда, тезиса чёрча и прочих сложныхштук. По-нашему, кратко, по-простому, но по делу.
>>5552
сагласен! я вот ещё кстате вычислил что канструктивные основания пративоречивы!!
ведь в них отрицается исключённае третье и доказывается двойное отрицание исключённого третьего!!
другими словами просто фууу....
сагласен! я вот ещё кстате вычислил что канструктивные основания пративоречивы!!
ведь в них отрицается исключённае третье и доказывается двойное отрицание исключённого третьего!!
другими словами просто фууу....
так... я даказал в гаматапической теории типав что исключённое третье неверно. из этого следует пративоречивость канструктивной
математики.
теорема: канструктивная математика противоречива.
доказательство:
исключённая третье говорит нам, что верно - для всех типав 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 вместо у и палучаем что все гаматопические группы (любого типа!!!) тривиальны!
куда можно это опубликовать?
7 Кб, 1200x1200извените...
там в конце доказательство должен был быть знак как на скриншоте.
там в конце доказательство должен был быть знак как на скриншоте.
>>5554
улыбнул, но лучше бы ты по теме что-нибудь писал про вычислимость. Очень кайфовая тема.
улыбнул, но лучше бы ты по теме что-нибудь писал про вычислимость. Очень кайфовая тема.
>>5569
тут дажы вычислимасть не нужна чтобы доказать пративаречивость вычислимасти.
тут дажы вычислимасть не нужна чтобы доказать пративаречивость вычислимасти.
Перекат https://2ch.hk/math/res/25624.html (М)
М)