Двач.hk не отвечает.
Вы видите копию треда, сохраненную 12 июня в 13:34.

Скачать тред: только с превью, с превью и прикрепленными файлами.
Второй вариант может долго скачиваться. Файлы будут только в живых или недавно утонувших тредах. Подробнее

Если вам полезен архив М.Двача, пожертвуйте на оплату сервера.
Оснований тред №3 17772 В конец треда | Веб
Тред обсуждений оснований математики. 3 основные направления в основаниях:
- Формализм. В изначальном виде закончился крахом программы Гильберта по формализации арифметики и кризисом оснований.
- Логицизм. Не пошел дальше труда Рассела и Уайтхеда Principia Mathematica.
- Интуиционизм. Дал начало конструктивному направлению, в настоящее время активно развивается в виде конструктивной теории типов Мартин-Лёфа и гомотопической теории типов Воеводского со товарищи.
Обсуждаем дальше.

Предыдущие треды
2 17775
Предыдущий - https://2ch.hk/math/res/3694.html (М)
3 17778
Конструктивная математика это не математика, а рак!
Такое слово, как вычислимость, не должно заботить математиков вообще, они же не считают. А вот инжинерам как раз без возможно посчитать что трудно поверить в возможность существования. Ведь как что-то может существовать, если это нельзя посчитать или построить? У них такое в уме не укладывается.
Алгоритмы построения - это computer science, по сути алоритмы нужны программистам и раздел о них - теория алгоритмов, часть информатики. Математика снова тут делать нечего. Вот пример быдлокода обезьяны >>15906
По-сути, становление конструктивистом есть не что инное, как опущение с математика до кодовай макаки или инженеробыдла.
4 17780
>>17778

>Такое слово, как вычислимость, не должно заботить математиков вообще,


Оно и не заботило, пока оказалось, что чисто формально нельзя даже доказать, что 1+1=2. Для этого нужны именно вычислимые построения, ординалы ли фон Неймана, нумералы ли Черча, однохуйственно. Но без вычислимости (построимости) никуда. По-сути, в математике кроме вычислимости и невычислимых объектов веры типа исключенного третьего и актуальной бесконечности, ничего и нет. Но, вера в невычислимые сущности это не математика.
5 17783
>>17780
Ещё раз говорю, программисты и инженеры таким занимаются.
Им это жизненно необходимо, а математик может класть болт на такие вещи.
quote-one-cannot-inquire-into-the-foundations-and-nature-of[...].jpg71 Кб, 850x400
6 17784
>>17783

>математик может класть болт на такие вещи.


И окукливаться в аутизме, не имеющем ничего общего с математикой.
7 17785
>>17784

>И окукливаться в аутизме, не имеющем ничего общего с математикой.


Идеальное названия для программерской параши под названием коструктивная математика.
8 17786
>>17785
Я тебя услышал, мнение клована с мейлру, разумеется перевешивает все остальное. Петросянишь такой на мочане, и кризис оснований сам собой рассосался. "Нинужно!!" это не дискуссия а детский сад, если что. Математика = вычислимость, все остальное это просто не математика.
9 17790
>>17786

>Я тебя услышал, мнение клована с мейлру, разумеется перевешивает все остальное.


Ты такой же клован, только и можешь, как попугай за Бровером повторять цитатки из библии, как верун. НУ ТАК ЖЕ БРАУЕР СКАЗАЛ, ТАК ЖЕ В БИБЛИИ НАПИСАНО РЯЯЯЯЯЯЯ!

>и кризис оснований сам собой рассосался.


Кризис оснований в 2017, ох лол. Может быть ты ещё от шока, что sqrt(2) не рациональное число, не отошел?

>"Нинужно!!" это не дискуссия а детский сад, если что


Как раз ты так про нормальную математику и кричишь, что вся математика, кроме твоей прогерской параши НИНУЖНАЯ.

>Математика = вычислимость, все остальное это просто не математика.


Ну раз так сказал клоун с мейлача, который начитался шизофазии Брауера, то так оно и есть.
10 17791
>>17790
Кукарекуй и дальше, фактов это не отменяет. А факты в том, что кроме конструктивных методов, кризис оснований не преодолим никак, остальные методы показали свою несостоятельность. И если не замечать кризис оснований, он никуда не денется. Методы, отличные от конструктивных работают только в пределах конструктивной математики.
11 17792
>>17791

>Кукарекуй и дальше, фактов это не отменяет


Твои фантазии не факты.

>А факты в том, что кроме конструктивных методов, кризис оснований не преодолим никак, остальные методы показали свою несостоятельность.


А разве он не преодолен сейчас?
12 17793
>>17792

>Твои фантазии не факты.


Что "мои фантазии", перечисли.

>А разве он не преодолен сейчас?


Нет, разумеется. Более того, никаких формальных и вообще отличных от конструктивных подходов к преодолению за более чем 100 лет не предложено. Собственно, даже Гильберт этого не потянул, куда уж всякой пузатой мелочи.
50KEN-WISKUNDIGE-BROUWERpreview-772x800.jpg84 Кб, 1200x800
13 17805
Да, я еще заметил, что тут на мейлру даже не понимают, что есть вычислимость. И есть подозрения, что сводят ее к арифметической вычислимости хотя в целом любую вычислимость можно свести к арифметике, через лексикографическое упорядосивание слов в алфавитах или через геделевскую нумерацию, но это слишком сложно для этой параши не понимая, что вообще говоря, речь о несколько ином. Скажем, о вычислимых функциях в лямбда-исчислении или в более простом объяснении к сводимости одного выражения к другому. Совсем никто не понимает, в чем разница между простой игрой в знакосочетания и вычислением построимых объектов, между каноническими и неканоническими элементами и множествами, и даже между языком и метаязыком. Зато, желающих покукарекать, при этом не понимая вышеперечисленных азов, всегда достаточно. Так вот, основной тезис в том, что математика = вычислимость, иначе это не математика, нужно понимать следующим образом: вы не сможете привести ни одного примера применения математики, не сводящегося к вычислению. Ни одного примера, противоречащего тезису Черча. Всякие исключенные третьи и актуальные бесконечности - это пример игры в знакосочетания, за которыми ничего не стоит, которые ни во что не вычисляются даже в виде потенциальной осуществимости, т.е. правил таких вычислений. И поэтому такая хуета есть источник парадоксов и кризисов в математике.
14 17807
>>17780
Как ты противопоставляешь "чисто формальное доказательство" и ординалы?
15 17813
>>17772 (OP)

>Логицизм. Не пошел дальше труда Рассела и Уайтхеда Principia Mathematica.



А разве теория типов - это не развитие идей логицизма?
16 17814
Вопрос по теореме Гёделя о неполноте.

Часто встречаю такую одну из интерпретаций его вывода: для любой формальной системы есть недоказуемое в рамках этой системы предложение, истинность которого мы тем не менее можем доказать (вне рамок системы).

Этот вывод основывается на предположении, что для формальной системы F мы строим гедёлево предложение A. Для системы F' = F+A мы строим гёделево предложение A'. Для системы F'' = F' + A' мы строим гёделево предложение A'' и так далее... Значит, для любой формальной системы мы можем построить гедёлево предложение - которое недоказуемо, но истинно.
Однако сам способ построения гёделевых предложений вполне алгоритмически формализуем, как и вообще все наши возможные способы доказать истинность какого-либо предложения.

Следовательно, мы можем построить формальную систему, которая в качестве одного из методов доказательств будет строить подобные гедёлевы предложения.
Данная формальная система также будет неполна (это легко доказать, отталкиваясь от проблемы остановки). То есть, будет существовать предложение B, для которого мы не можем доказать ни B, ни (не B). Однако доказать, какое из них истинно, мы не можем.
Следовательно, говорить о существовании истинного, не недоказуемого, мы можем лишь в смысле закона исключения третьего.
17 17819
>>17814
Ну и, кстати, тем самым опровергается дурацкий противоречивый аргумент Пенроуза, что человек якобы может доказать то, что не может доказать ни одна формальная система, а значит, наше мышление не может быть смоделировано Машиной Тьюринга.
18 17827
>>17819
Да, покопался в литературе и нашёл, что из теоремы Чёрча-Клини следует, "that no algorithmic method can tell how to apply the method of Gödel to all possible kinds of formal system". У нас нет общего алгоритма, который позволил бы строит Гёделево предложение для произвольной формальной системы; подобный алгоритм существует лишь для узкого класса формальных систем.
A Turing Machine - Overview.webm15,1 Мб, webm,
640x360
19 17829
>>17819

>противоречивый аргумент Пенроуза, что человек якобы может доказать то, что не может доказать ни одна формальная система, а значит, наше мышление не может быть смоделировано Машиной Тьюринга.


Это не аргумент, а как принято говорить на бордах, "вскукарек". Аргумент - это что-то более весомое чем батрушка от машины Тьюринга. Этот деятель же не приводит ни одного примера.
20 17842
>>17814
Теорем Гёделя о неполноте две. Ты используешь первую.
1ТГ использует непротиворечивость - в противоречивой системе доказуемо вообще всё.
2ТГ утверждает, что непротиворечивость недоказуема.

> Однако доказать, какое из них истинно, мы не можем.


С 2ТГ можем. Теория все еще непротиворечива, но не может доказать собственную непротиворечивость. Ты засунул в неё возможность строить гёделевы утверждения для любого конечного набора аксиом, а она построила бесконечный набор аксиом и уже не может построить гёделево утверждение для себя самой.
21 17859
>>17842

> она построила бесконечный набор аксиом и уже не может построить гёделево утверждение для себя самой.



Насколько я понимаю, мы тоже это гёделево утверждение в общем случае построить не можем (можем лишь утверждать, что оно есть). Так как если бы могли, то алгоритмически формализовали бы этот способ и вставили внутрь нашей формальной системы.
22 17864
Что почитать о теории доказательств если даже доказательство геометрических теорем в школе для меня были мукой и непонятными?
23 17866
>>17864
А как научиться варить борщ, если приготовление яичницы для меня сущее мучение?

Если слова "элиминация сечения в исчислении секвенций" тебе ни о чем не говорят, то теория доказательств тебе на фиг не нужна. Может, тебе просто какие-нибудь детские книжки почитать, типа Смальяна?
24 17868
>>17864
Советую "Теорию множеств" Бурбаки. Проблема школьной геометрии в том, что она требует "строгих" доказательств, при этом совершенно не аргументируя, в чём эта строгость заключается. Мне, когда я был школьником, например, было совершенно непонятно, какие методы доказательства можно использовать, а какие нет, и где вообще выход из порочного круга, когда и так очевидные выводы приходится доказывать с помощью ещё более очевидных. Бурбаки реально очень многое проясняют.
25 17870
>>17868
Не очень хороший совет - Бурбаки строят свою теорию на основе эпсилон-оператора Гильберта, который детально не описывают. У начинающих из-за этого возникает недоумение.
26 17871
>>17868

> какие методы доказательства можно использовать, а какие нет


Я уже давно не школьник, а мне до сих пор непонятно, только Бурбаки тут, боюсь, не поможет.

С одной стороны, всех пугают, что визуальную очевидность надо засунуть себе в жопу, иначе придет страшная Лемма Жордана и все сдохнут. Но при этом по факту все всё время смотрят на картинку и выводят из неё суждения вида "эта хуйня лежит между вон той и вот этой".

При этом если речь идёт о трёх лучах хер знает в каком порядке, то все говорят "на самом-то деле все углы ориентированные (т. е. ABC= -CBA), так что нам всем похуй".

Почему такие финты ушами можно делать с тремя точками на прямой, можно объяснить только через скалярное произведение, но до него еще дожить надо (да и все равно даже когда доживёшь, фиг тебе кто нормально объяснит).

Поэтому имеется крайне вредная идеология о том, что нужно всегда разбирать случаи, что между чем лежит. Вред прежде всего в том, что если кто решит разобрать действительно все случаи, то помрет в процессе.

Но тем не менее адепты этой ереси встречаются, поэтому ушлых школьников учат: если какое мудило на приёмных приебётся насчёт неразобранного случая про то, что между чем болтается, надо пиздеть так: вся эта ваша сраная геометрия на самом деле про равенство каких-то там ебучих полиномов, а полиномы - они такие твари, что если равны на куске пространства, то и везде равны, а не то у ихней разности будет овердохуя нулей; поэтому моё доказательство для частного случая доказывает также и общий случай. Предполагается, что после такого заявления любое мудило в ужасе съебётся.
27 17874
>>17871
Ну, я надеюсь, анон учит геометрию не для школьных экзаменов, а так, изучать евклидову геометрию через аксиомы Евклида-Гильберта - это давно устаревшее извращение. Естественней изучить основы алгебры, ввести векторное пространство, изучить свойства аффинности, а потом навесить на это пространство метрику - вуаля - и геометрия готова. Изучать неафинные метрические пространства (всякие геометрии Лобачевского) - это уже другой вопрос, но для начала этого не требуется.
геометрия.PNG189 Кб, 1497x854
28 17877
>>17874

>вуаля - и геометрия готова


Это будет не геометрия, это будет алгебра. Геометрия - это пикрелейтед.
29 17878
>>17874
Ты что-то сразу за многомерную геометрию взялся. Обычную планиметрию можно прекрасно сбацать просто на комплексных числах.

>>17877

>Это будет не геометрия, это будет алгебра.


Так геометрия и есть алгебра с картинками. Выбери одну задачу, я попробую продемонстрировать.
30 17881
>>17877
Твои задачи решаются на основе аксиом векторного пространства с метрикой ничуть не хуже, чем на основе стандартных геометрических аксиом.
31 17886
>>17878
Интересный эксперимент. Ок, 10.036.
32 17910
>>17870
Это с помощью этого оператора у бурбаков получилось определение единицы размером во сколько там квадрильенов знаков?
33 17915
>>17886
Хорошо. Углы - это по сути комплексные числа с модулем 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.
1.gif8 Кб, 950x128
34 17934
>>17910
Ага. Особенность эпсилон-оператора в том, что длина формальных определений при их усложнении растёт экспоненциально.

Сам по себе оператор у Бурбаков довольно прост. Для любой формулы (например, x < y) и любой переменной мы можем ввести терм ("такой x, что x < y"). Терм строится так: мы пишем логический символ t, после него формулу, в которой x заменяем на пустой квадратик; и соединяем символ t с этим квадратиком надстрочной линией.
То есть Бурбаки могут строить не только формулы из термов, но и термы из формул. В стандартной логике первого порядка таких термов нет. Замечу, что возможность построить терм "такой x, что x < y" вовсе не означает, что мы в рамках теории можем доказать существование этого терма. Формула, утверждающая "существует x, что x < y" выглядит так: мы пишем формулу (x < y), и все x в этой формуле заменяем термом "такой x, что x < y". Например, терм, обозначающий пустое множество на картинке. Расшифорывается как "такой x, что (не(существует у, где не(не(y принадлежит x))))". Формула "существует пустое множество" была бы ещё раза в 3 длиннее.
35 17953
>>17934
А в чем профиты такой нотации? Лямбда исчисление не проще разве?
30ANANASface.jpg209 Кб, 879x1275
36 17967
>>17953
Оно легко позволяет строить переходы между теорией и метатеорией - нужно просто доопределить эпсилон. Изначально Гильберт построил эпсилон-оператор, чтобы свести всю математику к арифметике. Оказалось, что он гораздо мощнее.
37 17973
>>17967
Но ведь это чистый конструктивизм, сводить всю математику к арифметике. Даже интуиционизм в смысле Брауэра. И это делается проще, безо всяких страшных операторов, в которых единицу можно представить только какими'то астрономическими количествами знаков. Геделевская нумерация, например или даже простая лексикографическая нумерация слов в алфавите. Это гильбертовское исчисление нигде не применяется же?
38 17983
>>17973

> Но ведь это чистый конструктивизм, сводить всю математику к арифметике.


Подозреваю, что тот анон имел в виду теорию множеств.

> Это гильбертовское исчисление нигде не применяется же?


Любой классический математик применяет эпсилон пять раз на дню, а тем более йоту. Это совершенно естественные операции.

Астрономические количества знаков возникают от низкоуровневости обычного исчисления предикатов. Это совершенно нормальная ситуация.
39 17985
>>17983

> Любой классический математик применяет эпсилон пять раз на дню, а


Пример?

> Астрономические количества знаков возникают от низкоуровневости обычного исчисления предикатов. Это совершенно нормальная ситуация.


Нет, это ненормальная ситуация. Исчисление предикатов выразимо в лямбде, т.н. изоморфизм Карри-Говарда, там почему'то нет никаких трильенов знаков для выражения простейших вещей.
40 17989
>>17953
Бурбаков совсем не интересовали алгоритмы - они занимались формализацией теорий не для этого, а с классических позиций формализма: "истинность значит выводимость в определённой формальной системе". Они предполагали, что работать с этими формальными системами будут живые математики и эти формальные системы должны быть удобны именно для живых математиков.
Эпсилон-формализм, например, требует всего одного правила вывода: modus ponens. В то же время в стандартных теориях первого порядка используются два правила вывода.
41 17991
>>17985

> Пример?


Я имею в виду сколемизацию. Классические предикаты первого порядка обычно что устно, что на компьютере считаются обычно сколемизацией. Скажем, если мы имеем AxEy f(y) = f(x) + 1, надо доказать AxEy f(y) = f(x) + 3. Любой классик сделает примерно так: пусть s - сколемизация, тогда s³ - то, что нужно.

> никаких трильенов знаков для выражения простейших вещей.


У тебя если лямбда нетипизирована, то можеть зависнуть, а если типизирована, то на каждой формуле надписано доказательство типизированности в специальном исчислении. Так что знаков у тебя тоже ой как много.
42 18000
>>17991
Но ведь Бурбаки формализируют не только арифметику, но и всю теорию множеств (по сути, система похожа на ZFC). Это тоже можно сделать лямбда-счислением?
43 18001
>>18000

> Это тоже можно сделать лямбда-счислением?


В принципе можно, но есть риск заразиться конструктивизмом и бегать потом объяснять всем, что теория множеств не нужна.

Однажды создатели Coq с удивлением обнаружили, что если в него добавить закон исключенного третьего, то аксиома выбора опровергается. После доработки напильником она больше не опровергается. А мораль этой истории в том, что попытки скрестить слона с китом (ZFC с лямбдами) могут привести к неожиданным результатам.
44 18003
>>17973

>это чистый конструктивизм, сводить всю математику к арифметике


Нет, это формализм. Программа Гильберта изначально заключалась в том, чтобы свести всю математику к арифметике, арифметику к некой финитной теории, а непротиворечивость этой финитной теории доказать конечным перебором случаев. Оказалось, что так нельзя.

>это делается проще


Нет, это не делается проще. Ты рассказываешь о наивном, неформализованном подходе, когда большая часть идей остаётся просто на уровне размахивания руками. Гильберт все эти идеи четко формализовал в легкочитаемой книжечке "Основания математики". Если ты нашёл в себе силы обмазываться Мартин-Лёфом, то эту книжку ты просто обязан прочитать.
45 18004
>>18001
А разве можно в кок исключенное третье добавить? Оно ж невычислимо, как его в calculus'e of construction выразить?
принцип исключенного третьего.PNG559 Кб, 1482x946
46 18005
>>18004
В простых случаях вычислимо, кстати. Гильберт и про это написал.
47 18006
>>18003
Книжку почитаю, спасибо. А насчет 'размахивания руками' не согласен. Построения и вычисления таки весомее размахивания руками, как ни крути.
48 18007
>>18005
В случае его применения к перечислимым множествам, ага. Но речь'то об исключенном третьем как об аксиоме, т.е. чем'то таком, что истинно в общем случае.
49 18008
>>18006
Гильбрет, что забавно, критикует Брауэра именно за недостаток в его интуиционизме построений с вычислениями.
50 18029
>>18004
делов-то:
Axiom lem: forall P, P \/ ~P.

хотя чё мелочиться-то:
Axiom fuck: False.
lcubemap.gif1 Кб, 258x229
51 18036
>>18000

>не только арифметику, но и всю теорию множеств (по сути, система похожа на ZFC). Это тоже можно сделать лямбда-счислением?


Скажем так, не вся лямбда одинаково полезна. В бестиповой и простой типизированной по Черчу нельзя. А вот в любой, включающей в себя лямбда Р (предикатная лямбда (передний правый нижний угол куба) в которой выразим изоморфизм Карри-Говарда), можно. Кок (соответствующий самому дальнему правому верхнему углу куба) включает в себя все остальные варианты как подмножества, поэтому в нем можно сделать ZFC, таки и сделали https://github.com/coq-contribs/zfc
52 18039
>>17991

>если лямбда нетипизирована, то можеть зависнуть, а если типизирована, то на каждой формуле надписано доказательство типизированности в специальном исчислении. Так что знаков у тебя тоже ой как много.


