Предыдущий - https://2ch.hk/math/res/3694.html
Конструктивная математика это не математика, а рак!
Такое слово, как вычислимость, не должно заботить математиков вообще, они же не считают. А вот инжинерам как раз без возможно посчитать что трудно поверить в возможность существования. Ведь как что-то может существовать, если это нельзя посчитать или построить? У них такое в уме не укладывается.
Алгоритмы построения - это computer science, по сути алоритмы нужны программистам и раздел о них - теория алгоритмов, часть информатики. Математика снова тут делать нечего. Вот пример быдлокода обезьяны
По-сути, становление конструктивистом есть не что инное, как опущение с математика до кодовай макаки или инженеробыдла.
Такое слово, как вычислимость, не должно заботить математиков вообще, они же не считают. А вот инжинерам как раз без возможно посчитать что трудно поверить в возможность существования. Ведь как что-то может существовать, если это нельзя посчитать или построить? У них такое в уме не укладывается.
Алгоритмы построения - это computer science, по сути алоритмы нужны программистам и раздел о них - теория алгоритмов, часть информатики. Математика снова тут делать нечего. Вот пример быдлокода обезьяны
По-сути, становление конструктивистом есть не что инное, как опущение с математика до кодовай макаки или инженеробыдла.
>Такое слово, как вычислимость, не должно заботить математиков вообще,
Оно и не заботило, пока оказалось, что чисто формально нельзя даже доказать, что 1+1=2. Для этого нужны именно вычислимые построения, ординалы ли фон Неймана, нумералы ли Черча, однохуйственно. Но без вычислимости (построимости) никуда. По-сути, в математике кроме вычислимости и невычислимых объектов веры типа исключенного третьего и актуальной бесконечности, ничего и нет. Но, вера в невычислимые сущности это не математика.
Ещё раз говорю, программисты и инженеры таким занимаются.
Им это жизненно необходимо, а математик может класть болт на такие вещи.
>математик может класть болт на такие вещи.
И окукливаться в аутизме, не имеющем ничего общего с математикой.
>И окукливаться в аутизме, не имеющем ничего общего с математикой.
Идеальное названия для программерской параши под названием коструктивная математика.
Я тебя услышал, мнение клована с мейлру, разумеется перевешивает все остальное. Петросянишь такой на мочане, и кризис оснований сам собой рассосался. "Нинужно!!" это не дискуссия а детский сад, если что. Математика = вычислимость, все остальное это просто не математика.
>Я тебя услышал, мнение клована с мейлру, разумеется перевешивает все остальное.
Ты такой же клован, только и можешь, как попугай за Бровером повторять цитатки из библии, как верун. НУ ТАК ЖЕ БРАУЕР СКАЗАЛ, ТАК ЖЕ В БИБЛИИ НАПИСАНО РЯЯЯЯЯЯЯ!
>и кризис оснований сам собой рассосался.
Кризис оснований в 2017, ох лол. Может быть ты ещё от шока, что sqrt(2) не рациональное число, не отошел?
>"Нинужно!!" это не дискуссия а детский сад, если что
Как раз ты так про нормальную математику и кричишь, что вся математика, кроме твоей прогерской параши НИНУЖНАЯ.
>Математика = вычислимость, все остальное это просто не математика.
Ну раз так сказал клоун с мейлача, который начитался шизофазии Брауера, то так оно и есть.
Кукарекуй и дальше, фактов это не отменяет. А факты в том, что кроме конструктивных методов, кризис оснований не преодолим никак, остальные методы показали свою несостоятельность. И если не замечать кризис оснований, он никуда не денется. Методы, отличные от конструктивных работают только в пределах конструктивной математики.
>Кукарекуй и дальше, фактов это не отменяет
Твои фантазии не факты.
>А факты в том, что кроме конструктивных методов, кризис оснований не преодолим никак, остальные методы показали свою несостоятельность.
А разве он не преодолен сейчас?
>Твои фантазии не факты.
Что "мои фантазии", перечисли.
>А разве он не преодолен сейчас?
Нет, разумеется. Более того, никаких формальных и вообще отличных от конструктивных подходов к преодолению за более чем 100 лет не предложено. Собственно, даже Гильберт этого не потянул, куда уж всякой пузатой мелочи.
Да, я еще заметил, что тут на мейлру даже не понимают, что есть вычислимость. И есть подозрения, что сводят ее к арифметической вычислимости хотя в целом любую вычислимость можно свести к арифметике, через лексикографическое упорядосивание слов в алфавитах или через геделевскую нумерацию, но это слишком сложно для этой параши не понимая, что вообще говоря, речь о несколько ином. Скажем, о вычислимых функциях в лямбда-исчислении или в более простом объяснении к сводимости одного выражения к другому. Совсем никто не понимает, в чем разница между простой игрой в знакосочетания и вычислением построимых объектов, между каноническими и неканоническими элементами и множествами, и даже между языком и метаязыком. Зато, желающих покукарекать, при этом не понимая вышеперечисленных азов, всегда достаточно. Так вот, основной тезис в том, что математика = вычислимость, иначе это не математика, нужно понимать следующим образом: вы не сможете привести ни одного примера применения математики, не сводящегося к вычислению. Ни одного примера, противоречащего тезису Черча. Всякие исключенные третьи и актуальные бесконечности - это пример игры в знакосочетания, за которыми ничего не стоит, которые ни во что не вычисляются даже в виде потенциальной осуществимости, т.е. правил таких вычислений. И поэтому такая хуета есть источник парадоксов и кризисов в математике.
Как ты противопоставляешь "чисто формальное доказательство" и ординалы?
>Логицизм. Не пошел дальше труда Рассела и Уайтхеда Principia Mathematica.
А разве теория типов - это не развитие идей логицизма?
Вопрос по теореме Гёделя о неполноте.
Часто встречаю такую одну из интерпретаций его вывода: для любой формальной системы есть недоказуемое в рамках этой системы предложение, истинность которого мы тем не менее можем доказать (вне рамок системы).
Этот вывод основывается на предположении, что для формальной системы F мы строим гедёлево предложение A. Для системы F' = F+A мы строим гёделево предложение A'. Для системы F'' = F' + A' мы строим гёделево предложение A'' и так далее... Значит, для любой формальной системы мы можем построить гедёлево предложение - которое недоказуемо, но истинно.
Однако сам способ построения гёделевых предложений вполне алгоритмически формализуем, как и вообще все наши возможные способы доказать истинность какого-либо предложения.
Следовательно, мы можем построить формальную систему, которая в качестве одного из методов доказательств будет строить подобные гедёлевы предложения.
Данная формальная система также будет неполна (это легко доказать, отталкиваясь от проблемы остановки). То есть, будет существовать предложение B, для которого мы не можем доказать ни B, ни (не B). Однако доказать, какое из них истинно, мы не можем.
Следовательно, говорить о существовании истинного, не недоказуемого, мы можем лишь в смысле закона исключения третьего.
Часто встречаю такую одну из интерпретаций его вывода: для любой формальной системы есть недоказуемое в рамках этой системы предложение, истинность которого мы тем не менее можем доказать (вне рамок системы).
Этот вывод основывается на предположении, что для формальной системы F мы строим гедёлево предложение A. Для системы F' = F+A мы строим гёделево предложение A'. Для системы F'' = F' + A' мы строим гёделево предложение A'' и так далее... Значит, для любой формальной системы мы можем построить гедёлево предложение - которое недоказуемо, но истинно.
Однако сам способ построения гёделевых предложений вполне алгоритмически формализуем, как и вообще все наши возможные способы доказать истинность какого-либо предложения.
Следовательно, мы можем построить формальную систему, которая в качестве одного из методов доказательств будет строить подобные гедёлевы предложения.
Данная формальная система также будет неполна (это легко доказать, отталкиваясь от проблемы остановки). То есть, будет существовать предложение B, для которого мы не можем доказать ни B, ни (не B). Однако доказать, какое из них истинно, мы не можем.
Следовательно, говорить о существовании истинного, не недоказуемого, мы можем лишь в смысле закона исключения третьего.
Ну и, кстати, тем самым опровергается дурацкий противоречивый аргумент Пенроуза, что человек якобы может доказать то, что не может доказать ни одна формальная система, а значит, наше мышление не может быть смоделировано Машиной Тьюринга.
Да, покопался в литературе и нашёл, что из теоремы Чёрча-Клини следует, "that no algorithmic method can tell how to apply the method of Gödel to all possible kinds of formal system". У нас нет общего алгоритма, который позволил бы строит Гёделево предложение для произвольной формальной системы; подобный алгоритм существует лишь для узкого класса формальных систем.
>противоречивый аргумент Пенроуза, что человек якобы может доказать то, что не может доказать ни одна формальная система, а значит, наше мышление не может быть смоделировано Машиной Тьюринга.
Это не аргумент, а как принято говорить на бордах, "вскукарек". Аргумент - это что-то более весомое чем батрушка от машины Тьюринга. Этот деятель же не приводит ни одного примера.
>Пенроуз
Распиареный хуй с горы. Любитель объяснять нерешенные вопросы другими нерешенными вопросами
Теорем Гёделя о неполноте две. Ты используешь первую.
1ТГ использует непротиворечивость - в противоречивой системе доказуемо вообще всё.
2ТГ утверждает, что непротиворечивость недоказуема.
> Однако доказать, какое из них истинно, мы не можем.
С 2ТГ можем. Теория все еще непротиворечива, но не может доказать собственную непротиворечивость. Ты засунул в неё возможность строить гёделевы утверждения для любого конечного набора аксиом, а она построила бесконечный набор аксиом и уже не может построить гёделево утверждение для себя самой.
> она построила бесконечный набор аксиом и уже не может построить гёделево утверждение для себя самой.
Насколько я понимаю, мы тоже это гёделево утверждение в общем случае построить не можем (можем лишь утверждать, что оно есть). Так как если бы могли, то алгоритмически формализовали бы этот способ и вставили внутрь нашей формальной системы.
Что почитать о теории доказательств если даже доказательство геометрических теорем в школе для меня были мукой и непонятными?
А как научиться варить борщ, если приготовление яичницы для меня сущее мучение?
Если слова "элиминация сечения в исчислении секвенций" тебе ни о чем не говорят, то теория доказательств тебе на фиг не нужна. Может, тебе просто какие-нибудь детские книжки почитать, типа Смальяна?
Советую "Теорию множеств" Бурбаки. Проблема школьной геометрии в том, что она требует "строгих" доказательств, при этом совершенно не аргументируя, в чём эта строгость заключается. Мне, когда я был школьником, например, было совершенно непонятно, какие методы доказательства можно использовать, а какие нет, и где вообще выход из порочного круга, когда и так очевидные выводы приходится доказывать с помощью ещё более очевидных. Бурбаки реально очень многое проясняют.
Не очень хороший совет - Бурбаки строят свою теорию на основе эпсилон-оператора Гильберта, который детально не описывают. У начинающих из-за этого возникает недоумение.
> какие методы доказательства можно использовать, а какие нет
Я уже давно не школьник, а мне до сих пор непонятно, только Бурбаки тут, боюсь, не поможет.
С одной стороны, всех пугают, что визуальную очевидность надо засунуть себе в жопу, иначе придет страшная Лемма Жордана и все сдохнут. Но при этом по факту все всё время смотрят на картинку и выводят из неё суждения вида "эта хуйня лежит между вон той и вот этой".
При этом если речь идёт о трёх лучах хер знает в каком порядке, то все говорят "на самом-то деле все углы ориентированные (т. е. ABC= -CBA), так что нам всем похуй".
Почему такие финты ушами можно делать с тремя точками на прямой, можно объяснить только через скалярное произведение, но до него еще дожить надо (да и все равно даже когда доживёшь, фиг тебе кто нормально объяснит).
Поэтому имеется крайне вредная идеология о том, что нужно всегда разбирать случаи, что между чем лежит. Вред прежде всего в том, что если кто решит разобрать действительно все случаи, то помрет в процессе.
Но тем не менее адепты этой ереси встречаются, поэтому ушлых школьников учат: если какое мудило на приёмных приебётся насчёт неразобранного случая про то, что между чем болтается, надо пиздеть так: вся эта ваша сраная геометрия на самом деле про равенство каких-то там ебучих полиномов, а полиномы - они такие твари, что если равны на куске пространства, то и везде равны, а не то у ихней разности будет овердохуя нулей; поэтому моё доказательство для частного случая доказывает также и общий случай. Предполагается, что после такого заявления любое мудило в ужасе съебётся.
Ну, я надеюсь, анон учит геометрию не для школьных экзаменов, а так, изучать евклидову геометрию через аксиомы Евклида-Гильберта - это давно устаревшее извращение. Естественней изучить основы алгебры, ввести векторное пространство, изучить свойства аффинности, а потом навесить на это пространство метрику - вуаля - и геометрия готова. Изучать неафинные метрические пространства (всякие геометрии Лобачевского) - это уже другой вопрос, но для начала этого не требуется.
>вуаля - и геометрия готова
Это будет не геометрия, это будет алгебра. Геометрия - это пикрелейтед.
Ты что-то сразу за многомерную геометрию взялся. Обычную планиметрию можно прекрасно сбацать просто на комплексных числах.
>Это будет не геометрия, это будет алгебра.
Так геометрия и есть алгебра с картинками. Выбери одну задачу, я попробую продемонстрировать.
Твои задачи решаются на основе аксиом векторного пространства с метрикой ничуть не хуже, чем на основе стандартных геометрических аксиом.
Интересный эксперимент. Ок, 10.036.
Это с помощью этого оператора у бурбаков получилось определение единицы размером во сколько там квадрильенов знаков?
Хорошо. Углы - это по сути комплексные числа с модулем 1. Обозначим угол в 60 градусов через a: a = exp(pi/3) = 1/2 + i sqrt(3)/2.
Обозначим гипотенузу треугольника через x. Прямоугольный треугольник естественно отложить от нуля и поставить прилежащий катет на действительную ось, то есть вершинами треугольника будут числа 0, ax и Re ax.
Ромб состоит из чисел 0, 6, 6a и 6a+6. По условию дальняя вершина ромба, то есть 6a+6, лежит на противолежащем катете, который задается уравнением Re z = Re ax.
Имеем: Re (6a + 6) = Re ax, а так как Re a = 1/2, то 9 = x/2, стало быть x = 18.
Ага. Особенность эпсилон-оператора в том, что длина формальных определений при их усложнении растёт экспоненциально.
Сам по себе оператор у Бурбаков довольно прост. Для любой формулы (например, x < y) и любой переменной мы можем ввести терм ("такой x, что x < y"). Терм строится так: мы пишем логический символ t, после него формулу, в которой x заменяем на пустой квадратик; и соединяем символ t с этим квадратиком надстрочной линией.
То есть Бурбаки могут строить не только формулы из термов, но и термы из формул. В стандартной логике первого порядка таких термов нет. Замечу, что возможность построить терм "такой x, что x < y" вовсе не означает, что мы в рамках теории можем доказать существование этого терма. Формула, утверждающая "существует x, что x < y" выглядит так: мы пишем формулу (x < y), и все x в этой формуле заменяем термом "такой x, что x < y". Например, терм, обозначающий пустое множество на картинке. Расшифорывается как "такой x, что (не(существует у, где не(не(y принадлежит x))))". Формула "существует пустое множество" была бы ещё раза в 3 длиннее.
А в чем профиты такой нотации? Лямбда исчисление не проще разве?
Оно легко позволяет строить переходы между теорией и метатеорией - нужно просто доопределить эпсилон. Изначально Гильберт построил эпсилон-оператор, чтобы свести всю математику к арифметике. Оказалось, что он гораздо мощнее.
Но ведь это чистый конструктивизм, сводить всю математику к арифметике. Даже интуиционизм в смысле Брауэра. И это делается проще, безо всяких страшных операторов, в которых единицу можно представить только какими'то астрономическими количествами знаков. Геделевская нумерация, например или даже простая лексикографическая нумерация слов в алфавите. Это гильбертовское исчисление нигде не применяется же?
> Но ведь это чистый конструктивизм, сводить всю математику к арифметике.
Подозреваю, что тот анон имел в виду теорию множеств.
> Это гильбертовское исчисление нигде не применяется же?
Любой классический математик применяет эпсилон пять раз на дню, а тем более йоту. Это совершенно естественные операции.
Астрономические количества знаков возникают от низкоуровневости обычного исчисления предикатов. Это совершенно нормальная ситуация.
> Любой классический математик применяет эпсилон пять раз на дню, а
Пример?
> Астрономические количества знаков возникают от низкоуровневости обычного исчисления предикатов. Это совершенно нормальная ситуация.
Нет, это ненормальная ситуация. Исчисление предикатов выразимо в лямбде, т.н. изоморфизм Карри-Говарда, там почему'то нет никаких трильенов знаков для выражения простейших вещей.
Бурбаков совсем не интересовали алгоритмы - они занимались формализацией теорий не для этого, а с классических позиций формализма: "истинность значит выводимость в определённой формальной системе". Они предполагали, что работать с этими формальными системами будут живые математики и эти формальные системы должны быть удобны именно для живых математиков.
Эпсилон-формализм, например, требует всего одного правила вывода: modus ponens. В то же время в стандартных теориях первого порядка используются два правила вывода.
> Пример?
Я имею в виду сколемизацию. Классические предикаты первого порядка обычно что устно, что на компьютере считаются обычно сколемизацией. Скажем, если мы имеем AxEy f(y) = f(x) + 1, надо доказать AxEy f(y) = f(x) + 3. Любой классик сделает примерно так: пусть s - сколемизация, тогда s³ - то, что нужно.
> никаких трильенов знаков для выражения простейших вещей.
У тебя если лямбда нетипизирована, то можеть зависнуть, а если типизирована, то на каждой формуле надписано доказательство типизированности в специальном исчислении. Так что знаков у тебя тоже ой как много.
лол, анонимный клован с мейлареподмывальни, который и не математик, и не программист и даже не компуктер сцайнист (т.е. гуманитарий), или философ критикует величайшего физика современности
максимка, просто лови смачную защёчину и иди дальше cock программируй, слесарь тупой
> анонимный клован
> критикует величайшего физика
Было бы неплохо рассуждать по существу, а не степени величия или низости тех или иных личностей.
Можно подумать, что местные критики Пенроуза хотя бы читали тот же "Новый ум короля".
Но ведь Бурбаки формализируют не только арифметику, но и всю теорию множеств (по сути, система похожа на ZFC). Это тоже можно сделать лямбда-счислением?
> Это тоже можно сделать лямбда-счислением?
В принципе можно, но есть риск заразиться конструктивизмом и бегать потом объяснять всем, что теория множеств не нужна.
Однажды создатели Coq с удивлением обнаружили, что если в него добавить закон исключенного третьего, то аксиома выбора опровергается. После доработки напильником она больше не опровергается. А мораль этой истории в том, что попытки скрестить слона с китом (ZFC с лямбдами) могут привести к неожиданным результатам.
>это чистый конструктивизм, сводить всю математику к арифметике
Нет, это формализм. Программа Гильберта изначально заключалась в том, чтобы свести всю математику к арифметике, арифметику к некой финитной теории, а непротиворечивость этой финитной теории доказать конечным перебором случаев. Оказалось, что так нельзя.
>это делается проще
Нет, это не делается проще. Ты рассказываешь о наивном, неформализованном подходе, когда большая часть идей остаётся просто на уровне размахивания руками. Гильберт все эти идеи четко формализовал в легкочитаемой книжечке "Основания математики". Если ты нашёл в себе силы обмазываться Мартин-Лёфом, то эту книжку ты просто обязан прочитать.
А разве можно в кок исключенное третье добавить? Оно ж невычислимо, как его в calculus'e of construction выразить?
В простых случаях вычислимо, кстати. Гильберт и про это написал.
Книжку почитаю, спасибо. А насчет 'размахивания руками' не согласен. Построения и вычисления таки весомее размахивания руками, как ни крути.
В случае его применения к перечислимым множествам, ага. Но речь'то об исключенном третьем как об аксиоме, т.е. чем'то таком, что истинно в общем случае.
Гильбрет, что забавно, критикует Брауэра именно за недостаток в его интуиционизме построений с вычислениями.
делов-то:
Axiom lem: forall P, P \/ ~P.
хотя чё мелочиться-то:
Axiom fuck: False.
>не только арифметику, но и всю теорию множеств (по сути, система похожа на ZFC). Это тоже можно сделать лямбда-счислением?
Скажем так, не вся лямбда одинаково полезна. В бестиповой и простой типизированной по Черчу нельзя. А вот в любой, включающей в себя лямбда Р (предикатная лямбда (передний правый нижний угол куба) в которой выразим изоморфизм Карри-Говарда), можно. Кок (соответствующий самому дальнему правому верхнему углу куба) включает в себя все остальные варианты как подмножества, поэтому в нем можно сделать ZFC, таки и сделали https://github.com/coq-contribs/zfc
>если лямбда нетипизирована, то можеть зависнуть, а если типизирована, то на каждой формуле надписано доказательство типизированности в специальном исчислении. Так что знаков у тебя тоже ой как много.
Ты о чем? Вот например, в MLTT используется аналог типизированной лямбды, с той разницей что там 4 операции получения выражений - аппликация, абстракция, селекция и комбинация, а вместо типов как таковых т.н. "арности". Т.е. каждое выражение от простой константы и переменной до сложных составных термов имеет соотв. ему арность. Все обозначения, нужные для этого, прямо приводятся, и там нет никаких триллионов знаков.
Помогите, я ничего не понимаю.
Барендрехтом решил обмазаться? Там надо все разбирать с самого начала вообще. Если чего-то не понял, дальше и читать не стоит, т.к. материал дается последовательно и на основе того, за что уже пояснено.
Да вроде и до 2.1.8 всё понятно. А уже совсем непонятные преобразования начались. С fixed point theorem есть какое-то только совсем интуитивное понимание (типа есть функция, которая просто возвращает аргумент и чего-то там еще), какой-то комбинатор, не пойми чего. Но от того что какой-то школьник из Румынии на английской (на слух он мне вообще непонятен) поясняет за это всё (хотя может чуть другое вроде) у меня неплохой такой Барендрехт. Для меня какой-то слишком резкий переход случился в этой книге, не знаю почему, как и что делать.
Вообще, если что-то в лямбде непонятно, лучше гуглить и на примерах разбирать в том же хаскелле. Типа комбинатора неподвижной точки http://www.wikiznanie.ru/wikipedia/index.php/%D0%9A%D0%BE%D0%BC%D0%B1%D0%B8%D0%BD%D0%B0%D1%82%D0%BE%D1%80_%D0%BD%D0%B5%D0%BF%D0%BE%D0%B4%D0%B2%D0%B8%D0%B6%D0%BD%D0%BE%D0%B9_%D1%82%D0%BE%D1%87%D0%BA%D0%B8
А доказательство какой-нибудь теоремы Цермело в такой системе тоже будет выглядеть не слишком длинным?
Wellordering - один из 4х типов в MLTT, вон у Максимки http://groupoid.space/mltt/semantics/ меньше полстраницы занимает.
> Формализм. В изначальном виде закончился крахом программы Гильберта по формализации арифметики и кризисом оснований
Святая толстота. Конструктивисто-сектанты as they are.
Аргументы?..
Чтобы истеризовать тред ещё раз: лоли и интернеты тому, кто объяснит в чём заключается суть операции "дать обоснование математики" и почему это должно кого-то волновать?
Ну если ты занимаешься математикой, тебе неплохо было бы представлять, чем именно ты занимаешься. Это не только математики касается, с любой наукой так.
Это, не полный ответ на вопрос.
Почему не полный? Чего конкретно тебе не хватило в этом ответе?
Какие могут быть аргументы для анимедебила? Если по основаниям математики напишут мангу, я дам тебе знать.
Объясните мне, почему Гильберту было так важно доказать непротиворечивость теории методами самой теории? Ведь этой какой-то замкнутый круг. Теория A либо противоречива, либо непротиворечива. Если теория A противоречива, то мы, конечно, можем доказать в ней её непротиворечивость, но это доказательство нам ничего не даёт. Если же мы доказываем её непротиворечивость, исходя из предположения, что она непротиворечива... ну так при таком предположении нам и доказательство не нужно - мы уже предполагаем её непротиворечивость. В общем, если бы такое доказательство мы и получили, то никакой ценности оно бы не несло, так как мы вполне могли бы получить доказательство непротиворечивости A в теории A при том, что теория A была бы противоречивой.
Ты уже треды путаешь, девочка. Закрой двач и выпей успокоительное.
Теория не может рассуждать про саму себя. Внутри нее можно построить изоморфную ей теорию, но сама теория об этом не "знает".
План такой:
- у нас есть мозги, надо бы их формализовать
- в формализациях бывают баги
- поэтому докажем непротиворечивость формальной системы при помощи мозгов, это будет значить, что там нет багов
- потом перенесём доказательство из мозгов в формализм, чтобы и в доказательстве не было багов
- ???
- либо ПРОФИТ, либо глючная система с глючным доказательством, но второе маловероятно
Насколько я могу понять, описанная схема была бы полезна в следующем случае:
Вероятность того, что доказательство (сделанное неформально) содержит баг мы оцениваем как больше вероятности того, что формальная система (для которой мы доказываем непротиворечивость) глючна. Только в таком случае имело бы смысл переносить наше докзательство внутрь формальной системы.
Но такая вот оценка вероятностей мне кажется сомнительной.
Хотя нет, гоню.
Система глючна => доказательство неверно
Доказательство верно => Система неглючна
Система неглючна => ничего не следует отсюда
Но я ещё сейчас попытаюсь сформулировать мысли...
Мы имеем неформальное доказательства неглючности системы => Система неглючна с вероятностью A (скажем, 90%)
(Мы перенесли доказательство неглючности системы в систему)&(Система глючна) => (Система глючна)
(Мы перенесли доказательство неглючности системы в систему)&(Система неглючна) => (Система неглючна)
Я не вижу, как возможность перенести доказательство в систему может поменять изначальные априорные оценки вероятности того, глючна система или неглючна.
Если, допустим, не сумев перенести доказательство в систему, я расценивал бы отношение вероятностей глючности/неглючности как 10%/90%, то и после перенесения доказательства в формальную систему оценка вероятностей осталась бы прежней.
Кажется, я понял идею "обоснования финитными средствами".
Допустим, мы уверены в непротиворечивости формальной арифметики на 99%.
И при этом уверены в непротиворечивости ZFC, скажем, на 50%.
Если бы утверждение о непротиворечивости ZFC мы смогли бы доказать внутри формальной арифметики, то мы были бы уверены в непротиворечивости ZFC на 99%.
Но из непротиворечивости ZFC следовала бы непротиворечивость арифметики, поэтому внутри формальной арифметики по теореме Гёделя доказать ZFC мы не можем. То есть мы не можем развеять сомнения в непротиворечивости слишком сильной теории, доказав эту непротиворечивость в теории более слабой, в которой мы более уверены.
Я читаю ваше обсуждение, и у меня такое чувство, что вы относитесь к теме как к какому-то мистицизму.
Ну, я как раз пытаюсь осмыслить вопрос наиболее рационально, именно поэтому и использую язык теории вероятностей.
Ладно, посмотрим, что из этого выйдет.
Что почитать по всяких Coq?
>Ну если ты занимаешься математикой, тебе неплохо было бы представлять, чем именно ты занимаешься. Это не только математики касается, с любой наукой так.
не является ответом на
>...кто объяснит в чём заключается суть операции "дать обоснование математики"...
Он хотел не методами самой теории, а "финитарными". По-поводу того, что такое "финитарные методы" он целую книжку написал: интуитивно, всякие комбинаторные рассуждения про значки и как и что из них выводить - это ок, трансфинитные индукции, большие кардиналы и прочее - это не ок. Потом (или сразу, или ранее, не суть) все поверили, что финитарные методы ~ доказуемо в PA (или IE_1 - это по вкусу), а дальше историю ты знаешь.
А что является?
Для начала можно Барендрехта, Lambda calculi with types.
На практике это не так. Как-то раз в HOL4 доказали ложь из-за какого-то извратного бага в бета-редукции. Но доказательства, формализованные в HOL4, выжили.
Даже глючная система может быть практически полезна. Конечно, теоретически она совершенно неинтересна, потому что в ней доказуемо всё. Но даже если такая система ловит 99% человеческих ошибок, она все равно поднимает вероятность, что всё правильно.
Смотря, что тебе надо, если Software Foundations - это одно, а если в ZFC палочкой потыкать, то другое.
Не знаю, но знаю, что ответ на вопрос: "Что такое Х?", не может состоять из оценочного суждения по поводу того, что мне было бы плохо, а что неплохо представлять, если я чем-то там занимаюсь.
Почему бы не взять стековые языки программирования?
>Не знаю,
Ну как узнаешь - приходи.
Для чего ты предлагаешь их взять?
Насколько я слышал сила конструктивистов оказалась их же слабостью, из-за тех ограничений, которые они наложили, они закрыли себе доступ ко многим результатам. Правда ли это?
Давай конкретнее, о каких именно ограничениях и результатах речь?
Понятия не имею.
>1:Ответьте на вопрос Х
>2:А что является ответом на вопрос Х?
>1:Не знаю
>2:Ну как узнаешь - приходи
У тебя ничего с математикой не получится.
Я тебя услышал, иди крути жопой куда-нибудь еще. Научишься внятно вопросы формулировать, тогда приходи.
Если тупой и можешь ответить - не вякал бы, а то воняет весь тред от тебя, а толку - 0.
>Ну как узнаешь - приходи.
В этом и заключается вопроc, тупенький ты наш.
А как же кубическая теория типов(к интуиционистам)? Про неё забыли, а ведь очень клёвая штука, посмотрите.
Там эта унивалентность прямо встраивается в правила вывода.
>А как же кубическая теория типов(к интуиционистам)?
Куб лямбда-исчислений "а-ля Черч" Барендрегта и соотв. ему по изоморфизму Карри-Говарда куб логических исчислений? Так это самый интуиционизм и есть, точнее конструктивизм, но обычно и то и другое используют как синонимы. Все логики в таком кубе априори конструктивные, поскольку лямбда типизирована и логические константы имеют конструктивное значение (пруф-объекты своих типов).
>очень клёвая штука, посмотрите. Там эта унивалентность прямо встраивается в правила вывода.
Да, это очень полезная вещь. Не какие-то там невычислимые объекты веры типа ислюченного третьего.
Почему конструктивность - это хорошо?
А почему плохо? Я заметил, тут у некоторых конкретный такой БАРЕНДРЕХТ от конструктивизма, даже от простого упоминания триггерятся и начинают вести себя как бесноватые на приеме у экзорциста.
так-то я сто раз уже говорил, почему хорошо - потому что вычислимо.
ну так на уровне метатеории классическая математика тоже вычислима (в том смысле, что все утверждения об объектах в ней вычислимы).
Во-первых, любая формальная система есть конструктивный объект, согласно Мартин-Лёфу.
Во-вторых есть вычислимость и вычислимость. В метаматематике "вычислим" и закон исключенного третьего в том смысле, что он не противоречит гильбертовскому исчислению высказываний, например. Однако, ему не во всех случаях может соответствовать вычислимое построение.
Ну раз это согласуется с учением пророка, то аминь.
"Согласно Мартин-Лёфу". Пздц.
Ну так почему первая вычислимость хуже второй вычислимости?
Допустим, у тебя есть предикат пиздатости и ты доказал в классической логике, что существует пиздатое число. Есть только маленькая проблема: у тебя нет никакой зацепки, чтобы это число построить. В каком смысле оно существует? Витает в воздухе вокруг тебя? А если не витает, то может быть, оно на самом-то деле и не существует-то?
А то, что утверждение доказуемо, это-то вычислимо, но это просто факт про скобочки и буквочки. Вдруг это утверждение не имеет никакого отношения к реальности?
Тебе выше правильно пояснили, выводимость чего'то в классической логике не обязана вести к построению этого чего'то, поскольку класмическая логика не рассматривает интерпретацию логических констант, там это просто буковы и их синтаксис без семантики. Полная аналогия такого подхода это выводимость существования Аллаха из корана. Правил его построения из такого доказательства ты не выведешь.
А зачем мне правила построения, объясни?
Правила построения дают возможность работать с объектами построения, доказывать их свойства непосредственно, а не выводить из каких'то заповедей. Гарантированная выводимость, непротиворечивость и отсутствие парадоксов. Классический подход всего этого не гарантирует, а значит не может служить основаниями математики, что доказал кризис оснований.
Где можно увидеть конструктивизм в деле? В каких книгах?
А зачем мне ZFC? Есть, например, такая секта, которая добавляет к ZF аксиому детерминированности (determinacy): в бесконечной игре один из игроков имеет выигрышную стратегию. Всё у них прекрасно: и континуум-гипотеза доказывается, и любое множество действительных чисел измеримо. Есть только маленькая такая проблема: аксиома выбора опровергается.
Вопрос: на каком основании делать выбор между ZFC и ZFD? Нас в детстве учили ZFC, так что пусть будет ZFC? Физический эксперимент может какой-нибудь предложишь?
Что значит "делать выбор"? Это просто две разные теории множеств. Как бывают разные геометрии, так бывают разные теории множеств. Одной единственно верной теории множеств нет.
А как жить без теоремы о среднем, например?
> Как бывают разные геометрии, так бывают разные теории множеств.
Вот не надо тут. Геометрия Лобачевского изучает что-то реально существующее, потому что есть модель Пуанкаре. А почему ZFC/ZFD имеет хоть какое-то отношение к реальности?
Странная постановка вопроса. А если бы у геометрии Лобачевского не было модели в геометрии Евклида, то ты бы воевал против Лобачевского? Я не понимаю твою философию. Объясни, пожалуйста, какими понятиями ты мыслишь. Без этого я не смогу тебе осмысленно отвечать.
Перестать веровать в исключенное третье как в нечто незыблемое, а использовать только в тех случаях, когда оно доказуемо непосредственно.
Мощно, мне нравится. А слабости какие-ти есть у такой позиции? Как доказать исключённость третьего? Это ведь аксиома.
> Мощно, мне нравится. А слабости какие-ти есть у такой позиции?
Никаких нету. У меня Мартин-Леф так даже парадокс Рассела разрулил. Всего лишь переправил определение с общего случая на перечислимую иерархию вложенных универсумов и все. Был парадокс Жирара, а потом вжух, и нету. Это классический подход уже второй век кризис оснований обойти не может.
Охуеть. А исключённое третье?
Походу конструктивизим это то, что я искал.
Бамп вопросу.
А исключенное третье признается не как аксиома, в которую надо веровать, а как нечто, истинное только для случаев доказуемых н'р в логике Гейтинга, безаприорного обобщения на все случаи жизни. Только вычислимые построения, только хардкор.
Yflj xbnfnm d j,otv/ Cgfcb,j/
Ой, ну ты понел. Спс.
Увидеть в действии можно не только в книгах, но и на компе, Coq жи есть. Книг много, начиная с Барендрегта и заканчивая HoTT.
Можно посмотреть на алгебру и анализ?
Анализ есть в книге Бишопа, 60х еще годов. Алгеброй не интересовался. Вообще, есть книжка Гейтинга 'Интуиционизм', там кратко поясняется и за алгебру, анализ, логику и т.д.
>книжка Гейтинга 'Интуиционизм'
Которая написана в стиле шуточного диалога масок?
Геометрия Евклида тут ни при чем, можно и из алгебры состряпать модель (как сам Лобачевский сделал).
Если бы у геометрии Лобачевского не было модели, то да, она была бы бесполезной. Собственно Бойяи, Гаусс и пр. думали в эту сторону, чтобы продемонстрировать независимость пятого постулата от остальных. Если бы модели не было, то ничего б они не добились.
> Объясни, пожалуйста, какими понятиями ты мыслишь.
Смотри, математики пасьянсы из скобочек раскладывают или всё-таки изучают что-то? А если изучают, то что?
Конструктивная математика начинается с описания того, что она изучает. Типа "возьмем в качестве универсума все выражения из скобок и слов". А классическая математика? Скажем, для теории категорий, мы берём ZFC с недостижимыми кардиналами. А в каком смысле эти лихие кардиналы существуют? Стоит ли вообще какой-нибудь смысл за квантором Е?
В конструктивизме квантора существования по сути нет, там просто всегда строится функция или константа, поэтому лишних философских вопросов не возникает.
В лекциях по конструктивному анализу Кушнера сказано, что конструктивный анализ - всего лишь сильно урезанная версия обычного анализа и не содержит ничего, что не было бы открыто ранее. Зато содержит много неудобств. Так, невозможно выяснить, равны ли два производных конструктивных вещественных числа, невозможно сравнивать два произвольных конструктивных вещественных числа, бывают конструктивно непрерывные конструктивно не ограниченные на конструктивном отрезке конструктивные функции, алгоритм поимки льва в пустыне запрещен ибо им можно решить великую теорему Ферма, и прочее в таком духе.
Зато с философской точки зрения это огого. Вот прям вообще ух. Сильно-сильно хорошее, не то что у этого мерзкого Коши-мафиози. Всем учить.
Последний вопрос: теорема Гёделя и конструктивная матемтаика. Как у них дела вместе? Работает там она или нет?
Вот про эти, анон.
Это не ограничения. Как и затыкание невычислимых дыр в анализе актуальной бесконечностью это не решение проблем. Нарисовать знак бесконечности не равно построить ее.
Конструктивные системы полны по Геделю, т.к все что есть в такой системе, выводимо. Поскольку конструктивные системы это построения, как и правила построений и правила проверки этих правил еа корректность это конструктивные объекты, то в такой системе нельзя выразить то, что из нее невозможно вывести или что в ней невозможно доказать.
Математика изучает воображаемые сущности. Эти сущности, согласно неокантианству, расположены в созерцательном пространстве, что даёт возможность делать о них априорные синтетические суждения. Эти суждения называются определениями. Применение к определениям аналитических рассуждений позволяет чётче осознать, чем же являются рассматриваемые (в созерцательном пространстве) объекты.
Проще говоря, математик сначала воображает что-то, затем делает несколько утверждений о воображенном объекте, затем из этих утверждений выводит следствия.
Поместить в созерцательное пространство и начать созерцать можно какую угодно идею. Но не всякие идеи обладают тем изящным свойством, что при их созерцании получается много аналитических суждений, сложным образом связанных друг с другом. Лишь те идеи, при воображении которых достоверно получается много нескучных теорем, изучаются математикой и называются математическими объектами.
Похожей деятельностью занимаются вообще все теоретики - все они воображают. Однако у математики есть всё-таки своя специфика. Говорить о ней я не буду, потому что это слишком интимная вещь. Продолжу разговор о созерцательном пространстве.
Обычно воображается не одна-единственная сущность, но целый сонм сущностей. Этот сонм называется универсумом. Сущности, входящие в универсум, однородны в следующем смысле. Каждое определение можно рассматривать как фильтр, сквозь который одни сущности универсума проходят, другие не проходят. Сущности, которые проходят через фильтр, неразличимы этим фильтром. Так вот, для всякого универсума есть определение, относительно которого все объекты универсума неразличимы. Для универсума теории групп таким определением является группа - все сущности универсума подходят под это определение. Для универсума теории колец таким определением является кольцо. Для метаматематики универсумом является сонм текстов. И т.п.
Для каких-то универсумов есть описания, позволяющие составить представление о сущностях, входящих в сонм, для каких-то универсумов таких описаний нет. Например, для универсума стандартной теории множеств есть описание: именно, под универсумом понимается кумулятивная иерархия фон Неймана. Этот универсум обозначается V. Вместе с тем, легко воображаются универсумы множеств, которые могут напоминать, а могут и не напоминать V. Эти универсумы описываются неклассическими теориями множеств.
Существование понимается относительно какого-то универсума. Если объект x существует относительно U, то это означает, что при воображении универсума U необходимо также иметь в виду и объект x. Несуществование x соответственно означает, что при воображении универсума не следует воображать x.
Конструктивизм занимается ровно этим же самым - исследует воображаемые сонмы сущностей. Однако делает это "со связанными руками", фанатично ограничивая себя требованием вычислимости. Вычислимость, о которой говорят конструктивисты, - воображаемая. Ведь все алгоритмы, которые рассматривают конструктивисты, существуют лишь в воображении конструктивистов. Выполнить эти алгоритмы в реальности невозможно - см. аргумент Вавилова о чернильной дыре. Так, в реальном мире невозможно построить два в степени гугол, несмотря на то, что вообразить алгоритм построения такого числа очень легко. Ибо для построения этого числа потребуется больше атомов, чем есть во всей вселенной. Претензии конструктивистов на якобы большую реалистичность по сравнению с математикой не имеют под собой почвы. Конструктивисты занимаются тем же самым воображением объектов, которым занимаются математики, однако почему-то кричат, что вовсе не пользуются никакими воображением.
У конструктивистов считается, что воображение не может быть связано с реальным миром. Конструктивисты заблуждаются. Например, если я возьму монетку и воображу её падение на землю, а потом действительно брошу монетку на землю, - я увижу почти то же самое, что я вообразил.
Для людей, которые стоят на позициях решительного утилитаризма и оценивают всякую деятельность постольку, поскольку она полезна в народном хозяйстве, также есть аргумент в защиту неограниченного воображения. А именно - математические теории можно рассматривать как черный ящик, как умозрительную машину, шестеренки которой приводятся в движение силой воображения; на вход подаются данные, на выходе получается предсказание. Никому не нужно, чтобы все воображаемые шестеренки такого калькулятора чему-либо соответствовали в реальном мире. Достаточно, чтобы он давал корректный результат при всех задачах, в которых ценное для утилитариста народное хозяйство нуждается. Если совершенно фантастические объекты верно предсказывают надои чугуна, то нет никаких причин требовать от этих объектов быть реальными. Математики занимаются созданием и обслуживаением фантастических шестеренок, строят в своём воображении конструкции, которые нужны лишь для других воображаемых конструкций. Каждый из математических объектов сам по себе для народного хозяйства бесполезен, однако из некоторых математических объектов в конце концов можно собрать очередную машину предсказаний. И нормальная математика справляется с этим куда лучше, чем конструктивизм. Достаточно указать на то, что все воображаемые шестеренки, лежащие под капотом классического анализа, в конструктивизме не существуют, - а вместе с этим невычислимый матан обусловил научную революцию и радикально изменил бытие человечества.
Математики, конечно, не видят смысл своей деятельности в создании калькуляторов. Математики в основном занимаются математикой, которая интересна внутри математики - употребляется в других разделах или даёт повод для воображения и изучения каких-то новых интересных сущностей. Полезные для народного хозяйства калькуляторы получаются непредсказуемым образом, лишь как случайный побочный продукт.
Алсо про безумного портного.
http://lib.ru/LEM/summa/summgl5e.htm
http://lib.ru/LEM/summa/summgl5e.htm
Плохая паста, неосиляторская. Впрочем, если уж Вейль в свое время интуиционизм неосилил, возможно я многого хочу от ноунейма из страны, где математику развивабт не больше чем в центральной африке.
Ты вот любишь говорить про Аллаха. Так вот, если бы Аллах был идеей, которую можно было бы поместить в созерцательное пространство и положить в фундамент красивой ажурной конструкции из аналитических суждений, то Аллах вполне бы был математическим объектом. Просто идея Аллаха на самом деле является очень блеклой и никакой математики не порождает, - это единственная причина, по которой математики не изучают Аллаха.
Существующее богословие на математическую теорию никак не тянет, поскольку является беспруфным алогичным кукареканием.
Почему паста? Ориджинал, только что написал.
Как бы там ни было, написал ты хуйню. Я смотрю, ты даже не очень в курсе, чем синтетическое суждение отличается от аналитического. Про отличие конструктивного подхода вообще набор слов.
Обычно так говорят, когда не могут ничего возразить по существу, но не соглашаются из-за идеологии.
Считай это первым возражением по'существу. Паста большая, хуйни написано много, с тилибона цитировать неудобно, завтра конкретнее напишу с чем не согласен.
Окей. Кстати, теперь я считаю себя вправе называть хуйнёй те твои слова, которые посчитаю хуйнёй.
По мне так тоже хуйня, какая-то платонистская риторика про непостижимые сущности, которые мы можем описывать, воздушные замки и тд
Вообще оба этих дискурса "романтическо-платонистский" и "прагматическо-конструктивистский" уже заебали пиздец как. Сколько можно одно и то же говно в ступе толочь, хоть бы кто что новое вбросил.
>то в такой системе нельзя выразить то, что из нее невозможно вывести или что в ней невозможно доказать.
>Если формальная система S непротиворечива, то формула A невыводима в S; если система S ω-непротиворечива, то формула ¬A невыводима в S. Таким образом, если система S ω-непротиворечива, то она неполна и A служит примером неразрешимой формулы.
Тогда получается, что конструктивная математика противоречива.
>Это не ограничения
>алгоритм поимки льва в пустыне запрещен ибо им можно решить великую теорему Ферма
>невозможно выяснить, равны ли два производных конструктивных вещественных числа
Это ограничения
> затыкание невычислимых дыр
А вот это не ограничения, никто ничего не затыкает, просто существует обозначение для "невычислимо большое". К тому же, раз уж конструктивная математика полна по Гегелю я теперь вообще не уверен, отличается и она чем-нибудь от религии или псевдонаучной теории какой-нибудь, скажем.
Ух, как ты его! Годнота же.
Вот только аргумент Вавилова о чернильной дыре уже обсосали в прошлом треде, разве нет? Конструктивисты не требуют никакой "физической" вычислимости и вообще никак не связывают себя с ограничениями реального мира, так что это рассуждение абсолютно мимо кассы, как мне кажется. Они просто требуют представить правило получения объекта - с дихотомией материальный мир\фантазия это никак не связано. С тем же успехом можно говорить о том, что классические математики фанатично ограничивают себя рамками зфц\классической логики\ю нейм ит - ну, или математики вообще фанатично ограничивают себя тем, что обычно называется рациональным мышлением, в то время как могли бы непосредственно ощущать узоры с разрывами.
Короче, красиво - но немного мимо, как мне кажется.
Потому что ты так сказал? Противоречивость непосредственно выводима в конструктивной системе, если она там есть. Для этого не нужны дополнительные теоремы и т.п. Излишне говорить, что противоречивость конструктивной математики это твои фантазии.
> > затыкание невычислимых дыр
> А вот это не ограничения, никто ничего не затыкает, просто существует обозначение для "невычислимо большое".
Ага, обозначение для Аллаха тоже существует.
К тому же, раз уж конструктивная математика полна по Гегелю я теперь вообще не уверен, отличается и она чем-нибудь от религии или псевдонаучной теории какой-нибудь, скажем.
Я уж понял, что ты ничего не понял.
Положняк таков:
Гильберт и Кантор - авторитеты, чёрная масть
приверженцы классической логики - мужики и стремящиеся
конструктивисты - козлы
интуиционисты - петухи
Марти-Лёф - вафлёр
Брауэр - газонюх
>Конструктивные системы полны по Геделю
>в такой системе нельзя выразить то, что из нее невозможно вывести или что в ней невозможно доказать.
Потому что ты так сказал.
Да, существует. И что? В каком месте это затыкание дыры или ограничение? Как раз наоборот, работа с неограниченным, ограниченные конструктивисты со своей полной по Гегелю очередной манятеорией, которая всё объясняет в такое никогда не смогут.
Я сто раз уже объяснял, в каком. Видимо, таки бесполезно. Ты простую вещь пойми, если бы к классическому подходу не было бы претензий и не было бы вызванного им кризиса оснований, то другие подходы вообще бы не понадобились. А так, обосрались по полной программе наотличненько, еще и кукуреканья в сторону тех, кто показал причину кризиса оснований и пути выхода из него. Затыкать невычислимое всякими актуальными бесконечностями и прочими аллахами, выражая невычислимое через неразрешимое, это путь в никуда. И уж точно это не математика.
Нет, не потому что я так сказал, а потому что так есть на самом деле, достаточно посмотреть хотя бы на варианты типизированной лямбды из куба Барендрегта. Точнее, на правила вывода. Там все выводится из контекста, нет ничего такогл, что нельзя вывести явно из данного контекста по данным правилам. Ну и доказательство непротиворечивости лямбда'исчисления нсть у того же Барендрегта.
> а потому что так есть на самом деле,
Ну так тем более.
Ну так я сто раз говорил: сила конструктивизма его же слабость, сами себя ограничили, закрыли доступ.
>нет ничего такогл, что нельзя вывести явно из данного контекста по данным правилам.
Просто если она непротиворечива, то должна а ней найтись такая формула A, что A и не A невыводимы в ней. А ты мне говоришь, что в конструктивизме вообще всё выводимо.
К слову, в математике Рыбникова тоже всё выводимо. В чём принципиальное отличие конструктивизма от рыбникизма?
> узоры с разрывами.
Решил мемоизировать это дело?
> Лишь те идеи, при воображении которых достоверно получается много нескучных теорем, изучаются математикой и называются математическими объектами.
>Математика изучает воображаемые сущности.
https://www.youtube.com/watch?v=Yawjc4Pg7x8
Нельзя вломить по треугольнику кувалдой. Числа не летают как птицы и на деревьях не растут. Функцию нельзя потрогать.
Если тебе это неочевидно, что ты вообще забыл в этом треде? Только честно.
> Просто если она непротиворечива, то должна а ней найтись такая формула A, что A и не A невыводимы в ней. А ты мне говоришь, что в конструктивизме вообще всё выводимо.
Я тебе привел пример, любое лямбда исчисление. Покажи такую формулу.
> Просто если она непротиворечива, то должна а ней найтись такая формула A, что A и не A невыводимы в ней.
Приведи полную формулировку теоремы Гегеля, а потом посмотри, что утверждаешь ты и найди 10 отличий.
Гегель - это чувак на . У него не было теорем. Даже если это шутка - не смешно.
Смешно очень, по-моему, смешнее только Вротендик или теорема Рохи-Картохи.
Но это же не отменяет того факта, что спорол ты лютую хуйню. Пусть будет Гедель, что это меняет?
Ну и дела. Неокантианство. Мало нам было простого мира идей, так теперь мы можем еще и населять мир идей реальными объектами посредством воображения. Кажется, что-то похожее прозвучало недавно в письме Холмогорова Познеру: "Тысячу лет миллионы людей в этой стране денно и нощно молились Богу с такой истовостью и серьезностью веры, жили в такой плотной атмосфере чуда, что даже если бы Вы и подобные Вам были бы правы, и Бога бы не существовало, то здесь, в России, Он стал реальность."
Вот по чётным дням недели я, например, воображаю множества из ZFC, и они, эти множества, красные. А по нечётным дням я воображаю множества из ZFD, и они синие. А по воскресеньям я просто воображаю действительную прямую и всматриваюсь в эту тварь, пытаясь определить, красная она или синяя. Иногда оказывается, что она зелёная, и при том является чёртиком, и тогда я делаю вывод, что с воображением на сегодня пора завязывать.
> кумулятивная иерархия фон Неймана.
Отличное описание универсума теории множеств через до фига ординалов, где до фига - недостижимый кардинал. Вот оно, оказывается, что такое множества, а я-то думал.
> невозможно построить два в степени гугол, несмотря на то, что вообразить алгоритм построения такого числа очень легко.
Ты, кажется, полагаешь, что десятичная запись - это настоящее число, а алгоритм типа "два в степени гугол" - ненастоящее. Но конструктивная математика не так работает. Любая программа типа число (при некоторых условиях насчёт независания) не просто "возвращает" число, а является им.
> а потом действительно брошу монетку на землю, - я увижу почти то же самое, что я вообразил.
Теперь для демонстрации применимости классической математики к реальному миру осталось только подбросить актуальную бесконечность монеток.
> все воображаемые шестеренки, лежащие под капотом классического анализа, в конструктивизме не существуют
Большинству математиков абсолютно насрать на шестеренки. Кто-то из них говорил, что континуум точно существует, 2^континуум - хз, а 2^2^континуум - точно нет. Джерри Бона припечатал еще лучше: "аксиома выбора очевидно верна, теорема Цермело очевидно неверна, а лемма Цорна - хз". Матанщики начали что-то верещать только тогда, когда им заявили, что неважно, одно у них яичко или два. И то только потому, что это-то они смогли понять, а про существование всяких долбанутых кардиналов никто из них ничего не понял.
>пикча
Лол.
Я не хочу спорить с человеком, который путает Гёделя и Гегеля. Верь хоть в Рыбникизм, хоть в конструктивизм, дело твоё. Отрицай закон исключённого третьего, придумывай как стакан может быть пуст и полон одновременно и тд. Не хочу тратить время.
Но я не путаю Геделя и Гегеля, из этих постов мои только 2. Дело не в этом, а в том, что ты спизданул про рыбникова и Геделя просто чтобы спиздануть, а когда тебя попросили обосновать, сразу слился, доебавшись до орфографии постороннего оратора.
>Не хочу тратить время.
Тебя ИТТ вобще не звали, претензия про потраченное время непонятна. Не хочешь - не трать, никаких проблем. Но если уж пишешь сюда, обосновывай хотя бы.
>мопед не мой
>орфография когда здесь тотальное непонимание
Манёвры пошли, ну да ладно.
> Покажи такую формулу.
Так её нет, в том и суть. По твоим словам всё выводимо.
>В чём принципиальное отличие конструктивизма от рыбникизма?
>Если тебе это неочевидно
Переводишь темы вместо ответа на вопрос.
> а когда тебя попросили обосновать, сразу слился
Это и были твои возражения? Я думал, лучше будет это всё.
Да, математические объекты живут только в воображении людей. "Идеальны", как некоторые говорят. И твои алгоритмы - они ведь тоже почти все идеальны, их нельзя потрогать, они лишь в твоём воображении находятся. Доказать это очень просто - достаточно открыть упоминавшуюся выше книгу Кушнера. В ней алгоритмы изображаются буквами, и нередки обороты вида "пусть B - алгорифм такой-то" (книжка старая, поэтому алгоритмы в ней пишутся через ф). Понятно, что тут вовсе не утверждается, что латинская буква B является алгоритмом. В таких местах читателю предлагается вообразить алгоритм и всякий раз иметь его в виду при встрече с буквой B. То есть речь идёт именно о воображаемых объектах.
Нет причин подвергать анализу одни лишь только те воображаемые объекты, которые являются алгоритмами.
Далее, кумулятивная иерархия фон Неймана - это не просто дофига ординалов. Это иерархия классов Vx, где x пробегает класс ординалов. V0 - пустое множество, Vx+1 - множество всех подмножеств Vx, Va для каждого предельного a - объединение всех Vx, у которых x<a. Объединение всех этих классов и обозначается буквой V. Понятно, что далеко не всякий элемент V будет ординалом.
Что до точки зрения, которую я раскрываю, - она придумана не мной. Ещё Лузину кровавыми коммуняками ставилось на вид заявление "натуральный ряд представляет собой функцию головы математика".
Наконец, точки зрения математиков эволюционируют, меняясь по мере накопления математических открытий. Сейчас некоторые теоретики оснований ведут речь о том, что для разных разделов математики следует использовать разные теории множеств - для общей алгебры ZFC, для анализа ZF+счетный выбор и т.п.
>Это и были твои возражения?
Это не мои. Я бы начал с того, что ты вообще не понимаешь сути "ментального построения" в интуиционизме. Но при этом сравниваешь его с другими, на твой взгляд похожими, явлениями в математике и даже с воображением в общем смысле. Вместе с твоим непониманием разницы между синтетическим и аналитическим суждением этого уже было бы достаточно, чтобы вместо какой-то дискуссии на эту тему предложить тебе делать уроки и собирать портфель. Как поется в той песенке, "не лезь малыш в политику, иди учи матчасть". Но и это не все, до кучи ты так же не понимаешь и идентичности ментального построения в интуиционизме и вычислимого алгоритмического построения в конструктивизме, говоря о том, что "представить алгоритм можно, а реализовать нет", игнорируя тот простой факт, что в конструктивизме (интерпретация логических констант по Колмогорову) алгоритм и результат его работы - это одно и то же, с поправкой на абстракцию потенциальной осуществимости и тонкости касающиеся канонических и неканонических элементов и множеств.
>Так, в реальном мире невозможно построить два в степени гугол, несмотря на то, что вообразить алгоритм построения такого числа очень легко.
Далее, ты абсолютно не понимаешь сути понятия "вычислимость", поскольку не знаком с такими вещами как понятие канонического и неканонического элемента и множества, нормальной формы, теоремы Черча-Россера, лямбда-определимости и ее связи с любыми другими уточнениями понятия алгоритма, это только навскидку. Поэтому более сложные вещи, такие как изоморфизм Карри-Говарда, ВНК-интерпретация и т.д. тебе не понятны тем более. Ты не понимаешь даже в чем разница между неканоническим символом, считающимся в канонический элемент и символом Аллаха или симаолом бесконечности, не считающимися ни во что, поскольку правила такого вычисления отсутствуют. Это все возражения чисто на вскидку, там еще много можно добавить.
"Вам не понять" не является возражением, равно как и взывание к Аллаху. Возражение должно быть логичным набором истинных утверждений. Нельзя сказать "Аллах" и считать, что опроверг собеседника.
Если ты считаешь, что нельзя рассматривать воображаемые объекты, не являющиеся алгоритмами, то будь любезен привести настоящие аргументы.
>Если ты считаешь, что нельзя рассматривать воображаемые объекты, не являющиеся алгоритмами, то будь любезен привести настоящие аргументы.
Рассматривать-то их можно, вот только к математике они отношения не имеют, а уж тем более не могут служить основаниями. Пример - определение множества у Кантора. Очевидно, это воображаемый объект, но не конструктивный объект и тем более не алгоритм. Рассматривать ты его можешь, конечно. Вот только парадоксов это не отменит.
Именно изучение воображаемых объектов и является математикой. А на идеях конструктивизма никакой математики не создано. Ну, если не считать внутренние построения конструктивистов, единственное назначение которых - обслуживание конструктивизма.
Выше реквестировали примеры конструктивной математики. Так вот, их нету. По конструктивному анализу на либгене одна унылая книга, конструктивной алгебры вообще не существует. Конструктивизм - это такая философская секта, которая учит, какой должна быть математика, но никакого вклада в математику не вносит и вообще математикой не занимается. Лишь нескучную терминологию генерирует, для внутреннего потребления.
Конструктивисты говорят, что есть классическая математика, а есть конструктивная математика. Конструктивисты лукавят. Есть математика, великая и неделимая, заключенная в миллионах книг. А есть полтора десятка конструктивистских брошюрок. И вот конструктивисты призывают выкинуть всю математику на свалку, а полтора десятка брошюрок изучать (и больше ничего не изучать). Это какое-то безумие.
>И вот конструктивисты призывают выкинуть всю математику на свалку, а полтора десятка брошюрок изучать (и больше ничего не изучать). Это какое-то безумие.
Вот я и спрашиваю, в чём принципиальное отличие от Рыбникова и ко.
Я тебя услышал. К вышесказанному добавлю, что использовать свое незнание и непонимание темы для обосновывания чего-либо, тем более как точку зрения в дискуссии - это уровень детского сада.
Это разные аноны.
Вот это
не я писал.
>Конструктивистская математика есть, правда-правда. Но мы вам её не покажем, потому что вам не понять. А ваша математика не математика.
Вот-вот, Рыбников стайл. А всё почему? А потому что
>Конструктивные системы полны по Геделю, т.к все что есть в такой системе, выводимо. Поскольку конструктивные системы это построения, как и правила построений и правила проверки этих правил еа корректность это конструктивные объекты, то в такой системе нельзя выразить то, что из нее невозможно вывести или что в ней невозможно доказать.
К чему все это писать вообще? Ну не осилил, не твой уровень, смирись. Бывает.
К тому, что в любой хорошей, годной системе должен быть парадокс. Убираешь парадокс получаешь КалКалыч. Так и живём.
>в любой хорошей, годной системе должен быть парадокс.
С какой стати?
Так Гёдель сказал. К слову,
>Последний вопрос: теорема Гёделя и конструктивная матемтаика. Как у них дела вместе? Работает там она или нет?
ты меня почти убедил обмазаться конструктивной математикой. Если бы на последнйи контрольный вопрос ответил, что да, там есть такие-то и такие-то проблемы, то-то и то-то невыводимо, я бы обмазался. Но оказалось, что это ещё одна объяснялка всего и вся.
Почему же, вполне осилил. Я просмотрел библиографию конструктивистских книжек и статей и утверждаю ответственно: никакой конструктивистской математики не существует.
А Тезис Черча-Тьюринга-Дойча волшебным образом обходится?
Да, есть тут один конструктивный чудик, который думает, что теорема Гёделя о неполноте на конструктивную арифметику не распространяется ибо харе лямбда харе лямбда харе Барендрегт харе лямбда. Но это неправда: конструктивная арифметика не может доказать собственную непротиворечивость. Обмазывайся спокойно.
Лол. Ну надо голову проветрить тогда, а то уже выработал негативное отношение. Проветрю и посмотрю, да. Спасибо. А так я читал как-то мельком, идеи показались интересными. Может тогда ты расскажешь немного об интуиционизме/конструктивизме? Чего достигли, плюсы минусы и тд.
Хотя забей, потом сам почитаю.
Ты объясни, откуда там неполнота, если все выводимо из данного контекста по данным правилам, а кроме контекста и правил ничего не дано?
>харе лямбда харе лямбда харе Барендрегт харе лямбда
Очень смешно. Однако, я ведь обосновываю свою позицию, даже со ссылками на Мартин-Лёфа и т.д.
> читателю предлагается вообразить алгоритм
Рассмотрим три способа использовать воображение:
1) вообразим, что буква B обозначает Windows
2) вообразим, что кардинал Вудина существует
3) вообразим, что мы эльфы и на нас напали гоблины
Конструктивисты же не против всего этого, просто (2) больше похоже на (3), чем на (1).
Ты вот, кстати, ругал богословие за нелогичность, а тот же Гёдель сбацал полностью формальное доказательства бытия Бога. Доказательство бесспорно верное и даже формализованное:
https://github.com/FormalTheology/GoedelGod
Аксиомы у него, правда, странноватые, но когда это останавливало классиков? Сам ведь говорил, что главное, чтобы следствия были интересными.
> для разных разделов математики следует использовать разные теории множеств
>Есть математика, великая и неделимая,
Вот это вот один великий и неделимый анон написал?
> все выводимо из данного контекста по данным правилам, а кроме контекста и правил ничего не дано?
Ты видимо думаешь, что раз истинности в классическом понимании нет, то и от неполноты ты избавлен. Но есть совершенно конкретное утверждение: модель системы в ней самой никогда не докажет ложь. И это утверждение недоказуемо, потому что вторая теорема Гёделя. Можно ли это назвать неполнотой - это другой вопрос, но все обычно считают, что это она самая.
> я ведь обосновываю свою позицию, даже со ссылками
Давай так попробуем:
https://plato.stanford.edu/entries/logic-intuitionistic/
By Gödel's famous Incompleteness Theorem, if HA is consistent then neither HA nor PA can prove its own consistency.
(HA = Heyting Arithmetic - конструктивная арифметика, PA = Peano Arithmetic - классическая арифметика)
Более того, это же доказательство обнаружил Миша Вербицкий и вывел из него существование Ктулху.
https://lj.rossia.org/users/tiphareth/768813.html
https://lj.rossia.org/users/tiphareth/463319.html
>модель системы в ней самой никогда не докажет ложь.
Если ложь выводима в такой системе, т.е. следует из данных правил вывода на данном контексте, то докажет.
>if HA is consistent then neither HA nor PA can prove its own consistency.
Если мы рассматриваем "пруф" как конструктивный пруф-объект, а не как какое-то отвлеченное понятие сферической истины в вакууме, то такой пруф непосредственно выводим, как и его отсутствие (пустой тип). Разве нет?
>Можно ли это назвать неполнотой - это другой вопрос, но все обычно считают, что это она самая.
А с какой стати так считать, не подскажешь?
Думаю это поколение 10-х тоже не будет использовать конструктивную математику. Нужно подготовить всё для поколения 20-х, вот они уже всё смогут.
> пруф непосредственно выводим, как и его отсутствие (пустой тип)
Тут надо аккуратнее говорить, потому что у тебя две системы - одна в другой - и по желанию можно еще завести третью снаружи, из которой можно наблюдать эквивалентность тех двух. А "конструктивный пруф-объект" хрен перенесёшь между уровнями.
> А с какой стати так считать, не подскажешь?
Ну например, чтобы разговаривать с остальными на одном языке. А так можешь назвать это световодозвуконепроницаемостью.
Есть такой интересный феномен "слишком много почему". Это когда вы начиная разбирать какую то область начинаете слишком сильно рыть к основаниям. Формально - действие совершенно правильное, ибо не установив истинность основ, можно ли говорить о движении дальше? да и картина выглядит прочней если под нее подведен крепкий фундамент......однако на практике это часто вырождается в то, во что вырождается наша правовая система - вроде формально все правильно, но процедурные моменты съедают все. То есть, я ограничен временем и силами, а именно это в расчет и не берется. Можно начав копать, так и не дойти до конца, утомившись, забыв для чего все начиналось, да и когда можно останавливаться? в конце концов (и это наверно главный аргумент поста) таким образом я ищу психологическое удовлетворение. В итоге можно так и остаться у разбитого корыта из-за неумерной жадности. Ведь судить о мысли можно только познав ее целиком, но между нулем и единицей находится целая жизнь психологических неудобств, сомнений, давящего непонимания, грызущего чувства, что "под этим кроется нечто иное". Не зря Шопенгауэр пишет в предисловии к своей главной книге, что его книгу читателю придется одолеть дважды - сначала не понимая ничего, а затем видя все целое сразу. Не зря Гегель говорит, что его науку логики можно начинать читать с любого места. К тому же, никто не гарантирует, что я не встречу задачу не по плечу в этом рытье - а скорее всего, только их и встречаю - но ведь нет способа узнать, что задача была не по плечу, кроме того, чтобы потратить на нее кучу времени, с которого мы и начали.....поэтому единственный порою выход - психологически изолировать себя от подобных вопросов и изучать только то, что перед глазами. Этим пользовался Ньютон, когда представлял, что мир наполнен Богом - это позволило ему открыть закон тяготения, не остановившись на деталях. То же и с Коперником. То же и с детьми, которым их наивность служит главным орудием на пути познания нового. Короче, надо быть проще
>у тебя две системы - одна в другой - и по желанию можно еще завести третью снаружи, из которой можно наблюдать эквивалентность тех двух.
А к чему все это анальное шапито? Из самой конструктивной системы можно вывести все, что из нее вообще выводимо. Ну построишь внутри нее такую же, результат-то тот же самый будет.
>А "конструктивный пруф-объект" хрен перенесёшь между уровнями.
Потому тчо как ни крути, результат будет одним и тем же. Так к чему все эти уровни?
> Ну построишь внутри нее такую же
Ну а как иначе теорию доказательств развивать?
> Потому тчо как ни крути, результат будет одним и тем же.
Да нет же, смотри:
докажешь в большой системе, что в большой системе нельзя доказать ложь? тривиально!
докажешь в большой системе, что в маленькой системе нельзя доказать ложь? облом!
Но если большая и маленькая система это одно и то же, как тогда? И еще раз, "доказательство" - это что? Если конструктивный пруф-объект, то он ведь и является своим доказательством. И он будет одним и тем же для того, что ты называешь большой и маленькой системой, разве нет?
> И он будет одним и тем же
Да нет же! Между системами есть изоморфизм, причём с точки зрения сверхбольшой ("нашей") системы это изоморфизм тривиален, но этот изоморфизм нельзя выразить на языке большой системы, потому что где-то обязательно поломаются типы. Вот такая она, неполнота.
>Между системами есть изоморфизм, причём с точки зрения сверхбольшой ("нашей") системы это изоморфизм тривиален, но этот изоморфизм нельзя выразить на языке большой системы, потому что где-то обязательно поломаются типы.
А с чего они поломаются, если они одни и те же для всех систем? И изоморфизм между ними в том, что они эквивалентны. Где и что поломается-то, поясни.
Проиграл с пикчи.
> если они одни и те же для всех систем?
Как же они одни и те же, если они разных типов? Доказательство лжи в большой системе имеет с точки зрения большой системы тип ложь, а доказательство лжи в маленькой системе имеет с точки зрения большой системы тип "доказательство чего-то в маленькой системе".
Ты еще скажи, что 1+1 и "1+1" - это одно и то же.
> Где и что поломается-то, поясни.
Теорема Гёделя не говорит конкретно, где что поломается. В коке я могу сказать, где - большую дизъюнкцию нельзя превратить в малую:
Coq < Definition f (A B: Prop) (D: A \/ B): {A} + {B}.
1 subgoal
A, B : Prop
D : A \/ B
============================
{A} + {B}
f < destruct D.
Toplevel input, characters 0-10:
> destruct D.
> ^^^^^^^^^^
Error: Case analysis on sort Set is not allowed for inductive definition or.
Я не знаю, где и что поломается в конкретно твоём любимом исчислении, но если нигде ничего не поломается, то твоё любимое исчисление противоречиво, потому что Гёдель.
Боже, кто ты такой?
В смысле ты охуенен, пеши есчо.
Проблема в индуктивном определении дизьюнкции?
Он прав, про Гегеля написал я, и это была шутка очевидная, но тебе очевидно нужно чуть снизить пафос, потому что даже беглым взглядом видно, что ты не в теме нихуя совершенно.
Не могу к сожалению, ты прав, я совершенно не разбираюсь в теме, но даже этого обывательского понимания достаточно, чтобы макнуть его в какаху. Другой анон сделал это на гораздо более высоком уровне, мне остаётся лишь наблюдать.
>Не могу к сожалению
Я к тому, что хотел бы снизить пафос, но тут пришли те, кто разбираются и теперь я только укрепился в правоте своей интуиции.
> даже этого обывательского понимания достаточно, чтобы макнуть его в какаху.
Правильно Пелевин в какой'то книжке назвал вас говнометариями. Гуманитарий без говна, это все равно что русский патриот без постоянных мыслей о хуях и жопе. Ты же даже не понимаешь, что там написано.
Вообще, теорема Геделя о неполноте это аналог парадокса лжеца или задаче о двух стульях 'на одном неполнота точена, на другом противоречивость дрочена, куда сам сядешь, куда мать посадишь?'. Очевидно, при любом ответе получается, что отвечающий пидр. В любой формальной системе, в т.ч в любом языке, на котором выращима математика, эта проблема неразрешима. Выходов тут в общемслучае два:
- толстоту толстотой вышибают. Можно поставить вопрос, а сама теорема Геделя, она противоречива или неполна? По аналогии с критерием Поппера, когда можно предложить оратору сфальсифицировать сам этот критерий.
- отказаться от попыток выразить основания математики формально, с помощью любого языка. Тогда приходим в двум актам интуиционизма Брауэра.
- толстоту толстотой вышибают. Можно поставить вопрос, а сама теорема Геделя, она противоречива или неполна? По аналогии с критерием Поппера, когда можно предложить оратору сфальсифицировать сам этот критерий.
- отказаться от попыток выразить основания математики формально, с помощью любого языка. Тогда приходим в двум актам интуиционизма Брауэра.
>- отказаться от попыток выразить основания математики формально, с помощью любого языка. Тогда приходим в двум актам интуиционизма Брауэра.
c интуиционизмом эта мысль имеет примерно нихуя общего.
c интуиционизмом эта мысль имеет примерно нихуя общего.
>Ты же даже не понимаешь, что там написано.
Ага, именно поэтому этот
и этот аноны тоже самое говорят, как раз потому, что я не понимаю, а ты всё понимаешь. Иди нахуй, даун.
>Пелевин
Блядь, ну ты и говноед. Ещё кого-то смеешь гуманитарием называть, быдлоид.
Теорема Гёделя несамоприменима же, она не является формальной системой.или является?
Ты так сказал? Гугли акты интуиционизма.
Является, это формальное доказательство же.
Хуяется, долбоёб. Сейчас бы путать высказывание внутри формальной системы с самой формальной системой. Пошёл нахуй.
Это не формальная система. Формальная система матлогика. В ней уже есть парадокс Лжеца, собственно. Что ты этим хотел сказать?
То и хотел сказать, что теорема о неполноте есть вариант парадокса лжеца. Ну и она так же часть матлогики. Тут другое интересно, какая польза математике от этих софизмов? Доказали возможность закодировать в матлогике неразрешимые парадоксы, так Брауэр об этом 110 лет назад говорил. Что любой язык, на котором выразима математика не нужно отождествлять с самой математикой. К слову, это задолго до Геделя было им сказано.
>вариант парадокса лжеца
Это не вариант парадокса лжеца. Теорема говорит, что такой парадокс должен быть грубо говоря. Не одно и то же ведь. Сама по себе теорема никаких противоречий внутри себя не несёт.
>Ну и она так же часть матлогики.
Нет, ну это ведь разные вещи: формальная система и теорема, построенная в ней.
>Тут другое интересно, какая польза математике от этих софизмов?
Вряд ли есть какая-то пользану кроме сорт оф критерия Поппера, хотя это дуристика на самом деле, просто вот есть они и всё, и в разное время люди пытаются сделать с ними что-то.
>дуристика на самом деле
Просто противоречивость/непротиворечивость тоже ведь в тех же рамках определяется. Получается, что все, кто не с нами, те говно. По нашему же определению.
>противоречивость
Закон противоречия(закон непротиворечия) — закон логики, который гласит, что два противоречащих друг другу суждения не могут быть оба истинными. Если тезис принимает истинностное значение «истина», то антитезис принимает значение «ложь».
А что если в системе не работает этот закон? Как к ней можно применять теорему Гёделя?
> Нет, ну это ведь разные вещи: формальная система и теорема, построенная в ней.
Разные. Но чего стоит формальная система, если в ней выразимы такие парадоксы? Даже больше, чего вообще стоит формализм в таком случае?
> Вряд ли есть какая-то пользану кроме сорт оф критерия Поппера, хотя это дуристика на самом деле, просто вот есть они и всё, и в разное время люди пытаются сделать с ними что-то.
Так получается, что в консерватории править надо, коль скоро теорема Геделя касается вообще любой формальной системы, разве нет?
https://en.wikipedia.org/wiki/Quantum_logic
Вот, например. Если так подумать, то теорема Гёделя применима только к семейству формальных систем, которые не выходят за некоторые рамки околоклассической логики. А она противоречива и все это знают ещё с древности. Потому неудивительно, что во всех таких системах будет противоречивость, унаследованная от классической логики.
Да вот я тоже думаю, дуристика какая-то если честно. Но конструктивизм входит в те формальные системы, на которые распространяется эта теорема. Дело не в законе исключённого третьего просто, а в самом первом законе. На деле ведь очень даже легко оба высказывания, противоречащие друг другу, могут быть истинными. Вова лжец, да, пиздобол знатный, вова честный, да, честный с самим собой. Ну я утрирую, но много примеров можно придумать. Или вот "Ты пидор". Для гея, прочитавшего данное выражение это будет истина, для натурала ложь. Аналогично "Ты не пидор". Если первое прочитает гей, а второе натурал, то оба будут истинными. Просто высказывания на самом деле содержат в себе суперпозицию и становятся истинными или ложными в зависимости от конкретной формулы, от ситуации, от наблюдателя,
Честно говоря мы давно уже пользуемся такой логикой, просто эмулируем её с помощью классической и других. Из-за эмуляции и парадоксы.
> Да вот я тоже думаю, дуристика какая-то если честно. Но конструктивизм входит в те формальные системы, на которые распространяется эта теорема.
Интуиционизм Брауэра не входит. Но его еще Гейтинг дропнул (ученик Брауэра, к слову), правда с оговоркой, что его интуиционистская логика не формализует интуиционизм. По Брауэру, это просто один из языков, в котором может быть выражена математика.
Сложно это всё. Нужно прокачаться как следует, прежде чем к таким вещам приступать.
Нет, теорема Гёделя формулируется в метатеории и существенно использует метаязык.
Метаматематика - не формальная система?
Метаматематика - это наука, начнем с этого.
Ой, все. Ок, метаязык это не формальная система?
Обычно нет. Потенциально есть лестница языков: формальный язык, его метаязык, метаязык метаязыка и т.д. На практике высокие этажи не строят. Тем не менее, они могут быть построены при необходимости.
Но ведь все эти языки - формальные системы. Как пример, у бурбаков в 1 главе 1 го тома.
Нет. Во многих случаях метаязыком является русский язык, например.
Но ведь русский язык при его использовании для описания формальной системы становится просто неканонической символикой для канонических элементов, и вычислим в эти элементы. Nominal definition ежжи, разве нет?
Эта мантра "метаязыком может быть русский язык" меня пиздец бесит. А язык чувств может быть, дебилы блять? Пиздец, основания математики они строят.
> Эта мантра "метаязыком может быть русский язык" меня пиздец бесит. А язык чувств может быть, дебилы блять?
Может. Почему нет?
Проблемы?
Хотел было написать тебе ответку, но потом глянул за что ты топишь.
>Только с развитием вычислительной техники, компьютеров, машинной математики оказалось, что наиболее эффективным языком математических программ для этой техники является язык именно конструктивной математики.
Если вот это правда то ладно.
Да, есть неконцептуальное мышление и восприятие.
Вот учебник:
https://studybuddhism.com/ru/prodvinutyy-uroven/lamrim/vipashyana/pustotnost-lozhnogo-ya
Если долго и упорно вчитываться в каждое предложение подолгу его обдумывая то в конце концов можешь научиться.
Собственно намного превосходит по мощности обычное словесное. Потому что вместо операций и восприятия какого то объекта, напрямую воспринимаешь и оперируешь его свойствами.
Ну и на уровне концептуального мышления не понять ни этот текст, ни вообще ни одно духовное учение. Только когда вывалишься в неконцептуальное тогда и осилишь. Сопровождается некоторым нарастающим чувством, которое затем резко сменяется на понимание и изменение восприятия.
>Только с развитием вычислительной техники, компьютеров, машинной математики оказалось, что наиболее эффективным языком математических программ для этой техники является язык именно конструктивной математики.
Не наиболее эффективным, а единственно возможным. Хотя бы потому что на комплюктере без вычислимости никуда. И да, тот же Тьюринг был конструктивистом, все его значимые работы это конструктивная математика. Алгоритм это вообще изначально конструктивное понятие, как и компьютерная программа. Поэтому вдвойне смешно как школьники копротивляются против конструктивизма, используя его плоды.
Ты это, ссылки давай на книжки об этой фигне, но что б понятные были. И желательно что бы требовался не математический бэкграунд, а программерский.
>желательно что бы требовался не математический бэкграунд, а программерский.
Такие вряд ли есть. Все-таки это прежде всего математика. Посмотри "Типы в языках программирования" Пирса, Type Theory & Functional Programming, Simon Thompson, из того что я знаю в этих минимум математики. Есть еще такая книжка, http://gen.lib.rus.ec/book/index.php?md5=F54C47275837DBC876940E067DB9FF0E попытка ученика Мартин-Лёфа изложить MLTT на пальцах, как по мне у него не очень вышло, но книжка довольно годная, хотя и сложнее чем хотелось бы. Вообще, классика жанра - http://www.cse.chalmers.se/research/group/logic/book/book.pdf самое полное и авторитетное изложение MLTT, но бэкграунд нужен выше среднего по этой теме, хоть авторы и заяляют, что книжка "self-contained".
Спасибо, глянем-с.
За сигнифицизм кто-нибудь что-нибудь пояснить может?
Рома?
Неа. Да и я даже не буддист если что.
А кто? На основании чего описываешь субъективный опыт постижения метапустотности? Имеет ли это непосредственное отношение к основаниям математики?
А оно сильно важно?
>На основании чего описываешь субъективный опыт постижения метапустотности?
Че то я тут не понял чего ты хочешь.
Имеет ли это непосредственное отношение к основаниям математики?
Естественно. Вы же должны копнуть так глубоко как это возможно что бы найти правильные основания. И умственный метод постижения того что я кинул по ссылке довольно сложен и может и вообще возможен только для людей с определенным складом ума, которых здесь точно больше чем где либо на борде.
Это просто дверка из одного мирка мышления в другой, более мощный и включающий в себя первый как часть.
Ну, без этого вся ваша математика выглядит очень бедно.
> вся ваша математика
Хорошо, я тебя услышал.
> Вы же должны копнуть так глубоко как это возможно что бы найти правильные основания.
Глубже Брауэра в смысле поиска оснований в ментальных построениях все равно никто пока не копнул. Но это не предел, т.к. сам Брауэр не идет дальше кантианского понимания праинтуиции, в его время не были известны нейрофизиологические субстраты восприятия времени и основанные на нем интуиции натурального числа и континуума. Это сейчас все это изучено довольно глубоко, но зато сам интуиционизм в брауэровском понимании дропнули.
Что-то много букв, есть какие-то основные принципы Бауэра?
Есть, конечно. Причем, там и букв не очень много. Вся суть это два акта интуиционизма пикрелейтед, но там надо пояснять, что он имел в виду. С телефона хз как ссылки дать, а с браузера на компе мейлру не работает. Кембриджские лекции Брауэра, например. На либгене есть. По хардкору и с комментариями - van Stigt, 'Brouwer's intuitionism', 3я глава.
А что про книгу Гейтинга про интуиционизм скажешь?
Гейтинг первый же и дропнул изначальные идеи Брауэра. Книжка неплохая, тем более советское издание с комментариями Маркова. Но это уже больше конструктивизм чем интуиционизм как его понимал Брауэр.
И у меня не работает, капчую с Германии теперь.
дяденьки-профессора помогите разложить анону второкласснику все по полочкам
все положения математики не противоречат философии Платона(или даже сводятся к ней) , то бишь:
1)Есть нечто(информация/универсум).
Аналогия свет.
2)Оно отображается в бесконечномерном пространстве(множестве), которое производит выборку информации: словно стекло, которое отражает одни фотоны и пропускает другие(отношения на множестве,система)
Поправьте меня если что не так.
все положения математики не противоречат философии Платона(или даже сводятся к ней) , то бишь:
1)Есть нечто(информация/универсум).
Аналогия свет.
2)Оно отображается в бесконечномерном пространстве(множестве), которое производит выборку информации: словно стекло, которое отражает одни фотоны и пропускает другие(отношения на множестве,система)
Поправьте меня если что не так.
>Глубже Брауэра в смысле поиска оснований в ментальных построениях все равно никто пока не копнул. Но это не предел, т.к. сам Брауэр не идет дальше кантианского понимания праинтуиции, в его время не были известны нейрофизиологические субстраты восприятия времени и основанные на нем интуиции натурального числа и континуума. Это сейчас все это изучено довольно глубоко, но зато сам интуиционизм в брауэровском понимании дропнули.
Принято считать, что ограниченность науки в изучении психических процессов состоит в том, что в кругу прочих возможных объектов исследования она избирает те, что хотя бы потенциально могут быть обнаружены в материальной реальности и поддаются измерению. Именно поэтому она предпочитает опираться на свет, который проливают инструментальные исследования мозга, притом что сама темнота этого предмета остается все такой же непроницаемой.
Тем не менее, Лакан показывает, что причина малых успехов нейрофизиологии не в этом, а в том, что наука стойко избегает коллизий, связанных с работой означающего. Это и является причиной, в силу которой она отделена стеной от феномена, к которому Фрейд подошел с такой легкостью — к феномену сновидения.
От Лакана мы знаем, чем эта легкость была оплачена — Фрейд взял ее в долг у лингвистики, как раз открывшей для себя к тому времени существование означающего. Тем не менее, произведенный Фрейдом продукт оказался лингвистике не нужен — Фрейд извлек из него совершенно особую логику, ставшую основой самостоятельной психоаналитической науки.
Наука эта способна объяснить некоторые примечательные явления, связанные с нарушением обычного процесса протекания сновидения. Так, когда некто видит «осознанный» сон, полагая, что его осознанность доказывается лишь тем, что он в этом сне способен сказать себе «я вижу этот сон», или просыпается от случайного звука, который задним числом оказался встроен в сновидение так, что к моменту внезапного пробуждения сон оказывает логически завершен, то все эти процессы обязаны именно работе означающего. Эта работа и обуславливает возможность занять в своем сне метапозицию, превратив его в люцидный, или же увидеть сон именно по той причине, что процесс сна оказался прерван — то есть, сделать невозможное и успеть сам пробуждающий стимул обыграть как полноразмерное сновидение.
Там где «строгая» наука, также соблазненная этими загадочными явлениями, в итоге с ними не справляется и, перебрав разнообразные физиологические причины, уступает место паранаучным догадкам, психоанализ объясняет их структуру и показывает, что все эти труднопостижимые трюки становятся возможными, поскольку работа означающего задает особый порядок времени.
По всей видимости, иные психические акты, происходящие в бодрствовании — такие как смех, забывание, принятие решения — в своей логике временного сбывания устроены так же сложно, как и нарушенное, прерванное сновидение. Это лишь подтверждает ту блеснувшую у Фрейда догадку, что само бодрствование — не что иное, как нарушение сна.
Принято считать, что ограниченность науки в изучении психических процессов состоит в том, что в кругу прочих возможных объектов исследования она избирает те, что хотя бы потенциально могут быть обнаружены в материальной реальности и поддаются измерению. Именно поэтому она предпочитает опираться на свет, который проливают инструментальные исследования мозга, притом что сама темнота этого предмета остается все такой же непроницаемой.
Тем не менее, Лакан показывает, что причина малых успехов нейрофизиологии не в этом, а в том, что наука стойко избегает коллизий, связанных с работой означающего. Это и является причиной, в силу которой она отделена стеной от феномена, к которому Фрейд подошел с такой легкостью — к феномену сновидения.
От Лакана мы знаем, чем эта легкость была оплачена — Фрейд взял ее в долг у лингвистики, как раз открывшей для себя к тому времени существование означающего. Тем не менее, произведенный Фрейдом продукт оказался лингвистике не нужен — Фрейд извлек из него совершенно особую логику, ставшую основой самостоятельной психоаналитической науки.
Наука эта способна объяснить некоторые примечательные явления, связанные с нарушением обычного процесса протекания сновидения. Так, когда некто видит «осознанный» сон, полагая, что его осознанность доказывается лишь тем, что он в этом сне способен сказать себе «я вижу этот сон», или просыпается от случайного звука, который задним числом оказался встроен в сновидение так, что к моменту внезапного пробуждения сон оказывает логически завершен, то все эти процессы обязаны именно работе означающего. Эта работа и обуславливает возможность занять в своем сне метапозицию, превратив его в люцидный, или же увидеть сон именно по той причине, что процесс сна оказался прерван — то есть, сделать невозможное и успеть сам пробуждающий стимул обыграть как полноразмерное сновидение.
Там где «строгая» наука, также соблазненная этими загадочными явлениями, в итоге с ними не справляется и, перебрав разнообразные физиологические причины, уступает место паранаучным догадкам, психоанализ объясняет их структуру и показывает, что все эти труднопостижимые трюки становятся возможными, поскольку работа означающего задает особый порядок времени.
По всей видимости, иные психические акты, происходящие в бодрствовании — такие как смех, забывание, принятие решения — в своей логике временного сбывания устроены так же сложно, как и нарушенное, прерванное сновидение. Это лишь подтверждает ту блеснувшую у Фрейда догадку, что само бодрствование — не что иное, как нарушение сна.
метафизические пассажи уже не в моде нихуя, никто на них ставки не сделает сегодня
Нет причин читать Лакана или Фрейда. Ума это не прибавит.
Тебе - наверняка (как и что либо вообще).
да, но аналогия бывает уместной, а бывает нет. задам вопрос иначе: выше прведенные аналогии уместны для понимания мат.понятий или нет?
По мне так неуместны, как и любые другие метафизические пассажи, потому что не в моде нихуя.
Впрочем, Вротендик вон 2к страниц заебашил про какие-то лучи в тёмной комнате (видение), божественные воздушные замки и прочие узоры с разрывами, так что кто-то такими вот пассажами истеризуется до такой степени, что всю жизнь из них мотивацию черпает. И норм.
Ну вообще нет. Неявно мб каждый математик в той или иной степени платонист, но в общем случае математика к платонизму не сводится, конструктивная уж точно.
Есть даже лингвистические основания математики, т.н. сигнифика Маннури. Там тоже все связано с семиотикой и прочим таким. Но инфы по этой теме даже на английском маловато, в основном оригиналы на датском. Так что Лакан этот твой вряд ли что'то может добавить в математику помимо того, что в нее уже добавили ребята из венского кружка сто+ лет назад.
ебень, зачем ты слушаешь полоумного школьника, который не смог осилить 70 страниц зорича?
фильтруй информациию, все, что он пишет - говно
А с чего ты взял, что всё написанное тобой не школьное говно?
Щас бы credentials'ами померятся бы с двачером, который ничего сложнее Зорича не читал...
Может быть. Но фишка той штуки в другом маленько.
>Лакан
Это не тот дешевый шут, которого обоссали в одной популярной книжке за неадекватное ничему разумному употребление математических терминов в своей шизофазии?
Да
не, это Лакан обстоятельно пояснил за весь научный дискурс, а Докинз и приближённые просто тонну баттхёрта на бумагу высрали, как какие-нибудь школьники Ларинофаги
Пришло время запостить "пояснения" Лакана.
...
Эта диаграмма (лента Мебиуса) может быть рассмотрена как основание некоей изначальной надписи, находящейся в ядре, конституирующем субъекта. Это значит гораздо больше, чем вы сперва могли бы подумать, поскольку вы можете поискать тип поверхности, способной принимать такие надписи. Вы, возможно заметите, что сфера, древний символ цельности, не подходит. Подобный разрез способны принимать на себя тор, бутылка Кляйна, поверхность cross-cut[16]. Причем само разнообразие весьма важно, поскольку оно многое объясняет в структуре душевных заболеваний. Если субъект можно символизировать таким фундаментальным разрезом, то точно так же можно показать, что разрез на торе соответствует невротическому субъекту, а разрез на поверхности cross-cut — другому виду душевного заболевания.
...
В этом пространстве наслаждения взять нечто ограниченное, закрытое — это взять место, и говорить о нем — это значит заниматься топологией.
...
Здесь я предлагаю ввести термин «компактность». Не может быть ничего компактнее зазора, если понять, что, допуская существование пересечения всего того, что закрывается, на бесконечном числе множеств, мы приходим к выводу, что пересечение включает в себя это бесконечное число. Это и есть определение компактности.
...
Формулу нам дает та топология, которую я охарактеризовал как самую позднюю по времени возникновения, поскольку она отправлялась от логики, построенной на исследовании числа, которое привело к заданию места, которое не является местом гомогенного пространства. Возьмем все то же ограниченное, закрытое, предположительно устойчивое место — эквивалент того, что я только что сказал о пересечении, расширяющемся до бесконечности. Если предположить, что оно покрыто открытыми множествами, то есть множествами, исключающими своей предел — предел, чтобы вам это вкратце напомнить, — это то, что определяется как большее одной точки и меньшее другой, но никогда не равное ни отправной точке, ни конечной[20] — обнаруживается доказательство того, что равным образом можно сказать так: множество этих открытых пространств всегда поддается неполному покрытию открытыми пространствами, задающими конечность; то есть последовательность элементов задает конечную последовательность.
...
Субъект в той половине, где он определяется отрицаемыми кванторами, относится к тому, что ничто существующее не создает предела функции, что невозможно удостовериться в чем бы то ни было, относящемся к универсуму. Таким образом, если основываться на этой половине, «они», женщины, не «не все», и, следовательно, отсюда же получается, что ни одна из них не является также всей.
...
Мы в свою очередь будем отправляться от того, что выражает буквенное сокращение S(∅), то есть от означающего.
Поскольку тем самым связка означающих дополняется, это означающее может быть лишь чертой, которая прочерчивается из круга означающих, не имея возможности быть подсчитанным в нем. Это символизируется внутренней связью (-1) с множеством означающих.
Как таковое его нельзя произнести, но не его действие, поскольку это действие совершается всякий раз, как произносится собственное имя. Его высказывание равно его значению.
Откуда вытекает следующая формула, если подсчитать это значение в используемой нами алгебре:
S(означающее) / S(означаемое) = S(высказывание)
а при S=(-l) мы имеем: s=√-1.
...
Вот каким образом эректильный орган начинает символизировать место наслаждения, причем не сам по себе и не в качестве образа, а как часть, недостающая желаемому образу: поэтому-то его и можно приравнять к √-1 более высоко произведенного значения, к √-1 наслаждения, которое он восстанавливает посредством коэффициента своего высказывания в функции нехватки означающего.
А в чём проблема? В "У-у-у НЕНОУЧНО, у нас за такое в НОУЧНОЙ ЛАБОРАТОРИИ убивают нахуй" или в чём-то другом? Он пользуется нужными ему частями математического тезауруса в своих целях, для достижения нужного ему эффекта.
Школьником быть хорошо, столько свободного времени, хочешь — ботай, хочешь — играй. Много всего интересного, много сил и энергии, на душе легко. Не понимаю, почему быть школьником зазорно. Куда лучше, чем быть занудным дяденькой, франтующимся перед каждым встречным своим интеллектуальным взглядом на вещи.
Это для тебя шизофазия. А для обычных людей это гениальные измышления великого математика и философа Лакана.
Набор слов, гуманитарный поток сознания. Причем тут математика и основания?
Нет, это не так.
мимо пубертатный невротик, которого все считают поехавшим
У меня Барендрехт от того, что там нет доказательства от противного.
> У меня Барендрехт от того, что там нет доказательства от противного.
Конструктивное доказательство - это построение. В общем случае методом от противного невозможно получить такое построение или хотя бы правила построения. Если в каком'то конкретном случае можно, то такое доказательство вполне конструктивно. Как и с исключенным третьим, принимаются только случаи, когда оно доказуемо непосредственно, а не вера в априорную применимость этого принципа.
Не суди остальных по себе, глупец. Если у тебя не было детства, это не значит, что его не было у всех школьников.
Господа, а ведь можно считать конструктивным доказательством от противного построение игры двух агентов, если показать, что фальсифицирующий агент всегда проигрывает. Что скажете?
У такого подхода есть большая проблема: что, если игрок хочет тянуть время до бесконечности? Придётся разрешать бесконечные игры, но это неконструктивно.
>Придётся разрешать бесконечные игры, но это неконструктивно.
Ну такое, есть методы
Если взять игру, где из проигрыша одного однозначно следует выигрыш другого, то в конкретно этом случае доказательство от противного будет носить конструктивный характер, т.к. оно построимо непосредственно, либо следует из правил игры. Но это никак не значит, что доказательство от противного применимо как общий метод в математике.
>Формализм
>Логицизм
>Интуиционизм
Поясните за всю эту фигню. В математике есть школы(и их3?), тип как в философии всякой? Я всегда думал что математика одна и монолитна, еще там с греков из одних и тех же аксиом всё выводят всё по логике там железобетонно, а тут шляпа какая то. А какой математике в школе учили?
>Логицизм
>Интуиционизм
Поясните за всю эту фигню. В математике есть школы(и их3?), тип как в философии всякой? Я всегда думал что математика одна и монолитна, еще там с греков из одних и тех же аксиом всё выводят всё по логике там железобетонно, а тут шляпа какая то. А какой математике в школе учили?
Комментарий - огонь. "Мнения лакановских аналитиков расходятся" и установить, чьё мнение верно, а чьё - нет, конечно, никак невозможно, потому что психоанализ не фальсифицируем.
В том то и дело, что эти цели не имеют никакого отношения к науке.
Вот каким образом эректильный орган начинает символизировать место наслаждения, причем не сам по себе и не в качестве образа, а как часть, недостающая желаемому образу: поэтому-то его и можно приравнять к Ö-1 более высоко произведенного значения, к Ö-1 наслаждения, которое он восстанавливает посредством коэффициента своего высказывания в функции нехватки означающего: (-1). (Лакан)
Ö - это корень.
Если корень из -1 - это эректильный орган, то что для Лакана многочлен?
Наброшу, пожалуй. Если не веровать в мировую душу и мир идей, как ни крути, а выходит, что математика это продукт деятельности человека. Причем, вне прикладухи и прочей десятой культуры, в общем случае не связана с физикой и т.п объективным. Математика при этом, даже сколь угодно сложная, всегда выразима в естественном языке, т.к все термы, формулы и т.п вербализуемы. Итого, основаниями математики может быть только язык, психолингвистика. Т'е нечто изначально неточное. Получается, что вера в абсолютную точность математики это просто суеверие, т.к основанное на неточном точным и абсолютным быть не может, ну если не веровать во всякий платонизм.
Значительная часть математики невербальна. Картины да Винчи могут быть описаны словами, но да Винчи не писал описания картин, он рисовал.
> Значительная часть математики невербальна.
Покажи, что в математике нельзя описать словами. Вот есть формула, у всего в этой формуле есть название. Любой математический текст можно зачитать вслух, грубо говоря.
Добавлю, если не зачитать, то записать. Текст это такой же язык.
Пикрелейтед можно описать текстом, но пикрелейтед - не текст. Так же и с математикой. Формулы - это всего лишь описание знания, но не собственно знание.
>Формулы - это всего лишь описание знания, но не собственно знание.
Что тогда по-твоему знание? Что-то из мира идей и прочей мировой души? Ты веришь в знание, которое невербализуемо?
>Пикрелейтед можно описать текстом, но пикрелейтед - не текст.
Текст. Твой пикрелейтед - всего лишь 3хмерный тензор, 3 матрицы градаций синего, красного и зеленого (мб еще канал прозрачности), т.е. это чистые циферки, текст. Далее, математика - это таки текст, в математике нет ничего, что нельзя записать, т.е. выразить текстом, т.е. в конечном счете свести к этому тексту. Более того, формально-аксиоматический подход - это вообще чистый текст без оговорок. По теории уровней языка Маннури, есть 5 уровней текста пикрелейтед. Все они производные от первого уровня и отличаются между собой только степенью применимости к тексту данного уровня формализации, причем эта разница чисто количественная, качественной разницы между уровнями нет. 1ый уровень формализовать очень сложно, если вообще возможно (это н-р разговорный язык детей), 5ый по-сути, формализм в чистом виде (н-р матлогика).
Ты путаешь символ и значение символа.
Любое значение символа так же выразимо в языке, н-р широко применяемое в конструктивных логиках т.н. nominal definition. Далее, чистый формализм изначально отказывается рассматривать значение знака, знакосочетания и правила работы с ними это только синтаксис, без семантики. Эта тема хорошо раскрыта у Бурбаков.
Няш, не трогай бурбаков. По-хорошему тебе советую. Тут есть некоторые люди, которые действительно прочитали книжку Бурбаки и могут насовать тебе хуев за воротник. Так что не говори о бурбаках, не стоит.
>не стоит вскрывать эту тему, вы молодые шутливые...
Я тебя услышал. А если предметнее? Вот конкретно мной про Бурбаков написанное, что там не так?
Генерал открыто утверждает, что математика не является всего лишь игрой в символы. Он даже ввел специальное обозначение для выделения тех участков текста, которые объясняют идею, стоящую за тем или иным определением/теоремой. Для Бурбаки аксиоматический метод - просто удобный способ избежать ошибок в математической работе, Бурбаки отнюдь не сводит математику к составлению текстов.
Ладно, более конкретный вопрос. Что именно в математике не вербализуется и не сводится к языку в широком понимании его (н-р в виде 5 уровней, см.выше)?
Читал ли ты "Плач математика"?
Не читал. Сейчас погуглил, судя по всему там как раз о том, что математика - это вид человеческой деятельности и лучше обучать ей детишек не через заучивание формализмов, а более естественным образом. Сигнифика как раз об этом, Маннури критиковал Гильберта именно по той причине, что он недооценивает значение эмоций и т.п. психолингыистических аспектов математики, а сводит все к манипуляции с символами. Но любой язык выводится из языка 1го уровня, в т.ч. и строго формальный, поэтому отрывать язык от его происхождения это неправильно. Все эти соображения никак не противоречат тому, что математика - это языковая деятельность человека.
>Суть математики — в игре и в поиске. Доказать, например, теорему Пифагора — весьма и весьма увлекательный квест для ребёнка. Проблема только в том, что на уроках дети не решают задачи, а всего лишь заучивают наизусть чужие решения, изложенные при этом заумным (даже для взрослого математика) языком.
Возможно мышление вообще без языка. Оно проявляется, например, при глубокой концентрации, при внутреннем созерцании идеи. Речь не о воображении трехмерного тела, конечно.
>Возможно мышление вообще без языка. Оно проявляется, например, при глубокой концентрации, при внутреннем созерцании идеи.
Идеи, которая в любом случае вербализуема. Если ты читал Кастанеду, у него есть понятие "тоналя" и "нагуаля", второе - это как раз деятельность, возможная после остановки внутреннего диалога. Но опять же, при желании оно сводится к первому.
Картину можно описать словами. Но словесное описание картины не будет картиной.
Зависит от языка. Я тебе выше показал, что таки будет. Нейросети так и распознают картинки, аппроксимируя функцию с тегами в области значений и тензорами в области определения. Это во'первых. Во'вторых, ты так и не ответил, причем тут математика и картина, и что конкретно в математике невербализуемо.
Интересно вы успели придти к соотношению карты и территории.
Ну, и если так интересует именно сознание, разум, вот это всё, но не хотите упасть куда-то совсем дебри, то могу посоветовать принять точку зрения функционализма (философия сознания) на этот вопрос, а дополнительно можете почитать, например, Джефф Хоккинс "Об интеллекте". Фактически, в этой книге говорится, что в новой коре мозга (а она собственно и отвечает за процесс мышления) нет ничего кроме памяти и прогнозирования (предсказания). Ну, это конкретно новая кора, мало рассматривается рептильный мозг и прочее. Книга научно-популярная вроде как.
Ну, и если так интересует именно сознание, разум, вот это всё, но не хотите упасть куда-то совсем дебри, то могу посоветовать принять точку зрения функционализма (философия сознания) на этот вопрос, а дополнительно можете почитать, например, Джефф Хоккинс "Об интеллекте". Фактически, в этой книге говорится, что в новой коре мозга (а она собственно и отвечает за процесс мышления) нет ничего кроме памяти и прогнозирования (предсказания). Ну, это конкретно новая кора, мало рассматривается рептильный мозг и прочее. Книга научно-популярная вроде как.
Научпоп не нужон кроме разве что Рамачандрана, чувак мощно задвигает, какие-то глобальные теории уровня "что есть интеллект" тем более. Нейролингвистики для нужд сигнифицизма как оснований математики более чем достаточно, для брауэровского неоинтуиционизма достаточно моделей АТОМ и МТ (metaphor theory).
А, как-то забыл где я нахожусь. Ну, есть различные модели Искусственного Интеллекта, которые впрочем нельзя вычислить в нашей Вселенной. Это Solomonoff induction (фактически, всё строится именно на ней), AIXI и UAi в целом.
В общем, там суть в переборе программ. И есть, например, даже версия почему природа выбрала именно нейросети в качестве аппроксимации индукции Соломонова. В общем, не знаю, может вы там будете читать сверхсерьезные статьи, но если погуглить "lesswrong solomonoff induction" то там есть хорошие статьи по этому всему для самых маленьких и рядом можно найти тоже по сходной теме, для самых маленьких, подчеркиваю.
Есть разница между вещью и моделью вещи, между картиной и текстовым описанием картины.
Как минимум, невербализуемы мысли и чувства, которые заставляют математика выбирать именно те слова, которые он выбирает, и писать именно те тексты, которые он пишет. Посмотри, например, на себя. Ты ведь не можешь заменить себя каким-нибудь текстом, ты не текст. И даже просто понять, каким образом ты разговариваешь, ты не можешь. Если ты попытаешься проанализировать, что происходит в твоей голове при разговоре, если ты внимательно сконцентрируешься на том, почему ты строишь свою речь так, а не иначе, - ты просто лишишься способности говорить и не напишешь ни слова (аналогично если сказать тебе, что ты дышишь, то ты ненадолго потеряешь способность свободно дышать). Потому что тексты ты генерируешь бессознательно, актом невербализуемого мышления. Мышление тут совершается несомненно, ведь если бы мышления не было, то ты бы генерировал белый шум, но ты генерируешь осмысленные тексты. И это мышление не является текстом, потому что ты не мыслишь словами вроде "первым словом, которое я скажу, будет слово 'Интересно'", ты просто берешь и разговариваешь.
>невербализуемы мысли и чувства, которые заставляют математика выбирать именно те слова, которые он выбирает, и писать именно те тексты, которые он пишет.
Выбранные слова и написанный текст в данном случае и является вербализацией психолингвистических процессов, их внешним проявлением, функцией от них. Ведь именно эти процессы в конечном счете и породили выбранные слова и текст, а не другие и не чистый рандом. Т.е. язык, в т.ч. математический, это прямое проявление психолингвистических процессов, стоящих за этим языком.
Но не сам процесс. Математический текст - это не единственный результат мышления математика, есть и другие результаты. Например, изменение состояния ума математика.
Вербализация - внешнее проявление психолингвистических процессов, породивших ее. В этом суть любой языковой деятельности человека, в т.ч. математики. Сами эти процессы можно полностью выявить нормальной нейровизуализацией, это чисто техническая проблема. В наше время не существует неинвазивных методов прямой записи ионного тока в ЦНС, без втыкания туда электродов и т.п. порнографии. Как только такие методы появятся, можно будет напрямую связать психолингвистические процессы и порождаемую ими вербализацию, т.к. такая связь будет напрямую выводимой из данных и т.о. вычислимой функцией, аппроксимируемой любым подходящим методом идентификации систем.
Тем не менее, по состоянию на "прямо сейчас" математика к текстам не сводится. Предлагаю вернуться к этому разговору, когда описанное тобой светлое будущее настанет.
>по состоянию на "прямо сейчас" математика к текстам не сводится.
Сводится, в целом сгодится и fMRI высокого разрешения. Модели АТОМ и МТ так и получили. Общие же соображения на этот счет были высказаны почти 100 лет назад и их опровергнуть нечем. Формализм, опять же, это чистый синтаксис и манипуляции с текстом. А это такие вещи как ZFC, например.
Хорошо. Ты утверждаешь, по сути, что человек - набор рентгеновских снимков. Тогда почему у рентгеновских снимков нет прав человека? Почему они не подают в суд?
>Ты утверждаешь, по сути, что человек - набор рентгеновских снимков
Этого я не утверждал. Скажем, элементы нейровизуализации это неканоничные представления каноничных элементов - ионных токов, вычислимых одно в другое в качестве nominal definition. То же с вербализацией.
Суть в том, что программа, которая не исполняется ни одним исполнителем, отличается от программы, которую прямо сейчас исполняет некоторый исполнитель.
Это отличие хорошо бы доказать. А то если речь о вышеупомянутой ZFC, то эта "программа" одна и та же как при наличии ее исполнителя в данный момент, так и при его отсутствии. Т.е. формализованный язык хоть и является производным от первичного и т.о. является продуктом языковой деятельности человека, но при этом в основе его правила механического манипулирования со знаками и знакосочетаниями на этом языке, т.е. такой язык можно использовать в пруверах и результат доказательства теоремы н-р не будет отличаться от сделанного на этом языке человеком. Соседний тред как раз про один из таких пруверов - metamath.
Доказать это очень легко: оцифруй человека, запиши его на болванку и положи в шкаф. Если он оттуда умудрится подать на тебя в суд или совершить иное действие, которое может совершить исполняемый каким-нибудь физическим телом этот же человек, то я буду очень сильно удивлен.
Это же ты автор этой пасты да? Очень заметно.
Угу. Только не надо воспринимать её слишком всерьёз, я просто набрасывал тогда.
Ну так вот, как я и написал выше, всякие общие теории интеллекта и т.д на текущем этапе их развития обсуждать смысла нет. Но по вопросам нейрофизиологических пруфов таких направлений в основаниях как интуиционищм Брауэра и сигнифика Маннури уже известно достаточно, чтобы утверждать, что упомянутые товарищи были правы. Намного интереснее вопрос, как получилось, что они оба правы (и это можно доказать) при том, что их позиции в вопросе на чем строить основания математики полностью взаимоисключающие? У меня есть некоторые соображения по этому поводу, и не только соображения, но и немного кода, но это тема не для мейлру.
Если они правы, то почему они не создали никакой математики?
Ты ж сам выше писал, что в математике не шаришь, это заметно. Иначе бы и вопроса такого не было. Про конструктивную математику ты не слышал, да? Насчет Маннури все сложнее, даже сейчас в 2017 технические возможности для создания математики по его идеям находятся в зачаточном состоянии, кое'что из нужного вообще не исследовано даже. Он больше чем на век свое время опередил.
Я шарю в математике. Конструктивной математики не существует.
> Конструктивной математики не существует.
А говоришь, шаришь. Ну поясняй, что у тебя за вера. Почему конструктивной математики не существует.
Допустим, конструктивная математика существует. Из каких разделов она состоит?
Это общий подход к любым разделам. Начиная от оснований. Все это обсуждалось уже и не один раз.
Подход есть, а результатов уже сто лет нет. Как так?
Давай представим мир, в котором "конструктивная математика" существует. Это мир, в котором конструктивизм служит инструментом, с помощью которого изучаются какие-то другие вещи. В котором количество конструктивистки написанных монографий настолько велико, что приходится разбивать их на области. Этими областями могут быть, например, конструктивная теория групп, конструктивный анализ, конструктивная теория множеств, конструктивная гомологическая алгебра и т.п. - как в математике, только со словом "конструктивная" в названии. Это мир, в котором конструктивная наука построила целое здание абстрактного знания.
Что же имеет место в нашем мире? В нашем мире во всех монографиях, традиционно относимых к конструктивизму, темой исследования всегда является сам конструктивизм. Суть таких книг всегда - основания конструктивизма и/или доказательство через боль и слезы какого-нибудь тривиального математического факта. В нашем мире конструктивизм не оформился как наука - в отличие от математики.
Когда человек говорит "я занимаюсь математикой", это даёт мало информации о его деятельности - он может как аутировать над дифурами, так и шатать большие кардиналы. А вот когда человек говорит, что занимается конструктивизмом, абсолютно всегда понятно, что он делает. Поэтому понятия "математика" и"конструктивизм" являются понятиями очень разных уровней. Математика - полноценная богатейшая наука. Конструктивизм - фанатичное толкование двух с половиной ветхих философских книжонок.
Конструктивизм - это никакой не "общий подход".
Еще одна паста типа про математику? Примерно 99,999% конструктивных вещей не имеют в своем названии слова "конструктивный", хотя бы это ты должен знать. Мне реально лениво сотый раз нарезать и постить сюда определения конструктивного объекта по Мартин-Лёфу, тем более что я прекрасно вижу, что смысла в этом 0, все равно приходит очередной или один и тот же, но предельно гениальный зеленый феласаф и сказка про белого бычка начинается сначала. Нету конструктивной математики? Ок, раз школьники на мейлру так пишут, то и правда нету. Я все понял, все услышал.
Я могу показать математику - мне достаточно дать ссылку на архив или на матнет.
Ты не можешь показать конструктивизм - максимум можешь вырезать скрин из Мартин-Лёфа.
А ссылка на Мартин-Лефа это не ссылка, и его конструктивная теория типов это не теория и не конструктивная и не типов, я тебя правильно же понимаю, да? Зачем ты вообще все это пишешь?
Представь, что некий философ Мартинда выдумал подход, который назвал "деконструктивная математика". Он написал много букв про то, какой деконструктивизм хороший и какая вся остальная математика плохая. Но все его тексты посвящены исключительно деконструктивной математике, никакие, скажем, теоремы об индексе он доказать даже и не пытался. Назовёшь ли ты математикой деятельность философа Мартинды? Будешь ли утверждать, что миллионы книг по математике равновелики трем с половиной его брошюркам?
То есть, конструктивные доказательства это не доказательства, пруверы это не пруверы? Может быть, я виноват, что ты про все это не слышал? Ты попробуй не просто писать, а думать о том, что пишешь.
Я могу перечислять книги по математике несколько часов подряд и ни разу не повториться. Ты, если попытаешься перечислить книги по якобы существующей "конструктивной математике", не наберешь и сотни. Да что там, даже десятка.
Предъяви набор конструктивных книг, равнообъемных хотя бы трактату Бурбаки.
Дарья Донцова написала больше книг, чем Бурбаки, значит математика бурбаков не существует, это твоя логика. Подумой и не пиши хуйни, ок?
Математика необъятна.
Конструктивизм исчерпывается двумя-тремя книжками.
И ты говоришь, что это равновеликие науки?
И да, если бы ты понимал в математике, то ты знал бы что метаматематика во многом даже более конструктивна, чем собственно конструктивизм, т.к Гильберт рассматривал возможность доказать непротиворечивость арифметики строго финитными методами. Поэтому противопоставлять бурбаков конструктивистам это вообще пушка. Я уже даже не говорю о том, что суть конструктивизма в применении у основаниям в том, чтобы дропнуть невычислимые суеверия типа исключенного третьего и доказательства, из которых не следует возможности построения доказываемого. И ведь все это сто раз уже писано мной на этой параше, так нет, вылезает один и тот же аутист, или разные, но похожие один в олин, и несут одну и ту же хуйню. Не надоело?
Особенно тау-символ конструктивен, эквивалентный глобальному выбору.
Просто дай список ъ-конструктивистской литературы. Хотя бы из ста наименований. Или не сможешь?
>чтобы дропнуть невычислимые суеверия
Ага подорвать пару столбов математики, а потом смотреть как всё здания к хуям разрушается. Конструктивистов как и ИГИЛ надо запретить.
Ты хотел сказать формалистов, да!?
Ничего не разрушили кроме пары суеверий, зато построили полностью вычислимые основания. Как оказалось, математика ничего не потеряла, если из нее выкинуть суеверия, такой нежданчик.
Во-первых, даже устоявшейся терминологии в конструктивизме нет. Во-вторых, на этих якобы "основаниях" никакой дальнейшей конструкции не возведено.
>кроме пары суеверий
Содержание программы Вербицкого - это пара суеверий?
> Во-первых, даже устоявшейся терминологии в конструктивизме нет. Во-вторых, на этих якобы "основаниях" никакой дальнейшей конструкции не возведено.
Завязывай уже хуйню писать, а.
Ты называешь всю программу Вербицкого суеверием.
> Ты называешь всю программу Вербицкого суеверием.
Вербицкий это бородатый такой, писал про АКАБов и цитировал стишок 'из западного ануса все жрете вы говно, за кока колу сраную продались вы давно'?
Вот смотри, я сто раз давал определение конструктивного объекта. Если после этого я вижу предъявы уровня того, что выше по треду, я не могу не отметить бесполезность своих попыток что-то объяснить. А имея в виду исключительную простоту такого определения, не могу не сделать напрашивающегося вывода об умственных способностях того, кому я пытаюсь что-то объяснить. Тут именно в личности проблема, а не в моем подходе, увы.
Конструктивизм не оставляет от математики камня на камне. Уничтоженным оказывается всё, что перечислено в программе Вербицкого. А ты только смеешься над этим.
>зато построили полностью вычислимые основания.
Когда там комплюктеры докажут гипотезу Римана?
>Как оказалось, математика ничего не потеряла
Математика тем и славится, что даже такое сборище аутяг, как конструктивисты имеют право на существование.
> Когда там комплюктеры докажут гипотезу Римана?
Ты ее без комплюктера докажи, умник. Понапридумывают всякой заведомо бесконечной хуйни, потом удивляются почему эти маняпроблемы столетиями никто решить не может. Очевидно же, что конструктивное решение есть построение, отсюда последнему довну ясно почему эти манягипотезы недоказуемы. Я тебе сходу могу таких выдумать и хуй ты их докажешь даже без конструктивизма. Например, прикол 'купи слона' неразрешим, это тоже теперь математическая проблема тысячелетия? Аутисты блядь кого'то в аутизме обвиняют, вообще пушка. Причем, обвиняют самых здравомыслящих, чья идея как раз в отказе от невычислимых верований.
Т.е. гипотеза Римана - ненужное суеверие, надо выгнать на мороз?
Ты читать умеешь? Не нужно выдумывать хуйни, нужно читать на что отвечаешь, раз уж отвечаешь (последнее вообще необязательно). В данном случае, там уже есть ответ.
Ты прямо ответь. Гипотеза Римана - суеверие?
Гипотеза - это гипотеза. Суеверия - это актуальная бесконечность, исключенное третье.
С Риманом всё ясно.
А ты можешь доказать, что всякое бесконечное множество содержит счетное подмножество?
>доказать, что всякое бесконечное
Пиздец, с кем сижу на одном мейлру. В предыдущем моем посте ответ про "всякое бесконечное". Ну вот что таким докажешь? Тебе сколько раз нужно написать, что "конструктивное доказательство это построение", чтобы до тебя наконец это бы дошло? Конструктивное множество - это правило, по которому можно порождать элементы множества, то есть строить их. Если таковых нет, то это не множество, а категория. Я даже могу сказать, что следующим вопросом будет привести примеры таких множеств и таких правил. Будто я это сто раз не делал. Сказка про белого бычка.
Допустимы ли обороты вроде "пусть M - множество решений уравнения x^7+3x^2+x+1=0"? При условии, что я не знаю формулы для порождения решений.
Если переменные х заданы в виде контекста, н-р если это лямбда-термы, принадлежащие своему типу, так же заданному в виде контекста, что-нибудь уровня х:А, то да. Такой "оборот" в данном случае был бы спецификацией программы, порождающей решения этого уравнения. Естественно, предварительно должны быть заданы операции "=, ^, +" как лямбда-термы имеющие свой тип, или выражения имеющие соотв. арности, что почти одно и то же.
И да, спецификация такой программы / доказательства что одно и то же, согласно изоморфизму Карри-Говарда, может быть задана, если ее решения низвестны, пикрелейтед - спецификация теоремы Ферма. Задать ее можно, решением было бы построение всех примеров, удовлетворяющих данной спецификации. Если в процессе построения нашлось бы решение, не удовлетворяющее такой спецификации, оно было бы конструктивным доказательством ложности теоремы Ферма. Опять же, я сто раз это писал уже.
Опять же, поскольку полный перебор всех решений невозможен технически, можно говорить только о потенциальной осуществимости такого доказательства. И это я сто раз уже писал.
> что я не знаю формулы для порождения решений.
Для конструктива не обязательно нужна формула. Смотри, если многочлен нечётной степени, то у него для некоторого большого K (K > 0) при подстановке K и -K получатся числа разных знаков, а значит бисекцией можно найти корень. Для многочлена чётной степени надо продифференцировать, если все экстремумы лежат где надо, то корней нет. Если нашли один корень, делим на него и повторяем всё это. Вот у тебя и получится множество корней.
Толсто.
В конструктивизме теорема Больцано-Коши неверна.
Само ты толсто.
Больцано-Коши неверна для произвольных непрерывных функций, но разные варианты с равномерной непрерывностью или гладкостью верны, а для многочленов-то вообще проблем нет.
>Ты ее без комплюктера докажи, умник.
Не погоди, твоя же конструктивная математика самая конструктивная и самая настоящая, а все остальные нужно выкинуть на помойку, так?
>Понапридумывают всякой заведомо бесконечной хуйни
Ну-ну, простые числа вполне осязаемы. Впрочем я не удивлюсь, если среднестатистический конструктивист сможет в них что-то понять.
>Очевидно же, что конструктивное решение есть построение
Мне насрать, ты говоришь что конструктивная хуйня лучше дедовского аксиоматического, формалистического картофана с аксиомами выбора и.т.д Так докажи, своим конструктивистким пиздежом, хоть что-нибудь новое, а не дрочи, как последний дрочила. Пока единственное, что я слышу от мамкиных конструктивистов тут, это пиздеж что их математика лучше. Моё мнение таково: пока каждый занимается своим аутизмом, всё в порядке, когда кто-нибудь начинает лезть в залупу, его надо загонять под шконарь.
> Мне насрать, ты говоришь что конструктивная хуйня лучше дедовского аксиоматического, формалистического картофана с аксиомами выбора и.т.д Так докажи, своим конструктивистким пиздежом, хоть что-нибудь новое, а не дрочи, как последний дрочила. Пока единственное, что я слышу от мамкиных конструктивистов тут, это пиздеж что их математика лучше. Моё мнение таково: пока каждый занимается своим аутизмом, всё в порядке, когда кто-нибудь начинает лезть в залупу, его надо загонять под шконарь.
Таблетки выпей, бесноватый. Дедовское как раз все конструктивное, это потом поналезло умников, затыкать все дыры в математике актуальной бесконечностью, исключенным третьим и прочей невычислимой шляпой. Итог очевиден - кризис оснований. И я уже сто раз говорил, что использовать свое незнание как доказательство чего- то есть признак долбаеба.
А что плохого в третьем исключённом и актуальной бесконечности?
мимо
Невычислимые (непостроимые) суеверия.
Окей. Может глупый вопрос, но делает ли трансцендентность pi это самое pi суеверием? Его же в принципе нельзя вычислить с окончательной точностью до n-го знака.
> Окей. Может глупый вопрос, но делает ли трансцендентность pi это самое pi суеверием? Его же в принципе нельзя вычислить с окончательной точностью до n-го знака.
Пи это правило построения. Это потенциальная бесконечность. Актуальная бесконечность не соответствует никакому построению либо правилам построения.
Но ведь потенциальная бесконечность ничем не лучше актуальной.
>Это потенциальная бесконечность
Ты что дурак что ли блять?
Вот хорошо, сумма ряда 1/2^n равна двум, как известно. По твоему что, этот ряд имеет конец?
Сумма ряда != ряд, не?
Ой, да у нас тут аниме, становится интересно.
>Итог очевиден - кризис оснований.
Итак появляются петухи, которые кукарекают, что надо всё до основания разрушить. Где-то я уже это слышал.
Давайте так. Вот вам тезис - любая практически осуществимая математика конструктивна, т.е. построима. Без разницы, какими формализмами там пользуются, хотя бы и не имеющими к интуиционизму никакого отношения и опирающиеся на всякие актуальные бесконечности и исключенные третьи. Я пони маю, что для аудитории мейлру это слишком сложно, поэтому конкретный пример, что именно я имею в виду. Вот есть такая тема, как теория статистического обучения Вапника, пытающаяся (и небезуспешно) обосновать саму суть машинного обучения. Меня тут упрекают в том, что я даю скриншоты вместо нормальных ссылок, поэтому вот ссылка http://gen.lib.rus.ec/book/index.php?md5=0BE90A2C820FB75B1C79E385101A5761 Собственно, о чем я:
1) упомянутая теория излагается автором с чисто классических позиций - православный матан, теорвер, все эти интегральчики, предельчики и прочий знакомый любому школьцу картофан. Никакой ереси типа лямбда-исчисления, MLTT и прочего Барендрехта даже не упоминается, хотя очевидно, что функции неплохо было бы рассмотреть с точки зрения самой нормальной теории функций - лямбда калькулюса, тем более что речь конкретно о вычислимых функциях.
2) тем не менее, сама теория про некоторый класс алгоритмов, их обоснование, в общем, о доказательствах некоторых их свойств, полезных с точки зрения машинного обучения. Т.е. про нечто изначально конструктивное и построимое на комплюктере. Опять же, конструктивный подход к вопросу, изоморфизм Карри-Говарда, не упоминается даже вскользь, хотя он именно об этом.
3) из предыдущих пунктов очевидно, что в теории статистического обучения классический подход используется как, скажем, "дискретизация" такового, ограниченная вычислительными возможностями железа и софта, т.е. значение функций, предела функции и т.д. на самом деле ограничены 12 или около того знаками после запятой, а не нарисованным знаком бесконечности, длина примеров в датасете тоже конечна, хотя в формулах попадаются выражение типа стремления длины выборки к бесконечности и т.д.
Отсюда вопрос, конструктивна ли теория статистического обучения? Если с одной стороны там даже не упоминается конструктивизм, а с другой - все теоремы, следствия и доказательства этой теории непосредственно построимы? Хотелось бы услышать манямнения.
1) упомянутая теория излагается автором с чисто классических позиций - православный матан, теорвер, все эти интегральчики, предельчики и прочий знакомый любому школьцу картофан. Никакой ереси типа лямбда-исчисления, MLTT и прочего Барендрехта даже не упоминается, хотя очевидно, что функции неплохо было бы рассмотреть с точки зрения самой нормальной теории функций - лямбда калькулюса, тем более что речь конкретно о вычислимых функциях.
2) тем не менее, сама теория про некоторый класс алгоритмов, их обоснование, в общем, о доказательствах некоторых их свойств, полезных с точки зрения машинного обучения. Т.е. про нечто изначально конструктивное и построимое на комплюктере. Опять же, конструктивный подход к вопросу, изоморфизм Карри-Говарда, не упоминается даже вскользь, хотя он именно об этом.
3) из предыдущих пунктов очевидно, что в теории статистического обучения классический подход используется как, скажем, "дискретизация" такового, ограниченная вычислительными возможностями железа и софта, т.е. значение функций, предела функции и т.д. на самом деле ограничены 12 или около того знаками после запятой, а не нарисованным знаком бесконечности, длина примеров в датасете тоже конечна, хотя в формулах попадаются выражение типа стремления длины выборки к бесконечности и т.д.
Отсюда вопрос, конструктивна ли теория статистического обучения? Если с одной стороны там даже не упоминается конструктивизм, а с другой - все теоремы, следствия и доказательства этой теории непосредственно построимы? Хотелось бы услышать манямнения.
По-моему ответ очевиден: нет. Построенная теория неконструктивна. Но можно построить аналогичную конструктивную теорию, которая, быть может, даже будет лучше. Но никто этим пока не занимался, видимо.
Новая тема треда: потенциальная и актуальная конструктивность.
>Построенная теория неконструктивна. Но можно построить аналогичную конструктивную теорию, которая, быть может, даже будет лучше.
Тогда в чем разница? Если вместо пределов, интегралов и т.д. можно гонять соответствующие этим выражениям лямбда-термы и наоборот, то возникает закономерный вопрос, а зачем всякие актуальные бесконечности, которые все равно ни к одной практической задаче не пришить? Где она, бесконечность, если любая практическая задача, любое осуществимое вычисление все равно имеет дело с чем-то конечным? Ну кроме потенциальной бесконечности типа программ для машины Тьюринга, не приводящих к останову. Еще Брауэр показал, что континуум непостроим, т.к. между двумя соседними вещественными числами всегда можно вкорячить их еще сколько угодно. Но на практике "сколько угодно" всегда ограничивается доступными вычислительными возможностями. Т.е. в конечном счете все равно все имеют дело с конструктивным, т.е. построимым и вычислимым.
Единственные реальные примеры неконструктивной математики - это парадоксы а единственное реальное достижение неконструктивной математики это кризис оснований. Все, что не сводится к антиномиям и программам для машины Тьюринга, не приводящим к останову, вычислимо и т.о. конструктивно, безотносительно в каких формализмах выражено.
Сделайте.
Покажите, что это лучше.
Потом воняйте.
у нас тут в треде есть адепт петушиной конструктивности, требую добавить к повестке треда.
>Еще Брауэр показал, что континуум непостроим, т.к. между двумя соседними вещественными числами всегда можно вкорячить их еще сколько угодно.
А какая разница построим он или нет?
Построимое - халяль, непостроимое - харам.
То есть нормальному математику должно быть похуй на эти конструктивистко-муслимские разборки?
А теория категорий халяль?
>А какая разница построим он или нет?
Вот есть всякие кардиналы алеф1 и выше, бет и т.д. Они ничему построимому и вычислимому не соответствуют, это чистая религия а не математика.
Нормальный математик во всех случаях пользуется конструктивной математикой, я же даже пример привел но как и предполагал, для мейлру это слишком сложно. Ты не приведешь пример практического использования неконструктивной математики кроме парадоксов и прочего кризиса оснований.
В MLTT и HoTT ее используют. Дальше сам.
> HoTT
Это какая-то модная йоба по типу новых оснований?
> Они ничему построимому
Но как-то же их построили или чисто с потолка взяли и решили, ага, вот охуенная штука алеф1, будем в неё веровать.
> и вычислимому не соответствуют
А должны?
>Но как-то же их построили или чисто с потолка взяли и решили, ага, вот охуенная штука алеф1, будем в неё веровать.
Их никак не построили, они непостроимы. Просто значок, за которым не стоит ничего. Взяли не с потолка, но около того.
>А должны?
Нет, конечно. Только невычислимое это не математика.
>Это какая-то модная йоба по типу новых оснований?
Пикрелейтед.
А как бы вот эти все пруверы и доказательства выглядели бы в светлом будущем? Какая цель? Даже школьники будут с ними работать?
>Даже школьники будут с ними работать?
Они будут работать даже без школьников. Полностью механизированные доказательства.
Автоматизация математиков?
Да.
>Ты не приведешь пример практического использования неконструктивной математики кроме парадоксов и прочего кризиса оснований.
>практического использования
Для копания картохи подойдёт только конструктивизм? Почему меня как математика должна интересовать практическая применимость.
Да и ясно, что у картофенов бомбит с парадоксов, картошку-то банахом-тарским не удвоишь.
> Тогда в чем разница?
В том, что одно есть, а другого - нет, очевидно же.
Чего нет-то, губошлеп? Ты читать пробовал на что отвечаешь?
Картофен, ищи практическое применение на /pr
Если триггернулся на слово "практическое", замени на "вычислимое". Невычислимой математики несуществует, т.к. это уже не математика. Отсюда, все эти актуальные бесконечности и т.д. на самом деле не используются никем, даже если подразумеваются.
>Невычислимой математики несуществует, т.к. это уже не математика.
>континуум непостроим
Инженеры используют интегральчики с континумом, постоянно разбивая график на бесконечное число прямоугольников. Где твой Бровер теперь?
Но они же не считают его напрямую в лоб как ты собирался бесконечность считать? ты что, дурак что ли блять?, а пользуются теоремой шницель птуцера и переводят из пустого в порожнее/повышают степень на единицу и делят на эту самую степень.
Или раскладывают в ряд по теореме ноги макаронины с округлением/указанием пределов в которых находится вычисляемая величина.
мимо
Я чуть выше привел похожий пример с теорией статистического обучения и объяснил для одаренных, что нет там никаких бесконечностей, даже если значки бесконечности и стоят, то подразумевается конечное. Даже если используются интегралы и пределы, по факту все считается до конечного числа знаков после запятой, редко превышающего 12. И где теперь ваша актуальная бесконечность, если ее нет ни в одной задаче?
>по факту все считается до конечного числа знаков после запятой, редко превышающего 12
А какая разница, как там инженеры считают? Математик может запросто сравнить числа с бесконечными знаками, после запятой.
>даже если значки бесконечности и стоят, то подразумевается конечное.
Тогда почему они так часто говорят о бесконечности, особенно им нравятся бесконечно малые.
> А какая разница, как там инженеры считают? Математик может запросто сравнить числа с бесконечными знаками, после запятой.
Не может. Практических методов сделать это не существует. Нарисовать значок бесконечности или Аллаха не равно построить эти сущности.
> Тогда почему они так часто говорят о бесконечности, особенно им нравятся бесконечно малые.
Какая разница, о чем они говорят? Важно то, что они делают.
Конструктивную топологию покажи мне.
Покажи неконструктивную для начала. Я еще раз говорю, все эти значки бесконечностей просто спецэффекты, работать можно только с вычислимым.
Показываю. Теперь ты.
Иди куда шел со своими картинками, во всяком случае, мимо этого треда, ты же даже не в состоянии понять, о чем тут вообще говорят, тем более понять аргументы. Сто раз уже сказал, что нет там никаких бесконечностей, их никто не способен считать, потому что они невычислимы. Нахуя ты мне картинку показываешь, ты что, ебнутый? Ты если не способен понять о чем речь, нахуя вообще сюда пишешь?
Маня, может ты хоть книжку откроешь. Там в самом начале аксиома выбора.
Маня, у Мартин-Лёфа есть конструктивное доказательство аксиомы выбора, в MLTT это не аксиома, в которую надобно веровать, а доказуемая теорема. И я сто раз давал ссылку на это доказательство. Сасай-кудасай.
>это не аксиома, в которую надобно веровать, а доказуемая теорема
Дай угодаю, только для конечных множест?
Как будто кто'то может пользоваться бесконечными. Бесконечность невычислима, алё, есть кто дома?
Большая часть математиков да. Инженеро-прогеры нет в большинстве своём.
Вера в возможность не равна возможности так же как нарисованный значок бесконечности не равен бесконечности.
Вообще, у меня есть подозрения, что ты, мил человек, селедка. По собственному опыту могу судить, что только бабе похуй на фактическую аргументацию, в угоду своему оценочному суждению. Покажи-ка сиськи пример как по'твоему математики могут вычислить невычислимое.
>фактическую аргументацию
Ты про?
>тебе не понять
>так сказал брауэер
>я уже сто раз говорил
>ваша математика не математика
>100 раз говорил
>кризис оснований, парадоксы
Раз мы говорим, по сути, о сущностях, которые находяться в платоновском мире идей, то почему бесконечное количество чего-то не может существовать?
> Раз мы говорим, по сути, о сущностях, которые находяться в платоновском мире идей, то почему бесконечное количество чего-то не может существовать?
Потому что математика это не вера в платоновский мир идей. Нет никакого мира идей, есть вычислимые построения и всякая вера. Последнее это не математика.
> Ты про?
Я про конкретные примеры выше, теорию статистического обучения как вариант.
Твои вычислимые построения такая же вера. У тебя не хватит атомов во вселенной, чтобы эксперементально всё вычислить. Ты даже десятичную запись числа Грэма не напишешь.
Я не собираюсь читать целую книгу о прикладухе, чтобы доказать что-то анону с двачей.
Не неси опять хуйни по новой. Никто неюикогда не утверждал фактическую построимость потенциально построимых объектов. Ты этого даже понять не способен, о чем тут вообще говорить.
Раз мы не можем её фактически построить, то получаем, что верим в существования этого объекта?
> Раз мы не можем её фактически построить, то получаем, что верим в существования этого объекта?
Я просто уже даже не помню, сколько раз объяснял разницу между фактическим конструктивным объектом, потенциально но не фактически построимым и актуальной бесконечностью. 1005001 ый раз не хочу, ты слишком тупой, алибидерчи.
Ненене, я понимаю.
Смотри, у нас есть платоновский мир, но ты выделяешь из него только те объекты, для построения которых есть алгоритм. Но платоновскими они не перестают быть, поскольку мы не можем проверить в реальности их существование.
Я другой анон. Конструктивные математики не привязываются никоим образом к реальному миру и не стараются ограничить себя им. Тебе следует разобраться, что такое ментальные математические конструкции и правила их построения. Я не смогу это сделать, тут нужен тот анон, но он кажется заеб*лся повторять всё это три треда подряд)
— Почему существует только то, что порождается алгоритмом?
— Потому.
— Ты ебанутый?
— На это неоднократно давался ответ.
— Ты можешь доказать формулу Гаусса?
— Твоя вера не нужна.
— Пошёл нахуй, ебанашка.
— Ты не воспринимаешь объективные аргументы.
— Какие?
— Хватит спрашивать одно и то же.
— Ты издеваешься. Ты не можешь писать это всерьёз.
— Я не виноват, что ты такой тупой.
— Потому.
— Ты ебанутый?
— На это неоднократно давался ответ.
— Ты можешь доказать формулу Гаусса?
— Твоя вера не нужна.
— Пошёл нахуй, ебанашка.
— Ты не воспринимаешь объективные аргументы.
— Какие?
— Хватит спрашивать одно и то же.
— Ты издеваешься. Ты не можешь писать это всерьёз.
— Я не виноват, что ты такой тупой.
>13/11/16
До сих пор актуально.
>Конструктивные математики не привязываются никоим образом к реальному миру и не стараются ограничить себя им.
Я понимаю это и в таком контексте обзывательства кого-то в вере выглядит бессмысленым.
Ага.
>нет там никаких бесконечностей
Тогда что на пикрелейтед?
>всякая вера.Последнее это не математика.
потому что ты так скозал? Повторюсь, отправляйся под шконарь.
http://e-science.ru/groups/%D0%A7%D0%B5%D0%BC-%D0%BE%D1%82%D0%BB%D0%B8%D1%87%D0%B0%D1%8E%D1%82%D1%81%D1%8F-%D0%BC%D0%B0%D1%82%D0%B5%D0%BC%D0%B0%D1%82%D0%B8%D0%BA%D0%B8-%D0%95%D0%B2%D0%BA%D0%BB%D0%B8%D0%B4%D0%B0-%D0%B8-%D0%9F%D0%B8%D0%B2%D0%B5%D0%BD%D1%8C-%D0%93%D1%80%D0%B8%D0%B3%D0%BE%D1%80%D0%B8%D1%8F
Чем отличаются математики Евклида и Пивень Григория?
Математика Евклида плоская, горизонтальная в пространстве, где измерения происходят с помощью «безразмерных» точек по ширине, но размерных по длине, что проявляется в форме линейки, и этот процесс описывается числами с нулевым индексом, т.е. без знаков (+) или (-).
Например: 4+5=9, 9-5=4.
Математика Пивень Григория объёмная, где измерения происходят с помощью размерных точек, как шариков с разными радиусами, т.е. не только по длине, но и по ширине, а этот процесс описывается с помощью чисел 3-х векторов движений относительно вертикали, т.е. с индексами-векторами (+), (-) и (0).
Например: (+4)+(+5)=(+9)- это положительные, центробежные числа.
(-9)-(-4)=(-5) – это отрицательные, центростремительные числа.
4+5=9 и 9-5=4 – это нейтральные, поперечные к вертикали движения.
В современной математике слагаемые 4+5=сумме 9 и из суммы 9 вычитается слагаемое 4 или 5 и получатся слагаемое 5 или 4: 9-4=5 или 9-5=4.
В математике Пивень Григория слагаемые могут быть только положительные числа- суммы, а при действии вычитания сумма меняет знак (+) на знак-вектр (-) и становится уменьшаемым, (+9)=(-9), из которого могут вычитаться не слагаемые (+4) или (+5), а вычитаемые (+4)=(-4) или (+5)=(-5) и в итоге получаем разность (-9)-(-4)=(-5) или (-9)-(-5)=(-4).
На математическом форуме MathHelpPlanet изучать новый взгляд на старые действия отказались, предпочтя кривую, с парадоксами, с двойными ответами математику вместо математики точной, без парадоксов, без двойных ответов, где нет гадания (или +n или –n?).
20/8/2016г. Пивень Григорий- автор новых основ математики.
Чем отличаются математики Евклида и Пивень Григория?
Математика Евклида плоская, горизонтальная в пространстве, где измерения происходят с помощью «безразмерных» точек по ширине, но размерных по длине, что проявляется в форме линейки, и этот процесс описывается числами с нулевым индексом, т.е. без знаков (+) или (-).
Например: 4+5=9, 9-5=4.
Математика Пивень Григория объёмная, где измерения происходят с помощью размерных точек, как шариков с разными радиусами, т.е. не только по длине, но и по ширине, а этот процесс описывается с помощью чисел 3-х векторов движений относительно вертикали, т.е. с индексами-векторами (+), (-) и (0).
Например: (+4)+(+5)=(+9)- это положительные, центробежные числа.
(-9)-(-4)=(-5) – это отрицательные, центростремительные числа.
4+5=9 и 9-5=4 – это нейтральные, поперечные к вертикали движения.
В современной математике слагаемые 4+5=сумме 9 и из суммы 9 вычитается слагаемое 4 или 5 и получатся слагаемое 5 или 4: 9-4=5 или 9-5=4.
В математике Пивень Григория слагаемые могут быть только положительные числа- суммы, а при действии вычитания сумма меняет знак (+) на знак-вектр (-) и становится уменьшаемым, (+9)=(-9), из которого могут вычитаться не слагаемые (+4) или (+5), а вычитаемые (+4)=(-4) или (+5)=(-5) и в итоге получаем разность (-9)-(-4)=(-5) или (-9)-(-5)=(-4).
На математическом форуме MathHelpPlanet изучать новый взгляд на старые действия отказались, предпочтя кривую, с парадоксами, с двойными ответами математику вместо математики точной, без парадоксов, без двойных ответов, где нет гадания (или +n или –n?).
20/8/2016г. Пивень Григорий- автор новых основ математики.
Конструктивиста напомнило фанатизмом и истерии о парадаксах.
Не уплываем.
Сколько уже доказанных с помощью Coq теорем? Ведется какая-то статистика?
Ну, можно посмотреть количество проектов на гитхабе, если хочется статистики... Но не уверен, что от этого будет толк. Единого репозитория всей математики, как я понимаю, нет.
В чем сложность создания такого репозитория?
>всей математики,
только маленького количества математики, конструктивной.
-пофиксил тебя
Нужно всех заставить им пользоваться, а Сталина у нас нету?
> В чем сложность создания такого репозитория?
Некому этим заняться. Потом, 99% использования кока это личные цели, задачи передоказать на нем всю математику никто не ставил и желающих этим заниматься нет. Главная проблема в том, что все это нужно пилить вручную, а это долго, нудно и сложно. Это одна из основных проблем пруверов вообще, в свое время де Браун сотоварищи перевели на язык первого прувера AUTOMATH аж целую книжку Ландау 'Grundlagen', все это есть в инторнетах, можно оценить ебейшую сложность такой задачи лично. Далее, чтобы перевести в кок некую теорию, нужно быть неплохим спецом в вопросах этой теории, ну если это не какое'нибудь исчисление пропозишенов. Как пример можно привести ядро НоТТ на коке, кроме Воеводского с соратниками вряд ли кто осилит такую задачу, см. соотв. пейперы. К счастью, автоматизация подобных задач таки возможна, если вспомнить некоторые идеи т.н. 'сигнифики'. Я сейчас как раз этим пытаюсь заниматься в свободное время, которого у меня нет нихуя. Возможно, скоро покажу конкретные примеры.
> только маленького количества математики, конструктивной.
> -пофиксил тебя
Не шаришь, так не нес бы хоть хуйни. Простой пример, озвученный в предыдущем посте, верификация Grundlagen Ландау, не имеющей ничего общего с конструктивной математикой с помощью изначально 100% конструктивной типизированной лямбды-Р. Как бы ты для себя объяснил возможность этого? Хотя о чем я спрашиваю анэнцефала из рашки.
Почему существует только то, что порождается алгоритмом?
Вы тут настолько убоги, что не способны даже элементарные вещи изложить своими словами. Сам'то читал что пишешь?
Это не считая того, что сто раз уже объяснялось, почему существование в математике сводится к построимости. Сто первый раз объяснить? А смысл, если это все равно не даст ничего?
>почему существование в математике сводится к построимости
Существует объединение любого множества.
> Существует объединение любого множества.
С этой стороны тоже бесполезно, придумай что'нибудь еще. Хотя бы потому, что твоя формулировка вызывает как минимум два вопроса, 'что значит 'существует'' и 'что значит 'любого''. Если существование сводить к платоновским верованиям в мировую душу и мир идей, то это чистая религия. Если к нарисованному значку на бамаге, то опять же, я и символ Аллаха могу нарисовать. И так далее. Все это уже обсуждалось и не интересно.
>я и символ Аллаха могу нарисовать
Ну нарисуй. Никто тебя за язык не тянул. Определение Аллаха на языке логики первого порядка в студию.
> . Определение Аллаха на языке логики первого порядка в студию.
Сорта на самом деле. И там и там невычислимые актуальные бесконечности, за которые предлагается верить, что это основа всего.
Ты уже который раз упоминаешь Аллаха.
Ну так давай, сделай это. Определи его.
Этот пример я привожу как раз по причине его невычислимости. Ты же ссылаешься на логику первого порядка, хотя в ней верен невычислимый общий случай исключённого третьего. Одно невычислимое ничем не лучше другого столь же невычислимого. Завязывай со своей демагогией, ты прекрасно понимаешь это. Понимаешь, что так или иначе невозможно обойти вопрос 'что есть существование в математике?'. Все это неоднократно обсуждалось, я стопервый раз все это пишу просто потому что мне на работке еще до утра сычевать и надо чем'то убить время.
Я могу предложить первопорядковую теорию множеств. Ты не можешь предложить первопорядковую теорию Аллаха. Поэтому я могу говорить про множества, а ты не можешь говорить про Аллаха.
Перестань упоминать Аллаха, это тупо и очень бесит. Или определяй его.
> Я могу предложить первопорядковую теорию множеств
Опирающуюся на невычислимые верования типа актуальной бесконечности и исключенного третьего.
Ты говоришь, что можешь формализовать Аллаха.
Сделай это.
> Ты говоришь, что можешь формализовать Аллаха.
Где я это говорил? Не разводи демагогию, я такого не говорил вообще никогда, ты уясни другое, логикой первого порядка ты можешь пользоваться лишь постольку, поскольку позволяет изоморфизм Карри-Говарда. Вне этих рамок ты ничего не докажешь этой логикой, т.к доказательства твои за пределами вышеупомянутого изоморфизма будут ничем не лучше корана.
Я указываю тебе на разницу между первопорядковыми теориями и кораном. Ты не можешь формализовать Аллаха первопорядковой теорией, в принципе. И ты об этом осведомлен. Поскольку ты продолжаешь использовать фразы "символ Аллаха могу нарисовать" и "не лучше корана", остаётся только один вывод. Ты осознанно лжёшь.
> Я указываю тебе на разницу между первопорядковыми теориями и кораном.
Вне изоморфизма Карри-Говарда их нет.
Хорошо. Предъяви аксиоматическую теорию аллаха.
> Хорошо. Предъяви аксиоматическую теорию аллаха.
Ты читать умеешь?
Жду примеров: ты заинтриговал.
Ты говоришь, что разницы нет. Тогда почему ты не можешь написать теорию Аллаха?
> Ты говоришь, что разницы нет. Тогда почему ты не можешь написать теорию Аллаха?
Выше отвечал уже.
На вопрос "почему ты не можешь дать первопорядковую теорию Аллаха" ты не отвечал.
Отвечал. Я ж говорю, ты даже читать не умеешь, какая тебе математика. Ладно читать, даже потралить не в состоянии. Ты либо реально селедка, либо аутист со стажем на бордах максимум месяца два.
Ну так процитируй свой ответ.
Как быть с теорией Рамсея в конструктивной математике?
Очень просто. Эта и ей подобные теории формулируются в виде спецификаций (я давал пример спецификации теоремы Ферма), затем находится решение, удовлетворяющее такой спецификации, если множество таких решений не пусто, это конструктивно доказывает исходную теорему. Конструктивное доказательство это построение, все просто же.
Поясните за этот мегасрач вообще. В чем суть конструктивной математики и почему так важно принять какие-то специальные логики для преодоления трудностей в основаниях математики? В чем ваши проблемы вообще?
Конструктивисты говорят, что вся математика - манявыдумки. У математиков от этого бугурт.
Зачем несешь хуйню? Полтора невычислимых верования - исключенное третье как общий принцип и актуальная бесконечность, это полтора верования, а не 'вся математика'.
> В чем суть конструктивной математики
В вычислимости. Источник кризиса оснований - невычислимые догмы, которые неясно зачем вообще в математику притащили.
На этом построена вся математика, начиная с анализа.
> Источник кризиса оснований - невычислимые догмы
Я думал, что источник кризиса – злоупотребление формализмом.
> которые неясно зачем вообще в математику притащили
Творческое удобство? Эвристический метод?
Весь кризис в головах.
Пока одни говорят что это все эзотеризм, вторые что это норма, третьи считают ящики и двигают науку вперед.
Короче, все как всегда. Полтора дебила друг друга говном поливают пока все остальные покуривают трубки и обсуждают дальнейший ход событий, посмеиваясь над клоунами в говне.
инб4 НА ПАЛЬЦАХ НИПАСЩЕТАТЬ!!! КАНТИНУМ НЕ КАНТИНУМ!!! АКСЕОМА ВИБОРА ЕТА АБМАН!!!
> Я думал, что источник кризиса – злоупотребление формализмом.
Злоупотребление невычислимыми сущностями тогда уж. Тут никто не понимает простейших вещей, даже не знаю как это можно объяснить еще проще, и так элементарные вещи обсуждаем. Похоже, по новой та же сказка про белого бычка намечается.
Расскажи, как ты пришёл к конструктивизму. Кто тебя ему научил?
>> Источник кризиса оснований - невычислимые догмы
Вычислимость такая же догма.
> Вычислимость такая же догма.
Да нет, вычислимость это не догма, это фактический результат. Ты даже и этого не понимаешь, пиздец же настоящий.
> Расскажи, как ты пришёл к конструктивизму. Кто тебя ему научил?
Конструктивизм is fine too, конечно же, особенно MLTT великая вещь, но мне наиболее интересен интуиционизм Брауэра в его первоначальном чистом варианте. Брауэру пришлось от него отказаться по причинам им же и озвученным, а вот я нашел, как можно обойти эти причины, как минимум частично. К слову, конструктивизм не формализует интуиционизма, но аргументы того же Гейтинга на этот счет даже некоторые авторы работ на эту тему не пони мают, чего говорить о мейлру. Как пришел, очевидно же, в книжках прочитал.
>а вот я нашел, как можно обойти эти причины, как минимум частично.
И как же, аниме?
> Да нет, вычислимость это не догма, это фактический результат.
Пруфов, конечно, не будет.
> Брауэра
Лженаука.
> Пруфов, конечно, не будет.
Изоморфизм Карри-Говарда пруф кококо лжинаука)))
> Лженаука.
Ну раз на мейлру так пишут, то ладно.
Кстати, в вашем петушином углу как решается вопрос: сколько всего простых чисел?
Не, я могу понять, когда до кого'то не доходит мочидзукина теория пространств Тейхмюллера. Но конструктивизм, там же просто все как 3 копейки, каким нужно быть деревянным по пояс, чтобы не осилить изоморфизм Карри-Говарда. Пруф конструктивного объекта жто сам конструктивный объект, даже термин 'пруф-объект' есть. Ну что сложного в ВНК интерпретации, да таблица умножения сложнее в разы. Пиздец с кем сижу на одном мейлру, даже бабки с семками у падика это гении математики по сравнению с некоторыми тута. Нахуй так жить?
>вычислимость это не догма, это фактический результат
>Изоморфизм Карри-Говарда пруф
Здесь нет логической связи. Из утверждения о существовании изоморфизма Карри-Говарда не вытекает логически, что вычислимость это не догма. С тем же успехом можно было бы говорить "теория струн ошибочна", а в ответ на резонные вопросы заявлять "диагональный метод Кантора пруф" и дальше молчать.
>сколько всего простых чисел?
Конечное число.
-Мимо Брауэр
> Здесь нет логической связи.
Я понял тебя, услышал. Уровень твоих знаний в данной теме мне ясен. Мне неясно другое, зачем ты мне пишешь и что пытаешься доказать? Что конструктивизм тебе непонятен, а его основные моменты и их взаимосвязи тебе ни о чем не говорят? Ок, ладно.
>Конечное число.
Перемножаем все известные простые числа
@
добавляем к результату единицу
@
маняматик с двоща обсасывает километры хуйцов
Но так можно сделать только конечно число раз, поскольку актуально бесконечности не существует, то количество простыз чисел конечно.
Ну я же говорю, о чем можно спорить с тем, кто не отличает актуальной бесконечности от абстракции потенциальной осуществимости. Школуйня, блядь.
>то количество простыз чисел конечно.
Ну тогда тебе не составит труда перечислить их прямо в этом итт тренде.
>так можно сделать только конечно число раз
Бесконечно число раз религия запрещает?
>Ну я же говорю, о чем можно спорить с тем, кто не отличает актуальной бесконечности от абстракции потенциальной осуществимости.
У нас нет компьютера для того, что все простые числа запрограммировать.
Нет, я не умею программировать. Тут кок запускать придёться.
Бесконечность и есть религия.
>Бесконечность и есть религия.
Мартин-Леф такого не писал.
Значит, он был веруном.
Бесконечность может быть вида доделаю, а может быть вида "не знаю как падступицца".
Анон с мейлру даже Кнута Исскуство Программирования не читал. О чем с вами говорить? Сколько раз про слова Брауэра говорю, может мне ещё количество Аллахов в треде подсчитать.
>Бесконечность может быть вида доделаю,
Бесконечности не существует, это вера сектантов. Можно и Аллаха доделовать бесконечно.
>Нет, я не умею программировать. Тут кок запускать придёться.
Не, ну давай пруф на то что простых чисел конечное число или всё таки не конечное?
>Бесконечности не существует, это вера сектантов.
>Чисел не существует, это вера сектантов.
Если нет правил построения актуальной бесконечности, то чисел конечное количество.
Только натуральные числа существуют, остальные игрушка дьявола и вера с непостроимыми сущностями.
Математика - это вычислимость. В математике нет ничего, что не сводится к вычислимости. Полтора невычислимых верования типа исключенного третьего и актуальной бесконечности - это не математика, т.к. при попытке их использования в основаниях имеем кризис этих оснований. Все просто же, и все кукурекующие выше по факту не приведут ни одного примера, опровергающего мной только что написанное. Можно писать всякую хуйню, можно пользоваться своей тупостью как доказательством (в своем манямире, ес-но), но по факту вам возразить нечего - невычислимой математики просто не существует, в любой математике ровно столько математики, сколько в ней вычислимости.
>Математика - это вычислимость.
Причем, вычислимость на компьютере! Только ультрафинитизм, только хардкор!
АЛГОРИТМ ПОСТРОЕНИЯ АЛЛАХА.
Аллах - тот, кто создал вселенную.
Так как, количество атомов во вселенной конечно и бесконечности не существует, то мы можем их все просмотреть.
Рано или поздно мы найдёт атомы Аллаха. Можно даже использовать аксиому выбора для конечных множеств. Из множества атомов нашей вселенной выбираем атомы Аллаха. Содираем атомы Аллах готов.
Аллах - тот, кто создал вселенную.
Так как, количество атомов во вселенной конечно и бесконечности не существует, то мы можем их все просмотреть.
Рано или поздно мы найдёт атомы Аллаха. Можно даже использовать аксиому выбора для конечных множеств. Из множества атомов нашей вселенной выбираем атомы Аллаха. Содираем атомы Аллах готов.
Вычислимость - это просто вычислимость, неважно на чем, на компьютере, на бумаге, в уме. Все равно вся она сводится к машине Тьюринга и любому другому уточнению понятия алгоритма.
>ультрафинитизм
Все равно практически ты дальше ультрафинитизма не уйдешь. Разве что до абстракции потенциальной осуществимости.
Верунство в чистом виде. Если объект нельзя осмотреть в реальности, то его не существует.
>то чисел конечное количество
перечисли их
>Только натуральные числа существуют
Единица также не существует, как и всё остальное.
Существование и его отличие от абстракции потенциальной осуществимости уже обсуждали, не вижу смысла пояснять 101й раз.
Боевая паста это серьезный аргумент, да. И конечно же, по-существу опровергает факт того, что все и правда сто раз уже обсуждалось. Я одного не пойму - ну не осилил ты что-то, так осиль или забудь, бывают вещи, которые понять невозможно, видимо для тебя планка чуть выше плинтуса. Но ты не расстраивайся, ты не один такой. Вот автор этой книжки http://gen.lib.rus.ec/book/index.php?md5=C98BD518044E72E05E4A9FA7FBF55312 тоже неосилил понятие ментальной конструкции по Брауэру. Хотя даже книжки пишет, а не батрушку на мейлру.
Нет, единица это одна палочка |
Абстрактная осуществивость верунство.
Абстракция палочки же. Один дилдак, одна бутыль, один N-петух, это разные вещи, но суть одна - во всех случаях это единица.
Но их может быть только конечное количество. Ты не сможешь нарисовать бесконечное количество палочек и продолжать это делать бесконечно.
Абстракция потенциальной осуществимости - это абстракция потенциальной осуществимости, а не верунство.
Нет, это и есть верунство. Вспомни про чернильную дыру.
>Ты не сможешь нарисовать бесконечное количество палочек и продолжать это делать бесконечно.
Именно поэтому это абстракция. Когда есть правила построения, но сам объект непостроим из-за своей бесконечности. Я это не писал уже не помню сколько раз? Писал. Так что непонятного? Давай, опять сошлись на свою боевую пасту.
>Когда есть правила построения, но сам объект непостроим из-за своей бесконечности.
Тогда существуют правила но не сам объект. Иначе пришлось бы признать существование Аллаха
>Тогда существуют правила но не сам объект.
Походу, начинает доходить. Да, существуют правила, но не объект. Я это не первый год уже пишу. Но возьмем неконструктивную математику. Вжух, и там "существует" уже и алеф0, и алеф100500, и бесконечность. А почему? потому что существование в неконструктивной математике - это непротиворечивость вывода из 10 заповедей аксиом исчисления предикатов. И никто ведь чернильными дырами не кидается. Только конструктивизм это плохо)))
И к проблемам это не приводит.
>И к проблемам это не приводит.
Нет, конечно. Подумаешь, программа Гильберта проебалась, да кризис оснований уже второй век как.
>Да, существуют правила, но не объект.
Тогда Аллах существует в конструктивной математике?
Опять пиши свою боевую пасту, т.к. сто раз обсуждалось, почему Аллах не существует в конструктивной математике - у тебя нет даже правил его построения. Но ты слишком гений, чтобы читать что тебе пишут, чюкча ж не читатель, а писатель? Три треда в бамплимите, и так кроме меня ни до кого ничего и не дошло. Но я это и до вас знал.
Алё, вы из какого века? Кризис оснований закончился, когда теория множеств была аксиоматизирована.
Перекат. https://2ch.hk/math/res/21361.html
- Формализм. В изначальном виде закончился крахом программы Гильберта по формализации арифметики и кризисом оснований.
- Логицизм. Не пошел дальше труда Рассела и Уайтхеда Principia Mathematica.
- Интуиционизм. Дал начало конструктивному направлению, в настоящее время активно развивается в виде конструктивной теории типов Мартин-Лёфа и гомотопической теории типов Воеводского со товарищи.
Обсуждаем дальше.
Предыдущие треды