Вы видите копию треда, сохраненную 12 июня в 13:34.
Скачать тред: только с превью, с превью и прикрепленными файлами.
Второй вариант может долго скачиваться. Файлы будут только в живых или недавно утонувших тредах. Подробнее
Если вам полезен архив М.Двача, пожертвуйте на оплату сервера.
- Формализм. В изначальном виде закончился крахом программы Гильберта по формализации арифметики и кризисом оснований.
- Логицизм. Не пошел дальше труда Рассела и Уайтхеда Principia Mathematica.
- Интуиционизм. Дал начало конструктивному направлению, в настоящее время активно развивается в виде конструктивной теории типов Мартин-Лёфа и гомотопической теории типов Воеводского со товарищи.
Обсуждаем дальше.
Предыдущие треды
Такое слово, как вычислимость, не должно заботить математиков вообще, они же не считают. А вот инжинерам как раз без возможно посчитать что трудно поверить в возможность существования. Ведь как что-то может существовать, если это нельзя посчитать или построить? У них такое в уме не укладывается.
Алгоритмы построения - это computer science, по сути алоритмы нужны программистам и раздел о них - теория алгоритмов, часть информатики. Математика снова тут делать нечего. Вот пример быдлокода обезьяны >>15906
По-сути, становление конструктивистом есть не что инное, как опущение с математика до кодовай макаки или инженеробыдла.
>Такое слово, как вычислимость, не должно заботить математиков вообще,
Оно и не заботило, пока оказалось, что чисто формально нельзя даже доказать, что 1+1=2. Для этого нужны именно вычислимые построения, ординалы ли фон Неймана, нумералы ли Черча, однохуйственно. Но без вычислимости (построимости) никуда. По-сути, в математике кроме вычислимости и невычислимых объектов веры типа исключенного третьего и актуальной бесконечности, ничего и нет. Но, вера в невычислимые сущности это не математика.
Ещё раз говорю, программисты и инженеры таким занимаются.
Им это жизненно необходимо, а математик может класть болт на такие вещи.
>математик может класть болт на такие вещи.
И окукливаться в аутизме, не имеющем ничего общего с математикой.
>И окукливаться в аутизме, не имеющем ничего общего с математикой.
Идеальное названия для программерской параши под названием коструктивная математика.
Я тебя услышал, мнение клована с мейлру, разумеется перевешивает все остальное. Петросянишь такой на мочане, и кризис оснований сам собой рассосался. "Нинужно!!" это не дискуссия а детский сад, если что. Математика = вычислимость, все остальное это просто не математика.
>Я тебя услышал, мнение клована с мейлру, разумеется перевешивает все остальное.
Ты такой же клован, только и можешь, как попугай за Бровером повторять цитатки из библии, как верун. НУ ТАК ЖЕ БРАУЕР СКАЗАЛ, ТАК ЖЕ В БИБЛИИ НАПИСАНО РЯЯЯЯЯЯЯ!
>и кризис оснований сам собой рассосался.
Кризис оснований в 2017, ох лол. Может быть ты ещё от шока, что sqrt(2) не рациональное число, не отошел?
>"Нинужно!!" это не дискуссия а детский сад, если что
Как раз ты так про нормальную математику и кричишь, что вся математика, кроме твоей прогерской параши НИНУЖНАЯ.
>Математика = вычислимость, все остальное это просто не математика.
Ну раз так сказал клоун с мейлача, который начитался шизофазии Брауера, то так оно и есть.
Кукарекуй и дальше, фактов это не отменяет. А факты в том, что кроме конструктивных методов, кризис оснований не преодолим никак, остальные методы показали свою несостоятельность. И если не замечать кризис оснований, он никуда не денется. Методы, отличные от конструктивных работают только в пределах конструктивной математики.
>Кукарекуй и дальше, фактов это не отменяет
Твои фантазии не факты.
>А факты в том, что кроме конструктивных методов, кризис оснований не преодолим никак, остальные методы показали свою несостоятельность.
А разве он не преодолен сейчас?
>Твои фантазии не факты.
Что "мои фантазии", перечисли.
>А разве он не преодолен сейчас?
Нет, разумеется. Более того, никаких формальных и вообще отличных от конструктивных подходов к преодолению за более чем 100 лет не предложено. Собственно, даже Гильберт этого не потянул, куда уж всякой пузатой мелочи.
Как ты противопоставляешь "чисто формальное доказательство" и ординалы?
>Логицизм. Не пошел дальше труда Рассела и Уайтхеда Principia Mathematica.
А разве теория типов - это не развитие идей логицизма?
Часто встречаю такую одну из интерпретаций его вывода: для любой формальной системы есть недоказуемое в рамках этой системы предложение, истинность которого мы тем не менее можем доказать (вне рамок системы).
Этот вывод основывается на предположении, что для формальной системы 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". У нас нет общего алгоритма, который позволил бы строит Гёделево предложение для произвольной формальной системы; подобный алгоритм существует лишь для узкого класса формальных систем.
640x360
>противоречивый аргумент Пенроуза, что человек якобы может доказать то, что не может доказать ни одна формальная система, а значит, наше мышление не может быть смоделировано Машиной Тьюринга.
Это не аргумент, а как принято говорить на бордах, "вскукарек". Аргумент - это что-то более весомое чем батрушка от машины Тьюринга. Этот деятель же не приводит ни одного примера.
Теорем Гёделя о неполноте две. Ты используешь первую.
1ТГ использует непротиворечивость - в противоречивой системе доказуемо вообще всё.
2ТГ утверждает, что непротиворечивость недоказуема.
> Однако доказать, какое из них истинно, мы не можем.
С 2ТГ можем. Теория все еще непротиворечива, но не может доказать собственную непротиворечивость. Ты засунул в неё возможность строить гёделевы утверждения для любого конечного набора аксиом, а она построила бесконечный набор аксиом и уже не может построить гёделево утверждение для себя самой.
> она построила бесконечный набор аксиом и уже не может построить гёделево утверждение для себя самой.
Насколько я понимаю, мы тоже это гёделево утверждение в общем случае построить не можем (можем лишь утверждать, что оно есть). Так как если бы могли, то алгоритмически формализовали бы этот способ и вставили внутрь нашей формальной системы.
А как научиться варить борщ, если приготовление яичницы для меня сущее мучение?
Если слова "элиминация сечения в исчислении секвенций" тебе ни о чем не говорят, то теория доказательств тебе на фиг не нужна. Может, тебе просто какие-нибудь детские книжки почитать, типа Смальяна?
Советую "Теорию множеств" Бурбаки. Проблема школьной геометрии в том, что она требует "строгих" доказательств, при этом совершенно не аргументируя, в чём эта строгость заключается. Мне, когда я был школьником, например, было совершенно непонятно, какие методы доказательства можно использовать, а какие нет, и где вообще выход из порочного круга, когда и так очевидные выводы приходится доказывать с помощью ещё более очевидных. Бурбаки реально очень многое проясняют.
Не очень хороший совет - Бурбаки строят свою теорию на основе эпсилон-оператора Гильберта, который детально не описывают. У начинающих из-за этого возникает недоумение.
> какие методы доказательства можно использовать, а какие нет
Я уже давно не школьник, а мне до сих пор непонятно, только Бурбаки тут, боюсь, не поможет.
С одной стороны, всех пугают, что визуальную очевидность надо засунуть себе в жопу, иначе придет страшная Лемма Жордана и все сдохнут. Но при этом по факту все всё время смотрят на картинку и выводят из неё суждения вида "эта хуйня лежит между вон той и вот этой".
При этом если речь идёт о трёх лучах хер знает в каком порядке, то все говорят "на самом-то деле все углы ориентированные (т. е. ABC= -CBA), так что нам всем похуй".
Почему такие финты ушами можно делать с тремя точками на прямой, можно объяснить только через скалярное произведение, но до него еще дожить надо (да и все равно даже когда доживёшь, фиг тебе кто нормально объяснит).
Поэтому имеется крайне вредная идеология о том, что нужно всегда разбирать случаи, что между чем лежит. Вред прежде всего в том, что если кто решит разобрать действительно все случаи, то помрет в процессе.
Но тем не менее адепты этой ереси встречаются, поэтому ушлых школьников учат: если какое мудило на приёмных приебётся насчёт неразобранного случая про то, что между чем болтается, надо пиздеть так: вся эта ваша сраная геометрия на самом деле про равенство каких-то там ебучих полиномов, а полиномы - они такие твари, что если равны на куске пространства, то и везде равны, а не то у ихней разности будет овердохуя нулей; поэтому моё доказательство для частного случая доказывает также и общий случай. Предполагается, что после такого заявления любое мудило в ужасе съебётся.
Ну, я надеюсь, анон учит геометрию не для школьных экзаменов, а так, изучать евклидову геометрию через аксиомы Евклида-Гильберта - это давно устаревшее извращение. Естественней изучить основы алгебры, ввести векторное пространство, изучить свойства аффинности, а потом навесить на это пространство метрику - вуаля - и геометрия готова. Изучать неафинные метрические пространства (всякие геометрии Лобачевского) - это уже другой вопрос, но для начала этого не требуется.
>вуаля - и геометрия готова
Это будет не геометрия, это будет алгебра. Геометрия - это пикрелейтед.
Твои задачи решаются на основе аксиом векторного пространства с метрикой ничуть не хуже, чем на основе стандартных геометрических аксиом.
Это с помощью этого оператора у бурбаков получилось определение единицы размером во сколько там квадрильенов знаков?
Хорошо. Углы - это по сути комплексные числа с модулем 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³ - то, что нужно.
> никаких трильенов знаков для выражения простейших вещей.
У тебя если лямбда нетипизирована, то можеть зависнуть, а если типизирована, то на каждой формуле надписано доказательство типизированности в специальном исчислении. Так что знаков у тебя тоже ой как много.
Но ведь Бурбаки формализируют не только арифметику, но и всю теорию множеств (по сути, система похожа на ZFC). Это тоже можно сделать лямбда-счислением?
> Это тоже можно сделать лямбда-счислением?
В принципе можно, но есть риск заразиться конструктивизмом и бегать потом объяснять всем, что теория множеств не нужна.
Однажды создатели Coq с удивлением обнаружили, что если в него добавить закон исключенного третьего, то аксиома выбора опровергается. После доработки напильником она больше не опровергается. А мораль этой истории в том, что попытки скрестить слона с китом (ZFC с лямбдами) могут привести к неожиданным результатам.
>это чистый конструктивизм, сводить всю математику к арифметике
Нет, это формализм. Программа Гильберта изначально заключалась в том, чтобы свести всю математику к арифметике, арифметику к некой финитной теории, а непротиворечивость этой финитной теории доказать конечным перебором случаев. Оказалось, что так нельзя.
>это делается проще
Нет, это не делается проще. Ты рассказываешь о наивном, неформализованном подходе, когда большая часть идей остаётся просто на уровне размахивания руками. Гильберт все эти идеи четко формализовал в легкочитаемой книжечке "Основания математики". Если ты нашёл в себе силы обмазываться Мартин-Лёфом, то эту книжку ты просто обязан прочитать.
А разве можно в кок исключенное третье добавить? Оно ж невычислимо, как его в calculus'e of construction выразить?
Книжку почитаю, спасибо. А насчет 'размахивания руками' не согласен. Построения и вычисления таки весомее размахивания руками, как ни крути.
В случае его применения к перечислимым множествам, ага. Но речь'то об исключенном третьем как об аксиоме, т.е. чем'то таком, что истинно в общем случае.
Гильбрет, что забавно, критикует Брауэра именно за недостаток в его интуиционизме построений с вычислениями.
>не только арифметику, но и всю теорию множеств (по сути, система похожа на ZFC). Это тоже можно сделать лямбда-счислением?
Скажем так, не вся лямбда одинаково полезна. В бестиповой и простой типизированной по Черчу нельзя. А вот в любой, включающей в себя лямбда Р (предикатная лямбда (передний правый нижний угол куба) в которой выразим изоморфизм Карри-Говарда), можно. Кок (соответствующий самому дальнему правому верхнему углу куба) включает в себя все остальные варианты как подмножества, поэтому в нем можно сделать ZFC, таки и сделали https://github.com/coq-contribs/zfc
>если лямбда нетипизирована, то можеть зависнуть, а если типизирована, то на каждой формуле надписано доказательство типизированности в специальном исчислении. Так что знаков у тебя тоже ой как много.
Ты о чем? Вот например, в MLTT используется аналог типизированной лямбды, с той разницей что там 4 операции получения выражений - аппликация, абстракция, селекция и комбинация, а вместо типов как таковых т.н. "арности". Т.е. каждое выражение от простой константы и переменной до сложных составных термов имеет соотв. ему арность. Все обозначения, нужные для этого, прямо приводятся, и там нет никаких триллионов знаков.
Барендрехтом решил обмазаться? Там надо все разбирать с самого начала вообще. Если чего-то не понял, дальше и читать не стоит, т.к. материал дается последовательно и на основе того, за что уже пояснено.
Да вроде и до 2.1.8 всё понятно. А уже совсем непонятные преобразования начались. С fixed point theorem есть какое-то только совсем интуитивное понимание (типа есть функция, которая просто возвращает аргумент и чего-то там еще), какой-то комбинатор, не пойми чего. Но от того что какой-то школьник из Румынии на английской (на слух он мне вообще непонятен) поясняет за это всё (хотя может чуть другое вроде) у меня неплохой такой Барендрехт. Для меня какой-то слишком резкий переход случился в этой книге, не знаю почему, как и что делать.
Вообще, если что-то в лямбде непонятно, лучше гуглить и на примерах разбирать в том же хаскелле. Типа комбинатора неподвижной точки http://www.wikiznanie.ru/wikipedia/index.php/Комбинатор_неподвижной_точки
А доказательство какой-нибудь теоремы Цермело в такой системе тоже будет выглядеть не слишком длинным?
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 мы не можем. То есть мы не можем развеять сомнения в непротиворечивости слишком сильной теории, доказав эту непротиворечивость в теории более слабой, в которой мы более уверены.
Ну, я как раз пытаюсь осмыслить вопрос наиболее рационально, именно поэтому и использую язык теории вероятностей.
Ладно, посмотрим, что из этого выйдет.
>Ну если ты занимаешься математикой, тебе неплохо было бы представлять, чем именно ты занимаешься. Это не только математики касается, с любой наукой так.
не является ответом на
>...кто объяснит в чём заключается суть операции "дать обоснование математики"...
Он хотел не методами самой теории, а "финитарными". По-поводу того, что такое "финитарные методы" он целую книжку написал: интуитивно, всякие комбинаторные рассуждения про значки и как и что из них выводить - это ок, трансфинитные индукции, большие кардиналы и прочее - это не ок. Потом (или сразу, или ранее, не суть) все поверили, что финитарные методы ~ доказуемо в PA (или IE_1 - это по вкусу), а дальше историю ты знаешь.
Для начала можно Барендрехта, Lambda calculi with types.
На практике это не так. Как-то раз в HOL4 доказали ложь из-за какого-то извратного бага в бета-редукции. Но доказательства, формализованные в HOL4, выжили.
Даже глючная система может быть практически полезна. Конечно, теоретически она совершенно неинтересна, потому что в ней доказуемо всё. Но даже если такая система ловит 99% человеческих ошибок, она все равно поднимает вероятность, что всё правильно.
Смотря, что тебе надо, если Software Foundations - это одно, а если в ZFC палочкой потыкать, то другое.
Не знаю, но знаю, что ответ на вопрос: "Что такое Х?", не может состоять из оценочного суждения по поводу того, что мне было бы плохо, а что неплохо представлять, если я чем-то там занимаюсь.
Насколько я слышал сила конструктивистов оказалась их же слабостью, из-за тех ограничений, которые они наложили, они закрыли себе доступ ко многим результатам. Правда ли это?
Понятия не имею.
А как же кубическая теория типов(к интуиционистам)? Про неё забыли, а ведь очень клёвая штука, посмотрите.
Там эта унивалентность прямо встраивается в правила вывода.
>А как же кубическая теория типов(к интуиционистам)?
Куб лямбда-исчислений "а-ля Черч" Барендрегта и соотв. ему по изоморфизму Карри-Говарда куб логических исчислений? Так это самый интуиционизм и есть, точнее конструктивизм, но обычно и то и другое используют как синонимы. Все логики в таком кубе априори конструктивные, поскольку лямбда типизирована и логические константы имеют конструктивное значение (пруф-объекты своих типов).
>очень клёвая штука, посмотрите. Там эта унивалентность прямо встраивается в правила вывода.
Да, это очень полезная вещь. Не какие-то там невычислимые объекты веры типа ислюченного третьего.
А почему плохо? Я заметил, тут у некоторых конкретный такой БАРЕНДРЕХТ от конструктивизма, даже от простого упоминания триггерятся и начинают вести себя как бесноватые на приеме у экзорциста.
так-то я сто раз уже говорил, почему хорошо - потому что вычислимо.
ну так на уровне метатеории классическая математика тоже вычислима (в том смысле, что все утверждения об объектах в ней вычислимы).
Во-первых, любая формальная система есть конструктивный объект, согласно Мартин-Лёфу.
Во-вторых есть вычислимость и вычислимость. В метаматематике "вычислим" и закон исключенного третьего в том смысле, что он не противоречит гильбертовскому исчислению высказываний, например. Однако, ему не во всех случаях может соответствовать вычислимое построение.
Допустим, у тебя есть предикат пиздатости и ты доказал в классической логике, что существует пиздатое число. Есть только маленькая проблема: у тебя нет никакой зацепки, чтобы это число построить. В каком смысле оно существует? Витает в воздухе вокруг тебя? А если не витает, то может быть, оно на самом-то деле и не существует-то?
А то, что утверждение доказуемо, это-то вычислимо, но это просто факт про скобочки и буквочки. Вдруг это утверждение не имеет никакого отношения к реальности?
Тебе выше правильно пояснили, выводимость чего'то в классической логике не обязана вести к построению этого чего'то, поскольку класмическая логика не рассматривает интерпретацию логических констант, там это просто буковы и их синтаксис без семантики. Полная аналогия такого подхода это выводимость существования Аллаха из корана. Правил его построения из такого доказательства ты не выведешь.
Правила построения дают возможность работать с объектами построения, доказывать их свойства непосредственно, а не выводить из каких'то заповедей. Гарантированная выводимость, непротиворечивость и отсутствие парадоксов. Классический подход всего этого не гарантирует, а значит не может служить основаниями математики, что доказал кризис оснований.
А зачем мне 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.
Конструктивизм занимается ровно этим же самым - исследует воображаемые сонмы сущностей. Однако делает это "со связанными руками", фанатично ограничивая себя требованием вычислимости. Вычислимость, о которой говорят конструктивисты, - воображаемая. Ведь все алгоритмы, которые рассматривают конструктивисты, существуют лишь в воображении конструктивистов. Выполнить эти алгоритмы в реальности невозможно - см. аргумент Вавилова о чернильной дыре. Так, в реальном мире невозможно построить два в степени гугол, несмотря на то, что вообразить алгоритм построения такого числа очень легко. Ибо для построения этого числа потребуется больше атомов, чем есть во всей вселенной. Претензии конструктивистов на якобы большую реалистичность по сравнению с математикой не имеют под собой почвы. Конструктивисты занимаются тем же самым воображением объектов, которым занимаются математики, однако почему-то кричат, что вовсе не пользуются никакими воображением.
У конструктивистов считается, что воображение не может быть связано с реальным миром. Конструктивисты заблуждаются. Например, если я возьму монетку и воображу её падение на землю, а потом действительно брошу монетку на землю, - я увижу почти то же самое, что я вообразил.
Для людей, которые стоят на позициях решительного утилитаризма и оценивают всякую деятельность постольку, поскольку она полезна в народном хозяйстве, также есть аргумент в защиту неограниченного воображения. А именно - математические теории можно рассматривать как черный ящик, как умозрительную машину, шестеренки которой приводятся в движение силой воображения; на вход подаются данные, на выходе получается предсказание. Никому не нужно, чтобы все воображаемые шестеренки такого калькулятора чему-либо соответствовали в реальном мире. Достаточно, чтобы он давал корректный результат при всех задачах, в которых ценное для утилитариста народное хозяйство нуждается. Если совершенно фантастические объекты верно предсказывают надои чугуна, то нет никаких причин требовать от этих объектов быть реальными. Математики занимаются созданием и обслуживаением фантастических шестеренок, строят в своём воображении конструкции, которые нужны лишь для других воображаемых конструкций. Каждый из математических объектов сам по себе для народного хозяйства бесполезен, однако из некоторых математических объектов в конце концов можно собрать очередную машину предсказаний. И нормальная математика справляется с этим куда лучше, чем конструктивизм. Достаточно указать на то, что все воображаемые шестеренки, лежащие под капотом классического анализа, в конструктивизме не существуют, - а вместе с этим невычислимый матан обусловил научную революцию и радикально изменил бытие человечества.
Математики, конечно, не видят смысл своей деятельности в создании калькуляторов. Математики в основном занимаются математикой, которая интересна внутри математики - употребляется в других разделах или даёт повод для воображения и изучения каких-то новых интересных сущностей. Полезные для народного хозяйства калькуляторы получаются непредсказуемым образом, лишь как случайный побочный продукт.
Математика изучает воображаемые сущности. Эти сущности, согласно неокантианству, расположены в созерцательном пространстве, что даёт возможность делать о них априорные синтетические суждения. Эти суждения называются определениями. Применение к определениям аналитических рассуждений позволяет чётче осознать, чем же являются рассматриваемые (в созерцательном пространстве) объекты.
Проще говоря, математик сначала воображает что-то, затем делает несколько утверждений о воображенном объекте, затем из этих утверждений выводит следствия.
Поместить в созерцательное пространство и начать созерцать можно какую угодно идею. Но не всякие идеи обладают тем изящным свойством, что при их созерцании получается много аналитических суждений, сложным образом связанных друг с другом. Лишь те идеи, при воображении которых достоверно получается много нескучных теорем, изучаются математикой и называются математическими объектами.
Похожей деятельностью занимаются вообще все теоретики - все они воображают. Однако у математики есть всё-таки своя специфика. Говорить о ней я не буду, потому что это слишком интимная вещь. Продолжу разговор о созерцательном пространстве.
Обычно воображается не одна-единственная сущность, но целый сонм сущностей. Этот сонм называется универсумом. Сущности, входящие в универсум, однородны в следующем смысле. Каждое определение можно рассматривать как фильтр, сквозь который одни сущности универсума проходят, другие не проходят. Сущности, которые проходят через фильтр, неразличимы этим фильтром. Так вот, для всякого универсума есть определение, относительно которого все объекты универсума неразличимы. Для универсума теории групп таким определением является группа - все сущности универсума подходят под это определение. Для универсума теории колец таким определением является кольцо. Для метаматематики универсумом является сонм текстов. И т.п.
Для каких-то универсумов есть описания, позволяющие составить представление о сущностях, входящих в сонм, для каких-то универсумов таких описаний нет. Например, для универсума стандартной теории множеств есть описание: именно, под универсумом понимается кумулятивная иерархия фон Неймана. Этот универсум обозначается V. Вместе с тем, легко воображаются универсумы множеств, которые могут напоминать, а могут и не напоминать V. Эти универсумы описываются неклассическими теориями множеств.
Существование понимается относительно какого-то универсума. Если объект x существует относительно U, то это означает, что при воображении универсума U необходимо также иметь в виду и объект x. Несуществование x соответственно означает, что при воображении универсума не следует воображать x.
Конструктивизм занимается ровно этим же самым - исследует воображаемые сонмы сущностей. Однако делает это "со связанными руками", фанатично ограничивая себя требованием вычислимости. Вычислимость, о которой говорят конструктивисты, - воображаемая. Ведь все алгоритмы, которые рассматривают конструктивисты, существуют лишь в воображении конструктивистов. Выполнить эти алгоритмы в реальности невозможно - см. аргумент Вавилова о чернильной дыре. Так, в реальном мире невозможно построить два в степени гугол, несмотря на то, что вообразить алгоритм построения такого числа очень легко. Ибо для построения этого числа потребуется больше атомов, чем есть во всей вселенной. Претензии конструктивистов на якобы большую реалистичность по сравнению с математикой не имеют под собой почвы. Конструктивисты занимаются тем же самым воображением объектов, которым занимаются математики, однако почему-то кричат, что вовсе не пользуются никакими воображением.
У конструктивистов считается, что воображение не может быть связано с реальным миром. Конструктивисты заблуждаются. Например, если я возьму монетку и воображу её падение на землю, а потом действительно брошу монетку на землю, - я увижу почти то же самое, что я вообразил.
Для людей, которые стоят на позициях решительного утилитаризма и оценивают всякую деятельность постольку, поскольку она полезна в народном хозяйстве, также есть аргумент в защиту неограниченного воображения. А именно - математические теории можно рассматривать как черный ящик, как умозрительную машину, шестеренки которой приводятся в движение силой воображения; на вход подаются данные, на выходе получается предсказание. Никому не нужно, чтобы все воображаемые шестеренки такого калькулятора чему-либо соответствовали в реальном мире. Достаточно, чтобы он давал корректный результат при всех задачах, в которых ценное для утилитариста народное хозяйство нуждается. Если совершенно фантастические объекты верно предсказывают надои чугуна, то нет никаких причин требовать от этих объектов быть реальными. Математики занимаются созданием и обслуживаением фантастических шестеренок, строят в своём воображении конструкции, которые нужны лишь для других воображаемых конструкций. Каждый из математических объектов сам по себе для народного хозяйства бесполезен, однако из некоторых математических объектов в конце концов можно собрать очередную машину предсказаний. И нормальная математика справляется с этим куда лучше, чем конструктивизм. Достаточно указать на то, что все воображаемые шестеренки, лежащие под капотом классического анализа, в конструктивизме не существуют, - а вместе с этим невычислимый матан обусловил научную революцию и радикально изменил бытие человечества.
Математики, конечно, не видят смысл своей деятельности в создании калькуляторов. Математики в основном занимаются математикой, которая интересна внутри математики - употребляется в других разделах или даёт повод для воображения и изучения каких-то новых интересных сущностей. Полезные для народного хозяйства калькуляторы получаются непредсказуемым образом, лишь как случайный побочный продукт.
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^континуум - точно нет. Джерри Бона припечатал еще лучше: "аксиома выбора очевидно верна, теорема Цермело очевидно неверна, а лемма Цорна - хз". Матанщики начали что-то верещать только тогда, когда им заявили, что неважно, одно у них яичко или два. И то только потому, что это-то они смогли понять, а про существование всяких долбанутых кардиналов никто из них ничего не понял.
Ну и дела. Неокантианство. Мало нам было простого мира идей, так теперь мы можем еще и населять мир идей реальными объектами посредством воображения. Кажется, что-то похожее прозвучало недавно в письме Холмогорова Познеру: "Тысячу лет миллионы людей в этой стране денно и нощно молились Богу с такой истовостью и серьезностью веры, жили в такой плотной атмосфере чуда, что даже если бы Вы и подобные Вам были бы правы, и Бога бы не существовало, то здесь, в России, Он стал реальность."
Вот по чётным дням недели я, например, воображаю множества из 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
Аксиомы у него, правда, странноватые, но когда это останавливало классиков? Сам ведь говорил, что главное, чтобы следствия были интересными.
> для разных разделов математики следует использовать разные теории множеств
>>18783
>Есть математика, великая и неделимая,
Вот это вот один великий и неделимый анон написал?
> все выводимо из данного контекста по данным правилам, а кроме контекста и правил ничего не дано?
Ты видимо думаешь, что раз истинности в классическом понимании нет, то и от неполноты ты избавлен. Но есть совершенно конкретное утверждение: модель системы в ней самой никогда не докажет ложь. И это утверждение недоказуемо, потому что вторая теорема Гёделя. Можно ли это назвать неполнотой - это другой вопрос, но все обычно считают, что это она самая.
> я ведь обосновываю свою позицию, даже со ссылками
Давай так попробуем:
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.
Если мы рассматриваем "пруф" как конструктивный пруф-объект, а не как какое-то отвлеченное понятие сферической истины в вакууме, то такой пруф непосредственно выводим, как и его отсутствие (пустой тип). Разве нет?
>Можно ли это назвать неполнотой - это другой вопрос, но все обычно считают, что это она самая.
А с какой стати так считать, не подскажешь?
> пруф непосредственно выводим, как и его отсутствие (пустой тип)
Тут надо аккуратнее говорить, потому что у тебя две системы - одна в другой - и по желанию можно еще завести третью снаружи, из которой можно наблюдать эквивалентность тех двух. А "конструктивный пруф-объект" хрен перенесёшь между уровнями.
> А с какой стати так считать, не подскажешь?
Ну например, чтобы разговаривать с остальными на одном языке. А так можешь назвать это световодозвуконепроницаемостью.
>у тебя две системы - одна в другой - и по желанию можно еще завести третью снаружи, из которой можно наблюдать эквивалентность тех двух.
А к чему все это анальное шапито? Из самой конструктивной системы можно вывести все, что из нее вообще выводимо. Ну построишь внутри нее такую же, результат-то тот же самый будет.
>А "конструктивный пруф-объект" хрен перенесёшь между уровнями.
Потому тчо как ни крути, результат будет одним и тем же. Так к чему все эти уровни?
> Ну построишь внутри нее такую же
Ну а как иначе теорию доказательств развивать?
> Потому тчо как ни крути, результат будет одним и тем же.
Да нет же, смотри:
докажешь в большой системе, что в большой системе нельзя доказать ложь? тривиально!
докажешь в большой системе, что в маленькой системе нельзя доказать ложь? облом!
Но если большая и маленькая система это одно и то же, как тогда? И еще раз, "доказательство" - это что? Если конструктивный пруф-объект, то он ведь и является своим доказательством. И он будет одним и тем же для того, что ты называешь большой и маленькой системой, разве нет?
> И он будет одним и тем же
Да нет же! Между системами есть изоморфизм, причём с точки зрения сверхбольшой ("нашей") системы это изоморфизм тривиален, но этот изоморфизм нельзя выразить на языке большой системы, потому что где-то обязательно поломаются типы. Вот такая она, неполнота.
>Между системами есть изоморфизм, причём с точки зрения сверхбольшой ("нашей") системы это изоморфизм тривиален, но этот изоморфизм нельзя выразить на языке большой системы, потому что где-то обязательно поломаются типы.
А с чего они поломаются, если они одни и те же для всех систем? И изоморфизм между ними в том, что они эквивалентны. Где и что поломается-то, поясни.
Проиграл с пикчи.
> если они одни и те же для всех систем?
Как же они одни и те же, если они разных типов? Доказательство лжи в большой системе имеет с точки зрения большой системы тип ложь, а доказательство лжи в маленькой системе имеет с точки зрения большой системы тип "доказательство чего-то в маленькой системе".
Ты еще скажи, что 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 интуиционизмом эта мысль имеет примерно нихуя общего.
Ты так сказал? Гугли акты интуиционизма.
Это не формальная система. Формальная система матлогика. В ней уже есть парадокс Лжеца, собственно. Что ты этим хотел сказать?
То и хотел сказать, что теорема о неполноте есть вариант парадокса лжеца. Ну и она так же часть матлогики. Тут другое интересно, какая польза математике от этих софизмов? Доказали возможность закодировать в матлогике неразрешимые парадоксы, так Брауэр об этом 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я глава.
Гейтинг первый же и дропнул изначальные идеи Брауэра. Книжка неплохая, тем более советское издание с комментариями Маркова. Но это уже больше конструктивизм чем интуиционизм как его понимал Брауэр.
И у меня не работает, капчую с Германии теперь.
>Глубже Брауэра в смысле поиска оснований в ментальных построениях все равно никто пока не копнул. Но это не предел, т.к. сам Брауэр не идет дальше кантианского понимания праинтуиции, в его время не были известны нейрофизиологические субстраты восприятия времени и основанные на нем интуиции натурального числа и континуума. Это сейчас все это изучено довольно глубоко, но зато сам интуиционизм в брауэровском понимании дропнули.
Принято считать, что ограниченность науки в изучении психических процессов состоит в том, что в кругу прочих возможных объектов исследования она избирает те, что хотя бы потенциально могут быть обнаружены в материальной реальности и поддаются измерению. Именно поэтому она предпочитает опираться на свет, который проливают инструментальные исследования мозга, притом что сама темнота этого предмета остается все такой же непроницаемой.
Тем не менее, Лакан показывает, что причина малых успехов нейрофизиологии не в этом, а в том, что наука стойко избегает коллизий, связанных с работой означающего. Это и является причиной, в силу которой она отделена стеной от феномена, к которому Фрейд подошел с такой легкостью — к феномену сновидения.
От Лакана мы знаем, чем эта легкость была оплачена — Фрейд взял ее в долг у лингвистики, как раз открывшей для себя к тому времени существование означающего. Тем не менее, произведенный Фрейдом продукт оказался лингвистике не нужен — Фрейд извлек из него совершенно особую логику, ставшую основой самостоятельной психоаналитической науки.
Наука эта способна объяснить некоторые примечательные явления, связанные с нарушением обычного процесса протекания сновидения. Так, когда некто видит «осознанный» сон, полагая, что его осознанность доказывается лишь тем, что он в этом сне способен сказать себе «я вижу этот сон», или просыпается от случайного звука, который задним числом оказался встроен в сновидение так, что к моменту внезапного пробуждения сон оказывает логически завершен, то все эти процессы обязаны именно работе означающего. Эта работа и обуславливает возможность занять в своем сне метапозицию, превратив его в люцидный, или же увидеть сон именно по той причине, что процесс сна оказался прерван — то есть, сделать невозможное и успеть сам пробуждающий стимул обыграть как полноразмерное сновидение.
Там где «строгая» наука, также соблазненная этими загадочными явлениями, в итоге с ними не справляется и, перебрав разнообразные физиологические причины, уступает место паранаучным догадкам, психоанализ объясняет их структуру и показывает, что все эти труднопостижимые трюки становятся возможными, поскольку работа означающего задает особый порядок времени.
По всей видимости, иные психические акты, происходящие в бодрствовании — такие как смех, забывание, принятие решения — в своей логике временного сбывания устроены так же сложно, как и нарушенное, прерванное сновидение. Это лишь подтверждает ту блеснувшую у Фрейда догадку, что само бодрствование — не что иное, как нарушение сна.
>Глубже Брауэра в смысле поиска оснований в ментальных построениях все равно никто пока не копнул. Но это не предел, т.к. сам Брауэр не идет дальше кантианского понимания праинтуиции, в его время не были известны нейрофизиологические субстраты восприятия времени и основанные на нем интуиции натурального числа и континуума. Это сейчас все это изучено довольно глубоко, но зато сам интуиционизм в брауэровском понимании дропнули.
Принято считать, что ограниченность науки в изучении психических процессов состоит в том, что в кругу прочих возможных объектов исследования она избирает те, что хотя бы потенциально могут быть обнаружены в материальной реальности и поддаются измерению. Именно поэтому она предпочитает опираться на свет, который проливают инструментальные исследования мозга, притом что сама темнота этого предмета остается все такой же непроницаемой.
Тем не менее, Лакан показывает, что причина малых успехов нейрофизиологии не в этом, а в том, что наука стойко избегает коллизий, связанных с работой означающего. Это и является причиной, в силу которой она отделена стеной от феномена, к которому Фрейд подошел с такой легкостью — к феномену сновидения.
От Лакана мы знаем, чем эта легкость была оплачена — Фрейд взял ее в долг у лингвистики, как раз открывшей для себя к тому времени существование означающего. Тем не менее, произведенный Фрейдом продукт оказался лингвистике не нужен — Фрейд извлек из него совершенно особую логику, ставшую основой самостоятельной психоаналитической науки.
Наука эта способна объяснить некоторые примечательные явления, связанные с нарушением обычного процесса протекания сновидения. Так, когда некто видит «осознанный» сон, полагая, что его осознанность доказывается лишь тем, что он в этом сне способен сказать себе «я вижу этот сон», или просыпается от случайного звука, который задним числом оказался встроен в сновидение так, что к моменту внезапного пробуждения сон оказывает логически завершен, то все эти процессы обязаны именно работе означающего. Эта работа и обуславливает возможность занять в своем сне метапозицию, превратив его в люцидный, или же увидеть сон именно по той причине, что процесс сна оказался прерван — то есть, сделать невозможное и успеть сам пробуждающий стимул обыграть как полноразмерное сновидение.
Там где «строгая» наука, также соблазненная этими загадочными явлениями, в итоге с ними не справляется и, перебрав разнообразные физиологические причины, уступает место паранаучным догадкам, психоанализ объясняет их структуру и показывает, что все эти труднопостижимые трюки становятся возможными, поскольку работа означающего задает особый порядок времени.
По всей видимости, иные психические акты, происходящие в бодрствовании — такие как смех, забывание, принятие решения — в своей логике временного сбывания устроены так же сложно, как и нарушенное, прерванное сновидение. Это лишь подтверждает ту блеснувшую у Фрейда догадку, что само бодрствование — не что иное, как нарушение сна.
Тебе - наверняка (как и что либо вообще).
Есть даже лингвистические основания математики, т.н. сигнифика Маннури. Там тоже все связано с семиотикой и прочим таким. Но инфы по этой теме даже на английском маловато, в основном оригиналы на датском. Так что Лакан этот твой вряд ли что'то может добавить в математику помимо того, что в нее уже добавили ребята из венского кружка сто+ лет назад.
Может быть. Но фишка той штуки в другом маленько.
>Лакан
Это не тот дешевый шут, которого обоссали в одной популярной книжке за неадекватное ничему разумному употребление математических терминов в своей шизофазии?
Да
не, это Лакан обстоятельно пояснил за весь научный дискурс, а Докинз и приближённые просто тонну баттхёрта на бумагу высрали, как какие-нибудь школьники Ларинофаги
Пришло время запостить "пояснения" Лакана.
...
Эта диаграмма (лента Мебиуса) может быть рассмотрена как основание некоей изначальной надписи, находящейся в ядре, конституирующем субъекта. Это значит гораздо больше, чем вы сперва могли бы подумать, поскольку вы можете поискать тип поверхности, способной принимать такие надписи. Вы, возможно заметите, что сфера, древний символ цельности, не подходит. Подобный разрез способны принимать на себя тор, бутылка Кляйна, поверхность cross-cut[16]. Причем само разнообразие весьма важно, поскольку оно многое объясняет в структуре душевных заболеваний. Если субъект можно символизировать таким фундаментальным разрезом, то точно так же можно показать, что разрез на торе соответствует невротическому субъекту, а разрез на поверхности cross-cut — другому виду душевного заболевания.
...
В этом пространстве наслаждения взять нечто ограниченное, закрытое — это взять место, и говорить о нем — это значит заниматься топологией.
...
Здесь я предлагаю ввести термин «компактность». Не может быть ничего компактнее зазора, если понять, что, допуская существование пересечения всего того, что закрывается, на бесконечном числе множеств, мы приходим к выводу, что пересечение включает в себя это бесконечное число. Это и есть определение компактности.
...
Формулу нам дает та топология, которую я охарактеризовал как самую позднюю по времени возникновения, поскольку она отправлялась от логики, построенной на исследовании числа, которое привело к заданию места, которое не является местом гомогенного пространства. Возьмем все то же ограниченное, закрытое, предположительно устойчивое место — эквивалент того, что я только что сказал о пересечении, расширяющемся до бесконечности. Если предположить, что оно покрыто открытыми множествами, то есть множествами, исключающими своей предел — предел, чтобы вам это вкратце напомнить, — это то, что определяется как большее одной точки и меньшее другой, но никогда не равное ни отправной точке, ни конечной[20] — обнаруживается доказательство того, что равным образом можно сказать так: множество этих открытых пространств всегда поддается неполному покрытию открытыми пространствами, задающими конечность; то есть последовательность элементов задает конечную последовательность.
...
Субъект в той половине, где он определяется отрицаемыми кванторами, относится к тому, что ничто существующее не создает предела функции, что невозможно удостовериться в чем бы то ни было, относящемся к универсуму. Таким образом, если основываться на этой половине, «они», женщины, не «не все», и, следовательно, отсюда же получается, что ни одна из них не является также всей.
...
Мы в свою очередь будем отправляться от того, что выражает буквенное сокращение S(∅), то есть от означающего.
Поскольку тем самым связка означающих дополняется, это означающее может быть лишь чертой, которая прочерчивается из круга означающих, не имея возможности быть подсчитанным в нем. Это символизируется внутренней связью (-1) с множеством означающих.
Как таковое его нельзя произнести, но не его действие, поскольку это действие совершается всякий раз, как произносится собственное имя. Его высказывание равно его значению.
Откуда вытекает следующая формула, если подсчитать это значение в используемой нами алгебре:
S(означающее) / S(означаемое) = S(высказывание)
а при S=(-l) мы имеем: s=√-1.
...
Вот каким образом эректильный орган начинает символизировать место наслаждения, причем не сам по себе и не в качестве образа, а как часть, недостающая желаемому образу: поэтому-то его и можно приравнять к √-1 более высоко произведенного значения, к √-1 наслаждения, которое он восстанавливает посредством коэффициента своего высказывания в функции нехватки означающего.
Пришло время запостить "пояснения" Лакана.
...
Эта диаграмма (лента Мебиуса) может быть рассмотрена как основание некоей изначальной надписи, находящейся в ядре, конституирующем субъекта. Это значит гораздо больше, чем вы сперва могли бы подумать, поскольку вы можете поискать тип поверхности, способной принимать такие надписи. Вы, возможно заметите, что сфера, древний символ цельности, не подходит. Подобный разрез способны принимать на себя тор, бутылка Кляйна, поверхность cross-cut[16]. Причем само разнообразие весьма важно, поскольку оно многое объясняет в структуре душевных заболеваний. Если субъект можно символизировать таким фундаментальным разрезом, то точно так же можно показать, что разрез на торе соответствует невротическому субъекту, а разрез на поверхности cross-cut — другому виду душевного заболевания.
...
В этом пространстве наслаждения взять нечто ограниченное, закрытое — это взять место, и говорить о нем — это значит заниматься топологией.
...
Здесь я предлагаю ввести термин «компактность». Не может быть ничего компактнее зазора, если понять, что, допуская существование пересечения всего того, что закрывается, на бесконечном числе множеств, мы приходим к выводу, что пересечение включает в себя это бесконечное число. Это и есть определение компактности.
...
Формулу нам дает та топология, которую я охарактеризовал как самую позднюю по времени возникновения, поскольку она отправлялась от логики, построенной на исследовании числа, которое привело к заданию места, которое не является местом гомогенного пространства. Возьмем все то же ограниченное, закрытое, предположительно устойчивое место — эквивалент того, что я только что сказал о пересечении, расширяющемся до бесконечности. Если предположить, что оно покрыто открытыми множествами, то есть множествами, исключающими своей предел — предел, чтобы вам это вкратце напомнить, — это то, что определяется как большее одной точки и меньшее другой, но никогда не равное ни отправной точке, ни конечной[20] — обнаруживается доказательство того, что равным образом можно сказать так: множество этих открытых пространств всегда поддается неполному покрытию открытыми пространствами, задающими конечность; то есть последовательность элементов задает конечную последовательность.
...
Субъект в той половине, где он определяется отрицаемыми кванторами, относится к тому, что ничто существующее не создает предела функции, что невозможно удостовериться в чем бы то ни было, относящемся к универсуму. Таким образом, если основываться на этой половине, «они», женщины, не «не все», и, следовательно, отсюда же получается, что ни одна из них не является также всей.
...
Мы в свою очередь будем отправляться от того, что выражает буквенное сокращение S(∅), то есть от означающего.
Поскольку тем самым связка означающих дополняется, это означающее может быть лишь чертой, которая прочерчивается из круга означающих, не имея возможности быть подсчитанным в нем. Это символизируется внутренней связью (-1) с множеством означающих.
Как таковое его нельзя произнести, но не его действие, поскольку это действие совершается всякий раз, как произносится собственное имя. Его высказывание равно его значению.
Откуда вытекает следующая формула, если подсчитать это значение в используемой нами алгебре:
S(означающее) / S(означаемое) = S(высказывание)
а при S=(-l) мы имеем: s=√-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, все равно приходит очередной или один и тот же, но предельно гениальный зеленый феласаф и сказка про белого бычка начинается сначала. Нету конструктивной математики? Ок, раз школьники на мейлру так пишут, то и правда нету. Я все понял, все услышал.
Я могу показать математику - мне достаточно дать ссылку на архив или на матнет.
Ты не можешь показать конструктивизм - максимум можешь вырезать скрин из Мартин-Лёфа.
А ссылка на Мартин-Лефа это не ссылка, и его конструктивная теория типов это не теория и не конструктивная и не типов, я тебя правильно же понимаю, да? Зачем ты вообще все это пишешь?
Представь, что некий философ Мартинда выдумал подход, который назвал "деконструктивная математика". Он написал много букв про то, какой деконструктивизм хороший и какая вся остальная математика плохая. Но все его тексты посвящены исключительно деконструктивной математике, никакие, скажем, теоремы об индексе он доказать даже и не пытался. Назовёшь ли ты математикой деятельность философа Мартинды? Будешь ли утверждать, что миллионы книг по математике равновелики трем с половиной его брошюркам?
То есть, конструктивные доказательства это не доказательства, пруверы это не пруверы? Может быть, я виноват, что ты про все это не слышал? Ты попробуй не просто писать, а думать о том, что пишешь.
Я могу перечислять книги по математике несколько часов подряд и ни разу не повториться. Ты, если попытаешься перечислить книги по якобы существующей "конструктивной математике", не наберешь и сотни. Да что там, даже десятка.
Предъяви набор конструктивных книг, равнообъемных хотя бы трактату Бурбаки.
Дарья Донцова написала больше книг, чем Бурбаки, значит математика бурбаков не существует, это твоя логика. Подумой и не пиши хуйни, ок?
Математика необъятна.
Конструктивизм исчерпывается двумя-тремя книжками.
И ты говоришь, что это равновеликие науки?
Особенно тау-символ конструктивен, эквивалентный глобальному выбору.
Просто дай список ъ-конструктивистской литературы. Хотя бы из ста наименований. Или не сможешь?
>чтобы дропнуть невычислимые суеверия
Ага подорвать пару столбов математики, а потом смотреть как всё здания к хуям разрушается. Конструктивистов как и ИГИЛ надо запретить.
Ты хотел сказать формалистов, да!?
Ничего не разрушили кроме пары суеверий, зато построили полностью вычислимые основания. Как оказалось, математика ничего не потеряла, если из нее выкинуть суеверия, такой нежданчик.
Во-первых, даже устоявшейся терминологии в конструктивизме нет. Во-вторых, на этих якобы "основаниях" никакой дальнейшей конструкции не возведено.
>кроме пары суеверий
Содержание программы Вербицкого - это пара суеверий?
> Во-первых, даже устоявшейся терминологии в конструктивизме нет. Во-вторых, на этих якобы "основаниях" никакой дальнейшей конструкции не возведено.
Завязывай уже хуйню писать, а.
> Ты называешь всю программу Вербицкого суеверием.
Вербицкий это бородатый такой, писал про АКАБов и цитировал стишок 'из западного ануса все жрете вы говно, за кока колу сраную продались вы давно'?
Переход на личности не делает тебе чести.
http://imperium.lenin.ru/~verbit/MATH/programma.html
Вот смотри, я сто раз давал определение конструктивного объекта. Если после этого я вижу предъявы уровня того, что выше по треду, я не могу не отметить бесполезность своих попыток что-то объяснить. А имея в виду исключительную простоту такого определения, не могу не сделать напрашивающегося вывода об умственных способностях того, кому я пытаюсь что-то объяснить. Тут именно в личности проблема, а не в моем подходе, увы.
Конструктивизм не оставляет от математики камня на камне. Уничтоженным оказывается всё, что перечислено в программе Вербицкого. А ты только смеешься над этим.
>зато построили полностью вычислимые основания.
Когда там комплюктеры докажут гипотезу Римана?
>Как оказалось, математика ничего не потеряла
Математика тем и славится, что даже такое сборище аутяг, как конструктивисты имеют право на существование.
> Когда там комплюктеры докажут гипотезу Римана?
Ты ее без комплюктера докажи, умник. Понапридумывают всякой заведомо бесконечной хуйни, потом удивляются почему эти маняпроблемы столетиями никто решить не может. Очевидно же, что конструктивное решение есть построение, отсюда последнему довну ясно почему эти манягипотезы недоказуемы. Я тебе сходу могу таких выдумать и хуй ты их докажешь даже без конструктивизма. Например, прикол 'купи слона' неразрешим, это тоже теперь математическая проблема тысячелетия? Аутисты блядь кого'то в аутизме обвиняют, вообще пушка. Причем, обвиняют самых здравомыслящих, чья идея как раз в отказе от невычислимых верований.
Ты читать умеешь? Не нужно выдумывать хуйни, нужно читать на что отвечаешь, раз уж отвечаешь (последнее вообще необязательно). В данном случае, там уже есть ответ.
Гипотеза - это гипотеза. Суеверия - это актуальная бесконечность, исключенное третье.
С Риманом всё ясно.
А ты можешь доказать, что всякое бесконечное множество содержит счетное подмножество?
>доказать, что всякое бесконечное
Пиздец, с кем сижу на одном мейлру. В предыдущем моем посте ответ про "всякое бесконечное". Ну вот что таким докажешь? Тебе сколько раз нужно написать, что "конструктивное доказательство это построение", чтобы до тебя наконец это бы дошло? Конструктивное множество - это правило, по которому можно порождать элементы множества, то есть строить их. Если таковых нет, то это не множество, а категория. Я даже могу сказать, что следующим вопросом будет привести примеры таких множеств и таких правил. Будто я это сто раз не делал. Сказка про белого бычка.
Допустимы ли обороты вроде "пусть M - множество решений уравнения x^7+3x^2+x+1=0"? При условии, что я не знаю формулы для порождения решений.
Если переменные х заданы в виде контекста, н-р если это лямбда-термы, принадлежащие своему типу, так же заданному в виде контекста, что-нибудь уровня х:А, то да. Такой "оборот" в данном случае был бы спецификацией программы, порождающей решения этого уравнения. Естественно, предварительно должны быть заданы операции "=, ^, +" как лямбда-термы имеющие свой тип, или выражения имеющие соотв. арности, что почти одно и то же.
И да, спецификация такой программы / доказательства что одно и то же, согласно изоморфизму Карри-Говарда, может быть задана, если ее решения низвестны, пикрелейтед - спецификация теоремы Ферма. Задать ее можно, решением было бы построение всех примеров, удовлетворяющих данной спецификации. Если в процессе построения нашлось бы решение, не удовлетворяющее такой спецификации, оно было бы конструктивным доказательством ложности теоремы Ферма. Опять же, я сто раз это писал уже.
> что я не знаю формулы для порождения решений.
Для конструктива не обязательно нужна формула. Смотри, если многочлен нечётной степени, то у него для некоторого большого K (K > 0) при подстановке K и -K получатся числа разных знаков, а значит бисекцией можно найти корень. Для многочлена чётной степени надо продифференцировать, если все экстремумы лежат где надо, то корней нет. Если нашли один корень, делим на него и повторяем всё это. Вот у тебя и получится множество корней.
Само ты толсто.
Больцано-Коши неверна для произвольных непрерывных функций, но разные варианты с равномерной непрерывностью или гладкостью верны, а для многочленов-то вообще проблем нет.
>Ты ее без комплюктера докажи, умник.
Не погоди, твоя же конструктивная математика самая конструктивная и самая настоящая, а все остальные нужно выкинуть на помойку, так?
>Понапридумывают всякой заведомо бесконечной хуйни
Ну-ну, простые числа вполне осязаемы. Впрочем я не удивлюсь, если среднестатистический конструктивист сможет в них что-то понять.
>Очевидно же, что конструктивное решение есть построение
Мне насрать, ты говоришь что конструктивная хуйня лучше дедовского аксиоматического, формалистического картофана с аксиомами выбора и.т.д Так докажи, своим конструктивистким пиздежом, хоть что-нибудь новое, а не дрочи, как последний дрочила. Пока единственное, что я слышу от мамкиных конструктивистов тут, это пиздеж что их математика лучше. Моё мнение таково: пока каждый занимается своим аутизмом, всё в порядке, когда кто-нибудь начинает лезть в залупу, его надо загонять под шконарь.
> Мне насрать, ты говоришь что конструктивная хуйня лучше дедовского аксиоматического, формалистического картофана с аксиомами выбора и.т.д Так докажи, своим конструктивистким пиздежом, хоть что-нибудь новое, а не дрочи, как последний дрочила. Пока единственное, что я слышу от мамкиных конструктивистов тут, это пиздеж что их математика лучше. Моё мнение таково: пока каждый занимается своим аутизмом, всё в порядке, когда кто-нибудь начинает лезть в залупу, его надо загонять под шконарь.
Таблетки выпей, бесноватый. Дедовское как раз все конструктивное, это потом поналезло умников, затыкать все дыры в математике актуальной бесконечностью, исключенным третьим и прочей невычислимой шляпой. Итог очевиден - кризис оснований. И я уже сто раз говорил, что использовать свое незнание как доказательство чего- то есть признак долбаеба.
Окей. Может глупый вопрос, но делает ли трансцендентность pi это самое pi суеверием? Его же в принципе нельзя вычислить с окончательной точностью до n-го знака.
> Окей. Может глупый вопрос, но делает ли трансцендентность pi это самое pi суеверием? Его же в принципе нельзя вычислить с окончательной точностью до n-го знака.
Пи это правило построения. Это потенциальная бесконечность. Актуальная бесконечность не соответствует никакому построению либо правилам построения.
Но ведь потенциальная бесконечность ничем не лучше актуальной.
>Это потенциальная бесконечность
Ты что дурак что ли блять?
Вот хорошо, сумма ряда 1/2^n равна двум, как известно. По твоему что, этот ряд имеет конец?
Сумма ряда != ряд, не?
Ой, да у нас тут аниме, становится интересно.
>Итог очевиден - кризис оснований.
Итак появляются петухи, которые кукарекают, что надо всё до основания разрушить. Где-то я уже это слышал.
1) упомянутая теория излагается автором с чисто классических позиций - православный матан, теорвер, все эти интегральчики, предельчики и прочий знакомый любому школьцу картофан. Никакой ереси типа лямбда-исчисления, MLTT и прочего Барендрехта даже не упоминается, хотя очевидно, что функции неплохо было бы рассмотреть с точки зрения самой нормальной теории функций - лямбда калькулюса, тем более что речь конкретно о вычислимых функциях.
2) тем не менее, сама теория про некоторый класс алгоритмов, их обоснование, в общем, о доказательствах некоторых их свойств, полезных с точки зрения машинного обучения. Т.е. про нечто изначально конструктивное и построимое на комплюктере. Опять же, конструктивный подход к вопросу, изоморфизм Карри-Говарда, не упоминается даже вскользь, хотя он именно об этом.
3) из предыдущих пунктов очевидно, что в теории статистического обучения классический подход используется как, скажем, "дискретизация" такового, ограниченная вычислительными возможностями железа и софта, т.е. значение функций, предела функции и т.д. на самом деле ограничены 12 или около того знаками после запятой, а не нарисованным знаком бесконечности, длина примеров в датасете тоже конечна, хотя в формулах попадаются выражение типа стремления длины выборки к бесконечности и т.д.
Отсюда вопрос, конструктивна ли теория статистического обучения? Если с одной стороны там даже не упоминается конструктивизм, а с другой - все теоремы, следствия и доказательства этой теории непосредственно построимы? Хотелось бы услышать манямнения.
1) упомянутая теория излагается автором с чисто классических позиций - православный матан, теорвер, все эти интегральчики, предельчики и прочий знакомый любому школьцу картофан. Никакой ереси типа лямбда-исчисления, MLTT и прочего Барендрехта даже не упоминается, хотя очевидно, что функции неплохо было бы рассмотреть с точки зрения самой нормальной теории функций - лямбда калькулюса, тем более что речь конкретно о вычислимых функциях.
2) тем не менее, сама теория про некоторый класс алгоритмов, их обоснование, в общем, о доказательствах некоторых их свойств, полезных с точки зрения машинного обучения. Т.е. про нечто изначально конструктивное и построимое на комплюктере. Опять же, конструктивный подход к вопросу, изоморфизм Карри-Говарда, не упоминается даже вскользь, хотя он именно об этом.
3) из предыдущих пунктов очевидно, что в теории статистического обучения классический подход используется как, скажем, "дискретизация" такового, ограниченная вычислительными возможностями железа и софта, т.е. значение функций, предела функции и т.д. на самом деле ограничены 12 или около того знаками после запятой, а не нарисованным знаком бесконечности, длина примеров в датасете тоже конечна, хотя в формулах попадаются выражение типа стремления длины выборки к бесконечности и т.д.
Отсюда вопрос, конструктивна ли теория статистического обучения? Если с одной стороны там даже не упоминается конструктивизм, а с другой - все теоремы, следствия и доказательства этой теории непосредственно построимы? Хотелось бы услышать манямнения.
По-моему ответ очевиден: нет. Построенная теория неконструктивна. Но можно построить аналогичную конструктивную теорию, которая, быть может, даже будет лучше. Но никто этим пока не занимался, видимо.
>Построенная теория неконструктивна. Но можно построить аналогичную конструктивную теорию, которая, быть может, даже будет лучше.
Тогда в чем разница? Если вместо пределов, интегралов и т.д. можно гонять соответствующие этим выражениям лямбда-термы и наоборот, то возникает закономерный вопрос, а зачем всякие актуальные бесконечности, которые все равно ни к одной практической задаче не пришить? Где она, бесконечность, если любая практическая задача, любое осуществимое вычисление все равно имеет дело с чем-то конечным? Ну кроме потенциальной бесконечности типа программ для машины Тьюринга, не приводящих к останову. Еще Брауэр показал, что континуум непостроим, т.к. между двумя соседними вещественными числами всегда можно вкорячить их еще сколько угодно. Но на практике "сколько угодно" всегда ограничивается доступными вычислительными возможностями. Т.е. в конечном счете все равно все имеют дело с конструктивным, т.е. построимым и вычислимым.
Единственные реальные примеры неконструктивной математики - это парадоксы а единственное реальное достижение неконструктивной математики это кризис оснований. Все, что не сводится к антиномиям и программам для машины Тьюринга, не приводящим к останову, вычислимо и т.о. конструктивно, безотносительно в каких формализмах выражено.
>Еще Брауэр показал, что континуум непостроим, т.к. между двумя соседними вещественными числами всегда можно вкорячить их еще сколько угодно.
А какая разница построим он или нет?
То есть нормальному математику должно быть похуй на эти конструктивистко-муслимские разборки?
>А какая разница построим он или нет?
Вот есть всякие кардиналы алеф1 и выше, бет и т.д. Они ничему построимому и вычислимому не соответствуют, это чистая религия а не математика.
>>20359
Нормальный математик во всех случаях пользуется конструктивной математикой, я же даже пример привел >>20313 но как и предполагал, для мейлру это слишком сложно. Ты не приведешь пример практического использования неконструктивной математики кроме парадоксов и прочего кризиса оснований.
>>20361
В MLTT и HoTT ее используют. Дальше сам.
> HoTT
Это какая-то модная йоба по типу новых оснований?
> Они ничему построимому
Но как-то же их построили или чисто с потолка взяли и решили, ага, вот охуенная штука алеф1, будем в неё веровать.
> и вычислимому не соответствуют
А должны?
>Но как-то же их построили или чисто с потолка взяли и решили, ага, вот охуенная штука алеф1, будем в неё веровать.
Их никак не построили, они непостроимы. Просто значок, за которым не стоит ничего. Взяли не с потолка, но около того.
>А должны?
Нет, конечно. Только невычислимое это не математика.
>Это какая-то модная йоба по типу новых оснований?
Пикрелейтед.
>Даже школьники будут с ними работать?
Они будут работать даже без школьников. Полностью механизированные доказательства.
Да.
>Ты не приведешь пример практического использования неконструктивной математики кроме парадоксов и прочего кризиса оснований.
>практического использования
Для копания картохи подойдёт только конструктивизм? Почему меня как математика должна интересовать практическая применимость.
Да и ясно, что у картофенов бомбит с парадоксов, картошку-то банахом-тарским не удвоишь.
Если триггернулся на слово "практическое", замени на "вычислимое". Невычислимой математики несуществует, т.к. это уже не математика. Отсюда, все эти актуальные бесконечности и т.д. на самом деле не используются никем, даже если подразумеваются.
>Невычислимой математики несуществует, т.к. это уже не математика.
>континуум непостроим
Инженеры используют интегральчики с континумом, постоянно разбивая график на бесконечное число прямоугольников. Где твой Бровер теперь?
Но они же не считают его напрямую в лоб как ты собирался бесконечность считать? ты что, дурак что ли блять?, а пользуются теоремой шницель птуцера и переводят из пустого в порожнее/повышают степень на единицу и делят на эту самую степень.
Или раскладывают в ряд по теореме ноги макаронины с округлением/указанием пределов в которых находится вычисляемая величина.
мимо
Я чуть выше привел похожий пример с теорией статистического обучения и объяснил для одаренных, что нет там никаких бесконечностей, даже если значки бесконечности и стоят, то подразумевается конечное. Даже если используются интегралы и пределы, по факту все считается до конечного числа знаков после запятой, редко превышающего 12. И где теперь ваша актуальная бесконечность, если ее нет ни в одной задаче?
>по факту все считается до конечного числа знаков после запятой, редко превышающего 12
А какая разница, как там инженеры считают? Математик может запросто сравнить числа с бесконечными знаками, после запятой.
>даже если значки бесконечности и стоят, то подразумевается конечное.
Тогда почему они так часто говорят о бесконечности, особенно им нравятся бесконечно малые.
> А какая разница, как там инженеры считают? Математик может запросто сравнить числа с бесконечными знаками, после запятой.
Не может. Практических методов сделать это не существует. Нарисовать значок бесконечности или Аллаха не равно построить эти сущности.
> Тогда почему они так часто говорят о бесконечности, особенно им нравятся бесконечно малые.
Какая разница, о чем они говорят? Важно то, что они делают.
Покажи неконструктивную для начала. Я еще раз говорю, все эти значки бесконечностей просто спецэффекты, работать можно только с вычислимым.
Иди куда шел со своими картинками, во всяком случае, мимо этого треда, ты же даже не в состоянии понять, о чем тут вообще говорят, тем более понять аргументы. Сто раз уже сказал, что нет там никаких бесконечностей, их никто не способен считать, потому что они невычислимы. Нахуя ты мне картинку показываешь, ты что, ебнутый? Ты если не способен понять о чем речь, нахуя вообще сюда пишешь?
Маня, у Мартин-Лёфа есть конструктивное доказательство аксиомы выбора, в MLTT это не аксиома, в которую надобно веровать, а доказуемая теорема. И я сто раз давал ссылку на это доказательство. Сасай-кудасай.
>это не аксиома, в которую надобно веровать, а доказуемая теорема
Дай угодаю, только для конечных множест?
Как будто кто'то может пользоваться бесконечными. Бесконечность невычислима, алё, есть кто дома?
Вера в возможность не равна возможности так же как нарисованный значок бесконечности не равен бесконечности.
Вообще, у меня есть подозрения, что ты, мил человек, селедка. По собственному опыту могу судить, что только бабе похуй на фактическую аргументацию, в угоду своему оценочному суждению. Покажи-ка сиськи пример как по'твоему математики могут вычислить невычислимое.
(Автор этого поста был предупрежден.)
>фактическую аргументацию
Ты про?
>тебе не понять
>так сказал брауэер
>я уже сто раз говорил
>ваша математика не математика
>100 раз говорил
>кризис оснований, парадоксы
>>20454
Раз мы говорим, по сути, о сущностях, которые находяться в платоновском мире идей, то почему бесконечное количество чего-то не может существовать?
> Раз мы говорим, по сути, о сущностях, которые находяться в платоновском мире идей, то почему бесконечное количество чего-то не может существовать?
Потому что математика это не вера в платоновский мир идей. Нет никакого мира идей, есть вычислимые построения и всякая вера. Последнее это не математика.
Твои вычислимые построения такая же вера. У тебя не хватит атомов во вселенной, чтобы эксперементально всё вычислить. Ты даже десятичную запись числа Грэма не напишешь.
Я не собираюсь читать целую книгу о прикладухе, чтобы доказать что-то анону с двачей.
Не неси опять хуйни по новой. Никто неюикогда не утверждал фактическую построимость потенциально построимых объектов. Ты этого даже понять не способен, о чем тут вообще говорить.
Раз мы не можем её фактически построить, то получаем, что верим в существования этого объекта?
> Раз мы не можем её фактически построить, то получаем, что верим в существования этого объекта?
Я просто уже даже не помню, сколько раз объяснял разницу между фактическим конструктивным объектом, потенциально но не фактически построимым и актуальной бесконечностью. 1005001 ый раз не хочу, ты слишком тупой, алибидерчи.
Ненене, я понимаю.
Смотри, у нас есть платоновский мир, но ты выделяешь из него только те объекты, для построения которых есть алгоритм. Но платоновскими они не перестают быть, поскольку мы не можем проверить в реальности их существование.
Я другой анон. Конструктивные математики не привязываются никоим образом к реальному миру и не стараются ограничить себя им. Тебе следует разобраться, что такое ментальные математические конструкции и правила их построения. Я не смогу это сделать, тут нужен тот анон, но он кажется заеб*лся повторять всё это три треда подряд)
— Потому.
— Ты ебанутый?
— На это неоднократно давался ответ.
— Ты можешь доказать формулу Гаусса?
— Твоя вера не нужна.
— Пошёл нахуй, ебанашка.
— Ты не воспринимаешь объективные аргументы.
— Какие?
— Хватит спрашивать одно и то же.
— Ты издеваешься. Ты не можешь писать это всерьёз.
— Я не виноват, что ты такой тупой.
>Конструктивные математики не привязываются никоим образом к реальному миру и не стараются ограничить себя им.
Я понимаю это и в таком контексте обзывательства кого-то в вере выглядит бессмысленым.
Ну, можно посмотреть количество проектов на гитхабе, если хочется статистики... Но не уверен, что от этого будет толк. Единого репозитория всей математики, как я понимаю, нет.
Нужно всех заставить им пользоваться, а Сталина у нас нету?
> В чем сложность создания такого репозитория?
Некому этим заняться. Потом, 99% использования кока это личные цели, задачи передоказать на нем всю математику никто не ставил и желающих этим заниматься нет. Главная проблема в том, что все это нужно пилить вручную, а это долго, нудно и сложно. Это одна из основных проблем пруверов вообще, в свое время де Браун сотоварищи перевели на язык первого прувера AUTOMATH аж целую книжку Ландау 'Grundlagen', все это есть в инторнетах, можно оценить ебейшую сложность такой задачи лично. Далее, чтобы перевести в кок некую теорию, нужно быть неплохим спецом в вопросах этой теории, ну если это не какое'нибудь исчисление пропозишенов. Как пример можно привести ядро НоТТ на коке, кроме Воеводского с соратниками вряд ли кто осилит такую задачу, см. соотв. пейперы. К счастью, автоматизация подобных задач таки возможна, если вспомнить некоторые идеи т.н. 'сигнифики'. Я сейчас как раз этим пытаюсь заниматься в свободное время, которого у меня нет нихуя. Возможно, скоро покажу конкретные примеры.
> только маленького количества математики, конструктивной.
> -пофиксил тебя
Не шаришь, так не нес бы хоть хуйни. Простой пример, озвученный в предыдущем посте, верификация Grundlagen Ландау, не имеющей ничего общего с конструктивной математикой с помощью изначально 100% конструктивной типизированной лямбды-Р. Как бы ты для себя объяснил возможность этого? Хотя о чем я спрашиваю анэнцефала из рашки.
Вы тут настолько убоги, что не способны даже элементарные вещи изложить своими словами. Сам'то читал что пишешь?
>почему существование в математике сводится к построимости
Существует объединение любого множества.
> Существует объединение любого множества.
С этой стороны тоже бесполезно, придумай что'нибудь еще. Хотя бы потому, что твоя формулировка вызывает как минимум два вопроса, 'что значит 'существует'' и 'что значит 'любого''. Если существование сводить к платоновским верованиям в мировую душу и мир идей, то это чистая религия. Если к нарисованному значку на бамаге, то опять же, я и символ Аллаха могу нарисовать. И так далее. Все это уже обсуждалось и не интересно.
>я и символ Аллаха могу нарисовать
Ну нарисуй. Никто тебя за язык не тянул. Определение Аллаха на языке логики первого порядка в студию.
> . Определение Аллаха на языке логики первого порядка в студию.
Сорта на самом деле. И там и там невычислимые актуальные бесконечности, за которые предлагается верить, что это основа всего.
Этот пример я привожу как раз по причине его невычислимости. Ты же ссылаешься на логику первого порядка, хотя в ней верен невычислимый общий случай исключённого третьего. Одно невычислимое ничем не лучше другого столь же невычислимого. Завязывай со своей демагогией, ты прекрасно понимаешь это. Понимаешь, что так или иначе невозможно обойти вопрос 'что есть существование в математике?'. Все это неоднократно обсуждалось, я стопервый раз все это пишу просто потому что мне на работке еще до утра сычевать и надо чем'то убить время.
Я могу предложить первопорядковую теорию множеств. Ты не можешь предложить первопорядковую теорию Аллаха. Поэтому я могу говорить про множества, а ты не можешь говорить про Аллаха.
Перестань упоминать Аллаха, это тупо и очень бесит. Или определяй его.
> Я могу предложить первопорядковую теорию множеств
Опирающуюся на невычислимые верования типа актуальной бесконечности и исключенного третьего.
> Ты говоришь, что можешь формализовать Аллаха.
Где я это говорил? Не разводи демагогию, я такого не говорил вообще никогда, ты уясни другое, логикой первого порядка ты можешь пользоваться лишь постольку, поскольку позволяет изоморфизм Карри-Говарда. Вне этих рамок ты ничего не докажешь этой логикой, т.к доказательства твои за пределами вышеупомянутого изоморфизма будут ничем не лучше корана.
Я указываю тебе на разницу между первопорядковыми теориями и кораном. Ты не можешь формализовать Аллаха первопорядковой теорией, в принципе. И ты об этом осведомлен. Поскольку ты продолжаешь использовать фразы "символ Аллаха могу нарисовать" и "не лучше корана", остаётся только один вывод. Ты осознанно лжёшь.
> Я указываю тебе на разницу между первопорядковыми теориями и кораном.
Вне изоморфизма Карри-Говарда их нет.
Жду примеров: ты заинтриговал.
> Ты говоришь, что разницы нет. Тогда почему ты не можешь написать теорию Аллаха?
Выше отвечал уже.
Отвечал. Я ж говорю, ты даже читать не умеешь, какая тебе математика. Ладно читать, даже потралить не в состоянии. Ты либо реально селедка, либо аутист со стажем на бордах максимум месяца два.
(Автор этого поста был предупрежден.)
Ну так процитируй свой ответ.
Очень просто. Эта и ей подобные теории формулируются в виде спецификаций (я давал пример спецификации теоремы Ферма), затем находится решение, удовлетворяющее такой спецификации, если множество таких решений не пусто, это конструктивно доказывает исходную теорему. Конструктивное доказательство это построение, все просто же.
Конструктивисты говорят, что вся математика - манявыдумки. У математиков от этого бугурт.
Зачем несешь хуйню? Полтора невычислимых верования - исключенное третье как общий принцип и актуальная бесконечность, это полтора верования, а не 'вся математика'.
> В чем суть конструктивной математики
В вычислимости. Источник кризиса оснований - невычислимые догмы, которые неясно зачем вообще в математику притащили.
На этом построена вся математика, начиная с анализа.
> Источник кризиса оснований - невычислимые догмы
Я думал, что источник кризиса – злоупотребление формализмом.
> которые неясно зачем вообще в математику притащили
Творческое удобство? Эвристический метод?
Весь кризис в головах.
Пока одни говорят что это все эзотеризм, вторые что это норма, третьи считают ящики и двигают науку вперед.
Короче, все как всегда. Полтора дебила друг друга говном поливают пока все остальные покуривают трубки и обсуждают дальнейший ход событий, посмеиваясь над клоунами в говне.
инб4 НА ПАЛЬЦАХ НИПАСЩЕТАТЬ!!! КАНТИНУМ НЕ КАНТИНУМ!!! АКСЕОМА ВИБОРА ЕТА АБМАН!!!
> Я думал, что источник кризиса – злоупотребление формализмом.
Злоупотребление невычислимыми сущностями тогда уж. Тут никто не понимает простейших вещей, даже не знаю как это можно объяснить еще проще, и так элементарные вещи обсуждаем. Похоже, по новой та же сказка про белого бычка намечается.
> Вычислимость такая же догма.
Да нет, вычислимость это не догма, это фактический результат. Ты даже и этого не понимаешь, пиздец же настоящий.
>>21254
> Расскажи, как ты пришёл к конструктивизму. Кто тебя ему научил?
Конструктивизм is fine too, конечно же, особенно MLTT великая вещь, но мне наиболее интересен интуиционизм Брауэра в его первоначальном чистом варианте. Брауэру пришлось от него отказаться по причинам им же и озвученным, а вот я нашел, как можно обойти эти причины, как минимум частично. К слову, конструктивизм не формализует интуиционизма, но аргументы того же Гейтинга на этот счет даже некоторые авторы работ на эту тему не пони мают, чего говорить о мейлру. Как пришел, очевидно же, в книжках прочитал.
> Да нет, вычислимость это не догма, это фактический результат.
Пруфов, конечно, не будет.
> Брауэра
Лженаука.
> Пруфов, конечно, не будет.
Изоморфизм Карри-Говарда пруф кококо лжинаука)))
> Лженаука.
Ну раз на мейлру так пишут, то ладно.
>вычислимость это не догма, это фактический результат
>Изоморфизм Карри-Говарда пруф
Здесь нет логической связи. Из утверждения о существовании изоморфизма Карри-Говарда не вытекает логически, что вычислимость это не догма. С тем же успехом можно было бы говорить "теория струн ошибочна", а в ответ на резонные вопросы заявлять "диагональный метод Кантора пруф" и дальше молчать.
> Здесь нет логической связи.
Я понял тебя, услышал. Уровень твоих знаний в данной теме мне ясен. Мне неясно другое, зачем ты мне пишешь и что пытаешься доказать? Что конструктивизм тебе непонятен, а его основные моменты и их взаимосвязи тебе ни о чем не говорят? Ок, ладно.
>Конечное число.
Перемножаем все известные простые числа
@
добавляем к результату единицу
@
маняматик с двоща обсасывает километры хуйцов
Но так можно сделать только конечно число раз, поскольку актуально бесконечности не существует, то количество простыз чисел конечно.
Ну я же говорю, о чем можно спорить с тем, кто не отличает актуальной бесконечности от абстракции потенциальной осуществимости. Школуйня, блядь.
>то количество простыз чисел конечно.
Ну тогда тебе не составит труда перечислить их прямо в этом итт тренде.
>Ну я же говорю, о чем можно спорить с тем, кто не отличает актуальной бесконечности от абстракции потенциальной осуществимости.
У нас нет компьютера для того, что все простые числа запрограммировать.
>>21280
Нет, я не умею программировать. Тут кок запускать придёться.
>>21285
Бесконечность и есть религия.
Значит, он был веруном.
Бесконечность может быть вида доделаю, а может быть вида "не знаю как падступицца".
Анон с мейлру даже Кнута Исскуство Программирования не читал. О чем с вами говорить? Сколько раз про слова Брауэра говорю, может мне ещё количество Аллахов в треде подсчитать.
>Бесконечность может быть вида доделаю,
Бесконечности не существует, это вера сектантов. Можно и Аллаха доделовать бесконечно.
>Нет, я не умею программировать. Тут кок запускать придёться.
Не, ну давай пруф на то что простых чисел конечное число или всё таки не конечное?
Если нет правил построения актуальной бесконечности, то чисел конечное количество.
Только натуральные числа существуют, остальные игрушка дьявола и вера с непостроимыми сущностями.
>Математика - это вычислимость.
Причем, вычислимость на компьютере! Только ультрафинитизм, только хардкор!
Аллах - тот, кто создал вселенную.
Так как, количество атомов во вселенной конечно и бесконечности не существует, то мы можем их все просмотреть.
Рано или поздно мы найдёт атомы Аллаха. Можно даже использовать аксиому выбора для конечных множеств. Из множества атомов нашей вселенной выбираем атомы Аллаха. Содираем атомы Аллах готов.
Вычислимость - это просто вычислимость, неважно на чем, на компьютере, на бумаге, в уме. Все равно вся она сводится к машине Тьюринга и любому другому уточнению понятия алгоритма.
>ультрафинитизм
Все равно практически ты дальше ультрафинитизма не уйдешь. Разве что до абстракции потенциальной осуществимости.
Верунство в чистом виде. Если объект нельзя осмотреть в реальности, то его не существует.
Существование и его отличие от абстракции потенциальной осуществимости уже обсуждали, не вижу смысла пояснять 101й раз.
Боевая паста это серьезный аргумент, да. И конечно же, по-существу опровергает факт того, что все и правда сто раз уже обсуждалось. Я одного не пойму - ну не осилил ты что-то, так осиль или забудь, бывают вещи, которые понять невозможно, видимо для тебя планка чуть выше плинтуса. Но ты не расстраивайся, ты не один такой. Вот автор этой книжки http://gen.lib.rus.ec/book/index.php?md5=C98BD518044E72E05E4A9FA7FBF55312 тоже неосилил понятие ментальной конструкции по Брауэру. Хотя даже книжки пишет, а не батрушку на мейлру.
Абстракция палочки же. Один дилдак, одна бутыль, один N-петух, это разные вещи, но суть одна - во всех случаях это единица.
Но их может быть только конечное количество. Ты не сможешь нарисовать бесконечное количество палочек и продолжать это делать бесконечно.
Абстракция потенциальной осуществимости - это абстракция потенциальной осуществимости, а не верунство.
Нет, это и есть верунство. Вспомни про чернильную дыру.
>Ты не сможешь нарисовать бесконечное количество палочек и продолжать это делать бесконечно.
Именно поэтому это абстракция. Когда есть правила построения, но сам объект непостроим из-за своей бесконечности. Я это не писал уже не помню сколько раз? Писал. Так что непонятного? Давай, опять сошлись на свою боевую пасту.
>Тогда существуют правила но не сам объект.
Походу, начинает доходить. Да, существуют правила, но не объект. Я это не первый год уже пишу. Но возьмем неконструктивную математику. Вжух, и там "существует" уже и алеф0, и алеф100500, и бесконечность. А почему? потому что существование в неконструктивной математике - это непротиворечивость вывода из 10 заповедей аксиом исчисления предикатов. И никто ведь чернильными дырами не кидается. Только конструктивизм это плохо)))
>И к проблемам это не приводит.
Нет, конечно. Подумаешь, программа Гильберта проебалась, да кризис оснований уже второй век как.
Опять пиши свою боевую пасту, т.к. сто раз обсуждалось, почему Аллах не существует в конструктивной математике - у тебя нет даже правил его построения. Но ты слишком гений, чтобы читать что тебе пишут, чюкча ж не читатель, а писатель? Три треда в бамплимите, и так кроме меня ни до кого ничего и не дошло. Но я это и до вас знал.
Алё, вы из какого века? Кризис оснований закончился, когда теория множеств была аксиоматизирована.
Вы видите копию треда, сохраненную 12 июня в 13:34.
Скачать тред: только с превью, с превью и прикрепленными файлами.
Второй вариант может долго скачиваться. Файлы будут только в живых или недавно утонувших тредах. Подробнее
Если вам полезен архив М.Двача, пожертвуйте на оплату сервера.