Ты о чем? Вот например, в MLTT используется аналог типизированной лямбды, с той разницей что там 4 операции получения выражений - аппликация, абстракция, селекция и комбинация, а вместо типов как таковых т.н. "арности". Т.е. каждое выражение от простой константы и переменной до сложных составных термов имеет соотв. ему арность. Все обозначения, нужные для этого, прямо приводятся, и там нет никаких триллионов знаков.
53 18054
Помогите, я ничего не понимаю.
54 18055
>>18054
Барендрехтом решил обмазаться? Там надо все разбирать с самого начала вообще. Если чего-то не понял, дальше и читать не стоит, т.к. материал дается последовательно и на основе того, за что уже пояснено.
55 18058
>>18055
Да вроде и до 2.1.8 всё понятно. А уже совсем непонятные преобразования начались. С fixed point theorem есть какое-то только совсем интуитивное понимание (типа есть функция, которая просто возвращает аргумент и чего-то там еще), какой-то комбинатор, не пойми чего. Но от того что какой-то школьник из Румынии на английской (на слух он мне вообще непонятен) поясняет за это всё (хотя может чуть другое вроде) у меня неплохой такой Барендрехт. Для меня какой-то слишком резкий переход случился в этой книге, не знаю почему, как и что делать.
56 18064
>>18058
Вообще, если что-то в лямбде непонятно, лучше гуглить и на примерах разбирать в том же хаскелле. Типа комбинатора неподвижной точки http://www.wikiznanie.ru/wikipedia/index.php/Комбинатор_неподвижной_точки
57 18065
>>18039
А доказательство какой-нибудь теоремы Цермело в такой системе тоже будет выглядеть не слишком длинным?
Снимок.PNG28 Кб, 991x343
58 18068
>>18065
Wellordering - один из 4х типов в MLTT, вон у Максимки http://groupoid.space/mltt/semantics/ меньше полстраницы занимает.
59 18424
>>17772 (OP)

> Формализм. В изначальном виде закончился крахом программы Гильберта по формализации арифметики и кризисом оснований


Святая толстота. Конструктивисто-сектанты as they are.
14950185472100.jpg121 Кб, 816x820
60 18425
>>18424
Аргументы?..
61 18441
Чтобы истеризовать тред ещё раз: лоли и интернеты тому, кто объяснит в чём заключается суть операции "дать обоснование математики" и почему это должно кого-то волновать?
62 18443
>>18441
Ну если ты занимаешься математикой, тебе неплохо было бы представлять, чем именно ты занимаешься. Это не только математики касается, с любой наукой так.
63 18445
>>18443
Это, не полный ответ на вопрос.
64 18447
>>18445
Почему не полный? Чего конкретно тебе не хватило в этом ответе?
65 18451
>>18424
Объясните мне, почему Гильберту было так важно доказать непротиворечивость теории методами самой теории? Ведь этой какой-то замкнутый круг. Теория A либо противоречива, либо непротиворечива. Если теория A противоречива, то мы, конечно, можем доказать в ней её непротиворечивость, но это доказательство нам ничего не даёт. Если же мы доказываем её непротиворечивость, исходя из предположения, что она непротиворечива... ну так при таком предположении нам и доказательство не нужно - мы уже предполагаем её непротиворечивость. В общем, если бы такое доказательство мы и получили, то никакой ценности оно бы не несло, так как мы вполне могли бы получить доказательство непротиворечивости A в теории A при том, что теория A была бы противоречивой.
66 18457
>>18451
Теория не может рассуждать про саму себя. Внутри нее можно построить изоморфную ей теорию, но сама теория об этом не "знает".

План такой:
- у нас есть мозги, надо бы их формализовать
- в формализациях бывают баги
- поэтому докажем непротиворечивость формальной системы при помощи мозгов, это будет значить, что там нет багов
- потом перенесём доказательство из мозгов в формализм, чтобы и в доказательстве не было багов
- ???
- либо ПРОФИТ, либо глючная система с глючным доказательством, но второе маловероятно
67 18460
>>18457
Насколько я могу понять, описанная схема была бы полезна в следующем случае:
Вероятность того, что доказательство (сделанное неформально) содержит баг мы оцениваем как больше вероятности того, что формальная система (для которой мы доказываем непротиворечивость) глючна. Только в таком случае имело бы смысл переносить наше докзательство внутрь формальной системы.
Но такая вот оценка вероятностей мне кажется сомнительной.
68 18461
>>18460
Хотя нет, гоню.
Система глючна => доказательство неверно
Доказательство верно => Система неглючна
Система неглючна => ничего не следует отсюда

Но я ещё сейчас попытаюсь сформулировать мысли...
69 18462
>>18461
Мы имеем неформальное доказательства неглючности системы => Система неглючна с вероятностью A (скажем, 90%)
(Мы перенесли доказательство неглючности системы в систему)&(Система глючна) => (Система глючна)
(Мы перенесли доказательство неглючности системы в систему)&(Система неглючна) => (Система неглючна)
Я не вижу, как возможность перенести доказательство в систему может поменять изначальные априорные оценки вероятности того, глючна система или неглючна.
Если, допустим, не сумев перенести доказательство в систему, я расценивал бы отношение вероятностей глючности/неглючности как 10%/90%, то и после перенесения доказательства в формальную систему оценка вероятностей осталась бы прежней.
70 18463
>>18462
Кажется, я понял идею "обоснования финитными средствами".
Допустим, мы уверены в непротиворечивости формальной арифметики на 99%.
И при этом уверены в непротиворечивости ZFC, скажем, на 50%.
Если бы утверждение о непротиворечивости ZFC мы смогли бы доказать внутри формальной арифметики, то мы были бы уверены в непротиворечивости ZFC на 99%.
Но из непротиворечивости ZFC следовала бы непротиворечивость арифметики, поэтому внутри формальной арифметики по теореме Гёделя доказать ZFC мы не можем. То есть мы не можем развеять сомнения в непротиворечивости слишком сильной теории, доказав эту непротиворечивость в теории более слабой, в которой мы более уверены.
71 18464
Я читаю ваше обсуждение, и у меня такое чувство, что вы относитесь к теме как к какому-то мистицизму.
72 18465
>>18464
Ну, я как раз пытаюсь осмыслить вопрос наиболее рационально, именно поэтому и использую язык теории вероятностей.
73 18466
>>18465
Ладно, посмотрим, что из этого выйдет.
74 18468
Что почитать по всяких Coq?
75 18472
>>18447

>Ну если ты занимаешься математикой, тебе неплохо было бы представлять, чем именно ты занимаешься. Это не только математики касается, с любой наукой так.


не является ответом на

>...кто объяснит в чём заключается суть операции "дать обоснование математики"...

76 18474
>>18451
Он хотел не методами самой теории, а "финитарными". По-поводу того, что такое "финитарные методы" он целую книжку написал: интуитивно, всякие комбинаторные рассуждения про значки и как и что из них выводить - это ок, трансфинитные индукции, большие кардиналы и прочее - это не ок. Потом (или сразу, или ранее, не суть) все поверили, что финитарные методы ~ доказуемо в PA (или IE_1 - это по вкусу), а дальше историю ты знаешь.
77 18486
>>18472
А что является?
78 18489
>>18468
Для начала можно Барендрехта, Lambda calculi with types.
79 18494
>>18462
На практике это не так. Как-то раз в HOL4 доказали ложь из-за какого-то извратного бага в бета-редукции. Но доказательства, формализованные в HOL4, выжили.

Даже глючная система может быть практически полезна. Конечно, теоретически она совершенно неинтересна, потому что в ней доказуемо всё. Но даже если такая система ловит 99% человеческих ошибок, она все равно поднимает вероятность, что всё правильно.
80 18496
>>18468
Смотря, что тебе надо, если Software Foundations - это одно, а если в ZFC палочкой потыкать, то другое.
81 18502
>>18486
Не знаю, но знаю, что ответ на вопрос: "Что такое Х?", не может состоять из оценочного суждения по поводу того, что мне было бы плохо, а что неплохо представлять, если я чем-то там занимаюсь.
82 18529
Почему бы не взять стековые языки программирования?
83 18531
>>18502

>Не знаю,


Ну как узнаешь - приходи.
>>18529
Для чего ты предлагаешь их взять?
84 18532
>>17772 (OP)
Насколько я слышал сила конструктивистов оказалась их же слабостью, из-за тех ограничений, которые они наложили, они закрыли себе доступ ко многим результатам. Правда ли это?
85 18533
>>18532
Давай конкретнее, о каких именно ограничениях и результатах речь?
86 18534
>>18533
Понятия не имею.
87 18614
>>17772 (OP)
А как же кубическая теория типов(к интуиционистам)? Про неё забыли, а ведь очень клёвая штука, посмотрите.
Там эта унивалентность прямо встраивается в правила вывода.
88 18615
>>18614

>А как же кубическая теория типов(к интуиционистам)?


Куб лямбда-исчислений "а-ля Черч" Барендрегта и соотв. ему по изоморфизму Карри-Говарда куб логических исчислений? Так это самый интуиционизм и есть, точнее конструктивизм, но обычно и то и другое используют как синонимы. Все логики в таком кубе априори конструктивные, поскольку лямбда типизирована и логические константы имеют конструктивное значение (пруф-объекты своих типов).

>очень клёвая штука, посмотрите. Там эта унивалентность прямо встраивается в правила вывода.


Да, это очень полезная вещь. Не какие-то там невычислимые объекты веры типа ислюченного третьего.
89 18619
>>18615
Почему конструктивность - это хорошо?
90 18620
>>18619
А почему плохо? Я заметил, тут у некоторых конкретный такой БАРЕНДРЕХТ от конструктивизма, даже от простого упоминания триггерятся и начинают вести себя как бесноватые на приеме у экзорциста.
так-то я сто раз уже говорил, почему хорошо - потому что вычислимо.
91 18623
>>18620
ну так на уровне метатеории классическая математика тоже вычислима (в том смысле, что все утверждения об объектах в ней вычислимы).
92 18627
>>18623
Во-первых, любая формальная система есть конструктивный объект, согласно Мартин-Лёфу.
Во-вторых есть вычислимость и вычислимость. В метаматематике "вычислим" и закон исключенного третьего в том смысле, что он не противоречит гильбертовскому исчислению высказываний, например. Однако, ему не во всех случаях может соответствовать вычислимое построение.
93 18656
>>18627
Ну так почему первая вычислимость хуже второй вычислимости?
94 18660
>>18656
Допустим, у тебя есть предикат пиздатости и ты доказал в классической логике, что существует пиздатое число. Есть только маленькая проблема: у тебя нет никакой зацепки, чтобы это число построить. В каком смысле оно существует? Витает в воздухе вокруг тебя? А если не витает, то может быть, оно на самом-то деле и не существует-то?

А то, что утверждение доказуемо, это-то вычислимо, но это просто факт про скобочки и буквочки. Вдруг это утверждение не имеет никакого отношения к реальности?
95 18669
>>18656
Тебе выше правильно пояснили, выводимость чего'то в классической логике не обязана вести к построению этого чего'то, поскольку класмическая логика не рассматривает интерпретацию логических констант, там это просто буковы и их синтаксис без семантики. Полная аналогия такого подхода это выводимость существования Аллаха из корана. Правил его построения из такого доказательства ты не выведешь.
96 18670
>>18669
А зачем мне правила построения, объясни?
97 18671
>>18670
Правила построения дают возможность работать с объектами построения, доказывать их свойства непосредственно, а не выводить из каких'то заповедей. Гарантированная выводимость, непротиворечивость и отсутствие парадоксов. Классический подход всего этого не гарантирует, а значит не может служить основаниями математики, что доказал кризис оснований.
98 18673
>>18671
Где можно увидеть конструктивизм в деле? В каких книгах?
99 18674
>>18670
А зачем мне ZFC? Есть, например, такая секта, которая добавляет к ZF аксиому детерминированности (determinacy): в бесконечной игре один из игроков имеет выигрышную стратегию. Всё у них прекрасно: и континуум-гипотеза доказывается, и любое множество действительных чисел измеримо. Есть только маленькая такая проблема: аксиома выбора опровергается.

Вопрос: на каком основании делать выбор между ZFC и ZFD? Нас в детстве учили ZFC, так что пусть будет ZFC? Физический эксперимент может какой-нибудь предложишь?
100 18676
>>18674
Что значит "делать выбор"? Это просто две разные теории множеств. Как бывают разные геометрии, так бывают разные теории множеств. Одной единственно верной теории множеств нет.
101 18677
>>18671
А как жить без теоремы о среднем, например?
102 18678
>>18676

> Как бывают разные геометрии, так бывают разные теории множеств.



Вот не надо тут. Геометрия Лобачевского изучает что-то реально существующее, потому что есть модель Пуанкаре. А почему ZFC/ZFD имеет хоть какое-то отношение к реальности?
103 18679
>>18678
Странная постановка вопроса. А если бы у геометрии Лобачевского не было модели в геометрии Евклида, то ты бы воевал против Лобачевского? Я не понимаю твою философию. Объясни, пожалуйста, какими понятиями ты мыслишь. Без этого я не смогу тебе осмысленно отвечать.
104 18681
>>18677
Перестать веровать в исключенное третье как в нечто незыблемое, а использовать только в тех случаях, когда оно доказуемо непосредственно.
105 18682
>>18681
Мощно, мне нравится. А слабости какие-ти есть у такой позиции? Как доказать исключённость третьего? Это ведь аксиома.
106 18683
>>18682

> Мощно, мне нравится. А слабости какие-ти есть у такой позиции?


Никаких нету. У меня Мартин-Леф так даже парадокс Рассела разрулил. Всего лишь переправил определение с общего случая на перечислимую иерархию вложенных универсумов и все. Был парадокс Жирара, а потом вжух, и нету. Это классический подход уже второй век кризис оснований обойти не может.
107 18685
>>18683
Охуеть. А исключённое третье?
108 18686
>>18683
Походу конструктивизим это то, что я искал.
109 18687
>>18673
Бамп вопросу.
110 18688
>>18685
А исключенное третье признается не как аксиома, в которую надо веровать, а как нечто, истинное только для случаев доказуемых н'р в логике Гейтинга, безаприорного обобщения на все случаи жизни. Только вычислимые построения, только хардкор.
111 18689
>>18688
Yflj xbnfnm d j,otv/ Cgfcb,j/
112 18690
>>18688
Ой, ну ты понел. Спс.
113 18691
>>18687
Увидеть в действии можно не только в книгах, но и на компе, Coq жи есть. Книг много, начиная с Барендрегта и заканчивая HoTT.
114 18692
>>18691
Можно посмотреть на алгебру и анализ?
115 18693
>>18692
Анализ есть в книге Бишопа, 60х еще годов. Алгеброй не интересовался. Вообще, есть книжка Гейтинга 'Интуиционизм', там кратко поясняется и за алгебру, анализ, логику и т.д.
116 18694
>>18693

>книжка Гейтинга 'Интуиционизм'


Которая написана в стиле шуточного диалога масок?
117 18695
>>18679
Геометрия Евклида тут ни при чем, можно и из алгебры состряпать модель (как сам Лобачевский сделал).

Если бы у геометрии Лобачевского не было модели, то да, она была бы бесполезной. Собственно Бойяи, Гаусс и пр. думали в эту сторону, чтобы продемонстрировать независимость пятого постулата от остальных. Если бы модели не было, то ничего б они не добились.

> Объясни, пожалуйста, какими понятиями ты мыслишь.


Смотри, математики пасьянсы из скобочек раскладывают или всё-таки изучают что-то? А если изучают, то что?

Конструктивная математика начинается с описания того, что она изучает. Типа "возьмем в качестве универсума все выражения из скобок и слов". А классическая математика? Скажем, для теории категорий, мы берём ZFC с недостижимыми кардиналами. А в каком смысле эти лихие кардиналы существуют? Стоит ли вообще какой-нибудь смысл за квантором Е?

В конструктивизме квантора существования по сути нет, там просто всегда строится функция или константа, поэтому лишних философских вопросов не возникает.
кушнер 043.png73 Кб, 1250x2010
118 18696
>>18693
В лекциях по конструктивному анализу Кушнера сказано, что конструктивный анализ - всего лишь сильно урезанная версия обычного анализа и не содержит ничего, что не было бы открыто ранее. Зато содержит много неудобств. Так, невозможно выяснить, равны ли два производных конструктивных вещественных числа, невозможно сравнивать два произвольных конструктивных вещественных числа, бывают конструктивно непрерывные конструктивно не ограниченные на конструктивном отрезке конструктивные функции, алгоритм поимки льва в пустыне запрещен ибо им можно решить великую теорему Ферма, и прочее в таком духе.

Зато с философской точки зрения это огого. Вот прям вообще ух. Сильно-сильно хорошее, не то что у этого мерзкого Коши-мафиози. Всем учить.
119 18697
>>18688
Последний вопрос: теорема Гёделя и конструктивная матемтаика. Как у них дела вместе? Работает там она или нет?
120 18698
>>18696
>>18533
Вот про эти, анон.
121 18700
>>18698
Это не ограничения. Как и затыкание невычислимых дыр в анализе актуальной бесконечностью это не решение проблем. Нарисовать знак бесконечности не равно построить ее.
122 18701
>>18697
Конструктивные системы полны по Геделю, т.к все что есть в такой системе, выводимо. Поскольку конструктивные системы это построения, как и правила построений и правила проверки этих правил еа корректность это конструктивные объекты, то в такой системе нельзя выразить то, что из нее невозможно вывести или что в ней невозможно доказать.
123 18702
>>18695
Математика изучает воображаемые сущности. Эти сущности, согласно неокантианству, расположены в созерцательном пространстве, что даёт возможность делать о них априорные синтетические суждения. Эти суждения называются определениями. Применение к определениям аналитических рассуждений позволяет чётче осознать, чем же являются рассматриваемые (в созерцательном пространстве) объекты.

Проще говоря, математик сначала воображает что-то, затем делает несколько утверждений о воображенном объекте, затем из этих утверждений выводит следствия.

Поместить в созерцательное пространство и начать созерцать можно какую угодно идею. Но не всякие идеи обладают тем изящным свойством, что при их созерцании получается много аналитических суждений, сложным образом связанных друг с другом. Лишь те идеи, при воображении которых достоверно получается много нескучных теорем, изучаются математикой и называются математическими объектами.

Похожей деятельностью занимаются вообще все теоретики - все они воображают. Однако у математики есть всё-таки своя специфика. Говорить о ней я не буду, потому что это слишком интимная вещь. Продолжу разговор о созерцательном пространстве.

Обычно воображается не одна-единственная сущность, но целый сонм сущностей. Этот сонм называется универсумом. Сущности, входящие в универсум, однородны в следующем смысле. Каждое определение можно рассматривать как фильтр, сквозь который одни сущности универсума проходят, другие не проходят. Сущности, которые проходят через фильтр, неразличимы этим фильтром. Так вот, для всякого универсума есть определение, относительно которого все объекты универсума неразличимы. Для универсума теории групп таким определением является группа - все сущности универсума подходят под это определение. Для универсума теории колец таким определением является кольцо. Для метаматематики универсумом является сонм текстов. И т.п.

Для каких-то универсумов есть описания, позволяющие составить представление о сущностях, входящих в сонм, для каких-то универсумов таких описаний нет. Например, для универсума стандартной теории множеств есть описание: именно, под универсумом понимается кумулятивная иерархия фон Неймана. Этот универсум обозначается V. Вместе с тем, легко воображаются универсумы множеств, которые могут напоминать, а могут и не напоминать V. Эти универсумы описываются неклассическими теориями множеств.

Существование понимается относительно какого-то универсума. Если объект x существует относительно U, то это означает, что при воображении универсума U необходимо также иметь в виду и объект x. Несуществование x соответственно означает, что при воображении универсума не следует воображать x.

Конструктивизм занимается ровно этим же самым - исследует воображаемые сонмы сущностей. Однако делает это "со связанными руками", фанатично ограничивая себя требованием вычислимости. Вычислимость, о которой говорят конструктивисты, - воображаемая. Ведь все алгоритмы, которые рассматривают конструктивисты, существуют лишь в воображении конструктивистов. Выполнить эти алгоритмы в реальности невозможно - см. аргумент Вавилова о чернильной дыре. Так, в реальном мире невозможно построить два в степени гугол, несмотря на то, что вообразить алгоритм построения такого числа очень легко. Ибо для построения этого числа потребуется больше атомов, чем есть во всей вселенной. Претензии конструктивистов на якобы большую реалистичность по сравнению с математикой не имеют под собой почвы. Конструктивисты занимаются тем же самым воображением объектов, которым занимаются математики, однако почему-то кричат, что вовсе не пользуются никакими воображением.

У конструктивистов считается, что воображение не может быть связано с реальным миром. Конструктивисты заблуждаются. Например, если я возьму монетку и воображу её падение на землю, а потом действительно брошу монетку на землю, - я увижу почти то же самое, что я вообразил.

Для людей, которые стоят на позициях решительного утилитаризма и оценивают всякую деятельность постольку, поскольку она полезна в народном хозяйстве, также есть аргумент в защиту неограниченного воображения. А именно - математические теории можно рассматривать как черный ящик, как умозрительную машину, шестеренки которой приводятся в движение силой воображения; на вход подаются данные, на выходе получается предсказание. Никому не нужно, чтобы все воображаемые шестеренки такого калькулятора чему-либо соответствовали в реальном мире. Достаточно, чтобы он давал корректный результат при всех задачах, в которых ценное для утилитариста народное хозяйство нуждается. Если совершенно фантастические объекты верно предсказывают надои чугуна, то нет никаких причин требовать от этих объектов быть реальными. Математики занимаются созданием и обслуживаением фантастических шестеренок, строят в своём воображении конструкции, которые нужны лишь для других воображаемых конструкций. Каждый из математических объектов сам по себе для народного хозяйства бесполезен, однако из некоторых математических объектов в конце концов можно собрать очередную машину предсказаний. И нормальная математика справляется с этим куда лучше, чем конструктивизм. Достаточно указать на то, что все воображаемые шестеренки, лежащие под капотом классического анализа, в конструктивизме не существуют, - а вместе с этим невычислимый матан обусловил научную революцию и радикально изменил бытие человечества.

Математики, конечно, не видят смысл своей деятельности в создании калькуляторов. Математики в основном занимаются математикой, которая интересна внутри математики - употребляется в других разделах или даёт повод для воображения и изучения каких-то новых интересных сущностей. Полезные для народного хозяйства калькуляторы получаются непредсказуемым образом, лишь как случайный побочный продукт.
123 18702
>>18695
Математика изучает воображаемые сущности. Эти сущности, согласно неокантианству, расположены в созерцательном пространстве, что даёт возможность делать о них априорные синтетические суждения. Эти суждения называются определениями. Применение к определениям аналитических рассуждений позволяет чётче осознать, чем же являются рассматриваемые (в созерцательном пространстве) объекты.

Проще говоря, математик сначала воображает что-то, затем делает несколько утверждений о воображенном объекте, затем из этих утверждений выводит следствия.

Поместить в созерцательное пространство и начать созерцать можно какую угодно идею. Но не всякие идеи обладают тем изящным свойством, что при их созерцании получается много аналитических суждений, сложным образом связанных друг с другом. Лишь те идеи, при воображении которых достоверно получается много нескучных теорем, изучаются математикой и называются математическими объектами.

Похожей деятельностью занимаются вообще все теоретики - все они воображают. Однако у математики есть всё-таки своя специфика. Говорить о ней я не буду, потому что это слишком интимная вещь. Продолжу разговор о созерцательном пространстве.

Обычно воображается не одна-единственная сущность, но целый сонм сущностей. Этот сонм называется универсумом. Сущности, входящие в универсум, однородны в следующем смысле. Каждое определение можно рассматривать как фильтр, сквозь который одни сущности универсума проходят, другие не проходят. Сущности, которые проходят через фильтр, неразличимы этим фильтром. Так вот, для всякого универсума есть определение, относительно которого все объекты универсума неразличимы. Для универсума теории групп таким определением является группа - все сущности универсума подходят под это определение. Для универсума теории колец таким определением является кольцо. Для метаматематики универсумом является сонм текстов. И т.п.

Для каких-то универсумов есть описания, позволяющие составить представление о сущностях, входящих в сонм, для каких-то универсумов таких описаний нет. Например, для универсума стандартной теории множеств есть описание: именно, под универсумом понимается кумулятивная иерархия фон Неймана. Этот универсум обозначается V. Вместе с тем, легко воображаются универсумы множеств, которые могут напоминать, а могут и не напоминать V. Эти универсумы описываются неклассическими теориями множеств.

Существование понимается относительно какого-то универсума. Если объект x существует относительно U, то это означает, что при воображении универсума U необходимо также иметь в виду и объект x. Несуществование x соответственно означает, что при воображении универсума не следует воображать x.

Конструктивизм занимается ровно этим же самым - исследует воображаемые сонмы сущностей. Однако делает это "со связанными руками", фанатично ограничивая себя требованием вычислимости. Вычислимость, о которой говорят конструктивисты, - воображаемая. Ведь все алгоритмы, которые рассматривают конструктивисты, существуют лишь в воображении конструктивистов. Выполнить эти алгоритмы в реальности невозможно - см. аргумент Вавилова о чернильной дыре. Так, в реальном мире невозможно построить два в степени гугол, несмотря на то, что вообразить алгоритм построения такого числа очень легко. Ибо для построения этого числа потребуется больше атомов, чем есть во всей вселенной. Претензии конструктивистов на якобы большую реалистичность по сравнению с математикой не имеют под собой почвы. Конструктивисты занимаются тем же самым воображением объектов, которым занимаются математики, однако почему-то кричат, что вовсе не пользуются никакими воображением.

У конструктивистов считается, что воображение не может быть связано с реальным миром. Конструктивисты заблуждаются. Например, если я возьму монетку и воображу её падение на землю, а потом действительно брошу монетку на землю, - я увижу почти то же самое, что я вообразил.

Для людей, которые стоят на позициях решительного утилитаризма и оценивают всякую деятельность постольку, поскольку она полезна в народном хозяйстве, также есть аргумент в защиту неограниченного воображения. А именно - математические теории можно рассматривать как черный ящик, как умозрительную машину, шестеренки которой приводятся в движение силой воображения; на вход подаются данные, на выходе получается предсказание. Никому не нужно, чтобы все воображаемые шестеренки такого калькулятора чему-либо соответствовали в реальном мире. Достаточно, чтобы он давал корректный результат при всех задачах, в которых ценное для утилитариста народное хозяйство нуждается. Если совершенно фантастические объекты верно предсказывают надои чугуна, то нет никаких причин требовать от этих объектов быть реальными. Математики занимаются созданием и обслуживаением фантастических шестеренок, строят в своём воображении конструкции, которые нужны лишь для других воображаемых конструкций. Каждый из математических объектов сам по себе для народного хозяйства бесполезен, однако из некоторых математических объектов в конце концов можно собрать очередную машину предсказаний. И нормальная математика справляется с этим куда лучше, чем конструктивизм. Достаточно указать на то, что все воображаемые шестеренки, лежащие под капотом классического анализа, в конструктивизме не существуют, - а вместе с этим невычислимый матан обусловил научную революцию и радикально изменил бытие человечества.

Математики, конечно, не видят смысл своей деятельности в создании калькуляторов. Математики в основном занимаются математикой, которая интересна внутри математики - употребляется в других разделах или даёт повод для воображения и изучения каких-то новых интересных сущностей. Полезные для народного хозяйства калькуляторы получаются непредсказуемым образом, лишь как случайный побочный продукт.
124 18703
Алсо про безумного портного.
http://lib.ru/LEM/summa/summgl5e.htm
125 18704
>>18702
Плохая паста, неосиляторская. Впрочем, если уж Вейль в свое время интуиционизм неосилил, возможно я многого хочу от ноунейма из страны, где математику развивабт не больше чем в центральной африке.
126 18705
>>18695
Ты вот любишь говорить про Аллаха. Так вот, если бы Аллах был идеей, которую можно было бы поместить в созерцательное пространство и положить в фундамент красивой ажурной конструкции из аналитических суждений, то Аллах вполне бы был математическим объектом. Просто идея Аллаха на самом деле является очень блеклой и никакой математики не порождает, - это единственная причина, по которой математики не изучают Аллаха.
Существующее богословие на математическую теорию никак не тянет, поскольку является беспруфным алогичным кукареканием.
127 18706
>>18704
Почему паста? Ориджинал, только что написал.
128 18714
>>18706
Как бы там ни было, написал ты хуйню. Я смотрю, ты даже не очень в курсе, чем синтетическое суждение отличается от аналитического. Про отличие конструктивного подхода вообще набор слов.
129 18716
>>18714
Обычно так говорят, когда не могут ничего возразить по существу, но не соглашаются из-за идеологии.
130 18717
>>18716
Считай это первым возражением по'существу. Паста большая, хуйни написано много, с тилибона цитировать неудобно, завтра конкретнее напишу с чем не согласен.
14914136546080.png387 Кб, 651x498
131 18718
>>18717
Окей. Кстати, теперь я считаю себя вправе называть хуйнёй те твои слова, которые посчитаю хуйнёй.
132 18722
>>18702
По мне так тоже хуйня, какая-то платонистская риторика про непостижимые сущности, которые мы можем описывать, воздушные замки и тд

Вообще оба этих дискурса "романтическо-платонистский" и "прагматическо-конструктивистский" уже заебали пиздец как. Сколько можно одно и то же говно в ступе толочь, хоть бы кто что новое вбросил.
133 18728
>>18701

>то в такой системе нельзя выразить то, что из нее невозможно вывести или что в ней невозможно доказать.


>Если формальная система S непротиворечива, то формула A невыводима в S; если система S ω-непротиворечива, то формула ¬A невыводима в S. Таким образом, если система S ω-непротиворечива, то она неполна и A служит примером неразрешимой формулы.


Тогда получается, что конструктивная математика противоречива.
134 18729
>>18700

>Это не ограничения


>алгоритм поимки льва в пустыне запрещен ибо им можно решить великую теорему Ферма


>невозможно выяснить, равны ли два производных конструктивных вещественных числа


Это ограничения

> затыкание невычислимых дыр


А вот это не ограничения, никто ничего не затыкает, просто существует обозначение для "невычислимо большое". К тому же, раз уж конструктивная математика полна по Гегелю я теперь вообще не уверен, отличается и она чем-нибудь от религии или псевдонаучной теории какой-нибудь, скажем.
135 18733
>>18702
Ух, как ты его! Годнота же.

Вот только аргумент Вавилова о чернильной дыре уже обсосали в прошлом треде, разве нет? Конструктивисты не требуют никакой "физической" вычислимости и вообще никак не связывают себя с ограничениями реального мира, так что это рассуждение абсолютно мимо кассы, как мне кажется. Они просто требуют представить правило получения объекта - с дихотомией материальный мир\фантазия это никак не связано. С тем же успехом можно говорить о том, что классические математики фанатично ограничивают себя рамками зфц\классической логики\ю нейм ит - ну, или математики вообще фанатично ограничивают себя тем, что обычно называется рациональным мышлением, в то время как могли бы непосредственно ощущать узоры с разрывами.

Короче, красиво - но немного мимо, как мне кажется.
136 18739
>>18728
Потому что ты так сказал? Противоречивость непосредственно выводима в конструктивной системе, если она там есть. Для этого не нужны дополнительные теоремы и т.п. Излишне говорить, что противоречивость конструктивной математики это твои фантазии.
137 18740
>>18729

> > затыкание невычислимых дыр


> А вот это не ограничения, никто ничего не затыкает, просто существует обозначение для "невычислимо большое".


Ага, обозначение для Аллаха тоже существует.

К тому же, раз уж конструктивная математика полна по Гегелю я теперь вообще не уверен, отличается и она чем-нибудь от религии или псевдонаучной теории какой-нибудь, скажем.

Я уж понял, что ты ничего не понял.
138 18741
>>17772 (OP)
Положняк таков:
Гильберт и Кантор - авторитеты, чёрная масть
приверженцы классической логики - мужики и стремящиеся
конструктивисты - козлы
интуиционисты - петухи
Марти-Лёф - вафлёр
Брауэр - газонюх
139 18744
>>18739

>Конструктивные системы полны по Геделю


>в такой системе нельзя выразить то, что из нее невозможно вывести или что в ней невозможно доказать.


Потому что ты так сказал.
140 18745
>>18740
Да, существует. И что? В каком месте это затыкание дыры или ограничение? Как раз наоборот, работа с неограниченным, ограниченные конструктивисты со своей полной по Гегелю очередной манятеорией, которая всё объясняет в такое никогда не смогут.
141 18746
>>18745
Я сто раз уже объяснял, в каком. Видимо, таки бесполезно. Ты простую вещь пойми, если бы к классическому подходу не было бы претензий и не было бы вызванного им кризиса оснований, то другие подходы вообще бы не понадобились. А так, обосрались по полной программе наотличненько, еще и кукуреканья в сторону тех, кто показал причину кризиса оснований и пути выхода из него. Затыкать невычислимое всякими актуальными бесконечностями и прочими аллахами, выражая невычислимое через неразрешимое, это путь в никуда. И уж точно это не математика.
142 18747
>>18744
Нет, не потому что я так сказал, а потому что так есть на самом деле, достаточно посмотреть хотя бы на варианты типизированной лямбды из куба Барендрегта. Точнее, на правила вывода. Там все выводится из контекста, нет ничего такогл, что нельзя вывести явно из данного контекста по данным правилам. Ну и доказательство непротиворечивости лямбда'исчисления нсть у того же Барендрегта.
143 18750
>>18747

> а потому что так есть на самом деле,


Ну так тем более.
144 18751
>>18746
Ну так я сто раз говорил: сила конструктивизма его же слабость, сами себя ограничили, закрыли доступ.>>18696
145 18752
>>18747

>нет ничего такогл, что нельзя вывести явно из данного контекста по данным правилам.


Просто если она непротиворечива, то должна а ней найтись такая формула A, что A и не A невыводимы в ней. А ты мне говоришь, что в конструктивизме вообще всё выводимо.
146 18753
>>18752
К слову, в математике Рыбникова тоже всё выводимо. В чём принципиальное отличие конструктивизма от рыбникизма?
147 18754
>>18733

> узоры с разрывами.


Решил мемоизировать это дело?
148 18755
>>18702

> Лишь те идеи, при воображении которых достоверно получается много нескучных теорем, изучаются математикой и называются математическими объектами.


>Математика изучает воображаемые сущности.


https://www.youtube.com/watch?v=Yawjc4Pg7x8
+.jpg140 Кб, 600x486
149 18762
>>18755
Нельзя вломить по треугольнику кувалдой. Числа не летают как птицы и на деревьях не растут. Функцию нельзя потрогать.
150 18764
>>18753
Если тебе это неочевидно, что ты вообще забыл в этом треде? Только честно.
151 18765
>>18752

> Просто если она непротиворечива, то должна а ней найтись такая формула A, что A и не A невыводимы в ней. А ты мне говоришь, что в конструктивизме вообще всё выводимо.


Я тебе привел пример, любое лямбда исчисление. Покажи такую формулу.
152 18766
>>18752

> Просто если она непротиворечива, то должна а ней найтись такая формула A, что A и не A невыводимы в ней.


Приведи полную формулировку теоремы Гегеля, а потом посмотри, что утверждаешь ты и найди 10 отличий.
153 18768
>>18766
Гегель - это чувак на >>18718. У него не было теорем. Даже если это шутка - не смешно.
154 18770
>>18768
Смешно очень, по-моему, смешнее только Вротендик или теорема Рохи-Картохи.
155 18771
>>18768
Но это же не отменяет того факта, что спорол ты лютую хуйню. Пусть будет Гедель, что это меняет?
156 18772
>>18702
Ну и дела. Неокантианство. Мало нам было простого мира идей, так теперь мы можем еще и населять мир идей реальными объектами посредством воображения. Кажется, что-то похожее прозвучало недавно в письме Холмогорова Познеру: "Тысячу лет миллионы людей в этой стране денно и нощно молились Богу с такой истовостью и серьезностью веры, жили в такой плотной атмосфере чуда, что даже если бы Вы и подобные Вам были бы правы, и Бога бы не существовало, то здесь, в России, Он стал реальность."

Вот по чётным дням недели я, например, воображаю множества из ZFC, и они, эти множества, красные. А по нечётным дням я воображаю множества из ZFD, и они синие. А по воскресеньям я просто воображаю действительную прямую и всматриваюсь в эту тварь, пытаясь определить, красная она или синяя. Иногда оказывается, что она зелёная, и при том является чёртиком, и тогда я делаю вывод, что с воображением на сегодня пора завязывать.

> кумулятивная иерархия фон Неймана.


Отличное описание универсума теории множеств через до фига ординалов, где до фига - недостижимый кардинал. Вот оно, оказывается, что такое множества, а я-то думал.

> невозможно построить два в степени гугол, несмотря на то, что вообразить алгоритм построения такого числа очень легко.


Ты, кажется, полагаешь, что десятичная запись - это настоящее число, а алгоритм типа "два в степени гугол" - ненастоящее. Но конструктивная математика не так работает. Любая программа типа число (при некоторых условиях насчёт независания) не просто "возвращает" число, а является им.

> а потом действительно брошу монетку на землю, - я увижу почти то же самое, что я вообразил.


Теперь для демонстрации применимости классической математики к реальному миру осталось только подбросить актуальную бесконечность монеток.

> все воображаемые шестеренки, лежащие под капотом классического анализа, в конструктивизме не существуют


Большинству математиков абсолютно насрать на шестеренки. Кто-то из них говорил, что континуум точно существует, 2^континуум - хз, а 2^2^континуум - точно нет. Джерри Бона припечатал еще лучше: "аксиома выбора очевидно верна, теорема Цермело очевидно неверна, а лемма Цорна - хз". Матанщики начали что-то верещать только тогда, когда им заявили, что неважно, одно у них яичко или два. И то только потому, что это-то они смогли понять, а про существование всяких долбанутых кардиналов никто из них ничего не понял.
156 18772
>>18702
Ну и дела. Неокантианство. Мало нам было простого мира идей, так теперь мы можем еще и населять мир идей реальными объектами посредством воображения. Кажется, что-то похожее прозвучало недавно в письме Холмогорова Познеру: "Тысячу лет миллионы людей в этой стране денно и нощно молились Богу с такой истовостью и серьезностью веры, жили в такой плотной атмосфере чуда, что даже если бы Вы и подобные Вам были бы правы, и Бога бы не существовало, то здесь, в России, Он стал реальность."

Вот по чётным дням недели я, например, воображаю множества из ZFC, и они, эти множества, красные. А по нечётным дням я воображаю множества из ZFD, и они синие. А по воскресеньям я просто воображаю действительную прямую и всматриваюсь в эту тварь, пытаясь определить, красная она или синяя. Иногда оказывается, что она зелёная, и при том является чёртиком, и тогда я делаю вывод, что с воображением на сегодня пора завязывать.

> кумулятивная иерархия фон Неймана.


Отличное описание универсума теории множеств через до фига ординалов, где до фига - недостижимый кардинал. Вот оно, оказывается, что такое множества, а я-то думал.

> невозможно построить два в степени гугол, несмотря на то, что вообразить алгоритм построения такого числа очень легко.


Ты, кажется, полагаешь, что десятичная запись - это настоящее число, а алгоритм типа "два в степени гугол" - ненастоящее. Но конструктивная математика не так работает. Любая программа типа число (при некоторых условиях насчёт независания) не просто "возвращает" число, а является им.

> а потом действительно брошу монетку на землю, - я увижу почти то же самое, что я вообразил.


Теперь для демонстрации применимости классической математики к реальному миру осталось только подбросить актуальную бесконечность монеток.

> все воображаемые шестеренки, лежащие под капотом классического анализа, в конструктивизме не существуют


Большинству математиков абсолютно насрать на шестеренки. Кто-то из них говорил, что континуум точно существует, 2^континуум - хз, а 2^2^континуум - точно нет. Джерри Бона припечатал еще лучше: "аксиома выбора очевидно верна, теорема Цермело очевидно неверна, а лемма Цорна - хз". Матанщики начали что-то верещать только тогда, когда им заявили, что неважно, одно у них яичко или два. И то только потому, что это-то они смогли понять, а про существование всяких долбанутых кардиналов никто из них ничего не понял.
157 18773
>>18762

>пикча


Лол.
158 18774
>>18765
>>18766
>>18764
Я не хочу спорить с человеком, который путает Гёделя и Гегеля. Верь хоть в Рыбникизм, хоть в конструктивизм, дело твоё. Отрицай закон исключённого третьего, придумывай как стакан может быть пуст и полон одновременно и тд. Не хочу тратить время.
Не возвращайся никогда!.jpg51 Кб, 400x307
159 18775
>>18774
Но я не путаю Геделя и Гегеля, из этих постов мои только 2. Дело не в этом, а в том, что ты спизданул про рыбникова и Геделя просто чтобы спиздануть, а когда тебя попросили обосновать, сразу слился, доебавшись до орфографии постороннего оратора.

>Не хочу тратить время.


Тебя ИТТ вобще не звали, претензия про потраченное время непонятна. Не хочешь - не трать, никаких проблем. Но если уж пишешь сюда, обосновывай хотя бы.
160 18777
>>18775

>мопед не мой


>орфография когда здесь тотальное непонимание


Манёвры пошли, ну да ладно.

> Покажи такую формулу.


Так её нет, в том и суть. По твоим словам всё выводимо.

>В чём принципиальное отличие конструктивизма от рыбникизма?


>Если тебе это неочевидно


Переводишь темы вместо ответа на вопрос.

> а когда тебя попросили обосновать, сразу слился

161 18778
>>18772
Это и были твои возражения? Я думал, лучше будет это всё.

Да, математические объекты живут только в воображении людей. "Идеальны", как некоторые говорят. И твои алгоритмы - они ведь тоже почти все идеальны, их нельзя потрогать, они лишь в твоём воображении находятся. Доказать это очень просто - достаточно открыть упоминавшуюся выше книгу Кушнера. В ней алгоритмы изображаются буквами, и нередки обороты вида "пусть B - алгорифм такой-то" (книжка старая, поэтому алгоритмы в ней пишутся через ф). Понятно, что тут вовсе не утверждается, что латинская буква B является алгоритмом. В таких местах читателю предлагается вообразить алгоритм и всякий раз иметь его в виду при встрече с буквой B. То есть речь идёт именно о воображаемых объектах.

Нет причин подвергать анализу одни лишь только те воображаемые объекты, которые являются алгоритмами.

Далее, кумулятивная иерархия фон Неймана - это не просто дофига ординалов. Это иерархия классов Vx, где x пробегает класс ординалов. V0 - пустое множество, Vx+1 - множество всех подмножеств Vx, Va для каждого предельного a - объединение всех Vx, у которых x<a. Объединение всех этих классов и обозначается буквой V. Понятно, что далеко не всякий элемент V будет ординалом.

Что до точки зрения, которую я раскрываю, - она придумана не мной. Ещё Лузину кровавыми коммуняками ставилось на вид заявление "натуральный ряд представляет собой функцию головы математика".

Наконец, точки зрения математиков эволюционируют, меняясь по мере накопления математических открытий. Сейчас некоторые теоретики оснований ведут речь о том, что для разных разделов математики следует использовать разные теории множеств - для общей алгебры ZFC, для анализа ZF+счетный выбор и т.п.
брауэр.png348 Кб, 924x539
162 18780
>>18778

>Это и были твои возражения?


Это не мои. Я бы начал с того, что ты вообще не понимаешь сути "ментального построения" в интуиционизме. Но при этом сравниваешь его с другими, на твой взгляд похожими, явлениями в математике и даже с воображением в общем смысле. Вместе с твоим непониманием разницы между синтетическим и аналитическим суждением этого уже было бы достаточно, чтобы вместо какой-то дискуссии на эту тему предложить тебе делать уроки и собирать портфель. Как поется в той песенке, "не лезь малыш в политику, иди учи матчасть". Но и это не все, до кучи ты так же не понимаешь и идентичности ментального построения в интуиционизме и вычислимого алгоритмического построения в конструктивизме, говоря о том, что "представить алгоритм можно, а реализовать нет", игнорируя тот простой факт, что в конструктивизме (интерпретация логических констант по Колмогорову) алгоритм и результат его работы - это одно и то же, с поправкой на абстракцию потенциальной осуществимости и тонкости касающиеся канонических и неканонических элементов и множеств.

>Так, в реальном мире невозможно построить два в степени гугол, несмотря на то, что вообразить алгоритм построения такого числа очень легко.


Далее, ты абсолютно не понимаешь сути понятия "вычислимость", поскольку не знаком с такими вещами как понятие канонического и неканонического элемента и множества, нормальной формы, теоремы Черча-Россера, лямбда-определимости и ее связи с любыми другими уточнениями понятия алгоритма, это только навскидку. Поэтому более сложные вещи, такие как изоморфизм Карри-Говарда, ВНК-интерпретация и т.д. тебе не понятны тем более. Ты не понимаешь даже в чем разница между неканоническим символом, считающимся в канонический элемент и символом Аллаха или симаолом бесконечности, не считающимися ни во что, поскольку правила такого вычисления отсутствуют. Это все возражения чисто на вскидку, там еще много можно добавить.
163 18781
>>18780
"Вам не понять" не является возражением, равно как и взывание к Аллаху. Возражение должно быть логичным набором истинных утверждений. Нельзя сказать "Аллах" и считать, что опроверг собеседника.

Если ты считаешь, что нельзя рассматривать воображаемые объекты, не являющиеся алгоритмами, то будь любезен привести настоящие аргументы.
164 18782
>>18781

>Если ты считаешь, что нельзя рассматривать воображаемые объекты, не являющиеся алгоритмами, то будь любезен привести настоящие аргументы.


Рассматривать-то их можно, вот только к математике они отношения не имеют, а уж тем более не могут служить основаниями. Пример - определение множества у Кантора. Очевидно, это воображаемый объект, но не конструктивный объект и тем более не алгоритм. Рассматривать ты его можешь, конечно. Вот только парадоксов это не отменит.
165 18783
>>18782
Именно изучение воображаемых объектов и является математикой. А на идеях конструктивизма никакой математики не создано. Ну, если не считать внутренние построения конструктивистов, единственное назначение которых - обслуживание конструктивизма.

Выше реквестировали примеры конструктивной математики. Так вот, их нету. По конструктивному анализу на либгене одна унылая книга, конструктивной алгебры вообще не существует. Конструктивизм - это такая философская секта, которая учит, какой должна быть математика, но никакого вклада в математику не вносит и вообще математикой не занимается. Лишь нескучную терминологию генерирует, для внутреннего потребления.

Конструктивисты говорят, что есть классическая математика, а есть конструктивная математика. Конструктивисты лукавят. Есть математика, великая и неделимая, заключенная в миллионах книг. А есть полтора десятка конструктивистских брошюрок. И вот конструктивисты призывают выкинуть всю математику на свалку, а полтора десятка брошюрок изучать (и больше ничего не изучать). Это какое-то безумие.
166 18784
>>18783

>И вот конструктивисты призывают выкинуть всю математику на свалку, а полтора десятка брошюрок изучать (и больше ничего не изучать). Это какое-то безумие.


Вот я и спрашиваю, в чём принципиальное отличие от Рыбникова и ко.
167 18786
>>18783
>>18784
Я тебя услышал. К вышесказанному добавлю, что использовать свое незнание и непонимание темы для обосновывания чего-либо, тем более как точку зрения в дискуссии - это уровень детского сада.
168 18787
>>18786
Это разные аноны.
169 18788
>>18786
Вот это>>18783
не я писал.
170 18789
>>18786

>Конструктивистская математика есть, правда-правда. Но мы вам её не покажем, потому что вам не понять. А ваша математика не математика.

171 18790
>>18789
Вот-вот, Рыбников стайл. А всё почему? А потому что

>Конструктивные системы полны по Геделю, т.к все что есть в такой системе, выводимо. Поскольку конструктивные системы это построения, как и правила построений и правила проверки этих правил еа корректность это конструктивные объекты, то в такой системе нельзя выразить то, что из нее невозможно вывести или что в ней невозможно доказать.

172 18793
>>18784
>>18789
>>18790
К чему все это писать вообще? Ну не осилил, не твой уровень, смирись. Бывает.
173 18794
>>18793
К тому, что в любой хорошей, годной системе должен быть парадокс. Убираешь парадокс получаешь КалКалыч. Так и живём.
174 18795
>>18794

>в любой хорошей, годной системе должен быть парадокс.


С какой стати?
175 18796
>>18795
Так Гёдель сказал. К слову,

>Последний вопрос: теорема Гёделя и конструктивная матемтаика. Как у них дела вместе? Работает там она или нет?


ты меня почти убедил обмазаться конструктивной математикой. Если бы на последнйи контрольный вопрос ответил, что да, там есть такие-то и такие-то проблемы, то-то и то-то невыводимо, я бы обмазался. Но оказалось, что это ещё одна объяснялка всего и вся.
176 18797
>>18793
Почему же, вполне осилил. Я просмотрел библиографию конструктивистских книжек и статей и утверждаю ответственно: никакой конструктивистской математики не существует.
177 18798
>>18733
А Тезис Черча-Тьюринга-Дойча волшебным образом обходится?
178 18799
>>18796
Да, есть тут один конструктивный чудик, который думает, что теорема Гёделя о неполноте на конструктивную арифметику не распространяется ибо харе лямбда харе лямбда харе Барендрегт харе лямбда. Но это неправда: конструктивная арифметика не может доказать собственную непротиворечивость. Обмазывайся спокойно.
179 18800
>>18799
Лол. Ну надо голову проветрить тогда, а то уже выработал негативное отношение. Проветрю и посмотрю, да. Спасибо. А так я читал как-то мельком, идеи показались интересными. Может тогда ты расскажешь немного об интуиционизме/конструктивизме? Чего достигли, плюсы минусы и тд.
180 18801
>>18799
Хотя забей, потом сам почитаю.
HenkBarendregtattheOldJewishCemeteryinPrague.jpg522 Кб, 1200x1800
181 18802
>>18799
Ты объясни, откуда там неполнота, если все выводимо из данного контекста по данным правилам, а кроме контекста и правил ничего не дано?

>харе лямбда харе лямбда харе Барендрегт харе лямбда


Очень смешно. Однако, я ведь обосновываю свою позицию, даже со ссылками на Мартин-Лёфа и т.д.
182 18803
>>18778

> читателю предлагается вообразить алгоритм


Рассмотрим три способа использовать воображение:
1) вообразим, что буква B обозначает Windows
2) вообразим, что кардинал Вудина существует
3) вообразим, что мы эльфы и на нас напали гоблины

Конструктивисты же не против всего этого, просто (2) больше похоже на (3), чем на (1).

Ты вот, кстати, ругал богословие за нелогичность, а тот же Гёдель сбацал полностью формальное доказательства бытия Бога. Доказательство бесспорно верное и даже формализованное:
https://github.com/FormalTheology/GoedelGod
Аксиомы у него, правда, странноватые, но когда это останавливало классиков? Сам ведь говорил, что главное, чтобы следствия были интересными.

> для разных разделов математики следует использовать разные теории множеств


>>18783

>Есть математика, великая и неделимая,



Вот это вот один великий и неделимый анон написал?
183 18805
>>18802

> все выводимо из данного контекста по данным правилам, а кроме контекста и правил ничего не дано?


Ты видимо думаешь, что раз истинности в классическом понимании нет, то и от неполноты ты избавлен. Но есть совершенно конкретное утверждение: модель системы в ней самой никогда не докажет ложь. И это утверждение недоказуемо, потому что вторая теорема Гёделя. Можно ли это назвать неполнотой - это другой вопрос, но все обычно считают, что это она самая.

> я ведь обосновываю свою позицию, даже со ссылками


Давай так попробуем:
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 - классическая арифметика)
184 18806
>>18803
Более того, это же доказательство обнаружил Миша Вербицкий и вывел из него существование Ктулху.

https://lj.rossia.org/users/tiphareth/768813.html
https://lj.rossia.org/users/tiphareth/463319.html
185 18809
>>18805

>модель системы в ней самой никогда не докажет ложь.


Если ложь выводима в такой системе, т.е. следует из данных правил вывода на данном контексте, то докажет.

>if HA is consistent then neither HA nor PA can prove its own consistency.


Если мы рассматриваем "пруф" как конструктивный пруф-объект, а не как какое-то отвлеченное понятие сферической истины в вакууме, то такой пруф непосредственно выводим, как и его отсутствие (пустой тип). Разве нет?

>Можно ли это назвать неполнотой - это другой вопрос, но все обычно считают, что это она самая.


А с какой стати так считать, не подскажешь?
186 18810
Думаю это поколение 10-х тоже не будет использовать конструктивную математику. Нужно подготовить всё для поколения 20-х, вот они уже всё смогут.
187 18815
>>18809

> пруф непосредственно выводим, как и его отсутствие (пустой тип)


Тут надо аккуратнее говорить, потому что у тебя две системы - одна в другой - и по желанию можно еще завести третью снаружи, из которой можно наблюдать эквивалентность тех двух. А "конструктивный пруф-объект" хрен перенесёшь между уровнями.

> А с какой стати так считать, не подскажешь?


Ну например, чтобы разговаривать с остальными на одном языке. А так можешь назвать это световодозвуконепроницаемостью.
188 18819
Есть такой интересный феномен "слишком много почему". Это когда вы начиная разбирать какую то область начинаете слишком сильно рыть к основаниям. Формально - действие совершенно правильное, ибо не установив истинность основ, можно ли говорить о движении дальше? да и картина выглядит прочней если под нее подведен крепкий фундамент......однако на практике это часто вырождается в то, во что вырождается наша правовая система - вроде формально все правильно, но процедурные моменты съедают все. То есть, я ограничен временем и силами, а именно это в расчет и не берется. Можно начав копать, так и не дойти до конца, утомившись, забыв для чего все начиналось, да и когда можно останавливаться? в конце концов (и это наверно главный аргумент поста) таким образом я ищу психологическое удовлетворение. В итоге можно так и остаться у разбитого корыта из-за неумерной жадности. Ведь судить о мысли можно только познав ее целиком, но между нулем и единицей находится целая жизнь психологических неудобств, сомнений, давящего непонимания, грызущего чувства, что "под этим кроется нечто иное". Не зря Шопенгауэр пишет в предисловии к своей главной книге, что его книгу читателю придется одолеть дважды - сначала не понимая ничего, а затем видя все целое сразу. Не зря Гегель говорит, что его науку логики можно начинать читать с любого места. К тому же, никто не гарантирует, что я не встречу задачу не по плечу в этом рытье - а скорее всего, только их и встречаю - но ведь нет способа узнать, что задача была не по плечу, кроме того, чтобы потратить на нее кучу времени, с которого мы и начали.....поэтому единственный порою выход - психологически изолировать себя от подобных вопросов и изучать только то, что перед глазами. Этим пользовался Ньютон, когда представлял, что мир наполнен Богом - это позволило ему открыть закон тяготения, не остановившись на деталях. То же и с Коперником. То же и с детьми, которым их наивность служит главным орудием на пути познания нового. Короче, надо быть проще
189 18820
>>18815

>у тебя две системы - одна в другой - и по желанию можно еще завести третью снаружи, из которой можно наблюдать эквивалентность тех двух.


А к чему все это анальное шапито? Из самой конструктивной системы можно вывести все, что из нее вообще выводимо. Ну построишь внутри нее такую же, результат-то тот же самый будет.

>А "конструктивный пруф-объект" хрен перенесёшь между уровнями.


Потому тчо как ни крути, результат будет одним и тем же. Так к чему все эти уровни?
190 18834
>>18820

> Ну построишь внутри нее такую же


Ну а как иначе теорию доказательств развивать?

> Потому тчо как ни крути, результат будет одним и тем же.


Да нет же, смотри:
докажешь в большой системе, что в большой системе нельзя доказать ложь? тривиально!
докажешь в большой системе, что в маленькой системе нельзя доказать ложь? облом!
191 18835
>>18834
Но если большая и маленькая система это одно и то же, как тогда? И еще раз, "доказательство" - это что? Если конструктивный пруф-объект, то он ведь и является своим доказательством. И он будет одним и тем же для того, что ты называешь большой и маленькой системой, разве нет?
192 18836
>>18835

> И он будет одним и тем же


Да нет же! Между системами есть изоморфизм, причём с точки зрения сверхбольшой ("нашей") системы это изоморфизм тривиален, но этот изоморфизм нельзя выразить на языке большой системы, потому что где-то обязательно поломаются типы. Вот такая она, неполнота.
Снимок.PNG117 Кб, 1182x632
193 18837
>>18836

>Между системами есть изоморфизм, причём с точки зрения сверхбольшой ("нашей") системы это изоморфизм тривиален, но этот изоморфизм нельзя выразить на языке большой системы, потому что где-то обязательно поломаются типы.


А с чего они поломаются, если они одни и те же для всех систем? И изоморфизм между ними в том, что они эквивалентны. Где и что поломается-то, поясни.
194 18838
>>18837
Проиграл с пикчи.
195 18839
>>18837

> если они одни и те же для всех систем?


Как же они одни и те же, если они разных типов? Доказательство лжи в большой системе имеет с точки зрения большой системы тип ложь, а доказательство лжи в маленькой системе имеет с точки зрения большой системы тип "доказательство чего-то в маленькой системе".
Ты еще скажи, что 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.

Я не знаю, где и что поломается в конкретно твоём любимом исчислении, но если нигде ничего не поломается, то твоё любимое исчисление противоречиво, потому что Гёдель.
196 18840
>>18839
Боже, кто ты такой?
197 18841
>>18839
В смысле ты охуенен, пеши есчо.
198 18842
>>18839
Проблема в индуктивном определении дизьюнкции?
199 18861
>>18777
Он прав, про Гегеля написал я, и это была шутка очевидная, но тебе очевидно нужно чуть снизить пафос, потому что даже беглым взглядом видно, что ты не в теме нихуя совершенно.
14925132359350.jpg71 Кб, 850x400
200 18920
Вообще, теорема Геделя о неполноте это аналог парадокса лжеца или задаче о двух стульях 'на одном неполнота точена, на другом противоречивость дрочена, куда сам сядешь, куда мать посадишь?'. Очевидно, при любом ответе получается, что отвечающий пидр. В любой формальной системе, в т.ч в любом языке, на котором выращима математика, эта проблема неразрешима. Выходов тут в общемслучае два:
- толстоту толстотой вышибают. Можно поставить вопрос, а сама теорема Геделя, она противоречива или неполна? По аналогии с критерием Поппера, когда можно предложить оратору сфальсифицировать сам этот критерий.
- отказаться от попыток выразить основания математики формально, с помощью любого языка. Тогда приходим в двум актам интуиционизма Брауэра.
201 18921

>- отказаться от попыток выразить основания математики формально, с помощью любого языка. Тогда приходим в двум актам интуиционизма Брауэра.


c интуиционизмом эта мысль имеет примерно нихуя общего.
202 18924
>>18920
Теорема Гёделя несамоприменима же, она не является формальной системой.или является?
203 18927
>>18921
Ты так сказал? Гугли акты интуиционизма.
204 18929
>>18924
Является, это формальное доказательство же.
205 18935
>>18920
Это не формальная система. Формальная система матлогика. В ней уже есть парадокс Лжеца, собственно. Что ты этим хотел сказать?
206 18937
>>18935
То и хотел сказать, что теорема о неполноте есть вариант парадокса лжеца. Ну и она так же часть матлогики. Тут другое интересно, какая польза математике от этих софизмов? Доказали возможность закодировать в матлогике неразрешимые парадоксы, так Брауэр об этом 110 лет назад говорил. Что любой язык, на котором выразима математика не нужно отождествлять с самой математикой. К слову, это задолго до Геделя было им сказано.
207 18938
>>18937

>вариант парадокса лжеца


Это не вариант парадокса лжеца. Теорема говорит, что такой парадокс должен быть грубо говоря. Не одно и то же ведь. Сама по себе теорема никаких противоречий внутри себя не несёт.

>Ну и она так же часть матлогики.


Нет, ну это ведь разные вещи: формальная система и теорема, построенная в ней.

>Тут другое интересно, какая польза математике от этих софизмов?


Вряд ли есть какая-то пользану кроме сорт оф критерия Поппера, хотя это дуристика на самом деле, просто вот есть они и всё, и в разное время люди пытаются сделать с ними что-то.
208 18939
>>18938

>дуристика на самом деле


Просто противоречивость/непротиворечивость тоже ведь в тех же рамках определяется. Получается, что все, кто не с нами, те говно. По нашему же определению.
209 18940
>>18939

>противоречивость


Закон противоречия(закон непротиворечия) — закон логики, который гласит, что два противоречащих друг другу суждения не могут быть оба истинными. Если тезис принимает истинностное значение «истина», то антитезис принимает значение «ложь».
А что если в системе не работает этот закон? Как к ней можно применять теорему Гёделя?
210 18941
>>18938

> Нет, ну это ведь разные вещи: формальная система и теорема, построенная в ней.


Разные. Но чего стоит формальная система, если в ней выразимы такие парадоксы? Даже больше, чего вообще стоит формализм в таком случае?

> Вряд ли есть какая-то пользану кроме сорт оф критерия Поппера, хотя это дуристика на самом деле, просто вот есть они и всё, и в разное время люди пытаются сделать с ними что-то.


Так получается, что в консерватории править надо, коль скоро теорема Геделя касается вообще любой формальной системы, разве нет?
211 18942
>>18940
https://en.wikipedia.org/wiki/Quantum_logic
Вот, например. Если так подумать, то теорема Гёделя применима только к семейству формальных систем, которые не выходят за некоторые рамки околоклассической логики. А она противоречива и все это знают ещё с древности. Потому неудивительно, что во всех таких системах будет противоречивость, унаследованная от классической логики.
212 18943
>>18941
Да вот я тоже думаю, дуристика какая-то если честно. Но конструктивизм входит в те формальные системы, на которые распространяется эта теорема. Дело не в законе исключённого третьего просто, а в самом первом законе. На деле ведь очень даже легко оба высказывания, противоречащие друг другу, могут быть истинными. Вова лжец, да, пиздобол знатный, вова честный, да, честный с самим собой. Ну я утрирую, но много примеров можно придумать. Или вот "Ты пидор". Для гея, прочитавшего данное выражение это будет истина, для натурала ложь. Аналогично "Ты не пидор". Если первое прочитает гей, а второе натурал, то оба будут истинными. Просто высказывания на самом деле содержат в себе суперпозицию и становятся истинными или ложными в зависимости от конкретной формулы, от ситуации, от наблюдателя,
213 18944
>>18943
Честно говоря мы давно уже пользуемся такой логикой, просто эмулируем её с помощью классической и других. Из-за эмуляции и парадоксы.
214 18946
>>18943

> Да вот я тоже думаю, дуристика какая-то если честно. Но конструктивизм входит в те формальные системы, на которые распространяется эта теорема.


Интуиционизм Брауэра не входит. Но его еще Гейтинг дропнул (ученик Брауэра, к слову), правда с оговоркой, что его интуиционистская логика не формализует интуиционизм. По Брауэру, это просто один из языков, в котором может быть выражена математика.
215 18947
>>18946
Сложно это всё. Нужно прокачаться как следует, прежде чем к таким вещам приступать.
216 18949
>>18929
Нет, теорема Гёделя формулируется в метатеории и существенно использует метаязык.
217 18950
>>18949
Метаматематика - не формальная система?
218 18951
>>18950
Метаматематика - это наука, начнем с этого.
219 18957
>>18951
Ой, все. Ок, метаязык это не формальная система?
220 18958
>>18957
Обычно нет. Потенциально есть лестница языков: формальный язык, его метаязык, метаязык метаязыка и т.д. На практике высокие этажи не строят. Тем не менее, они могут быть построены при необходимости.
221 18959
>>18958
Но ведь все эти языки - формальные системы. Как пример, у бурбаков в 1 главе 1 го тома.
222 18960
>>18959
Нет. Во многих случаях метаязыком является русский язык, например.
223 18962
>>18960
Но ведь русский язык при его использовании для описания формальной системы становится просто неканонической символикой для канонических элементов, и вычислим в эти элементы. Nominal definition ежжи, разве нет?
224 18963
Эта мантра "метаязыком может быть русский язык" меня пиздец бесит. А язык чувств может быть, дебилы блять? Пиздец, основания математики они строят.
225 18964
>>18963

> Эта мантра "метаязыком может быть русский язык" меня пиздец бесит. А язык чувств может быть, дебилы блять?


Может. Почему нет?
226 18965
>>18963
Проблемы?
5472843.jpg56 Кб, 600x429
227 19066
>>18920
Хотел было написать тебе ответку, но потом глянул за что ты топишь.

>Только с развитием вычислительной техники, компьютеров, машинной математики оказалось, что наиболее эффективным языком математических программ для этой техники является язык именно конструктивной математики.


Если вот это правда то ладно.
228 19068
>>18963
Да, есть неконцептуальное мышление и восприятие.

Вот учебник:
https://studybuddhism.com/ru/prodvinutyy-uroven/lamrim/vipashyana/pustotnost-lozhnogo-ya
Если долго и упорно вчитываться в каждое предложение подолгу его обдумывая то в конце концов можешь научиться.

Собственно намного превосходит по мощности обычное словесное. Потому что вместо операций и восприятия какого то объекта, напрямую воспринимаешь и оперируешь его свойствами.

Ну и на уровне концептуального мышления не понять ни этот текст, ни вообще ни одно духовное учение. Только когда вывалишься в неконцептуальное тогда и осилишь. Сопровождается некоторым нарастающим чувством, которое затем резко сменяется на понимание и изменение восприятия.
229 19073
>>19066

>Только с развитием вычислительной техники, компьютеров, машинной математики оказалось, что наиболее эффективным языком математических программ для этой техники является язык именно конструктивной математики.


Не наиболее эффективным, а единственно возможным. Хотя бы потому что на комплюктере без вычислимости никуда. И да, тот же Тьюринг был конструктивистом, все его значимые работы это конструктивная математика. Алгоритм это вообще изначально конструктивное понятие, как и компьютерная программа. Поэтому вдвойне смешно как школьники копротивляются против конструктивизма, используя его плоды.
230 19075
>>19073
Ты это, ссылки давай на книжки об этой фигне, но что б понятные были. И желательно что бы требовался не математический бэкграунд, а программерский.
231 19091
>>19075

>желательно что бы требовался не математический бэкграунд, а программерский.


Такие вряд ли есть. Все-таки это прежде всего математика. Посмотри "Типы в языках программирования" Пирса, 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".
232 19104
>>19091
Спасибо, глянем-с.
ladywelbyoriginal.jpg67 Кб, 620x780
233 19135
За сигнифицизм кто-нибудь что-нибудь пояснить может?
234 19150
>>19068
Рома?
235 19159
>>19150
Неа. Да и я даже не буддист если что.
236 19164
>>19159
А кто? На основании чего описываешь субъективный опыт постижения метапустотности? Имеет ли это непосредственное отношение к основаниям математики?
237 19183
>>19164
А оно сильно важно?

>На основании чего описываешь субъективный опыт постижения метапустотности?


Че то я тут не понял чего ты хочешь.

Имеет ли это непосредственное отношение к основаниям математики?
Естественно. Вы же должны копнуть так глубоко как это возможно что бы найти правильные основания. И умственный метод постижения того что я кинул по ссылке довольно сложен и может и вообще возможен только для людей с определенным складом ума, которых здесь точно больше чем где либо на борде.

Это просто дверка из одного мирка мышления в другой, более мощный и включающий в себя первый как часть.

Ну, без этого вся ваша математика выглядит очень бедно.
238 19186
>>19183

> вся ваша математика


Хорошо, я тебя услышал.
239 19188
>>19183

> Вы же должны копнуть так глубоко как это возможно что бы найти правильные основания.


Глубже Брауэра в смысле поиска оснований в ментальных построениях все равно никто пока не копнул. Но это не предел, т.к. сам Брауэр не идет дальше кантианского понимания праинтуиции, в его время не были известны нейрофизиологические субстраты восприятия времени и основанные на нем интуиции натурального числа и континуума. Это сейчас все это изучено довольно глубоко, но зато сам интуиционизм в брауэровском понимании дропнули.
240 19205
Что-то много букв, есть какие-то основные принципы Бауэра?
brouwer.png653 Кб, 1709x744
241 19206
>>19205
Есть, конечно. Причем, там и букв не очень много. Вся суть это два акта интуиционизма пикрелейтед, но там надо пояснять, что он имел в виду. С телефона хз как ссылки дать, а с браузера на компе мейлру не работает. Кембриджские лекции Брауэра, например. На либгене есть. По хардкору и с комментариями - van Stigt, 'Brouwer's intuitionism', 3я глава.
242 19210
>>19206
А что про книгу Гейтинга про интуиционизм скажешь?
243 19211
>>19210
Гейтинг первый же и дропнул изначальные идеи Брауэра. Книжка неплохая, тем более советское издание с комментариями Маркова. Но это уже больше конструктивизм чем интуиционизм как его понимал Брауэр.
244 19230
>>19206
И у меня не работает, капчую с Германии теперь.
245 19243

>Глубже Брауэра в смысле поиска оснований в ментальных построениях все равно никто пока не копнул. Но это не предел, т.к. сам Брауэр не идет дальше кантианского понимания праинтуиции, в его время не были известны нейрофизиологические субстраты восприятия времени и основанные на нем интуиции натурального числа и континуума. Это сейчас все это изучено довольно глубоко, но зато сам интуиционизм в брауэровском понимании дропнули.



Принято считать, что ограниченность науки в изучении психических процессов состоит в том, что в кругу прочих возможных объектов исследования она избирает те, что хотя бы потенциально могут быть обнаружены в материальной реальности и поддаются измерению. Именно поэтому она предпочитает опираться на свет, который проливают инструментальные исследования мозга, притом что сама темнота этого предмета остается все такой же непроницаемой.

Тем не менее, Лакан показывает, что причина малых успехов нейрофизиологии не в этом, а в том, что наука стойко избегает коллизий, связанных с работой означающего. Это и является причиной, в силу которой она отделена стеной от феномена, к которому Фрейд подошел с такой легкостью — к феномену сновидения.
От Лакана мы знаем, чем эта легкость была оплачена — Фрейд взял ее в долг у лингвистики, как раз открывшей для себя к тому времени существование означающего. Тем не менее, произведенный Фрейдом продукт оказался лингвистике не нужен — Фрейд извлек из него совершенно особую логику, ставшую основой самостоятельной психоаналитической науки.

Наука эта способна объяснить некоторые примечательные явления, связанные с нарушением обычного процесса протекания сновидения. Так, когда некто видит «осознанный» сон, полагая, что его осознанность доказывается лишь тем, что он в этом сне способен сказать себе «я вижу этот сон», или просыпается от случайного звука, который задним числом оказался встроен в сновидение так, что к моменту внезапного пробуждения сон оказывает логически завершен, то все эти процессы обязаны именно работе означающего. Эта работа и обуславливает возможность занять в своем сне метапозицию, превратив его в люцидный, или же увидеть сон именно по той причине, что процесс сна оказался прерван — то есть, сделать невозможное и успеть сам пробуждающий стимул обыграть как полноразмерное сновидение.

Там где «строгая» наука, также соблазненная этими загадочными явлениями, в итоге с ними не справляется и, перебрав разнообразные физиологические причины, уступает место паранаучным догадкам, психоанализ объясняет их структуру и показывает, что все эти труднопостижимые трюки становятся возможными, поскольку работа означающего задает особый порядок времени.
По всей видимости, иные психические акты, происходящие в бодрствовании — такие как смех, забывание, принятие решения — в своей логике временного сбывания устроены так же сложно, как и нарушенное, прерванное сновидение. Это лишь подтверждает ту блеснувшую у Фрейда догадку, что само бодрствование — не что иное, как нарушение сна.
245 19243

>Глубже Брауэра в смысле поиска оснований в ментальных построениях все равно никто пока не копнул. Но это не предел, т.к. сам Брауэр не идет дальше кантианского понимания праинтуиции, в его время не были известны нейрофизиологические субстраты восприятия времени и основанные на нем интуиции натурального числа и континуума. Это сейчас все это изучено довольно глубоко, но зато сам интуиционизм в брауэровском понимании дропнули.



Принято считать, что ограниченность науки в изучении психических процессов состоит в том, что в кругу прочих возможных объектов исследования она избирает те, что хотя бы потенциально могут быть обнаружены в материальной реальности и поддаются измерению. Именно поэтому она предпочитает опираться на свет, который проливают инструментальные исследования мозга, притом что сама темнота этого предмета остается все такой же непроницаемой.

Тем не менее, Лакан показывает, что причина малых успехов нейрофизиологии не в этом, а в том, что наука стойко избегает коллизий, связанных с работой означающего. Это и является причиной, в силу которой она отделена стеной от феномена, к которому Фрейд подошел с такой легкостью — к феномену сновидения.
От Лакана мы знаем, чем эта легкость была оплачена — Фрейд взял ее в долг у лингвистики, как раз открывшей для себя к тому времени существование означающего. Тем не менее, произведенный Фрейдом продукт оказался лингвистике не нужен — Фрейд извлек из него совершенно особую логику, ставшую основой самостоятельной психоаналитической науки.

Наука эта способна объяснить некоторые примечательные явления, связанные с нарушением обычного процесса протекания сновидения. Так, когда некто видит «осознанный» сон, полагая, что его осознанность доказывается лишь тем, что он в этом сне способен сказать себе «я вижу этот сон», или просыпается от случайного звука, который задним числом оказался встроен в сновидение так, что к моменту внезапного пробуждения сон оказывает логически завершен, то все эти процессы обязаны именно работе означающего. Эта работа и обуславливает возможность занять в своем сне метапозицию, превратив его в люцидный, или же увидеть сон именно по той причине, что процесс сна оказался прерван — то есть, сделать невозможное и успеть сам пробуждающий стимул обыграть как полноразмерное сновидение.

Там где «строгая» наука, также соблазненная этими загадочными явлениями, в итоге с ними не справляется и, перебрав разнообразные физиологические причины, уступает место паранаучным догадкам, психоанализ объясняет их структуру и показывает, что все эти труднопостижимые трюки становятся возможными, поскольку работа означающего задает особый порядок времени.
По всей видимости, иные психические акты, происходящие в бодрствовании — такие как смех, забывание, принятие решения — в своей логике временного сбывания устроены так же сложно, как и нарушенное, прерванное сновидение. Это лишь подтверждает ту блеснувшую у Фрейда догадку, что само бодрствование — не что иное, как нарушение сна.
246 19245
>>19243
Нет причин читать Лакана или Фрейда. Ума это не прибавит.
247 19246
>>19245
Тебе - наверняка (как и что либо вообще).
248 19290
>>19243
Есть даже лингвистические основания математики, т.н. сигнифика Маннури. Там тоже все связано с семиотикой и прочим таким. Но инфы по этой теме даже на английском маловато, в основном оригиналы на датском. Так что Лакан этот твой вряд ли что'то может добавить в математику помимо того, что в нее уже добавили ребята из венского кружка сто+ лет назад.
249 19315
>>19188
Может быть. Но фишка той штуки в другом маленько.
sage 250 19339
>>19243

>Лакан


Это не тот дешевый шут, которого обоссали в одной популярной книжке за неадекватное ничему разумному употребление математических терминов в своей шизофазии?
251 19345
252 19400
>>19339
не, это Лакан обстоятельно пояснил за весь научный дискурс, а Докинз и приближённые просто тонну баттхёрта на бумагу высрали, как какие-нибудь школьники Ларинофаги
253 19402
>>19400
Пришло время запостить "пояснения" Лакана.
...
Эта диаграмма (лента Мебиуса) может быть рассмотрена как основание некоей изначальной надписи, находящейся в ядре, конституирующем субъекта. Это значит гораздо больше, чем вы сперва могли бы подумать, поскольку вы можете поискать тип поверхности, способной принимать такие надписи. Вы, возможно заметите, что сфера, древний символ цельности, не подходит. Подобный разрез способны принимать на себя тор, бутылка Кляйна, поверхность cross-cut[16]. Причем само разнообразие весьма важно, поскольку оно многое объясняет в структуре душевных заболеваний. Если субъект можно символизировать таким фундаментальным разрезом, то точно так же можно показать, что разрез на торе соответствует невротическому субъекту, а разрез на поверхности cross-cut — другому виду душевного заболевания.
...

В этом пространстве наслаждения взять нечто ограниченное, закрытое — это взять место, и говорить о нем — это значит заниматься топологией.
...
Здесь я предлагаю ввести термин «компактность». Не может быть ничего компактнее зазора, если понять, что, допуская существование пересечения всего того, что закрывается, на бесконечном числе множеств, мы приходим к выводу, что пересечение включает в себя это бесконечное число. Это и есть определение компактности.
...
Формулу нам дает та топология, которую я охарактеризовал как самую позднюю по времени возникновения, поскольку она отправлялась от логики, построенной на исследовании числа, которое привело к заданию места, которое не является местом гомогенного пространства. Возьмем все то же ограниченное, закрытое, предположительно устойчивое место — эквивалент того, что я только что сказал о пересечении, расширяющемся до бесконечности. Если предположить, что оно покрыто открытыми множествами, то есть множествами, исключающими своей предел — предел, чтобы вам это вкратце напомнить, — это то, что определяется как большее одной точки и меньшее другой, но никогда не равное ни отправной точке, ни конечной[20] — обнаруживается доказательство того, что равным образом можно сказать так: множество этих открытых пространств всегда поддается неполному покрытию открытыми пространствами, задающими конечность; то есть последовательность элементов задает конечную последовательность.
...
Субъект в той половине, где он определяется отрицаемыми кванторами, относится к тому, что ничто существующее не создает предела функции, что невозможно удостовериться в чем бы то ни было, относящемся к универсуму. Таким образом, если основываться на этой половине, «они», женщины, не «не все», и, следовательно, отсюда же получается, что ни одна из них не является также всей.
...
Мы в свою очередь будем отправляться от того, что выражает буквенное сокращение S(∅), то есть от означающего.
Поскольку тем самым связка означающих дополняется, это означающее может быть лишь чертой, которая прочерчивается из круга означающих, не имея возможности быть подсчитанным в нем. Это символизируется внутренней связью (-1) с множеством означающих.
Как таковое его нельзя произнести, но не его действие, поскольку это действие совершается всякий раз, как произносится собственное имя. Его высказывание равно его значению.

Откуда вытекает следующая формула, если подсчитать это значение в используемой нами алгебре:

S(означающее) / S(означаемое) = S(высказывание)
а при S=(-l) мы имеем: s=√-1.
...
Вот каким образом эректильный орган начинает символизировать место наслаждения, причем не сам по себе и не в качестве образа, а как часть, недостающая желаемому образу: поэтому-то его и можно приравнять к √-1 более высоко произведенного значения, к √-1 наслаждения, которое он восстанавливает посредством коэффициента своего высказывания в функции нехватки означающего.
253 19402
>>19400
Пришло время запостить "пояснения" Лакана.
...
Эта диаграмма (лента Мебиуса) может быть рассмотрена как основание некоей изначальной надписи, находящейся в ядре, конституирующем субъекта. Это значит гораздо больше, чем вы сперва могли бы подумать, поскольку вы можете поискать тип поверхности, способной принимать такие надписи. Вы, возможно заметите, что сфера, древний символ цельности, не подходит. Подобный разрез способны принимать на себя тор, бутылка Кляйна, поверхность cross-cut[16]. Причем само разнообразие весьма важно, поскольку оно многое объясняет в структуре душевных заболеваний. Если субъект можно символизировать таким фундаментальным разрезом, то точно так же можно показать, что разрез на торе соответствует невротическому субъекту, а разрез на поверхности cross-cut — другому виду душевного заболевания.
...

В этом пространстве наслаждения взять нечто ограниченное, закрытое — это взять место, и говорить о нем — это значит заниматься топологией.
...
Здесь я предлагаю ввести термин «компактность». Не может быть ничего компактнее зазора, если понять, что, допуская существование пересечения всего того, что закрывается, на бесконечном числе множеств, мы приходим к выводу, что пересечение включает в себя это бесконечное число. Это и есть определение компактности.
...
Формулу нам дает та топология, которую я охарактеризовал как самую позднюю по времени возникновения, поскольку она отправлялась от логики, построенной на исследовании числа, которое привело к заданию места, которое не является местом гомогенного пространства. Возьмем все то же ограниченное, закрытое, предположительно устойчивое место — эквивалент того, что я только что сказал о пересечении, расширяющемся до бесконечности. Если предположить, что оно покрыто открытыми множествами, то есть множествами, исключающими своей предел — предел, чтобы вам это вкратце напомнить, — это то, что определяется как большее одной точки и меньшее другой, но никогда не равное ни отправной точке, ни конечной[20] — обнаруживается доказательство того, что равным образом можно сказать так: множество этих открытых пространств всегда поддается неполному покрытию открытыми пространствами, задающими конечность; то есть последовательность элементов задает конечную последовательность.
...
Субъект в той половине, где он определяется отрицаемыми кванторами, относится к тому, что ничто существующее не создает предела функции, что невозможно удостовериться в чем бы то ни было, относящемся к универсуму. Таким образом, если основываться на этой половине, «они», женщины, не «не все», и, следовательно, отсюда же получается, что ни одна из них не является также всей.
...
Мы в свою очередь будем отправляться от того, что выражает буквенное сокращение S(∅), то есть от означающего.
Поскольку тем самым связка означающих дополняется, это означающее может быть лишь чертой, которая прочерчивается из круга означающих, не имея возможности быть подсчитанным в нем. Это символизируется внутренней связью (-1) с множеством означающих.
Как таковое его нельзя произнести, но не его действие, поскольку это действие совершается всякий раз, как произносится собственное имя. Его высказывание равно его значению.

Откуда вытекает следующая формула, если подсчитать это значение в используемой нами алгебре:

S(означающее) / S(означаемое) = S(высказывание)
а при S=(-l) мы имеем: s=√-1.
...
Вот каким образом эректильный орган начинает символизировать место наслаждения, причем не сам по себе и не в качестве образа, а как часть, недостающая желаемому образу: поэтому-то его и можно приравнять к √-1 более высоко произведенного значения, к √-1 наслаждения, которое он восстанавливает посредством коэффициента своего высказывания в функции нехватки означающего.
254 19403
>>19402
А в чём проблема? В "У-у-у НЕНОУЧНО, у нас за такое в НОУЧНОЙ ЛАБОРАТОРИИ убивают нахуй" или в чём-то другом? Он пользуется нужными ему частями математического тезауруса в своих целях, для достижения нужного ему эффекта.
image.png312 Кб, 487x459
255 19409
>>19339
>>19402
Тот самый.
256 19414
>>19402
Набор слов, гуманитарный поток сознания. Причем тут математика и основания?
257 19418
>>18620
У меня Барендрехт от того, что там нет доказательства от противного.
258 19420
>>19418

> У меня Барендрехт от того, что там нет доказательства от противного.


Конструктивное доказательство - это построение. В общем случае методом от противного невозможно получить такое построение или хотя бы правила построения. Если в каком'то конкретном случае можно, то такое доказательство вполне конструктивно. Как и с исключенным третьим, принимаются только случаи, когда оно доказуемо непосредственно, а не вера в априорную применимость этого принципа.
259 19567
>>19420 >>19418
Господа, а ведь можно считать конструктивным доказательством от противного построение игры двух агентов, если показать, что фальсифицирующий агент всегда проигрывает. Что скажете?
260 19673
>>19567
У такого подхода есть большая проблема: что, если игрок хочет тянуть время до бесконечности? Придётся разрешать бесконечные игры, но это неконструктивно.
lar.jpg315 Кб, 1390x521
261 19679
>>19673

>Придётся разрешать бесконечные игры, но это неконструктивно.


Ну такое, есть методы
262 19681
>>19567
Если взять игру, где из проигрыша одного однозначно следует выигрыш другого, то в конкретно этом случае доказательство от противного будет носить конструктивный характер, т.к. оно построимо непосредственно, либо следует из правил игры. Но это никак не значит, что доказательство от противного применимо как общий метод в математике.
263 19682
>>19673
https://www.youtube.com/watch?v=JqLX4LzFBn4
Вот лекция на эту тему, если интересно
264 19740
>>19409
Комментарий - огонь. "Мнения лакановских аналитиков расходятся" и установить, чьё мнение верно, а чьё - нет, конечно, никак невозможно, потому что психоанализ не фальсифицируем.
265 19741
>>19403
В том то и дело, что эти цели не имеют никакого отношения к науке.
266 19742
Вот каким образом эректильный орган начинает символизировать место наслаждения, причем не сам по себе и не в качестве образа, а как часть, недостающая желаемому образу: поэтому-то его и можно приравнять к Ö-1 более высоко произведенного значения, к Ö-1 наслаждения, которое он восстанавливает посредством коэффициента своего высказывания в функции нехватки означающего: (-1). (Лакан)
267 19748
>>19742
Ö - это корень.
268 19788
>>19748
Если корень из -1 - это эректильный орган, то что для Лакана многочлен?
GerritMannoury,1917.jpg17 Кб, 220x281
269 19842
Наброшу, пожалуй. Если не веровать в мировую душу и мир идей, как ни крути, а выходит, что математика это продукт деятельности человека. Причем, вне прикладухи и прочей десятой культуры, в общем случае не связана с физикой и т.п объективным. Математика при этом, даже сколь угодно сложная, всегда выразима в естественном языке, т.к все термы, формулы и т.п вербализуемы. Итого, основаниями математики может быть только язык, психолингвистика. Т'е нечто изначально неточное. Получается, что вера в абсолютную точность математики это просто суеверие, т.к основанное на неточном точным и абсолютным быть не может, ну если не веровать во всякий платонизм.
270 19843
>>19842
Значительная часть математики невербальна. Картины да Винчи могут быть описаны словами, но да Винчи не писал описания картин, он рисовал.
271 19846
>>19843

> Значительная часть математики невербальна.


Покажи, что в математике нельзя описать словами. Вот есть формула, у всего в этой формуле есть название. Любой математический текст можно зачитать вслух, грубо говоря.
272 19847
>>19846
Добавлю, если не зачитать, то записать. Текст это такой же язык.
22695202.jpg264 Кб, 1099x1476
273 19848
>>19846
Пикрелейтед можно описать текстом, но пикрелейтед - не текст. Так же и с математикой. Формулы - это всего лишь описание знания, но не собственно знание.
274 19852
>>19848

>Формулы - это всего лишь описание знания, но не собственно знание.


Что тогда по-твоему знание? Что-то из мира идей и прочей мировой души? Ты веришь в знание, которое невербализуемо?

>Пикрелейтед можно описать текстом, но пикрелейтед - не текст.


Текст. Твой пикрелейтед - всего лишь 3хмерный тензор, 3 матрицы градаций синего, красного и зеленого (мб еще канал прозрачности), т.е. это чистые циферки, текст. Далее, математика - это таки текст, в математике нет ничего, что нельзя записать, т.е. выразить текстом, т.е. в конечном счете свести к этому тексту. Более того, формально-аксиоматический подход - это вообще чистый текст без оговорок. По теории уровней языка Маннури, есть 5 уровней текста пикрелейтед. Все они производные от первого уровня и отличаются между собой только степенью применимости к тексту данного уровня формализации, причем эта разница чисто количественная, качественной разницы между уровнями нет. 1ый уровень формализовать очень сложно, если вообще возможно (это н-р разговорный язык детей), 5ый по-сути, формализм в чистом виде (н-р матлогика).
275 19856
>>19852
Ты путаешь символ и значение символа.
276 19857
>>19856
Любое значение символа так же выразимо в языке, н-р широко применяемое в конструктивных логиках т.н. nominal definition. Далее, чистый формализм изначально отказывается рассматривать значение знака, знакосочетания и правила работы с ними это только синтаксис, без семантики. Эта тема хорошо раскрыта у Бурбаков.
277 19858
>>19857
Няш, не трогай бурбаков. По-хорошему тебе советую. Тут есть некоторые люди, которые действительно прочитали книжку Бурбаки и могут насовать тебе хуев за воротник. Так что не говори о бурбаках, не стоит.
278 19859
>>19858

>не стоит вскрывать эту тему, вы молодые шутливые...


Я тебя услышал. А если предметнее? Вот конкретно мной про Бурбаков написанное, что там не так?
интуиция у бурбаки.png55 Кб, 615x181
279 19861
>>19859
Генерал открыто утверждает, что математика не является всего лишь игрой в символы. Он даже ввел специальное обозначение для выделения тех участков текста, которые объясняют идею, стоящую за тем или иным определением/теоремой. Для Бурбаки аксиоматический метод - просто удобный способ избежать ошибок в математической работе, Бурбаки отнюдь не сводит математику к составлению текстов.
280 19863
>>19861
Ладно, более конкретный вопрос. Что именно в математике не вербализуется и не сводится к языку в широком понимании его (н-р в виде 5 уровней, см.выше)?
281 19864
>>19863
Читал ли ты "Плач математика"?
282 19866
>>19864
Не читал. Сейчас погуглил, судя по всему там как раз о том, что математика - это вид человеческой деятельности и лучше обучать ей детишек не через заучивание формализмов, а более естественным образом. Сигнифика как раз об этом, Маннури критиковал Гильберта именно по той причине, что он недооценивает значение эмоций и т.п. психолингыистических аспектов математики, а сводит все к манипуляции с символами. Но любой язык выводится из языка 1го уровня, в т.ч. и строго формальный, поэтому отрывать язык от его происхождения это неправильно. Все эти соображения никак не противоречат тому, что математика - это языковая деятельность человека.

>Суть математики — в игре и в поиске. Доказать, например, теорему Пифагора — весьма и весьма увлекательный квест для ребёнка. Проблема только в том, что на уроках дети не решают задачи, а всего лишь заучивают наизусть чужие решения, изложенные при этом заумным (даже для взрослого математика) языком.

283 19867
>>19866
Возможно мышление вообще без языка. Оно проявляется, например, при глубокой концентрации, при внутреннем созерцании идеи. Речь не о воображении трехмерного тела, конечно.
1404483564012.jpg223 Кб, 785x1018
284 19868
>>19867

>Возможно мышление вообще без языка. Оно проявляется, например, при глубокой концентрации, при внутреннем созерцании идеи.


Идеи, которая в любом случае вербализуема. Если ты читал Кастанеду, у него есть понятие "тоналя" и "нагуаля", второе - это как раз деятельность, возможная после остановки внутреннего диалога. Но опять же, при желании оно сводится к первому.
285 19871
>>19868
Картину можно описать словами. Но словесное описание картины не будет картиной.
286 19872
>>19871
Зависит от языка. Я тебе выше показал, что таки будет. Нейросети так и распознают картинки, аппроксимируя функцию с тегами в области значений и тензорами в области определения. Это во'первых. Во'вторых, ты так и не ответил, причем тут математика и картина, и что конкретно в математике невербализуемо.
287 19879
Интересно вы успели придти к соотношению карты и территории.

Ну, и если так интересует именно сознание, разум, вот это всё, но не хотите упасть куда-то совсем дебри, то могу посоветовать принять точку зрения функционализма (философия сознания) на этот вопрос, а дополнительно можете почитать, например, Джефф Хоккинс "Об интеллекте". Фактически, в этой книге говорится, что в новой коре мозга (а она собственно и отвечает за процесс мышления) нет ничего кроме памяти и прогнозирования (предсказания). Ну, это конкретно новая кора, мало рассматривается рептильный мозг и прочее. Книга научно-популярная вроде как.
288 19880
>>19879
Научпоп не нужон кроме разве что Рамачандрана, чувак мощно задвигает, какие-то глобальные теории уровня "что есть интеллект" тем более. Нейролингвистики для нужд сигнифицизма как оснований математики более чем достаточно, для брауэровского неоинтуиционизма достаточно моделей АТОМ и МТ (metaphor theory).
289 19881
>>19879
А, как-то забыл где я нахожусь. Ну, есть различные модели Искусственного Интеллекта, которые впрочем нельзя вычислить в нашей Вселенной. Это Solomonoff induction (фактически, всё строится именно на ней), AIXI и UAi в целом.

В общем, там суть в переборе программ. И есть, например, даже версия почему природа выбрала именно нейросети в качестве аппроксимации индукции Соломонова. В общем, не знаю, может вы там будете читать сверхсерьезные статьи, но если погуглить "lesswrong solomonoff induction" то там есть хорошие статьи по этому всему для самых маленьких и рядом можно найти тоже по сходной теме, для самых маленьких, подчеркиваю.
290 19887
>>19872
Есть разница между вещью и моделью вещи, между картиной и текстовым описанием картины.

Как минимум, невербализуемы мысли и чувства, которые заставляют математика выбирать именно те слова, которые он выбирает, и писать именно те тексты, которые он пишет. Посмотри, например, на себя. Ты ведь не можешь заменить себя каким-нибудь текстом, ты не текст. И даже просто понять, каким образом ты разговариваешь, ты не можешь. Если ты попытаешься проанализировать, что происходит в твоей голове при разговоре, если ты внимательно сконцентрируешься на том, почему ты строишь свою речь так, а не иначе, - ты просто лишишься способности говорить и не напишешь ни слова (аналогично если сказать тебе, что ты дышишь, то ты ненадолго потеряешь способность свободно дышать). Потому что тексты ты генерируешь бессознательно, актом невербализуемого мышления. Мышление тут совершается несомненно, ведь если бы мышления не было, то ты бы генерировал белый шум, но ты генерируешь осмысленные тексты. И это мышление не является текстом, потому что ты не мыслишь словами вроде "первым словом, которое я скажу, будет слово 'Интересно'", ты просто берешь и разговариваешь.
GerritMannoury,1911.jpg10 Кб, 220x314
291 19888
>>19887

>невербализуемы мысли и чувства, которые заставляют математика выбирать именно те слова, которые он выбирает, и писать именно те тексты, которые он пишет.


Выбранные слова и написанный текст в данном случае и является вербализацией психолингвистических процессов, их внешним проявлением, функцией от них. Ведь именно эти процессы в конечном счете и породили выбранные слова и текст, а не другие и не чистый рандом. Т.е. язык, в т.ч. математический, это прямое проявление психолингвистических процессов, стоящих за этим языком.
292 19889
>>19888
Но не сам процесс. Математический текст - это не единственный результат мышления математика, есть и другие результаты. Например, изменение состояния ума математика.
293 19890
>>19889
Вербализация - внешнее проявление психолингвистических процессов, породивших ее. В этом суть любой языковой деятельности человека, в т.ч. математики. Сами эти процессы можно полностью выявить нормальной нейровизуализацией, это чисто техническая проблема. В наше время не существует неинвазивных методов прямой записи ионного тока в ЦНС, без втыкания туда электродов и т.п. порнографии. Как только такие методы появятся, можно будет напрямую связать психолингвистические процессы и порождаемую ими вербализацию, т.к. такая связь будет напрямую выводимой из данных и т.о. вычислимой функцией, аппроксимируемой любым подходящим методом идентификации систем.
294 19892
>>19890
Тем не менее, по состоянию на "прямо сейчас" математика к текстам не сводится. Предлагаю вернуться к этому разговору, когда описанное тобой светлое будущее настанет.
ZFC.png246 Кб, 736x732
295 19893
>>19892

>по состоянию на "прямо сейчас" математика к текстам не сводится.


Сводится, в целом сгодится и fMRI высокого разрешения. Модели АТОМ и МТ так и получили. Общие же соображения на этот счет были высказаны почти 100 лет назад и их опровергнуть нечем. Формализм, опять же, это чистый синтаксис и манипуляции с текстом. А это такие вещи как ZFC, например.
296 19894
>>19893
Хорошо. Ты утверждаешь, по сути, что человек - набор рентгеновских снимков. Тогда почему у рентгеновских снимков нет прав человека? Почему они не подают в суд?
297 19895
>>19894

>Ты утверждаешь, по сути, что человек - набор рентгеновских снимков


Этого я не утверждал. Скажем, элементы нейровизуализации это неканоничные представления каноничных элементов - ионных токов, вычислимых одно в другое в качестве nominal definition. То же с вербализацией.
298 19897
>>19895
Суть в том, что программа, которая не исполняется ни одним исполнителем, отличается от программы, которую прямо сейчас исполняет некоторый исполнитель.
299 19899
>>19897
Это отличие хорошо бы доказать. А то если речь о вышеупомянутой ZFC, то эта "программа" одна и та же как при наличии ее исполнителя в данный момент, так и при его отсутствии. Т.е. формализованный язык хоть и является производным от первичного и т.о. является продуктом языковой деятельности человека, но при этом в основе его правила механического манипулирования со знаками и знакосочетаниями на этом языке, т.е. такой язык можно использовать в пруверах и результат доказательства теоремы н-р не будет отличаться от сделанного на этом языке человеком. Соседний тред как раз про один из таких пруверов - metamath.
300 19900
>>19899
Доказать это очень легко: оцифруй человека, запиши его на болванку и положи в шкаф. Если он оттуда умудрится подать на тебя в суд или совершить иное действие, которое может совершить исполняемый каким-нибудь физическим телом этот же человек, то я буду очень сильно удивлен.
301 19904
>>19900
Это же ты автор этой пасты >>18702 да? Очень заметно.
302 19915
>>19904
Угу. Только не надо воспринимать её слишком всерьёз, я просто набрасывал тогда.
303 19931
>>19915
Ну так вот, как я и написал выше, всякие общие теории интеллекта и т.д на текущем этапе их развития обсуждать смысла нет. Но по вопросам нейрофизиологических пруфов таких направлений в основаниях как интуиционищм Брауэра и сигнифика Маннури уже известно достаточно, чтобы утверждать, что упомянутые товарищи были правы. Намного интереснее вопрос, как получилось, что они оба правы (и это можно доказать) при том, что их позиции в вопросе на чем строить основания математики полностью взаимоисключающие? У меня есть некоторые соображения по этому поводу, и не только соображения, но и немного кода, но это тема не для мейлру.
304 19973
>>19931
Если они правы, то почему они не создали никакой математики?
305 19976
>>19973
Ты ж сам выше писал, что в математике не шаришь, это заметно. Иначе бы и вопроса такого не было. Про конструктивную математику ты не слышал, да? Насчет Маннури все сложнее, даже сейчас в 2017 технические возможности для создания математики по его идеям находятся в зачаточном состоянии, кое'что из нужного вообще не исследовано даже. Он больше чем на век свое время опередил.
306 19983
>>19976
Я шарю в математике. Конструктивной математики не существует.
307 19986
>>19983

> Конструктивной математики не существует.


А говоришь, шаришь. Ну поясняй, что у тебя за вера. Почему конструктивной математики не существует.
308 19993
>>19986
Допустим, конструктивная математика существует. Из каких разделов она состоит?
309 20013
>>19993
Это общий подход к любым разделам. Начиная от оснований. Все это обсуждалось уже и не один раз.
310 20014
>>20013
Подход есть, а результатов уже сто лет нет. Как так?
311 20015
312 20021
>>20015
Давай представим мир, в котором "конструктивная математика" существует. Это мир, в котором конструктивизм служит инструментом, с помощью которого изучаются какие-то другие вещи. В котором количество конструктивистки написанных монографий настолько велико, что приходится разбивать их на области. Этими областями могут быть, например, конструктивная теория групп, конструктивный анализ, конструктивная теория множеств, конструктивная гомологическая алгебра и т.п. - как в математике, только со словом "конструктивная" в названии. Это мир, в котором конструктивная наука построила целое здание абстрактного знания.

Что же имеет место в нашем мире? В нашем мире во всех монографиях, традиционно относимых к конструктивизму, темой исследования всегда является сам конструктивизм. Суть таких книг всегда - основания конструктивизма и/или доказательство через боль и слезы какого-нибудь тривиального математического факта. В нашем мире конструктивизм не оформился как наука - в отличие от математики.

Когда человек говорит "я занимаюсь математикой", это даёт мало информации о его деятельности - он может как аутировать над дифурами, так и шатать большие кардиналы. А вот когда человек говорит, что занимается конструктивизмом, абсолютно всегда понятно, что он делает. Поэтому понятия "математика" и"конструктивизм" являются понятиями очень разных уровней. Математика - полноценная богатейшая наука. Конструктивизм - фанатичное толкование двух с половиной ветхих философских книжонок.

Конструктивизм - это никакой не "общий подход".
313 20023
>>20021
Еще одна паста типа про математику? Примерно 99,999% конструктивных вещей не имеют в своем названии слова "конструктивный", хотя бы это ты должен знать. Мне реально лениво сотый раз нарезать и постить сюда определения конструктивного объекта по Мартин-Лёфу, тем более что я прекрасно вижу, что смысла в этом 0, все равно приходит очередной или один и тот же, но предельно гениальный зеленый феласаф и сказка про белого бычка начинается сначала. Нету конструктивной математики? Ок, раз школьники на мейлру так пишут, то и правда нету. Я все понял, все услышал.
314 20027
>>20023
Я могу показать математику - мне достаточно дать ссылку на архив или на матнет.
Ты не можешь показать конструктивизм - максимум можешь вырезать скрин из Мартин-Лёфа.
315 20068
>>20027
А ссылка на Мартин-Лефа это не ссылка, и его конструктивная теория типов это не теория и не конструктивная и не типов, я тебя правильно же понимаю, да? Зачем ты вообще все это пишешь?
316 20069
>>20068
Представь, что некий философ Мартинда выдумал подход, который назвал "деконструктивная математика". Он написал много букв про то, какой деконструктивизм хороший и какая вся остальная математика плохая. Но все его тексты посвящены исключительно деконструктивной математике, никакие, скажем, теоремы об индексе он доказать даже и не пытался. Назовёшь ли ты математикой деятельность философа Мартинды? Будешь ли утверждать, что миллионы книг по математике равновелики трем с половиной его брошюркам?
317 20070
>>20069
То есть, конструктивные доказательства это не доказательства, пруверы это не пруверы? Может быть, я виноват, что ты про все это не слышал? Ты попробуй не просто писать, а думать о том, что пишешь.
318 20071
>>20070
Я могу перечислять книги по математике несколько часов подряд и ни разу не повториться. Ты, если попытаешься перечислить книги по якобы существующей "конструктивной математике", не наберешь и сотни. Да что там, даже десятка.

Предъяви набор конструктивных книг, равнообъемных хотя бы трактату Бурбаки.
319 20072
>>20071
Дарья Донцова написала больше книг, чем Бурбаки, значит математика бурбаков не существует, это твоя логика. Подумой и не пиши хуйни, ок?
320 20073
>>20072
Математика необъятна.
Конструктивизм исчерпывается двумя-тремя книжками.
И ты говоришь, что это равновеликие науки?
321 20074
И да, если бы ты понимал в математике, то ты знал бы что метаматематика во многом даже более конструктивна, чем собственно конструктивизм, т.к Гильберт рассматривал возможность доказать непротиворечивость арифметики строго финитными методами. Поэтому противопоставлять бурбаков конструктивистам это вообще пушка. Я уже даже не говорю о том, что суть конструктивизма в применении у основаниям в том, чтобы дропнуть невычислимые суеверия типа исключенного третьего и доказательства, из которых не следует возможности построения доказываемого. И ведь все это сто раз уже писано мной на этой параше, так нет, вылезает один и тот же аутист, или разные, но похожие один в олин, и несут одну и ту же хуйню. Не надоело?
322 20075
>>20074
Особенно тау-символ конструктивен, эквивалентный глобальному выбору.

Просто дай список ъ-конструктивистской литературы. Хотя бы из ста наименований. Или не сможешь?
323 20084
>>20074

>чтобы дропнуть невычислимые суеверия


Ага подорвать пару столбов математики, а потом смотреть как всё здания к хуям разрушается. Конструктивистов как и ИГИЛ надо запретить.
324 20092
>>20084
Ты хотел сказать формалистов, да!?
325 20106
>>20084
Ничего не разрушили кроме пары суеверий, зато построили полностью вычислимые основания. Как оказалось, математика ничего не потеряла, если из нее выкинуть суеверия, такой нежданчик.
326 20108
>>20106
Во-первых, даже устоявшейся терминологии в конструктивизме нет. Во-вторых, на этих якобы "основаниях" никакой дальнейшей конструкции не возведено.

>кроме пары суеверий


Содержание программы Вербицкого - это пара суеверий?
327 20110
>>20108

> Во-первых, даже устоявшейся терминологии в конструктивизме нет. Во-вторых, на этих якобы "основаниях" никакой дальнейшей конструкции не возведено.


Завязывай уже хуйню писать, а.
328 20115
>>20110
Ты называешь всю программу Вербицкого суеверием.
329 20116
>>20115

> Ты называешь всю программу Вербицкого суеверием.


Вербицкий это бородатый такой, писал про АКАБов и цитировал стишок 'из западного ануса все жрете вы говно, за кока колу сраную продались вы давно'?
330 20123
>>20116
Переход на личности не делает тебе чести.
http://imperium.lenin.ru/~verbit/MATH/programma.html
дебилыматематика.jpg60 Кб, 600x433
331 20124
>>20123
Вот смотри, я сто раз давал определение конструктивного объекта. Если после этого я вижу предъявы уровня того, что выше по треду, я не могу не отметить бесполезность своих попыток что-то объяснить. А имея в виду исключительную простоту такого определения, не могу не сделать напрашивающегося вывода об умственных способностях того, кому я пытаюсь что-то объяснить. Тут именно в личности проблема, а не в моем подходе, увы.
332 20128
>>20124
Конструктивизм не оставляет от математики камня на камне. Уничтоженным оказывается всё, что перечислено в программе Вербицкого. А ты только смеешься над этим.
333 20162
>>20106

>зато построили полностью вычислимые основания.


Когда там комплюктеры докажут гипотезу Римана?

>Как оказалось, математика ничего не потеряла


Математика тем и славится, что даже такое сборище аутяг, как конструктивисты имеют право на существование.
334 20169
>>20162

> Когда там комплюктеры докажут гипотезу Римана?


Ты ее без комплюктера докажи, умник. Понапридумывают всякой заведомо бесконечной хуйни, потом удивляются почему эти маняпроблемы столетиями никто решить не может. Очевидно же, что конструктивное решение есть построение, отсюда последнему довну ясно почему эти манягипотезы недоказуемы. Я тебе сходу могу таких выдумать и хуй ты их докажешь даже без конструктивизма. Например, прикол 'купи слона' неразрешим, это тоже теперь математическая проблема тысячелетия? Аутисты блядь кого'то в аутизме обвиняют, вообще пушка. Причем, обвиняют самых здравомыслящих, чья идея как раз в отказе от невычислимых верований.
335 20171
>>20169
Т.е. гипотеза Римана - ненужное суеверие, надо выгнать на мороз?
336 20172
>>20171
Ты читать умеешь? Не нужно выдумывать хуйни, нужно читать на что отвечаешь, раз уж отвечаешь (последнее вообще необязательно). В данном случае, там уже есть ответ.
337 20173
>>20172
Ты прямо ответь. Гипотеза Римана - суеверие?
338 20175
>>20173
Гипотеза - это гипотеза. Суеверия - это актуальная бесконечность, исключенное третье.
339 20176
>>20175
С Риманом всё ясно.
А ты можешь доказать, что всякое бесконечное множество содержит счетное подмножество?
школота3.gif362 Кб, 262x219
340 20178
>>20176

>доказать, что всякое бесконечное


Пиздец, с кем сижу на одном мейлру. В предыдущем моем посте ответ про "всякое бесконечное". Ну вот что таким докажешь? Тебе сколько раз нужно написать, что "конструктивное доказательство это построение", чтобы до тебя наконец это бы дошло? Конструктивное множество - это правило, по которому можно порождать элементы множества, то есть строить их. Если таковых нет, то это не множество, а категория. Я даже могу сказать, что следующим вопросом будет привести примеры таких множеств и таких правил. Будто я это сто раз не делал. Сказка про белого бычка.
341 20181
>>20178
Допустимы ли обороты вроде "пусть M - множество решений уравнения x^7+3x^2+x+1=0"? При условии, что я не знаю формулы для порождения решений.
342 20183
>>20181
Если переменные х заданы в виде контекста, н-р если это лямбда-термы, принадлежащие своему типу, так же заданному в виде контекста, что-нибудь уровня х:А, то да. Такой "оборот" в данном случае был бы спецификацией программы, порождающей решения этого уравнения. Естественно, предварительно должны быть заданы операции "=, ^, +" как лямбда-термы имеющие свой тип, или выражения имеющие соотв. арности, что почти одно и то же.
Снимок.PNG87 Кб, 836x364
343 20184
>>20181
И да, спецификация такой программы / доказательства что одно и то же, согласно изоморфизму Карри-Говарда, может быть задана, если ее решения низвестны, пикрелейтед - спецификация теоремы Ферма. Задать ее можно, решением было бы построение всех примеров, удовлетворяющих данной спецификации. Если в процессе построения нашлось бы решение, не удовлетворяющее такой спецификации, оно было бы конструктивным доказательством ложности теоремы Ферма. Опять же, я сто раз это писал уже.
344 20185
Опять же, поскольку полный перебор всех решений невозможен технически, можно говорить только о потенциальной осуществимости такого доказательства. И это я сто раз уже писал.
345 20194
>>20181

> что я не знаю формулы для порождения решений.



Для конструктива не обязательно нужна формула. Смотри, если многочлен нечётной степени, то у него для некоторого большого K (K > 0) при подстановке K и -K получатся числа разных знаков, а значит бисекцией можно найти корень. Для многочлена чётной степени надо продифференцировать, если все экстремумы лежат где надо, то корней нет. Если нашли один корень, делим на него и повторяем всё это. Вот у тебя и получится множество корней.
346 20204
>>20194
Толсто.
В конструктивизме теорема Больцано-Коши неверна.
347 20245
>>20204
Само ты толсто.
Больцано-Коши неверна для произвольных непрерывных функций, но разные варианты с равномерной непрерывностью или гладкостью верны, а для многочленов-то вообще проблем нет.
348 20248
>>20169

>Ты ее без комплюктера докажи, умник.


Не погоди, твоя же конструктивная математика самая конструктивная и самая настоящая, а все остальные нужно выкинуть на помойку, так?

>Понапридумывают всякой заведомо бесконечной хуйни


Ну-ну, простые числа вполне осязаемы. Впрочем я не удивлюсь, если среднестатистический конструктивист сможет в них что-то понять.

>Очевидно же, что конструктивное решение есть построение


Мне насрать, ты говоришь что конструктивная хуйня лучше дедовского аксиоматического, формалистического картофана с аксиомами выбора и.т.д Так докажи, своим конструктивистким пиздежом, хоть что-нибудь новое, а не дрочи, как последний дрочила. Пока единственное, что я слышу от мамкиных конструктивистов тут, это пиздеж что их математика лучше. Моё мнение таково: пока каждый занимается своим аутизмом, всё в порядке, когда кто-нибудь начинает лезть в залупу, его надо загонять под шконарь.
14961588549890.png320 Кб, 719x403
349 20253
>>20248

> Мне насрать, ты говоришь что конструктивная хуйня лучше дедовского аксиоматического, формалистического картофана с аксиомами выбора и.т.д Так докажи, своим конструктивистким пиздежом, хоть что-нибудь новое, а не дрочи, как последний дрочила. Пока единственное, что я слышу от мамкиных конструктивистов тут, это пиздеж что их математика лучше. Моё мнение таково: пока каждый занимается своим аутизмом, всё в порядке, когда кто-нибудь начинает лезть в залупу, его надо загонять под шконарь.


Таблетки выпей, бесноватый. Дедовское как раз все конструктивное, это потом поналезло умников, затыкать все дыры в математике актуальной бесконечностью, исключенным третьим и прочей невычислимой шляпой. Итог очевиден - кризис оснований. И я уже сто раз говорил, что использовать свое незнание как доказательство чего- то есть признак долбаеба.
350 20254
>>20253
А что плохого в третьем исключённом и актуальной бесконечности?
мимо
351 20255
>>20254
Невычислимые (непостроимые) суеверия.
352 20256
>>20255
Окей. Может глупый вопрос, но делает ли трансцендентность pi это самое pi суеверием? Его же в принципе нельзя вычислить с окончательной точностью до n-го знака.
353 20260
>>20256

> Окей. Может глупый вопрос, но делает ли трансцендентность pi это самое pi суеверием? Его же в принципе нельзя вычислить с окончательной точностью до n-го знака.


Пи это правило построения. Это потенциальная бесконечность. Актуальная бесконечность не соответствует никакому построению либо правилам построения.
354 20262
>>20260
Но ведь потенциальная бесконечность ничем не лучше актуальной.
355 20268
>>20260

>Это потенциальная бесконечность


Ты что дурак что ли блять?

Вот хорошо, сумма ряда 1/2^n равна двум, как известно. По твоему что, этот ряд имеет конец?
356 20286
>>20268
Сумма ряда != ряд, не?
357 20288
>>20253
Ой, да у нас тут аниме, становится интересно.

>Итог очевиден - кризис оснований.


Итак появляются петухи, которые кукарекают, что надо всё до основания разрушить. Где-то я уже это слышал.
SDC116191.jpg1,1 Мб, 2592x1944
358 20313
Давайте так. Вот вам тезис - любая практически осуществимая математика конструктивна, т.е. построима. Без разницы, какими формализмами там пользуются, хотя бы и не имеющими к интуиционизму никакого отношения и опирающиеся на всякие актуальные бесконечности и исключенные третьи. Я пони маю, что для аудитории мейлру это слишком сложно, поэтому конкретный пример, что именно я имею в виду. Вот есть такая тема, как теория статистического обучения Вапника, пытающаяся (и небезуспешно) обосновать саму суть машинного обучения. Меня тут упрекают в том, что я даю скриншоты вместо нормальных ссылок, поэтому вот ссылка http://gen.lib.rus.ec/book/index.php?md5=0BE90A2C820FB75B1C79E385101A5761 Собственно, о чем я:
1) упомянутая теория излагается автором с чисто классических позиций - православный матан, теорвер, все эти интегральчики, предельчики и прочий знакомый любому школьцу картофан. Никакой ереси типа лямбда-исчисления, MLTT и прочего Барендрехта даже не упоминается, хотя очевидно, что функции неплохо было бы рассмотреть с точки зрения самой нормальной теории функций - лямбда калькулюса, тем более что речь конкретно о вычислимых функциях.
2) тем не менее, сама теория про некоторый класс алгоритмов, их обоснование, в общем, о доказательствах некоторых их свойств, полезных с точки зрения машинного обучения. Т.е. про нечто изначально конструктивное и построимое на комплюктере. Опять же, конструктивный подход к вопросу, изоморфизм Карри-Говарда, не упоминается даже вскользь, хотя он именно об этом.
3) из предыдущих пунктов очевидно, что в теории статистического обучения классический подход используется как, скажем, "дискретизация" такового, ограниченная вычислительными возможностями железа и софта, т.е. значение функций, предела функции и т.д. на самом деле ограничены 12 или около того знаками после запятой, а не нарисованным знаком бесконечности, длина примеров в датасете тоже конечна, хотя в формулах попадаются выражение типа стремления длины выборки к бесконечности и т.д.
Отсюда вопрос, конструктивна ли теория статистического обучения? Если с одной стороны там даже не упоминается конструктивизм, а с другой - все теоремы, следствия и доказательства этой теории непосредственно построимы? Хотелось бы услышать манямнения.
SDC116191.jpg1,1 Мб, 2592x1944
358 20313
Давайте так. Вот вам тезис - любая практически осуществимая математика конструктивна, т.е. построима. Без разницы, какими формализмами там пользуются, хотя бы и не имеющими к интуиционизму никакого отношения и опирающиеся на всякие актуальные бесконечности и исключенные третьи. Я пони маю, что для аудитории мейлру это слишком сложно, поэтому конкретный пример, что именно я имею в виду. Вот есть такая тема, как теория статистического обучения Вапника, пытающаяся (и небезуспешно) обосновать саму суть машинного обучения. Меня тут упрекают в том, что я даю скриншоты вместо нормальных ссылок, поэтому вот ссылка http://gen.lib.rus.ec/book/index.php?md5=0BE90A2C820FB75B1C79E385101A5761 Собственно, о чем я:
1) упомянутая теория излагается автором с чисто классических позиций - православный матан, теорвер, все эти интегральчики, предельчики и прочий знакомый любому школьцу картофан. Никакой ереси типа лямбда-исчисления, MLTT и прочего Барендрехта даже не упоминается, хотя очевидно, что функции неплохо было бы рассмотреть с точки зрения самой нормальной теории функций - лямбда калькулюса, тем более что речь конкретно о вычислимых функциях.
2) тем не менее, сама теория про некоторый класс алгоритмов, их обоснование, в общем, о доказательствах некоторых их свойств, полезных с точки зрения машинного обучения. Т.е. про нечто изначально конструктивное и построимое на комплюктере. Опять же, конструктивный подход к вопросу, изоморфизм Карри-Говарда, не упоминается даже вскользь, хотя он именно об этом.
3) из предыдущих пунктов очевидно, что в теории статистического обучения классический подход используется как, скажем, "дискретизация" такового, ограниченная вычислительными возможностями железа и софта, т.е. значение функций, предела функции и т.д. на самом деле ограничены 12 или около того знаками после запятой, а не нарисованным знаком бесконечности, длина примеров в датасете тоже конечна, хотя в формулах попадаются выражение типа стремления длины выборки к бесконечности и т.д.
Отсюда вопрос, конструктивна ли теория статистического обучения? Если с одной стороны там даже не упоминается конструктивизм, а с другой - все теоремы, следствия и доказательства этой теории непосредственно построимы? Хотелось бы услышать манямнения.
359 20316
>>20313
По-моему ответ очевиден: нет. Построенная теория неконструктивна. Но можно построить аналогичную конструктивную теорию, которая, быть может, даже будет лучше. Но никто этим пока не занимался, видимо.
360 20317
Новая тема треда: потенциальная и актуальная конструктивность.
361 20319
>>20316

>Построенная теория неконструктивна. Но можно построить аналогичную конструктивную теорию, которая, быть может, даже будет лучше.


Тогда в чем разница? Если вместо пределов, интегралов и т.д. можно гонять соответствующие этим выражениям лямбда-термы и наоборот, то возникает закономерный вопрос, а зачем всякие актуальные бесконечности, которые все равно ни к одной практической задаче не пришить? Где она, бесконечность, если любая практическая задача, любое осуществимое вычисление все равно имеет дело с чем-то конечным? Ну кроме потенциальной бесконечности типа программ для машины Тьюринга, не приводящих к останову. Еще Брауэр показал, что континуум непостроим, т.к. между двумя соседними вещественными числами всегда можно вкорячить их еще сколько угодно. Но на практике "сколько угодно" всегда ограничивается доступными вычислительными возможностями. Т.е. в конечном счете все равно все имеют дело с конструктивным, т.е. построимым и вычислимым.
362 20320
>>20317
Единственные реальные примеры неконструктивной математики - это парадоксы а единственное реальное достижение неконструктивной математики это кризис оснований. Все, что не сводится к антиномиям и программам для машины Тьюринга, не приводящим к останову, вычислимо и т.о. конструктивно, безотносительно в каких формализмах выражено.
363 20326
>>20319
Сделайте.
Покажите, что это лучше.
Потом воняйте.
364 20356
>>20317

>Еще Брауэр показал, что континуум непостроим, т.к. между двумя соседними вещественными числами всегда можно вкорячить их еще сколько угодно.


А какая разница построим он или нет?
365 20357
>>20356
Построимое - халяль, непостроимое - харам.
366 20359
>>20357
То есть нормальному математику должно быть похуй на эти конструктивистко-муслимские разборки?
367 20361
>>20320>>20357
А теория категорий халяль?
368 20363
>>20356

>А какая разница построим он или нет?


Вот есть всякие кардиналы алеф1 и выше, бет и т.д. Они ничему построимому и вычислимому не соответствуют, это чистая религия а не математика.
>>20359
Нормальный математик во всех случаях пользуется конструктивной математикой, я же даже пример привел >>20313 но как и предполагал, для мейлру это слишком сложно. Ты не приведешь пример практического использования неконструктивной математики кроме парадоксов и прочего кризиса оснований.
>>20361
В MLTT и HoTT ее используют. Дальше сам.
369 20364
>>20363

> HoTT


Это какая-то модная йоба по типу новых оснований?

> Они ничему построимому


Но как-то же их построили или чисто с потолка взяли и решили, ага, вот охуенная штука алеф1, будем в неё веровать.

> и вычислимому не соответствуют


А должны?
гугл.jpg156 Кб, 787x830
370 20365
>>20364

>Но как-то же их построили или чисто с потолка взяли и решили, ага, вот охуенная штука алеф1, будем в неё веровать.


Их никак не построили, они непостроимы. Просто значок, за которым не стоит ничего. Взяли не с потолка, но около того.

>А должны?


Нет, конечно. Только невычислимое это не математика.

>Это какая-то модная йоба по типу новых оснований?


Пикрелейтед.
371 20366
А как бы вот эти все пруверы и доказательства выглядели бы в светлом будущем? Какая цель? Даже школьники будут с ними работать?
372 20367
>>20366

>Даже школьники будут с ними работать?


Они будут работать даже без школьников. Полностью механизированные доказательства.
373 20368
>>20367
Автоматизация математиков?
374 20369
>>20368
Да.
375 20370
>>20363

>Ты не приведешь пример практического использования неконструктивной математики кроме парадоксов и прочего кризиса оснований.


>практического использования


Для копания картохи подойдёт только конструктивизм? Почему меня как математика должна интересовать практическая применимость.
Да и ясно, что у картофенов бомбит с парадоксов, картошку-то банахом-тарским не удвоишь.
376 20371
>>20319

> Тогда в чем разница?


В том, что одно есть, а другого - нет, очевидно же.
377 20374
>>20371>>20370
Чего нет-то, губошлеп? Ты читать пробовал на что отвечаешь?
(Автор этого поста был предупрежден.)
378 20377
>>20374
Картофен, ищи практическое применение на /pr
(Автор этого поста был предупрежден.)
379 20379
>>20377
Если триггернулся на слово "практическое", замени на "вычислимое". Невычислимой математики несуществует, т.к. это уже не математика. Отсюда, все эти актуальные бесконечности и т.д. на самом деле не используются никем, даже если подразумеваются.
380 20409
>>20379

>Невычислимой математики несуществует, т.к. это уже не математика.


>континуум непостроим


Инженеры используют интегральчики с континумом, постоянно разбивая график на бесконечное число прямоугольников. Где твой Бровер теперь?
381 20437
>>20409
Но они же не считают его напрямую в лоб как ты собирался бесконечность считать? ты что, дурак что ли блять?, а пользуются теоремой шницель птуцера и переводят из пустого в порожнее/повышают степень на единицу и делят на эту самую степень.
Или раскладывают в ряд по теореме ноги макаронины с округлением/указанием пределов в которых находится вычисляемая величина.

мимо
382 20440
>>20409
Я чуть выше привел похожий пример с теорией статистического обучения и объяснил для одаренных, что нет там никаких бесконечностей, даже если значки бесконечности и стоят, то подразумевается конечное. Даже если используются интегралы и пределы, по факту все считается до конечного числа знаков после запятой, редко превышающего 12. И где теперь ваша актуальная бесконечность, если ее нет ни в одной задаче?
383 20441
>>20440

>по факту все считается до конечного числа знаков после запятой, редко превышающего 12


А какая разница, как там инженеры считают? Математик может запросто сравнить числа с бесконечными знаками, после запятой.

>даже если значки бесконечности и стоят, то подразумевается конечное.


Тогда почему они так часто говорят о бесконечности, особенно им нравятся бесконечно малые.
384 20442
>>20441

> А какая разница, как там инженеры считают? Математик может запросто сравнить числа с бесконечными знаками, после запятой.


Не может. Практических методов сделать это не существует. Нарисовать значок бесконечности или Аллаха не равно построить эти сущности.

> Тогда почему они так часто говорят о бесконечности, особенно им нравятся бесконечно малые.


Какая разница, о чем они говорят? Важно то, что они делают.
385 20443
>>20442
Конструктивную топологию покажи мне.
386 20444
>>20443
Покажи неконструктивную для начала. Я еще раз говорю, все эти значки бесконечностей просто спецэффекты, работать можно только с вычислимым.
1014426172.jpg50 Кб, 777x1200
387 20445
>>20444
Показываю. Теперь ты.
14961588549890.png320 Кб, 719x403
388 20446
>>20445
Иди куда шел со своими картинками, во всяком случае, мимо этого треда, ты же даже не в состоянии понять, о чем тут вообще говорят, тем более понять аргументы. Сто раз уже сказал, что нет там никаких бесконечностей, их никто не способен считать, потому что они невычислимы. Нахуя ты мне картинку показываешь, ты что, ебнутый? Ты если не способен понять о чем речь, нахуя вообще сюда пишешь?
389 20447
>>20446
Маня, может ты хоть книжку откроешь. Там в самом начале аксиома выбора.
14954667056540.jpg46 Кб, 400x400
390 20448
>>20447
Маня, у Мартин-Лёфа есть конструктивное доказательство аксиомы выбора, в MLTT это не аксиома, в которую надобно веровать, а доказуемая теорема. И я сто раз давал ссылку на это доказательство. Сасай-кудасай.
391 20449
>>20448

>это не аксиома, в которую надобно веровать, а доказуемая теорема


Дай угодаю, только для конечных множест?
392 20450
>>20449
Как будто кто'то может пользоваться бесконечными. Бесконечность невычислима, алё, есть кто дома?
393 20451
>>20450
Большая часть математиков да. Инженеро-прогеры нет в большинстве своём.
394 20454
>>20451
Вера в возможность не равна возможности так же как нарисованный значок бесконечности не равен бесконечности.
14974714398940.jpg20 Кб, 604x340
395 20455
>>20451
Вообще, у меня есть подозрения, что ты, мил человек, селедка. По собственному опыту могу судить, что только бабе похуй на фактическую аргументацию, в угоду своему оценочному суждению. Покажи-ка сиськи пример как по'твоему математики могут вычислить невычислимое.
(Автор этого поста был предупрежден.)
396 20456
>>20455

>фактическую аргументацию


Ты про?

>тебе не понять


>так сказал брауэер


>я уже сто раз говорил


>ваша математика не математика


>100 раз говорил


>кризис оснований, парадоксы



>>20454
Раз мы говорим, по сути, о сущностях, которые находяться в платоновском мире идей, то почему бесконечное количество чего-то не может существовать?
397 20457
>>20456

> Раз мы говорим, по сути, о сущностях, которые находяться в платоновском мире идей, то почему бесконечное количество чего-то не может существовать?


Потому что математика это не вера в платоновский мир идей. Нет никакого мира идей, есть вычислимые построения и всякая вера. Последнее это не математика.
398 20458
>>20456

> Ты про?


Я про конкретные примеры выше, теорию статистического обучения как вариант.
399 20459
>>20457
Твои вычислимые построения такая же вера. У тебя не хватит атомов во вселенной, чтобы эксперементально всё вычислить. Ты даже десятичную запись числа Грэма не напишешь.
400 20460
>>20458
Я не собираюсь читать целую книгу о прикладухе, чтобы доказать что-то анону с двачей.
401 20461
>>20459
Не неси опять хуйни по новой. Никто неюикогда не утверждал фактическую построимость потенциально построимых объектов. Ты этого даже понять не способен, о чем тут вообще говорить.
402 20462
>>20461
Раз мы не можем её фактически построить, то получаем, что верим в существования этого объекта?
403 20463
>>20462

> Раз мы не можем её фактически построить, то получаем, что верим в существования этого объекта?


Я просто уже даже не помню, сколько раз объяснял разницу между фактическим конструктивным объектом, потенциально но не фактически построимым и актуальной бесконечностью. 1005001 ый раз не хочу, ты слишком тупой, алибидерчи.
404 20464
>>20463
Ненене, я понимаю.
Смотри, у нас есть платоновский мир, но ты выделяешь из него только те объекты, для построения которых есть алгоритм. Но платоновскими они не перестают быть, поскольку мы не можем проверить в реальности их существование.
405 20466
>>20464
Я другой анон. Конструктивные математики не привязываются никоим образом к реальному миру и не стараются ограничить себя им. Тебе следует разобраться, что такое ментальные математические конструкции и правила их построения. Я не смогу это сделать, тут нужен тот анон, но он кажется заеб*лся повторять всё это три треда подряд)
howto отвечать как конструктивист 406 20467
— Почему существует только то, что порождается алгоритмом?
— Потому.

— Ты ебанутый?
— На это неоднократно давался ответ.

— Ты можешь доказать формулу Гаусса?
— Твоя вера не нужна.

— Пошёл нахуй, ебанашка.
— Ты не воспринимаешь объективные аргументы.

— Какие?
— Хватит спрашивать одно и то же.

— Ты издеваешься. Ты не можешь писать это всерьёз.
— Я не виноват, что ты такой тупой.
407 20468
>>20467

>13/11/16


До сих пор актуально.
408 20469
>>20466

>Конструктивные математики не привязываются никоим образом к реальному миру и не стараются ограничить себя им.


Я понимаю это и в таком контексте обзывательства кого-то в вере выглядит бессмысленым.
409 20470
410 20478
>>20446

>нет там никаких бесконечностей


Тогда что на пикрелейтед?
411 20804
Не уплываем.
412 20863
Сколько уже доказанных с помощью Coq теорем? Ведется какая-то статистика?
413 20879
>>20863
Ну, можно посмотреть количество проектов на гитхабе, если хочется статистики... Но не уверен, что от этого будет толк. Единого репозитория всей математики, как я понимаю, нет.
414 20889
>>20879
В чем сложность создания такого репозитория?
415 20892
>>20879

>всей математики,


только маленького количества математики, конструктивной.
-пофиксил тебя
416 20894
>>20889
Нужно всех заставить им пользоваться, а Сталина у нас нету?
417 20919
>>20889

> В чем сложность создания такого репозитория?


Некому этим заняться. Потом, 99% использования кока это личные цели, задачи передоказать на нем всю математику никто не ставил и желающих этим заниматься нет. Главная проблема в том, что все это нужно пилить вручную, а это долго, нудно и сложно. Это одна из основных проблем пруверов вообще, в свое время де Браун сотоварищи перевели на язык первого прувера AUTOMATH аж целую книжку Ландау 'Grundlagen', все это есть в инторнетах, можно оценить ебейшую сложность такой задачи лично. Далее, чтобы перевести в кок некую теорию, нужно быть неплохим спецом в вопросах этой теории, ну если это не какое'нибудь исчисление пропозишенов. Как пример можно привести ядро НоТТ на коке, кроме Воеводского с соратниками вряд ли кто осилит такую задачу, см. соотв. пейперы. К счастью, автоматизация подобных задач таки возможна, если вспомнить некоторые идеи т.н. 'сигнифики'. Я сейчас как раз этим пытаюсь заниматься в свободное время, которого у меня нет нихуя. Возможно, скоро покажу конкретные примеры.
418 20925
>>20892

> только маленького количества математики, конструктивной.


> -пофиксил тебя


Не шаришь, так не нес бы хоть хуйни. Простой пример, озвученный в предыдущем посте, верификация Grundlagen Ландау, не имеющей ничего общего с конструктивной математикой с помощью изначально 100% конструктивной типизированной лямбды-Р. Как бы ты для себя объяснил возможность этого? Хотя о чем я спрашиваю анэнцефала из рашки.
419 20931
Почему существует только то, что порождается алгоритмом?
420 20933
>>20931
Вы тут настолько убоги, что не способны даже элементарные вещи изложить своими словами. Сам'то читал что пишешь?
421 20934
Это не считая того, что сто раз уже объяснялось, почему существование в математике сводится к построимости. Сто первый раз объяснить? А смысл, если это все равно не даст ничего?
422 20936
>>20934

>почему существование в математике сводится к построимости


Существует объединение любого множества.
14981397797110.jpg79 Кб, 620x350
423 20945
>>20936

> Существует объединение любого множества.


С этой стороны тоже бесполезно, придумай что'нибудь еще. Хотя бы потому, что твоя формулировка вызывает как минимум два вопроса, 'что значит 'существует'' и 'что значит 'любого''. Если существование сводить к платоновским верованиям в мировую душу и мир идей, то это чистая религия. Если к нарисованному значку на бамаге, то опять же, я и символ Аллаха могу нарисовать. И так далее. Все это уже обсуждалось и не интересно.
424 20950
>>20945

>я и символ Аллаха могу нарисовать


Ну нарисуй. Никто тебя за язык не тянул. Определение Аллаха на языке логики первого порядка в студию.
425 20951
>>20950

> . Определение Аллаха на языке логики первого порядка в студию.


Сорта на самом деле. И там и там невычислимые актуальные бесконечности, за которые предлагается верить, что это основа всего.
426 20952
>>20951
Ты уже который раз упоминаешь Аллаха.
Ну так давай, сделай это. Определи его.
427 20953
>>20952
Этот пример я привожу как раз по причине его невычислимости. Ты же ссылаешься на логику первого порядка, хотя в ней верен невычислимый общий случай исключённого третьего. Одно невычислимое ничем не лучше другого столь же невычислимого. Завязывай со своей демагогией, ты прекрасно понимаешь это. Понимаешь, что так или иначе невозможно обойти вопрос 'что есть существование в математике?'. Все это неоднократно обсуждалось, я стопервый раз все это пишу просто потому что мне на работке еще до утра сычевать и надо чем'то убить время.
428 20954
>>20953
Я могу предложить первопорядковую теорию множеств. Ты не можешь предложить первопорядковую теорию Аллаха. Поэтому я могу говорить про множества, а ты не можешь говорить про Аллаха.

Перестань упоминать Аллаха, это тупо и очень бесит. Или определяй его.
429 20956
>>20954

> Я могу предложить первопорядковую теорию множеств


Опирающуюся на невычислимые верования типа актуальной бесконечности и исключенного третьего.
430 20957
>>20956
Ты говоришь, что можешь формализовать Аллаха.
Сделай это.
14958989594291.png610 Кб, 700x525
431 20958
>>20957

> Ты говоришь, что можешь формализовать Аллаха.


Где я это говорил? Не разводи демагогию, я такого не говорил вообще никогда, ты уясни другое, логикой первого порядка ты можешь пользоваться лишь постольку, поскольку позволяет изоморфизм Карри-Говарда. Вне этих рамок ты ничего не докажешь этой логикой, т.к доказательства твои за пределами вышеупомянутого изоморфизма будут ничем не лучше корана.
432 20959
>>20958
Я указываю тебе на разницу между первопорядковыми теориями и кораном. Ты не можешь формализовать Аллаха первопорядковой теорией, в принципе. И ты об этом осведомлен. Поскольку ты продолжаешь использовать фразы "символ Аллаха могу нарисовать" и "не лучше корана", остаётся только один вывод. Ты осознанно лжёшь.
433 20960
>>20959

> Я указываю тебе на разницу между первопорядковыми теориями и кораном.


Вне изоморфизма Карри-Говарда их нет.
434 20961
>>20960
Хорошо. Предъяви аксиоматическую теорию аллаха.
435 20963
>>20961

> Хорошо. Предъяви аксиоматическую теорию аллаха.


Ты читать умеешь?
436 20970
>>20919
Жду примеров: ты заинтриговал.
437 20971
>>20963
Ты говоришь, что разницы нет. Тогда почему ты не можешь написать теорию Аллаха?
438 20973
>>20971

> Ты говоришь, что разницы нет. Тогда почему ты не можешь написать теорию Аллаха?


Выше отвечал уже.
439 20974
>>20973
На вопрос "почему ты не можешь дать первопорядковую теорию Аллаха" ты не отвечал.
440 20975
>>20974
Отвечал. Я ж говорю, ты даже читать не умеешь, какая тебе математика. Ладно читать, даже потралить не в состоянии. Ты либо реально селедка, либо аутист со стажем на бордах максимум месяца два.
(Автор этого поста был предупрежден.)
441 20976
>>20975
Ну так процитируй свой ответ.
442 21177
Как быть с теорией Рамсея в конструктивной математике?
443 21183
>>21177
Очень просто. Эта и ей подобные теории формулируются в виде спецификаций (я давал пример спецификации теоремы Ферма), затем находится решение, удовлетворяющее такой спецификации, если множество таких решений не пусто, это конструктивно доказывает исходную теорему. Конструктивное доказательство это построение, все просто же.
444 21243
Поясните за этот мегасрач вообще. В чем суть конструктивной математики и почему так важно принять какие-то специальные логики для преодоления трудностей в основаниях математики? В чем ваши проблемы вообще?
445 21244
>>21243
Конструктивисты говорят, что вся математика - манявыдумки. У математиков от этого бугурт.
446 21246
>>21244
Зачем несешь хуйню? Полтора невычислимых верования - исключенное третье как общий принцип и актуальная бесконечность, это полтора верования, а не 'вся математика'.
447 21247
>>21243

> В чем суть конструктивной математики


В вычислимости. Источник кризиса оснований - невычислимые догмы, которые неясно зачем вообще в математику притащили.
448 21248
>>21246
На этом построена вся математика, начиная с анализа.
449 21249
>>21247

> Источник кризиса оснований - невычислимые догмы



Я думал, что источник кризиса – злоупотребление формализмом.

> которые неясно зачем вообще в математику притащили



Творческое удобство? Эвристический метод?
450 21252
>>21243
Весь кризис в головах.
Пока одни говорят что это все эзотеризм, вторые что это норма, третьи считают ящики и двигают науку вперед.
Короче, все как всегда. Полтора дебила друг друга говном поливают пока все остальные покуривают трубки и обсуждают дальнейший ход событий, посмеиваясь над клоунами в говне.
инб4 НА ПАЛЬЦАХ НИПАСЩЕТАТЬ!!! КАНТИНУМ НЕ КАНТИНУМ!!! АКСЕОМА ВИБОРА ЕТА АБМАН!!!
451 21253
>>21249

> Я думал, что источник кризиса – злоупотребление формализмом.


Злоупотребление невычислимыми сущностями тогда уж. Тут никто не понимает простейших вещей, даже не знаю как это можно объяснить еще проще, и так элементарные вещи обсуждаем. Похоже, по новой та же сказка про белого бычка намечается.
452 21254
>>21253
Расскажи, как ты пришёл к конструктивизму. Кто тебя ему научил?
453 21255
>>21253

>> Источник кризиса оснований - невычислимые догмы


Вычислимость такая же догма.
14944924623790.gif72 Кб, 942x942
454 21257
>>21255

> Вычислимость такая же догма.


Да нет, вычислимость это не догма, это фактический результат. Ты даже и этого не понимаешь, пиздец же настоящий.
>>21254

> Расскажи, как ты пришёл к конструктивизму. Кто тебя ему научил?


Конструктивизм is fine too, конечно же, особенно MLTT великая вещь, но мне наиболее интересен интуиционизм Брауэра в его первоначальном чистом варианте. Брауэру пришлось от него отказаться по причинам им же и озвученным, а вот я нашел, как можно обойти эти причины, как минимум частично. К слову, конструктивизм не формализует интуиционизма, но аргументы того же Гейтинга на этот счет даже некоторые авторы работ на эту тему не пони мают, чего говорить о мейлру. Как пришел, очевидно же, в книжках прочитал.
455 21258
>>21257

>а вот я нашел, как можно обойти эти причины, как минимум частично.


И как же, аниме?
456 21260
>>21257

> Да нет, вычислимость это не догма, это фактический результат.



Пруфов, конечно, не будет.

> Брауэра



Лженаука.
457 21261
>>21260

> Пруфов, конечно, не будет.


Изоморфизм Карри-Говарда пруф кококо лжинаука)))

> Лженаука.


Ну раз на мейлру так пишут, то ладно.
458 21263
>>21257
Кстати, в вашем петушином углу как решается вопрос: сколько всего простых чисел?
459 21264
Не, я могу понять, когда до кого'то не доходит мочидзукина теория пространств Тейхмюллера. Но конструктивизм, там же просто все как 3 копейки, каким нужно быть деревянным по пояс, чтобы не осилить изоморфизм Карри-Говарда. Пруф конструктивного объекта жто сам конструктивный объект, даже термин 'пруф-объект' есть. Ну что сложного в ВНК интерпретации, да таблица умножения сложнее в разы. Пиздец с кем сижу на одном мейлру, даже бабки с семками у падика это гении математики по сравнению с некоторыми тута. Нахуй так жить?
460 21265
>>21261

>вычислимость это не догма, это фактический результат


>Изоморфизм Карри-Говарда пруф



Здесь нет логической связи. Из утверждения о существовании изоморфизма Карри-Говарда не вытекает логически, что вычислимость это не догма. С тем же успехом можно было бы говорить "теория струн ошибочна", а в ответ на резонные вопросы заявлять "диагональный метод Кантора пруф" и дальше молчать.
461 21269
>>21263

>сколько всего простых чисел?


Конечное число.
-Мимо Брауэр
462 21270
>>21265

> Здесь нет логической связи.


Я понял тебя, услышал. Уровень твоих знаний в данной теме мне ясен. Мне неясно другое, зачем ты мне пишешь и что пытаешься доказать? Что конструктивизм тебе непонятен, а его основные моменты и их взаимосвязи тебе ни о чем не говорят? Ок, ладно.
463 21271
>>21269

>Конечное число.


Перемножаем все известные простые числа
@
добавляем к результату единицу
@
маняматик с двоща обсасывает километры хуйцов
464 21275
>>21271
Но так можно сделать только конечно число раз, поскольку актуально бесконечности не существует, то количество простыз чисел конечно.
465 21276
>>21275
Ну я же говорю, о чем можно спорить с тем, кто не отличает актуальной бесконечности от абстракции потенциальной осуществимости. Школуйня, блядь.
466 21280
>>21275

>то количество простыз чисел конечно.


Ну тогда тебе не составит труда перечислить их прямо в этом итт тренде.
467 21285
>>21275

>так можно сделать только конечно число раз


Бесконечно число раз религия запрещает?
468 21286
>>21276

>Ну я же говорю, о чем можно спорить с тем, кто не отличает актуальной бесконечности от абстракции потенциальной осуществимости.


У нас нет компьютера для того, что все простые числа запрограммировать.

>>21280
Нет, я не умею программировать. Тут кок запускать придёться.

>>21285
Бесконечность и есть религия.
469 21288
>>21286

>Бесконечность и есть религия.


Мартин-Леф такого не писал.
470 21289
>>21288
Значит, он был веруном.
471 21314
>>21286
Бесконечность может быть вида доделаю, а может быть вида "не знаю как падступицца".
472 21315
>>21314
Анон с мейлру даже Кнута Исскуство Программирования не читал. О чем с вами говорить? Сколько раз про слова Брауэра говорю, может мне ещё количество Аллахов в треде подсчитать.
473 21316
>>21314

>Бесконечность может быть вида доделаю,


Бесконечности не существует, это вера сектантов. Можно и Аллаха доделовать бесконечно.
474 21320
>>21286

>Нет, я не умею программировать. Тут кок запускать придёться.


Не, ну давай пруф на то что простых чисел конечное число или всё таки не конечное?
475 21321
>>21316

>Бесконечности не существует, это вера сектантов.


>Чисел не существует, это вера сектантов.

476 21322
>>21320
Если нет правил построения актуальной бесконечности, то чисел конечное количество.
477 21323
>>21321
Только натуральные числа существуют, остальные игрушка дьявола и вера с непостроимыми сущностями.
lejb.jpg31 Кб, 489x471
478 21324
Математика - это вычислимость. В математике нет ничего, что не сводится к вычислимости. Полтора невычислимых верования типа исключенного третьего и актуальной бесконечности - это не математика, т.к. при попытке их использования в основаниях имеем кризис этих оснований. Все просто же, и все кукурекующие выше по факту не приведут ни одного примера, опровергающего мной только что написанное. Можно писать всякую хуйню, можно пользоваться своей тупостью как доказательством (в своем манямире, ес-но), но по факту вам возразить нечего - невычислимой математики просто не существует, в любой математике ровно столько математики, сколько в ней вычислимости.
479 21326
>>21324

>Математика - это вычислимость.


Причем, вычислимость на компьютере! Только ультрафинитизм, только хардкор!
480 21329
АЛГОРИТМ ПОСТРОЕНИЯ АЛЛАХА.
Аллах - тот, кто создал вселенную.
Так как, количество атомов во вселенной конечно и бесконечности не существует, то мы можем их все просмотреть.
Рано или поздно мы найдёт атомы Аллаха. Можно даже использовать аксиому выбора для конечных множеств. Из множества атомов нашей вселенной выбираем атомы Аллаха. Содираем атомы Аллах готов.
481 21330
>>21326
Вычислимость - это просто вычислимость, неважно на чем, на компьютере, на бумаге, в уме. Все равно вся она сводится к машине Тьюринга и любому другому уточнению понятия алгоритма.

>ультрафинитизм


Все равно практически ты дальше ультрафинитизма не уйдешь. Разве что до абстракции потенциальной осуществимости.
482 21331
>>21330
Верунство в чистом виде. Если объект нельзя осмотреть в реальности, то его не существует.
483 21334
>>21322

>то чисел конечное количество


перечисли их
484 21335
>>21323

>Только натуральные числа существуют


Единица также не существует, как и всё остальное.
485 21336
>>21331
Существование и его отличие от абстракции потенциальной осуществимости уже обсуждали, не вижу смысла пояснять 101й раз.
486 21337
487 21342
>>21337
Боевая паста это серьезный аргумент, да. И конечно же, по-существу опровергает факт того, что все и правда сто раз уже обсуждалось. Я одного не пойму - ну не осилил ты что-то, так осиль или забудь, бывают вещи, которые понять невозможно, видимо для тебя планка чуть выше плинтуса. Но ты не расстраивайся, ты не один такой. Вот автор этой книжки http://gen.lib.rus.ec/book/index.php?md5=C98BD518044E72E05E4A9FA7FBF55312 тоже неосилил понятие ментальной конструкции по Брауэру. Хотя даже книжки пишет, а не батрушку на мейлру.
488 21343
>>21335
Нет, единица это одна палочка |
489 21344
>>21336
Абстрактная осуществивость верунство.
9bc6d490b1163c2e46e7bb955716dd8e.jpg123 Кб, 1100x733
490 21345
>>21343
Абстракция палочки же. Один дилдак, одна бутыль, один N-петух, это разные вещи, но суть одна - во всех случаях это единица.
491 21346
>>21345
Но их может быть только конечное количество. Ты не сможешь нарисовать бесконечное количество палочек и продолжать это делать бесконечно.
492 21347
>>21344
Абстракция потенциальной осуществимости - это абстракция потенциальной осуществимости, а не верунство.
493 21348
>>21347
Нет, это и есть верунство. Вспомни про чернильную дыру.
494 21349
>>21346

>Ты не сможешь нарисовать бесконечное количество палочек и продолжать это делать бесконечно.


Именно поэтому это абстракция. Когда есть правила построения, но сам объект непостроим из-за своей бесконечности. Я это не писал уже не помню сколько раз? Писал. Так что непонятного? Давай, опять сошлись на свою боевую пасту.
495 21350
>>21349

>Когда есть правила построения, но сам объект непостроим из-за своей бесконечности.


Тогда существуют правила но не сам объект. Иначе пришлось бы признать существование Аллаха >>21329
496 21352
>>21350

>Тогда существуют правила но не сам объект.


Походу, начинает доходить. Да, существуют правила, но не объект. Я это не первый год уже пишу. Но возьмем неконструктивную математику. Вжух, и там "существует" уже и алеф0, и алеф100500, и бесконечность. А почему? потому что существование в неконструктивной математике - это непротиворечивость вывода из 10 заповедей аксиом исчисления предикатов. И никто ведь чернильными дырами не кидается. Только конструктивизм это плохо)))
497 21353
>>21352
И к проблемам это не приводит.
498 21354
>>21353

>И к проблемам это не приводит.


Нет, конечно. Подумаешь, программа Гильберта проебалась, да кризис оснований уже второй век как.
499 21355
>>21352

>Да, существуют правила, но не объект.


Тогда Аллах существует в конструктивной математике?
500 21356
>>21355
Опять пиши свою боевую пасту, т.к. сто раз обсуждалось, почему Аллах не существует в конструктивной математике - у тебя нет даже правил его построения. Но ты слишком гений, чтобы читать что тебе пишут, чюкча ж не читатель, а писатель? Три треда в бамплимите, и так кроме меня ни до кого ничего и не дошло. Но я это и до вас знал.
501 21357
>>21354
Алё, вы из какого века? Кризис оснований закончился, когда теория множеств была аксиоматизирована.
502 21362
Тред закрытОбновить закрытый тред
Двач.hk не отвечает.
Вы видите копию треда, сохраненную 12 июня в 13:34.

Скачать тред: только с превью, с превью и прикрепленными файлами.
Второй вариант может долго скачиваться. Файлы будут только в живых или недавно утонувших тредах. Подробнее

Если вам полезен архив М.Двача, пожертвуйте на оплату сервера.
« /math/В начало тредаВеб-версияНастройки
/a//b//mu//s//vg/Все доски