Математика

Тред закрыт.

Check this out!
Оснований математики тред 2 Аноним 22/11/16 Втр 21:34:00 36941
npetuh.jpg 60Кб, 790x593
790x593
Аноним 22/11/16 Втр 21:40:09 36962
Решил научиться доказывать теоремы с помощью и Coq и первое же доказательство не понял. Читаю вот этот туториал https://coq.inria.fr/tutorial-nahas
>The state after the second "intros" command, looks like:
> A : Prop
> proof_of_A : A
> ============================
> A
> Now, we can talk about "Prop". "proof_of_A" is a proof. It has type "A", which means that "A" is something that could have a proof. In logic, that is called a "proposition". Since the proposition "A" has type "Prop", "Prop" must be the type of propositions.
Поясните, как у утверждения может быть тип? В чем смысл?
Аноним 22/11/16 Втр 22:27:19 37013
>>3696
Там же дальше об этом говорится!
Аноним 22/11/16 Втр 22:34:12 37034
>>3701
Можно конкретное предложение?
Аноним 22/11/16 Втр 22:45:57 37055
>>3703
Ну, прямо следующий абзац же об этом... Или я твоего вопроса не понял? Если бы у пропозишнов не было типа, ты бы не смог доказывать никакие утверждения о пропозишнах. Он там и дает примеры: можно сказать "для всех натуральных чисел, если число меньше пяти, то меньше и шести", а можно сказать "для всех пропозишнов, если у нас есть пропозишн, то он у нас есть".
Аноним 22/11/16 Втр 22:57:54 37066
>>3705
> Или я твоего вопроса не понял?
Да. Мой вопрос: что такое тип?
Аноним 22/11/16 Втр 23:08:56 37077
Аноним 23/11/16 Срд 08:55:49 37338
lean.png 4Кб, 240x240
240x240
>>3696
Кук не нужон, зашквар же. Есть няшный LEAN http://leanprover.github.io/ в том числе с браузерным вариантом https://leanprover.github.io/tutorial/?live и учебником https://leanprover.github.io/tutorial/ онлайн и в пдф. Помимо прочего, это первый прувер с ядром на HoTT - гомотопической теории типов, но основное ядро CiC, как и у Кука.
>Поясните, как у утверждения может быть тип? В чем смысл?
Изоморфизм Карри-Говарда жи есть. Пропозишены/формулы как типы/множества. Я в прошлом треде сколько годноты на эту тему спалил быдлу, а все зря. Например, http://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf со 2 по 7 страницы
Аноним 23/11/16 Срд 09:09:04 37349
зт.png 225Кб, 1425x740
1425x740
>>3706
>что такое тип?
Тип - это конструктивный объект, который есть элемент самого себя. Да, в общем случае это приводит к парадоксу Жирара (по-сути, все тот жи парадокс Рассела), что было показано для первого варианта MLTT, поэтому сейчас там все немного хитрее - иерархия вложенных универсумов - U. Подробности опять же в вышеупомянутой книге, либо в учебнике по LEAN. Если не интересны философические объяснения - считай тип множеством, элементы которого определены заданными правилами.
Аноним 23/11/16 Срд 12:00:45 373910
т1.PNG 58Кб, 728x412
728x412
т3.PNG 52Кб, 630x342
630x342
Да, есть еще важный момент. Даже в классической логике логические операции можно рассматривать как операции над множествами. "или" соответствует операции объединения множеств, "и" - пересечение, импликация - подмножество и т.д., пик2. Эта хуйня просто расширяется дальше - пик1, плюс используется интерпретация логических констант по Брауэру-Гейтингу-Колмогорову. В итоге получается логическая система, полная и выводимая по Геделю, поскольку опирается не на синтетическое суждение, оторванное от конструктивного построения, а на аналитическое. Подробнее, на пальцах и с примерами тута http://archive-pml.github.io/martin-lof/pdfs/Martin-Lof-Analytic-and-Synthetic-Judgements-in-Type-Theory.pdf
Аноним 23/11/16 Срд 14:26:15 374211
>>3733
У тебя мания величия походу, бро.
Аноним 23/11/16 Срд 14:45:35 374412
>>3739
> полная и выводимая по Геделю
Что очевидно, ведь теорема Гёделя распространяется только на те системы, где можно построить PRA.
Аноним 24/11/16 Чтв 02:23:13 377713
Аноним 24/11/16 Чтв 14:06:03 379814
>>3739
>В итоге получается логическая система, полная и выводимая по Геделю
Ну сколько можно распространять дезинформацию?
>полная
Она не полна т.к. к ней вполне применимы теоремы Гёделя о неполноте, в частности, она не может ни доказать, ни опровергнуть утверждение о своей собственной непротиворечивости. Напомню, что полнота означает, что всякое предложений либо доказуемо, либо опровержимо. Если теория обладает таким свойством только для специального класса предложений, а не для всех предложений своего языка, то называть это полнотой некорректно.
>выводимая по Геделю
Не то, чтобы я прочел все работы Геделя, но я видел этот термин тоько у тебя, почти уверен, что ввел его вовсе не Гедель - ссылку на Геделя в студию, если придерживаешься другой точки зрения.

>>3744
>Что очевидно, ведь теорема Гёделя распространяется только на те системы, где можно построить PRA.
На самом деле теоремы Геделя о неполноте распространяются и на более слабые системы (1-ую так и вовсе можно доказать в арифметике Робинсона). Кроме того, эквациональная версия PRA (для которой тоже имеют место обе теоремы о неполноте) погружается в интуиционистскую теорию типов.
Аноним 25/11/16 Птн 09:02:23 382515
>>3798
>в частности, она не может ни доказать, ни опровергнуть утверждение о своей собственной непротиворечивости.
Для этого есть проверка типов, ведь по изоморфизму Карри-Говарда все утверждения в конструктивной логике соответствуют своим типам. Т.е. такая система как MLTT сама по себе конструктивный объект.
>Не то, чтобы я прочел все работы Геделя, но я видел этот термин тоько у тебя, почти уверен, что ввел его вовсе не Гедель - ссылку на Геделя в студию, если придерживаешься другой точки зрения.
Естественно, ты видел этот термин только у меня, ты ведь упорно игнорируешь его источник - статьи Мартин-Лёфа, где все это не только описано, но и разжевано на элементарных примерах. http://archive-pml.github.io/martin-lof/pdfs/Martin-Lof-Analytic-and-Synthetic-Judgements-in-Type-Theory.pdf и http://archive-pml.github.io/martin-lof/pdfs/Meanings-of-the-Logical-Constants-1983.pdf
>Напомню, что полнота означает, что всякое предложений либо доказуемо, либо опровержимо.
Спасибо, я знаю что такое полнота. Интерпретация логических констант по Брауэру-Гейтингу-Колмогорову полна именно в этом смысле, поскольку любое суждение в ней либо построимо, либо абсурдно и т.о. соответствует пустому множеству своих пруфов (типу по изоморфизму Карри-Говарда).
Аноним 25/11/16 Птн 09:07:09 382616
Снимок.PNG 101Кб, 499x734
499x734
Да, MLTT не только сама по себе конструктивный объект, но исходя из интерпретации логических констант по Колмогорову, по-сути, готовая спецификация для языка программирования http://www.cse.chalmers.se/research/group/logic/book/book.pdf
Аноним 30/11/16 Срд 08:38:19 426517
1.gif 8Кб, 950x128
950x128
>>3694 (OP)
Шарящий в мат.логике анон, ответь.
Может ли теоретически получиться так, что ZFC непротиворечива, однако омега-противоречива, и если так, то возможно ли было бы эту омега-противоречивость некими метаматематическими методами (вроде тех, что использовал Гёдель) доказать?
Аноним 30/11/16 Срд 10:13:18 426918
>>4265
Если кратко, то может. Будучи точным, вопрос о том, что значит "может ли теоретически получиться" довольно тонкий.

Например, используя вторую теорему Гёделя о неполноте можно показать, что если непротиворечива ZFC + omega-Con(ZFC), то непротиворечива и теория ZFC + Con(ZFC+Сon(ZFC)) + not omega-Con(ZFC).

Доказать это можно довольно просто. Покажем, что ZFC + omega-Con(ZFC) доказывает Con(ZFC+Сon(ZFC)). Рассуждаем в ZFC + omega-Con(ZFC). Очевидно, из omega-Con(ZFC) следует Con(ZFC). Но так как Con(ZFC) арифметическое предложение, то omega-Con(ZFC) влечет искомое Con(ZFC+Сon(ZFC)). Также отметим, что рассуждая аналогично дальше мы получим Con(ZFC+Сon(ZFC+Сon(ZFC))).

Отсюда из непротиворечивости ZFC + omega-Con(ZFC) следует непротиворечивость ZFC + Con(ZFC+Сon(ZFC)). В силу второй теоремы Гёделя о неполноте, ZFC + Con(ZFC+Сon(ZFC)) не доказывает Con(ZFC+Con(ZFC+Сon(ZFC))) и тем самым непротиворечива теория ZFC + Con(ZFC+Сon(ZFC))+ not Con(ZFC+Con(ZFC+Сon(ZFC))). В силу того, что мы уже видели, что в ZFC предложение omega-Con(ZFC) влечет Con(ZFC+Con(ZFC+Сon(ZFC))), мы заключаем, что ZFC + Con(ZFC+Сon(ZFC))+ not Con(ZFC+Con(ZFC+Сon(ZFC))) доказывает not omega-Con(ZFC). Таким образом, непротиворечива теория ZFC + Con(ZFC+Сon(ZFC)) + not omega-Con(ZFC).
Аноним 30/11/16 Срд 11:51:50 427119
>>4269
Спасибо, анон!
Отсюда даже виден дальнейший ход того, как можно было бы доказать omega-Con(ZFC) - доказав неким образом верность арифметического выражения, эквивалентного not Con(ZFC+Con(ZFC+Сon(ZFC)))
Аноним 30/11/16 Срд 11:52:40 427220
>>4271
fix: доказать not omega-Con(ZFC)
Аноним 30/11/16 Срд 23:52:45 430321
>>4271
Я на самом деле переусложнил. Для ответа на твой вопрос нужно было лишь доказать непротиворечивость ZFC + Сon(ZFC) + not omega-Con(ZFC). Что требовало немного меньше усилий.
Аноним 03/12/16 Суб 15:25:14 454622
Анон, помоги доказать, что все тавтологии логики высказываний с modus ponens и двумя связками (-, V) может быть выведены из одной схемы аксиом:

-(-(-A V B) V (C V (D V E))V(-(-D V A) V (C V (E V A))

Понимаю, что достаточно было бы вывести из этой схемы три стандартные схемы логики высказываний, из которых уже доказуемо всё остальное, но вообще не представляю как это делать.
Статью, в которой это доказывается, найти не могу:
Meredith Carew A.. Single axioms for the systems (C, N), (C, O) and (A, N) of the two-valued propositional calculus. The journal of computing systems, vol. 1 no. 3 (1953), pp. 155–164.
Аноним 21/12/16 Срд 09:00:28 592923
73bb4bc1ea23e5b[...].png 271Кб, 1097x1221
1097x1221
Бамп божественным Вавиловым.
Аноним 21/12/16 Срд 09:13:33 593124
>>5929
Да никакой он не божественный. Мало того, что конструктивистов с кое-кем другим перепутал, так еще и ночью у него там кто-то символы дорисовывает. Теорем-пруверы, оказывается, опираются на тысячи неявных предположений - вот оно как! Просто черная магия и сильный ИИ какие-то.
Аноним 21/12/16 Срд 09:42:20 593225
>>5931
> Теорем-пруверы, оказывается, опираются на тысячи неявных предположений - вот оно как!
Вавилов тенденциозен, но собственно критика того, что конструктивность так называемой конструктивной математики довольно условна и опирается на то, что допускаются явно физически нереализуемые вычисления остается. В чем, в конце-концов, утверждение об обрывании последовательностей Гудстейна конструктивнее, чем утверждение о возможности удвоить шар путем перемещения конечного числа частей, учитывая, что ни одно из них не является физически реализуемым.
Аноним 21/12/16 Срд 12:22:23 594026
>>5931
>>5929
Да нормальный парень он, просто платонист. Так бывает, к сожалению. Но в остальном вкусы у него хорошие, литературу интересную цитирует. Можно же фильтровать информацию, правда? Пенроуз вон тоже отбитый платонист, но в остальном, исключая этот пункт, мне нравится его читать.
Аноним 21/12/16 Срд 14:08:25 594127
>>5940
>Да нормальный парень он, просто платонист.
Проблема не в том, что он платонист, а в том, что его заносит и он выдает мало адекватную аргументацию против несимпатичных ему позиций. Например теже "тысячи неявных аксиом" нужные конструктивной математике или что теорема Гёделя о неполноте говорит о "генерации некоторого специального вида текстов" (и ничего не говорит о математике).
Но, впрочем, пишет увлекательно (хотя, отчасти, это следствие того, что он выдвигает совершенно скандальные тезисы).
Аноним 21/12/16 Срд 14:54:22 594428
>>5941
Каждый математик в душе хотябы чуточку платонист. Даже ℕ-петух
Аноним 21/12/16 Срд 15:14:02 594629
>>5944
Да, видимо так, просто потому что сомнения в реальности математических объектов однозначно являются большой помехой, когда реально занимаешься доказательством теорем.
Хотя, разумеется, это касается только собственно математиков. Философы математики, не являющиеся, а тем более никогда не являвшиеся действующими математиками вполне могут не быть платонистами ни в какой степени.
Аноним 22/12/16 Чтв 14:40:51 602030
martinlof2.jpg 54Кб, 453x679
453x679
>>5929
>пик
Какой же этот клоун неосилятор, господи. Он бы хоть попытался разобраться в том, что критикует. Вместо того, чтобы мазать калом математиков, до которых ему как до Луны пешком и всё лесом. Впрочем, наверное, я слишком многого хочу от рашкованского быдлана. Сто раз уже было сказано об абстракции потенциальной осуществимости, общей для всей математики, но нет. Дебилы будут кукарекать про чернильные дыры. Дебил, он на то и дебил, чтобы не понимать очевидного. В частности, что число 10^10^10^...^10 относится к натуральным исходя из конструктивно определенных правил построения N. В частности, у этого числа есть предваряющее его 10^10^10^...^10-1 и следущее за ним 10^10^10^...^10+1 Т.о., хотя данное число физически и непостроимо, о его свойствах (принадлежности к N) мы можем судить из вышесказанного. И еще раз - абстракция потенциальной осуществимости, она общая для всей математики, какого хуя за нее предъявляют только конструктивизму? Если об этом еще Евклид писал? Вот этой своей обличающей писаниной этот ваш вавилов вообще что и кому доказал? Практическое применение у нее какое? С MLTT все ясно, при интерпретации логических констант по Колмогорову это по факту готовая спецификация для языка программирования с зависимыми типами, который может служить для доказательства теорем на компьютере. При интерпретации этих же логических констант по Брауэру-Гейтингу MLTT может служить конструктивными основаниями математики. А вот эта ваша вавиловщина, какие у нее задачи? Парашу тралить?
>>5932
>критика того, что конструктивность так называемой конструктивной математики довольно условна и опирается на то, что допускаются явно физически нереализуемые вычисления остается.
Он просто про MLTT не слышал, если слышал, то не читал, если читал, то не понял, если понял, то не так.
Аноним 22/12/16 Чтв 20:33:10 606731
Составьте, пожалуйста, список значимых работ по философии математики. Типа "Структуры" Куна, работ Поппера и Фейерабенда относительно философии науки. А также посоветуйте какое-то годное введение в мат. философию, можно на английском
Аноним 22/12/16 Чтв 20:54:32 606832
Аноним 23/12/16 Птн 07:09:21 610033
sosnoole.png 224Кб, 690x622
690x622
Аноним 23/12/16 Птн 08:38:03 610834
>>6067
>типа Куна и Фейерабенда
Harold Edwards
Gian-Carlo Rota
>>6068
Хуйня.
Аноним 23/12/16 Птн 09:57:08 611735
Снимок.PNG 163Кб, 972x232
972x232
инт3.png 488Кб, 1194x1269
1194x1269
инт4.png 579Кб, 1276x1257
1276x1257
>>6100
Ой, какая милота эта ваша грязноштанная математика. "Яскозал, что это буржуазная теория и вы так делайте". На самом же деле, а не в калмунистических манямирах, есть нейрофизиологические данные, доказывающие сводимость натурального числа к восприятию времени, о чем писал еще Брауэр. Т.н. модель ATOM Уолша. Ну, цитата Кронекера про бога хуета, конечно.
Аноним 23/12/16 Птн 10:07:03 612136
>>6117
>о чем писал еще Брауэр.
Ох и давно я этого не слышал.
>есть нейрофизиологические данные, доказывающие сводимость натурального числа к восприятию времени
Пруф?
Аноним 23/12/16 Птн 10:37:44 612737
23/12/16 Птн 21:35:44 617538
Аноним 24/12/16 Суб 10:28:28 620639
>>6175
Нейровизуализация - объективные данные, они не могут быть хуйней, они либо что-то показывают, либо нет. По этой теории, на которую ты ссылаешься, я тоже пояснял уже. Там авторы сами себе противоречат, результаты нейровизуализации у них показывают связь в обоих направлениях, но в одном меньше, чем в другом, из чего они от балды заключают, что то направление, по которому корелляция меньше - это метафора и его на самом деле не существует. Еще раз скажу, в их же статье показана реальная корелляция на реальной нейровизуализации. Т.е. исходя из их же данных, они просто дополнили результаты Уолша, показав несимметричность пространственно-временных отношений, т.е. фиолетовый, зеленый и розовый кружочки на втором пике >>6117 должны быть разных диаметров, чтобы точнее показывать реальную картину.
Аноним 26/12/16 Пнд 16:19:16 639340
Решил изучать математику с логики и оснований. Читаю Клини, все правильно делаю?
Аноним 01/01/17 Вск 14:30:16 691341
>>3694 (OP)
Поздравляю всех любителей кококатегорий с Новым Годом! Дорогие подгорающие и сотрудничающие с администрацией красные петушки, я очень рад, что вы есть:3

Аноним 03/01/17 Втр 20:42:09 697242
антифундированн[...].jpg 26Кб, 640x550
640x550
Аноним 04/01/17 Срд 06:26:38 698943
>>6913
Спасибо.
любитель кокотегорий :3
Аноним 04/01/17 Срд 16:28:57 701444
1.jpeg 9Кб, 180x280
180x280
>>6393
Советую пик-релейтед. Книжка посовременнее, и изложено всё яснее и компактнее.
Аноним 04/01/17 Срд 16:32:17 701545
2 190Кб, 2540x728
2540x728
>>7014
Там, например, вся логика высказываний строится на основе всего 3 схем аксиом.
Аноним 09/01/17 Пнд 18:04:03 761746
Absolutely-Disg[...].jpg 36Кб, 600x450
600x450
>>7014
>"modus ponens"
>вместо "элиминатор импликации"
Аноним 11/01/17 Срд 22:57:13 779247
>>7014
Не читал, но...
1) часть серии из десятков книг
2) в названии серии "applied"
3) в названии "an introduction"
4) ОДИН АВТОР
5) в аксиомах ниже - символ точки поставлен так, что совершенно непонятно, что же он обозначает. НИКОГДА такое не встречал.

Предполагаю, что книга - говно, перехожу к дегустации.
Аноним 11/01/17 Срд 23:06:53 779348
>>7014
Фу, буэ, действительно говно. Ты откуда такой выполз, что советуешь это? Сам что-ли нашёл. Небось первокур ВУЗ-а с непрофильной математикой?
13/01/17 Птн 12:55:20 787649
Сделаем ещё несколько замечаний относительно аксиоматического метода в математической логике. Термин «аксиоматический методы» используется в различных смыслах, что иногда ведёт к недоразумениям.
Прежде всего это содержательно-аксиоматический метод. Он употребляется, когда изучается род структур, удовлетворяющих одному и тому же списку свойств. Например, один род структур составляют группы, другой род структур — кольца, третий род структур — структуры Пеано и т.п. Под аксиомами при этом понимаются просто конкретные условия, которым должна удовлетворять любая из структур изучаемого рода. Эти условия понимаются содержательно и записываются на рабочем математическом языке, например на русском или английском. Впрочем, часто аксиомы какого-либо рода структур записывают и на точном логико-математическом языке, но понимают содержательно как утверждения о структурах; для одних структур эти аксиомы могут быть истинны, а для других — ложны.

И где же тут вера кокококонсруктивист?
Аноним 14/01/17 Суб 14:21:33 795850
brouwer.jpg 102Кб, 696x919
696x919
>>7876
>И где же тут вера
Сейчас бы веруну за веру пояснять на подтираче. Ты ж очевидных вещей не видишь, что такому объяснишь. Самый очевидный пример веры - как раз матлогика. Вот есть логические константы, например А. Есть их комбинации. Например "А или не А". Последнее, например, считается истиной, невзирая ни на что. А если подумать головой, а не как обычно, то с каких хуев-то? Если у нас нет конкретного построения, на основании которого мы можем показать свойства А или не А, то надо веровать что все равно это правило истинно для всех возможных случаев априори. Отсюда и неполнота по Геделю - мы делаем предположение, недоказуемое в общем случае. Простейший пример - расеянский автопром. Пусть А будет высказыванием "дверь закрыта", не А - соответственно "дверь открыта". Так есть еще вариант "дверь не закрыта", не сводящееся к открытой двери, т.к. формально-то она выглядит закрытой, но она и не закрыта, т.к. если прислониться - вывалишься из таза к хуям. Но формально у нас только 2 варианта - "А или не А". Совсем другое дело - интерпретация логических констант по Гейтингу. В этом случае мы можем принять А только в случае наличия доказательства А (наличия пруф-объекта, принадлежащего к множеству А и т.о. доказывающего, что множество А ненулевое). Так же и с "не А", мы это принимаем только в случае доказательства того, что множество А пустое (т.е. не содержит никаких объектов). Никакой веры не требуется, требуется только построение. Собственно, к матлогике как формальным правилам еще при Гильберте были большие претензии, отсюда и необходимость создания других подходов к вопросу ощущалась еще в начале 20 века, что н-р привело к созданию натуральной дедукция Генценом и т.д. Аксиоматическая матлогика была фейлом уже во времена ее создания, просто Гильберт яскозал что можно вот так формализовать все, потому что до этого у него получилось формализовать геометрию. Ну и догма Гильберта, конечно. Тут уже чистая религия.
14/01/17 Суб 14:33:26 795951
>>7958
Приведи пример в математике, когда закон исключающего третьего не выполняется. Без теоремы генделя о неполноте.
Аноним 14/01/17 Суб 14:45:30 796152
>>7959
Во всех случаях, когда нет построения, доказывающего свойства "А" или "не А", остается только веровать, что этот закон выполняется (т.к. непосредственно мы не можем этого заключить). Это вообще не математический закон, а онтологический. Аристотель в него веровал, и ты так делай.
Аноним 14/01/17 Суб 23:58:53 803153
>>7961
Закон исключенного третьего утверждает, что для любого A верно A или не A.
Отрицание закона исключенного третьего утверждает, что существует такое A, что верно A и не A.
Предъяви такое A.
Аноним 15/01/17 Вск 01:52:57 803254
>>8031
>мам, вот они веруны, ну скажи
Наличие в формальной системе каких-либо законов регулируется только правилами вывода.
15/01/17 Вск 03:11:12 803655
>>8032
То есть ты не можешь привести такое А?
Аноним 15/01/17 Вск 10:14:18 804756
>>8031
>>8036

В твоём вопросе ошибка, ведь при сокращении двойного отрицания ты неявно подразумеваешь, что верен закон исключения третьего.
Отрицание закона исключенного третьего - это утверждение, что верно не(А или неА) = неА и ненеА.
Отрицанием "неB" я обозначаю то, что определена вычислимая функция из пустого множества в множество B.
В такой формулировке на роль А подходит пустое множество.
Это и есть искомый контрпример существования интерпретации интуиционисткой логики, которую нельзя расширить до интерпретации классической логики.
Аноним 15/01/17 Вск 10:19:29 804857
p.s.
(ну и да, под верностью С я понимаю существование вычислимой функции из одноэлементного множества - в С)
Аноним 15/01/17 Вск 10:30:11 804958
p.p.s. "понимаю" именно в той интерпретации, офк.
Ты же, скорее всего, говоришь, что "Пропозициональная логика лучше, чем логика предикатов!", что весело. Ведь если проводить аналогию с молотком и микроскопом, то ты предлагаешь смотреть на инфузорий в молоток.
Однако - спасибо за провокационный вброс, мне понравилось.
Аноним 15/01/17 Вск 13:10:04 805959
>>8031
>Отрицание закона исключенного третьего утверждает, что существует такое A, что верно A и не A.
Хуйню не неси, пожалуйста. Прочитай, что ты написал и подумай головой. Ты же даже дизъюнкцию не понимаешь, о каком интуиционизме с тобой говорить вообще? Сам написал хуйню, сам опроверг, ахаха кококонструктивисты соснули. Детский сад блядь, штаны на лямках.
Аноним 15/01/17 Вск 13:16:10 806260
>>3694 (OP)
p.p.p.s. - я не он, и хз что он там насчёт Аристотеля и онтологий говорил. Не могу утверждать, что он сказал либо верно, либо неверно. Может он сказал, что он лжёт. И как тогда решить - верно или неверно? Надо мне было именно так, по-Антисфенофски возразить.
Аноним 15/01/17 Вск 19:37:26 809461
>>8036
>>8031
Итак, создадим две параллельных вселенные, где у нас А равно одному и тому же значению. Равно ли А самому себе в другой вселенной?
Аноним 17/01/17 Втр 01:03:20 820262
>>7961
другие аксиомы логики тоже онтологические. Уверуем же.
Аноним 17/01/17 Втр 01:13:38 820363
2.png 38Кб, 506x170
506x170
>>7958
>Так есть еще вариант "дверь не закрыта", не сводящееся к открытой двери, т.к. формально-то она выглядит закрытой, но она и не закрыта, т.к. если прислониться - вывалишься из таза к хуям
Эх щас бы естественным языком формальную логику опровергать...
Приходит к конструктивисту мамка и спрашивает: тебе суп или котлеты? А он такой: мать ты че охуела такое спрашивать ты че под гильберта легла...

>Аксиоматическая матлогика была фейлом уже во времена ее создания
кто б создателям HoTT рассказал, они еще новые аксиомы придумали, дебичи
Аноним 17/01/17 Втр 09:42:53 821664
Аноним 17/01/17 Втр 15:25:42 822765
>>8216
ДОБАВЛЯЙТЕ ТЭГИ, КОГДА АРХИВИРУЕТЕ

мимо кислота-архиватор-кун
Аноним 24/01/17 Втр 13:34:37 931566
>>8227
Тег для раздела вроде должен автоматом добавляться же. Или надо админа стукнуть, чтобы он его добавил?
Аноним 27/01/17 Птн 06:27:24 946667
Объясните мне, что значит "дать основания" и почему это всех так тревожит.
Аноним 27/01/17 Птн 06:50:06 946768
>>9466
Допустим, есть N утверждений, про которые известно, что они должны быть истинными. Требуется предоставить набор аксиом и определений такой, что в нём каждое из N утверждений будет теоремой, причем аксиомами будут далеко не все из этих N утверждений (желательно - ни одно).
Аноним 27/01/17 Птн 06:58:36 946869
>>9466
Допустим, есть N утверждений, про которые известно, что они должны быть истинными. Требуется предоставить набор аксиом и определений такой, что в нём каждое из N утверждений будет теоремой, причем аксиомами будут далеко не все из этих N утверждений (желательно - ни одно).
Аноним 27/01/17 Птн 22:24:42 953270
Поясните про полноту евклидовой/афинной/любой геометрии. В книгах обычно дается доказательство категоричности, но причем здесь полнота?
Аноним 28/01/17 Суб 06:36:24 955471
>>5929
А я ведь всю книгу прочёл, по совету с двача. В конце было ощущение, что меня протроллили. Хуже книги по логике я просто не встречал
Аноним 28/01/17 Суб 06:43:37 955572
>>9467
Разве об этом тред?
Аноним 28/01/17 Суб 06:57:24 955673
На самом деле спор об основаниях имеет сугубо психологически-невротическую природу, и вполне очевидно, что никогда не будет текста, который раз и навсегда удовлетворил бы всех. Все эти попытки свести множества к чисто синтаксической игре утверждений о множествах, или к конструктивным типам, или ещё к какому-то такому синтаксису очевидно не могут привести к какому-то удовлетворению. Вот кажется что синтаксические игры - это "более близкие" объекты чем множества, потому что они "более осязаемые", потому что это "финитарные средства", но это мысль чисто социально-культурологическая, это стереотип; если бы не было вот этого вот дискурса классической логики и попыток свести всю математику к формальным теориям, то никому бы не казалось, что абстракция алгоритма или конструктивного типа чем-то проще или сложнее, чем абстракция множества. Категорщики, кстати, это поняли уже и ебашут свои (\infty,1)-категории, зачастую, без всяких ремарок о том, как это всё можно свести к формальным первопорядковым теориям (хотя на начальном уровне всё же различие "больших и малых категорий" осталось, но я надеюсь, что всё же откажутся вскоре и от этого). Потому что ебать себе мозги по-поводу оснований в 2к17 это уже такая же пошлятина как и ебать себе мозги по поводу того, что первичнее - материализм или идеализм.
Аноним 28/01/17 Суб 12:15:58 956374
>>9556
>различие "больших и малых категорий" осталось, но я надеюсь, что всё же откажутся вскоре и от этого
Чистая педагогика же. Отказываться тут не получится, нужно новое поколение, которое со школы обучено категориям.
Аноним 28/01/17 Суб 23:29:36 960375
>>9556
>Потому что ебать себе мозги по-поводу оснований в 2к17 это уже такая же пошлятина как и ебать себе мозги по поводу того, что первичнее - материализм или идеализм.
Я тебя помню. У тебя подход к вопросу о том, что важно в математике - это что-то в духе отождествления важного с модным. Вполне понятно, почему с таким мировоззрением тебе претят основания, онтологические вопросы вообще, как и вероятно остальная философская проблематика. Но вообще, для остальных людей (более склонных к независимым суждениям) такого рода вопросы часто могут быть важнее.


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


>если бы не было вот этого вот дискурса классической логики и попыток свести всю математику к формальным теориям, то никому бы не казалось, что абстракция алгоритма или конструктивного типа чем-то проще или сложнее, чем абстракция множества.
Нет, конечно. Алгоритм на текущий день (исторически это, разумеется, было скорее наоборот) можно считать непосредственной абстракцией от программы на компьютере. Это гораздо боле приближенно к обычной жизни, чем множества или конструктивные типы (я бы сказал, что лишь немного сложнее понятия натурального числа).
Аноним 29/01/17 Вск 01:08:09 961076
>Я тебя помню.
Ты меня не можешь помнить.

>Но вообще, для остальных людей (более склонных к независимым суждениям)
>Это гораздо боле приближенно к обычной жизни, чем множества или конструктивные типы
Самая большая загадка на свете: почему люди, позицианирующие себя как рационально-мыслящие-с-независимыми-суждениями упорнее всего талдычат одни и те же догмы? Не загадка никакая, конечно, примерно понятно из какого желания ноги у независимо-судящих растут.
Аноним 29/01/17 Вск 01:59:34 961577
>>9610
>Ты меня не можешь помнить.
Технически я не могу исключать, что ошибаюсь, но определенно у меня был небольшой диалог с аноном с явно родственной позицией и похожим стилем.
>позицианирующие себя как рационально-мыслящие-с-независимыми-суждениями
Да бог с тобой, я лишь подчеркивал то, что идея о сведение ценности исключительно к моде - это, в сущности, радикальная позиция состоящая в полном отказе от самостоятельных суждений (по данному вопросу).
> талдычат одни и те же догмы
Если у тебя все-таки есть аргументы почему это довольно очевидно наблюдение несостоятельно, то можешь поделиться.
Аноним 29/01/17 Вск 02:27:35 961878
>>9563
>Отказываться тут не получится, нужно новое поколение, которое со школы обучено категориям.
Думаю, что в любом случае учить сразу категориям, в обход множеств, неэффективный подход. Дело в том, что очень похоже, что основной набор интуиций касательно категорий (в независимом от теории множеств контексте) заметно сложнее чем набор интуиций для самих множеств. В пользу этого явно говорит то, что набор формальных аксиом для теории множеств более-менее вразумителен, а вопрос о аксиоматизации категории Cat, если мне не изменяет память, провисел открытым полтора десятилетия, в итоге был решен, но аксиоматизация оказалась весьма сложной и в итоге никакой заметной популярностью не пользуется.
Аноним 29/01/17 Вск 03:09:23 962179
>Если у тебя все-таки есть аргументы почему это довольно очевидно наблюдение несостоятельно, то можешь поделиться.
Аргументы должны быть у тебя почему оно состоятельно. (Бремя доказательства) Сразу скажу, что аргумент эта же ачивидно - не очень сильный.

>Да бог с тобой, я лишь подчеркивал то, что идея о сведение ценности исключительно к моде - это, в сущности, радикальная позиция состоящая в полном отказе от самостоятельных суждений (по данному вопросу).
Я ни к чему "ценность" не сводил, так как не понимаю, что слово "ценность" значит.
Аноним 29/01/17 Вск 07:21:55 962380
>>9618
Точки, стрелочки, композиция, идентичность. Охуеть как сложно.
Аноним 29/01/17 Вск 07:44:37 962481
>>9618
>набор формальных аксиом для теории множеств более-менее вразумителен
Объясни, пожалуйста, чем мотивированы
а) аксиома подстановки
б) аксиома регулярности
Аноним 29/01/17 Вск 13:18:56 964282
>>9623
Это простая часть. Проблема состоит в том, чтобы очертить допустимые методы формации новых категорий, не опираясь на аппарат теории множеств. И если доводить дело до честного выписывания набора аксиом, то выходит сложно (сложнее чем с множествами).
>>9624
a) если некоторая коллекция является множеством, то всякая коллекция того же или меньшего размера тоже множество;
б) множества и вселенная фон Неймана - это одно и тоже.
Но строго говоря, это аксиомы, которые были добавлены на позднем этапе разработки теории множеств и если их выбросить, то получится теория вполне подходящая для погружения обычной математики, но плохо подходящая для собственно теоретико-множественных исследований. В силу этого они отражают боле "продвинутые" интуиции.
Аноним 29/01/17 Вск 13:24:20 964383
>>9621
Ладно, у меня нет особенного желания ввязываться в пустой спор с человеком, который в основном занимается словесной эквелибристикой, а не содержательной аргументацией своей позиции.
Аноним 29/01/17 Вск 13:49:27 964484
>>9643
>Ачивидно, что алгоритм понятнее и проще, чем множество
>Почему?
>А почему нет?
>Ты сделал утверждение, ты и обосновывай
>Пропало всякое желание с тобой разговаривать, эквилибрист словесный
yaasno
Аноним 29/01/17 Вск 13:52:48 964585
>>9642
>Это простая часть. Проблема состоит в том, чтобы очертить допустимые методы формации новых категорий
Вот у меня два вопроса всегда
1) Зачем их очерчивать?
2) Почему останавливаются только на первой итерации и не очерчивают допустимые методы очерчивания допустимых методов образования новых категорий?
Аноним 29/01/17 Вск 14:45:46 964686
>>9645
1)Чтобы различать корректные рассуждения и некорректные. Для практики обычного математика аксиоматизация, как правило, здесь избыточна и в подавляющем большинстве случаев понимания получаемого из разбора большого числа допустимых построений и нескольких приводящих к парадоксам вполне достаточно. Хотя, конечно, не исключено, что например однажды может прийти на рецензию статья, где ошибка кроется в построение парадоксальность которого не ясна из рассмотренных примеров.
2)Без комментариев.
Аноним 29/01/17 Вск 15:11:44 964987
>>9646
Почему без комментариев? Почему корректность важна, а корректность корректности "без комментариев"? Что это за фашизм такой?
Аноним 29/01/17 Вск 15:40:28 965588
>>9649
Я же говорю, тебе прежде всего хочется заниматься словесной эквилибристикой. Речь шла о обучении теории категорий, ты же для полемических целей акцентируешь внимание на совершенно очевидно иррелевантном здесь вопросе.
Аноним 30/01/17 Пнд 00:13:45 967989
>>9642
>Проблема состоит в том, чтобы очертить допустимые методы формации новых категорий, не опираясь на аппарат теории множеств.

Таки да. Но тут такая штука , что просто так взять и раз и навсегда очертить математику и успокоится ( как хотел Гильберт, например) ведь не получится. Точнее, оно может и получится, только смысла тогда особого в категориях нет - тут теория множеств как раз лучше послужит, как статичная система.
Как по мне, весь смак категорий в том, чтобы не мешать творческой ( а для упоротых платонистов - исследовательской) составляющей процесса. Т.е. да - ты можешь наворотить лютейшую хуйню не оглядываясь ни на кого, лишь бы ты сам видел в этом смысл. Тогда вопрос корректности выходит за рамки формализма - это уже вопрос того, как другие относятся к твоей работе.
Ну а прелесть еще в том, что по сути даже школьную программу менять не надо. Просто математика должна начинаться с показа объектов и морфизмов и слов типа "ну вот в целом это и есть математика". Дети сначала нихуя не поймут, конечно. И дальше все пусть идет по старому, но каждая пройденная тема, хоть в алгебре, хоть в геометрии, должна кончаться показом соответствующей категории. И вот так постепенно к концу школы до некоторых действительно дойдет, что значит абстракция и конструирование. А это уже будет лютейшим вином, как по мне.
Аноним 30/01/17 Пнд 01:02:58 968090
>>9679
Почему каждый хуй мечтает отреформировать школьную программу? Т.е. вообще каждый, поголовно.
Аноним 30/01/17 Пнд 15:28:03 971691
>>9680
Потому что фундамент
Аноним 30/01/17 Пнд 22:51:44 974292
>>9680
потому что хочется как-то связать ее с математикой, а так они лишь имеют одинаковое название. Почему бы просто не переименовать школьный предмет в "практические вычислительные навыки".
Аноним 30/01/17 Пнд 23:26:53 974393
>>9742
Проблема есть. Но исправить это далек не просто, особенно если говорить об общеобразовательной школе и тем более, если заходить с позиций математика с ограниченным/отсутствующим опытом преподавания рядовым школьникам. Например, уверен, что план
>Просто математика должна начинаться с показа объектов и морфизмов и слов типа "ну вот в целом это и есть математика". Дети сначала нихуя не поймут, конечно. И дальше все пусть идет по старому, но каждая пройденная тема, хоть в алгебре, хоть в геометрии, должна кончаться показом соответствующей категории. И вот так постепенно к концу школы до некоторых действительно дойдет, что значит абстракция и конструирование.
полностью провалится и просто никто ничего не поймет (включая преподавателей математики). Думаю, что это провалится и в матшколах.
Можно вспомнить колмогоровскую реформу школьного курса геометрии в рамках которой например простая замена термина "равенство фигур" на более корректный "конгруэнтность фигур" привела к большим проблемам с пониманием содержания школьниками.
Из своего ограниченного опыта преподавания в кружках школьникам 5-7 классов могу сказать, что навык восприятия абстрактных конструкций находится на низком уровне и развивается медленно. Например, задачи которые сводятся к тому или иному разбору конкретных случаев даются школьникам куда легче, чем задачи где нужно дать, пусть и тривиальное, но общее рассуждение.
Аноним 31/01/17 Втр 07:34:24 974994
p0127.png 45Кб, 1292x1962
1292x1962
>>9743
Колмогоровская реформа была гораздо более радикальной, нежели просто замена термина "равенство" на термин "конгруэнтность". Например, он определил вектор как изометрию плоскости/пространства, буквально такими словами. Естественно, что учителя его не поняли.
Аноним 31/01/17 Втр 11:05:12 975595
>>9749
>то чувство, когда искренне не понимаешь, что не так
как вектор то определять правильно? как стрелочку с хвостиком?
Аноним 31/01/17 Втр 12:36:08 975996
Аноним 31/01/17 Втр 13:20:42 976197
>>9755
Неориентированный отрезок - это неупорядоченная пара точек плоскости.

Ориентированный отрезок - это упорядоченная пара точек плоскости.

Два ориентированных отрезка называются эквивалентными, если совмещаются параллельным переносом.

Свободные векторы - классы множества ориентированных отрезков по этому отношению эквивалентности.
Аноним 31/01/17 Втр 19:21:08 977398
>>9761
ну и с какого хуя такой подход верный? эти определения не дают никакой интуиции: определи теперь сумму векторов, разнообразные произведения, получится вообще невыносимая поебень.
Аноним 31/01/17 Втр 19:39:47 977599
>>9749
Вот это проиграл с теоретико-множественных дидов, лил.
31/01/17 Втр 20:04:12 9778100
>>9773
Что там определять? Правило треугольника очень простое. А "вектор это изотропия пространства" хуйня какая-то. Много векторов = много изотропий? Сумма векторов = сумма изотропий? Это тоже не даёт никакой интуиции. Поебень непонятная. Никогда школьник не вдуплит это.
31/01/17 Втр 20:18:04 9787101
Во видал, даже я перепутал слова, школьники с ваших изометрий вообщей охуеют. Но тем, кто школьников ничему никогда не учил не понять.
>>9778-кун
Аноним 31/01/17 Втр 20:39:04 9791102
Единственная реформа которая нужна школьному образованию - это укоротить его раза в 3, чтобы не мешать нормальным школьникам заниматься нормальными делами (ходить на кружки и заниматься самоподготовкой, например) и не ебать мозги всяким долбоёбам, которые всё равно ничего не выучат. Ну и, конечно же, не ебать мозги учителям, которые тоже школьной программы в полном объеме не знают.
Аноним 31/01/17 Втр 21:32:57 9795103
>>9778
композиция изометрий - изометрия. Изометрии образуют группу Ли. все же просто.
31/01/17 Втр 21:36:58 9798104
>>9795
Расскажи о своём опыте обучения 7-ми классников группам Ли.
Аноним 31/01/17 Втр 21:45:55 9800105
>>9798
ну можно сказать просто "группа", это совсем простое понятие.
Аноним 31/01/17 Втр 22:16:08 9810106
>>9773
Суммой ориентированного отрезка (ab) и ориентированного отрезка (bc) называется ориентированный отрезок (ac).

Пусть x и y - свободные векторы. Выберем в x представителя (pq). Найдем в y ориентированный отрезок (qr), начало которого равно q. Суммой x и y называется класс эквивалентности отрезка (pq)+(qr). Определение не зависит от выбора представителя, очевидно.
Аноним 01/02/17 Срд 10:40:37 9819107
>>9773
Пусть векторы определены как изометрии плоскости. Ну и как определить тогда сумму?
Аноним 01/02/17 Срд 14:24:04 9843108
>>9819
>Пусть векторы определены как изометрии плоскости.
Это неправильное определение - хочется отождествить вектора с параллельными переносами, а кроме них изометриями являются еще повороты и отражения.
Аноним 01/02/17 Срд 14:43:08 9851109
>>9819
Как композицию биекций, но не мат. школьникам такое будет очень сложно переварить. Им ещё придётся строить заново геометрическую интуицию. Ещё школьнику понятно будет что такое параллельный перенос конкретных фигур и векторов, но преобразования всей плоскости будет сложнее понять.

В общем всем реформаторам предлагаю пойти в обычную школу, взять там обычных школьников и попытаться им рассказать что-то на вашем любимом языке. в рамках факультатива
Аноним 01/02/17 Срд 18:46:33 9924110
А на вопрос мой так никто и не ответил - почему тот же Гильберт был дико заинтересован в том, что бы дать "непротиворечивые финитарные основания для математики", но тот факт, что "непротиворечивые финитарные основания" сами оставались без "непротиворечивых финитарных оснований" его нисколько не смущал? Неужто он не видел, что он просто смещает "стартовую точку", но никакого принципиального парадигмального сдвига не происходит? Не понимаю этот момент серьезно.
Аноним 01/02/17 Срд 18:48:34 9926111
>>9924
Существуют фс, которые могут подтвердить собственную непротиворечивость, именно этот факт и заставил гильберта верить.
Аноним 01/02/17 Срд 18:55:42 9930112
>>9926
Но ведь они доказывают не собственную непротиворечивость, а непротиворечивость "маленькой модели самой себя", то есть тут происходит расщепление на "большую ФС" и "маленькую ФС внутри большой ФС" и "большая ФС" не может, вообще говоря, провести отождествление "маленькой ФС" с самой собой. То есть тут размахивают руками и говорят о какой-то "эффективной непротиворечивости", дескать да, формально не можем отождествить, но мы-то понимаем как оно на самом деле. Ну так мы и раньше понимали как оно на самом деле, без программ Гильберта всяких.
Аноним 01/02/17 Срд 19:23:55 9940113
>>9924
У Гильберта не стояло задачи обосновать корректность финитных методов - они как раз и были очерчены таким образом, чтобы быть куском математики, который признается всеми математиками (не уверен, были ли в те времена ультрафинитисты, которые и с этим были не согласны, но в любом случае они никогда не были чем-то большим, чем незначительное меньшинство). Была проблема с более абстрактными теоретико-множественными методами в свете парадоксов теории множеств и вполне заметного числа математиков, которые эти методы отвергали. Гильберт хотел защитить теоретико-множественные методы от этих нападок, сведя их к финитным. Насколько я понимаю, Гильберт не был точен в формулировках целей так как в силу ошибочных предположений считал, что можно достичь "всего и сразу". Тем не менее, видимо главным здесь было доказать финитными средствами, что всякое теоретико-множественное доказательство финитного факта преобразуется в финитное доказательство того же факта.

>>9926
>Существуют фс, которые могут подтвердить собственную непротиворечивость, именно этот факт и заставил гильберта верить.
Во времена Гильберта ничего такого известно не было. Современные же примеры совершенно экзотичны.
Аноним 01/02/17 Срд 19:33:12 9941114
>>9930
Понятно. То есть, если грубо, этот аргумент в каком-то роде должен был быть социальным, а не метафизическим.
Аноним 01/02/17 Срд 19:33:32 9942115
Аноним 01/02/17 Срд 19:42:37 9945116
>>9941
Видимо так.
Но строго говоря, я Гильберта не читал (и не факт, что он непосредственно об этом пишет), а просто пересказываю интерпретации, которые слышал.
Аноним 03/02/17 Птн 11:50:19 10200117
мэгумин.jpg 167Кб, 782x543
782x543
>>9924
У Гильберта получилось (и надо признать, годно получилось) аксиоматически построить геометрию. Этот успех заставил его уверовать, что и с арифметикой и вообще со всем остальным можно так же. Но реальность оказалось несколько сложнее, что прямо показывает нам сомнительную ценность таких экстраполяций от одного-пары частных случаев оптом и априори на все остальные как закон исключенного третьего, например. То же самое можно сказать про т.н. "догму Гильберта", это же чистая религия.
Аноним 03/02/17 Птн 12:33:39 10204118
Аноним 03/02/17 Птн 14:46:20 10222119
>>10200
> как закон исключенного третьего, например
и собственно модус поненс.
Аноним 03/02/17 Птн 14:55:14 10228120
140542860164tnl[...].jpg 43Кб, 536x604
536x604
>>10222
>поненс.
С элиминатором импликации-то что не так?
Аноним 03/02/17 Птн 15:01:12 10229121
>>10228
Все так, если веруешь.
Аноним 03/02/17 Птн 15:04:27 10230122
Снимок.PNG 7Кб, 343x134
343x134
>>10229
>если веруешь.
Во что?
Аноним 03/02/17 Птн 15:10:17 10232123
>>10230
В правила резолюции.
Аноним 03/02/17 Птн 15:12:53 10233124
>>10228
Если начать применять этот принцип
>прямо показывает нам сомнительную ценность таких экстраполяций от одного-пары частных случаев оптом и априори на все остальные
последовательно (т.е. отказываться от индукции вообще), то и от модус поненс нужно отказаться.
Аноним 03/02/17 Птн 15:23:09 10234125
>>10232
Ну вот я тебе принес это правило, покажи что там не так.
>>10233
Но у нас пропозишен - это всегда множество пруф-объектов, его доказывающих. Только конструктивные объекты, только хардкор.
Аноним 03/02/17 Птн 15:27:09 10238126
>>10234
>Только конструктивные объекты, только хардкор.
Ну это вера из двух частей:
- вера в тезис черча, так что любая математическая задача может быть сведена к алгоритму
- вера в непогрешимость вычислительной техники (тот же модус поненс по сути)
Аноним 03/02/17 Птн 15:28:18 10239127
>>10238
О какой вере ты говоришь применительно к вычислимым объектам?
Аноним 03/02/17 Птн 15:36:18 10241128
>>10239
о вере в функциональные типы. Еще разок: у нас есть эмпирический закон, что транзисторы ведут себя определенным образом. Остается только верить, что они будут вести себя так и дальше. Согласно этой вере вычисление всегда предсказуемо. А дальше по изоморфизму карри-говарда модус поненс может быть сведен к функциональным типам.

Теперь у нас есть такой же закон исключенного третьего. Эмпирически он всегда выполнен для вычислимых объектов. В чем же дело? Почему нельзя в него верить?
Аноним 03/02/17 Птн 15:48:02 10243129
Аноним 03/02/17 Птн 15:51:57 10245130
>>10241
>у нас есть эмпирический закон, что транзисторы ведут себя определенным образом. Остается только верить, что они будут вести себя так и дальше.
Именно что эмпирически. Зачем верить, если есть факты?
>закон исключенного третьего. Эмпирически он всегда выполнен для вычислимых объектов. В чем же дело? Почему нельзя в него верить?
Потому что он невычислим в общем случае. А на конечных множествах его и Брауэр не отрицал.
Аноним 03/02/17 Птн 16:01:48 10246131
>>10245
>Зачем верить, если есть факты?
Математик и физик доказывают теорему о том, что все нечетные числа - простые. Математик: - 1 - простое, 3 - простое, 5 - простое, 7 - простое, 9 - не простое. Это контрпример, значит теорема неверна. Физик: - 3, 5 и 7 - простые, 9 - ошибка эксперимента, 11 - простое и т.д. Возьмем ещё несколько случайно выбранных нечетных чисел. 17 - простое, 19 - простое, 23 - простое... Теорема доказана.

>Потому что он невычислим в общем случае
Это доказанный факт?

Но вернемся к >Зачем верить, если есть факты
На 2017 год закон исключенного третьего всегда работал для любых математических объектов.
Аноним 03/02/17 Птн 16:03:38 10247132
>>8031
Высказывание - моя мамка старше меня и моложе, например. Вообще, логика времени нужна, а не пространства.
Аноним 03/02/17 Птн 16:05:32 10248133
>>10247
Невыводимая формула, конечно, отличный пример.
Аноним 03/02/17 Птн 16:06:41 10249134
>>10246
>На 2017 год закон исключенного третьего всегда работал для любых математических объектов.
Для любых, на которых его можно показать непосредственно. Т.е. на любых построимых, вычислимых, в общем случае - конструктивных объектах. Хватит тупить уже, самому тебе не надоело нести хуйню?
Аноним 03/02/17 Птн 16:10:26 10251135
>>10249
Я сказал просто для любых. Утверждение, доказанное в классической логике, всегда может быть доказано в интуитивистской. (эмпирический факт)
Аноним 03/02/17 Птн 16:15:15 10252136
>>10251
Классическая логика - это просто синтаксические правила. Считается, что они истинны для всех случаев оприори. Конструктивная - манипуляции с конструктивными объектами, действие правил распространяется только на конструктивные объекты.
Аноним 03/02/17 Птн 16:24:00 10255137
screen.png 54Кб, 586x253
586x253
>>10252
Ты оперируешь какими-то бредовыми определениями. Классическая логика это интуитивистская + LEM. Собственно, нахера я опять пересказываю HoTT?
Аноним 03/02/17 Птн 16:30:44 10257138
>>10255
>Ты оперируешь какими-то бредовыми определениями.
Ты не слышал про интуиционстскую логику Гейтинга, интерпретацию логических констант по Брауэру-Гейтингу-Колмогорову, изоморфизм Карри-Говарда, раз уж называешь "мои" определения бредовыми. Видимо, и про MLTT мало что знаешь. Но при этом лезешь в НоТТ. Это напоминает школьников из треда про машинное обучение и нейросети в /пр - не зная даже азов уровня учебников Вентцель и Зорича/Фихтенгольца, лезут читать ISLR и т.д. Итог закономерен.
Аноним 03/02/17 Птн 16:45:01 10260139
screen.png 32Кб, 564x151
564x151
>>10257
HoTT не нужны никакие пререквизиты, она предназначена для математиков, желающих изучить новые основания. Читателю не нужно знать даже, что такое теория типов, а все твои исторические термины он может изучить в википедии.

Пока что я могу судить, что ты до сих пор не удосужился открыть HoTT и почитать, раз я должен вычитывать правильные определения за тебя.
Аноним 03/02/17 Птн 17:10:42 10265140
>>9940
>>9941
Я хотел бы переделать свой ответ. Мне кажется ты говоришь не про то, ибо если бы программа Гильберта действительно бы заключалась в
>всякое теоретико-множественное доказательство финитного факта преобразуется в финитное доказательство того же факта.
то, естественно, она была бы успешной. Ведь есть тупо теорема о том, что ZFC доказывает те же самые арифметические утверждения, что и PA (я её запомнил как "теорема об элиминации"), значит дело тут не в том.
Аноним 03/02/17 Птн 17:11:54 10266141
>>10260
>HoTT не нужны никакие пререквизиты
Ой, все. Там самая первая глава - изложение MLTT. Для MLTT не нужны пререквизиты? И как, много ты там понял?
Аноним 03/02/17 Птн 17:43:53 10273142
>>10265
> Ведь есть тупо теорема о том, что ZFC доказывает те же самые арифметические утверждения, что и PA (я её запомнил как "теорема об элиминации"), значит дело тут не в том.
Такой теоремы нет. В силу второй теоремы Гёделя о неполноте, предполагая непротиворечивость PA, верно обратное. В ZFC несложно доказать, что PA непротиворечива (рассмотреть натуральные числа с функциями сложения, умножения и следования и показать, что это модель PA), но по второй теореме Гёделя о неполноте PA не доказывает собственную непротиворечивость.
Аноним 03/02/17 Птн 18:11:31 10275143
>>10273
Извиняюсь, перепутал с другой теоремой о том, что ZFC+CH доказывает те же самые арифм. утверждения, что и ZFC.
Аноним 03/02/17 Птн 18:28:08 10276144
>>10266
Мне всю книгу скринить надо, чтобы ты ее тут прочитал? Книга начинается с пояснения, что такое тип, что такое теория типов, что такое суждение. Кому нужны такие пояснения? Вестимо, что математикам, кому знакомы общие понятия наивной теории множеств и гомотопической алгебры. Далее идет сравнение с классическими основаниями.
Читателю, знакомому с MLTT, рекомендуют вообще читать первую главу по диагонали.
Аноним 03/02/17 Птн 21:11:07 10289145
поехал1.png 134Кб, 1136x736
1136x736
поехал2.png 173Кб, 1442x814
1442x814
поехал3.png 217Кб, 1678x971
1678x971
поехал4.png 141Кб, 1661x840
1661x840
Хотя прозвучали кодовые слова...
Аноним 04/02/17 Суб 12:09:38 10308146
проиграл.webm 2778Кб, 480x360, 00:01:16
480x360
>>10289
Ты в моих постах триггеры выискиваешь, чтобы потом гореть с них? Зачем? Это же обычная терминология.
Аноним 04/02/17 Суб 19:14:43 10338147
Аноним 04/02/17 Суб 19:19:40 10339148
Аноним 04/02/17 Суб 22:53:30 10348149
>>10339
А ты хорош. Но интуиционизм тоже неплох
Аноним 05/02/17 Вск 13:20:37 10358150
>>10338
>>10339
Пиздец. А ниче, что по этой теме на русском языке полторы книжки и есть? Мне, может быть, использовать термин meaning of the logical constants, использующийся Мартин-Лёфом http://people.inf.elte.hu/divip/AgdaTutorial/Further_Reading/Meanings_and_justification.pdf и авторами Programming in
Martin-Löf’s Type Theory? Ты правда аутист какой-то, сам себе придумываешь триггеры, чтобы потом с них на батрушку высаживаться.
Аноним 05/02/17 Вск 15:09:21 10364151
>>10358
миллионы книг и статей - харам
@
халяль - полторы книжки
Аноним 11/02/17 Суб 18:36:39 10795152
пахомматематика2.jpg 82Кб, 782x550
782x550
p0008.png 194Кб, 2889x4500
2889x4500
Почитал тута за ультраинтуиционизм Есенина-Вольпина пикрелейтед, это разве серьезная математическая точка зрения? Он отвергает марковскую абстракцию потенциальной осуществимости, но тут же предлагает "гипотезу осуществимости следующего шага", что то же самое, вид сбоку. Далее, говорит, что функция следования - это не закон, а только намек на закон (хотя по факту это конструктивная функция, конструктивный объект, т.е. именно совершенно конкретная формулировка закона). Потом вообще какой-то аутизм уровня того анекдота:
-Дохуя-это сколько?
- Иди вдоль рельсов и считай шпалы. Когда досчитаешь до "а ну его
нахуй"-это будет как раз половина.
Аноним 11/02/17 Суб 19:09:11 10796153
>>10795
На твоем пикрелейтеде же вполне четко и понятно даны ответы на твои вопросы. Не очень понятно, что именно непонятно. Вот он говорит: пусть у нас есть ребенок и функция следования для него, которая берет ребенка и дает ребенка в следующий момент времени. То есть р, р', р''- это все ребенки, но интуитивно ясно, что после некоторого (неопределенного) количества применений этой операции результат уже никак ребенком быть не может. Это он и постулирует утверждением под номером три. Я просто пересказываю текст еще раз, да.

Ну а про "и так далее" и вовсе говорить нечего. Определим натуральные числа: 1, 2, 3 и так далее. Ну ты понял.
Аноним 11/02/17 Суб 19:22:56 10797154
>>10796
Пример с ребенком дурной какой-то, что-то уровня парадокса лысого или парадокса кучи. Такое решается с помощью нечеткой логики, функция следования и потенциальная осуществимость тут вообще не при чем.
>Ну а про "и так далее" и вовсе говорить нечего. Определим натуральные числа: 1, 2, 3 и так далее. Ну ты понял.
И что тут не так?
Аноним 12/02/17 Вск 00:31:40 10808155
>>10797
> что тут не так
Это не определение.

> тут вообще не при чем
Ну как они не при чем, если он об этом и говорит? Никто же не спорит, что эти ситуации можно смоделировать в рамках дефолтной модели. Это у него просто философский аргумент такой: вот, посмотрите - понятие, которые мы принимаем за интуитивно ясное, на самом деле работает совсем не так, а эдак.
Аноним 12/02/17 Вск 06:55:52 10810156
>>10797
Не более дурной, чем пример с брадобреем в кое-какой другой некогда популярной теории.

>>10795
1. Если убрать с головы волосатого человека один волосок, он не станет лысым. Начнём убирать с головы человека волосы по одной штучке за раз; через некоторое время получим лысого человека. Таким образом, имеем антиномию. Объекты, обладающие такой антиномией, будем называть собственно ультрафинитистскими.

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

3. Не существует доказательств, что объекты, используемые в метаматематических построениях, не являются собственно ультрафинитистскими.

4. Пользуясь случаем, передаю привет чернильной дыре.
Аноним 12/02/17 Вск 13:09:52 10821157
>>10810
>1. Если убрать с головы волосатого человека один волосок, он не станет лысым. Начнём убирать с головы человека волосы по одной штучке за раз; через некоторое время получим лысого человека. Таким образом, имеем антиномию. Объекты, обладающие такой антиномией, будем называть собственно ультрафинитистскими.
Тут нет никакой антиномии, просто бинарная логика неприменима к подобным задачам, т.к. мы не можем в точности указать, с какого конкретно количества волос считать человека лысым. Непрерывная функция принадлежности вопрос снимает полностью, т.к. появляется возможность считать человека лысым и волосатым в какой-то степени от 0 до 1. Не понимаю, зачем тащить в такие задачи какой-то ультрафинитизм, когда все элементарно сводится к нечетким множествам.
>>10808
>Это не определение.
А что это? 0:N, if a:N then succ(a):N, закон построения (функция следования).
Аноним 12/02/17 Вск 14:45:05 10823158
>>10821
А где гарантия, что "бинарная логика" применима к основным умозрительным объектам метаматематики, таким как строка символов, алфавит, возможность в любой момент времени ввести новую, не использованную ранее букву?
Аноним 12/02/17 Вск 15:55:44 10825159
>>10823
В случае конечных объектов можно проверить непосредственно, применима или нет. В общем случае, безотносительно возможности построения, никакой гарантии, только вера.
12/02/17 Вск 16:10:27 10827160
>>10825
Тогда получается мы не можем нормально работать с натуральными числами?
Аноним 12/02/17 Вск 16:10:35 10828161
>>10825
А ультрафинитисты вот не веруют, но доказывают.
Аноним 12/02/17 Вск 16:17:23 10829162
>>10827
С какими-то можем, с какими-то нет. Так-то 10^100^1000^10000 тоже натуральное число.
>>10828
На эту тему вообще есть что почитать интересного? Я вот гуглил, на русском языке одну статью нашел, которую и процитировал, на английском тоже почти ничего.
12/02/17 Вск 16:19:13 10830163
>>10829
>С какими-то можем, с какими-то нет. Так-то 10^100^1000^10000 тоже натуральное число.
Выходит, конструктивная математика основанна на вере ?
Аноним 12/02/17 Вск 16:23:58 10831164
>>10830
Я уже столько раз писал про марковскую абстракцию потенциальной осуществимости, что даже не помню сколько раз конкретно. И чем конструктивный объект отличается от потенциально существующего, писал не меньше. С себя начни, если такие простые вещи понять не можешь.
Аноним 12/02/17 Вск 16:30:18 10832165
>>10831
проговаривать название != писать
12/02/17 Вск 16:32:27 10833166
>>10831
Ну у тебя и пичот.
>марковскую абстракцию потенциальной осуществимости
Вера. Обычная вера в то, что алгоритм может работать верно и выдавать нужные результаты, при этом не останавливаясь. Раз можно проверить потенциальное сущствование только конечное количество объектов, в нашем случае чисел, то как проверить, что алгоритм верен?
> С себя начни, если такие простые вещи понять не можешь.
Ты опять берёшь и уходишь от ответа, мань.
Аноним 12/02/17 Вск 18:09:48 10842167
>>10830
>Выходит, конструктивная математика основанна на вере ?
Мозг конструирует для нас реальность. И мы в нее верим, а что ещё остается делать?
Аноним 12/02/17 Вск 18:13:55 10845168
Аноним 12/02/17 Вск 18:45:46 10852169
>>10833
В алгоритмы веровать не нужно. Алгоритм либо работает правильно и выдает правильный результат, либо он работает неправильно и выдает результат, доказывающий абсурдность предположения, что алгоритм работает правильно. Любой алгоритм сводится к типизированной лямбде, корректность его можно проверить методами MLTT, опять же, про интерпретацию логических констант и изоморфизм Карри-Говарда я писал достаточно, чтобы тут у какого-то кловна жопа горела с этой терминологии.
12/02/17 Вск 18:48:37 10853170
>>10852
>Алгоритм либо работает правильно и выдает правильный результат, либо он работает неправильно и выдает результат, доказывающий абсурдность предположения, что алгоритм работает правильно.
Разве это не закон исключённого третьего? Ты берёшь и веруешь в то, что твой алгоритм работет либо правильно либо неправильно? Чем эта вера отличается от веры в аллаха?
Аноним 12/02/17 Вск 18:59:57 10855171
>>10853
>Разве это не закон исключённого третьего? Ты берёшь и веруешь в то, что твой алгоритм работет либо правильно либо неправильно? Чем эта вера отличается от веры в аллаха?
Пиздец. А я ведь специально сформулировал отрицание именно в интуиционистском смысле. Но что можно объяснить школьнику на батрушке. Закон исключенного третьего это "А или не А". "А" в данном случае означает "у нас есть пруф-объект, подтверждающий, что А не пусто, а:А". "не А" можно представить в двух вариантах: "у нас есть пруф-объект, доказывающий, что построение А неосуществимо, б:Б" и "у нас нет нихуя". В классическом смысле оба этих случая равнозначны. В интуиционизме допустимо только доказательство через конкретное построение, т.е. только первый вариант. Тогда как второй не доказывает ничего, т.к. это не построение. В интуиционизме закон исключенного третьего не принимается как общее правило по простой причине - у нас нет построений А или построений, отрицающих А на все возможные случаи. Поэтому закон исключенного третьего, принимаемый априори - чистая вера.
Аноним 12/02/17 Вск 19:18:23 10858172
Поясните за New Foundations. Что это?
Аноним 12/02/17 Вск 19:22:33 10859173
>>10852
Охуенный у тебя манямирок, в котором все алгоритмы всегда выдают результат. Нам бы всем не помешал такой.
Аноним 12/02/17 Вск 19:25:50 10860174
p0180.png 207Кб, 2811x4481
2811x4481
p0181.png 209Кб, 2811x4481
2811x4481
p0182.png 211Кб, 2811x4481
2811x4481
>>10858
Пикрелейтед.
>>10859
>все алгоритмы всегда выдают результат.
Пустой тип как результат проверки на корректность - тоже построенный результат.
Аноним 12/02/17 Вск 19:32:29 10862175
>>10860
> Пустой тип как результат проверки
> результат
Ты так говоришь, будто проблема остановки решена. Я не против твоих ХоТТов, да и в споре не участвую, но никогда не пиши хуйню вроде
>Алгоритм либо работает правильно и выдает правильный результат, либо он работает неправильно и выдает результат
Алгоритм может начать работу и никогда не завершиться, и никакие методы проверки, в том числе MLTT не выдадут на таком алгоритме никакого ответа, они просто зависнут.
Аноним 12/02/17 Вск 19:38:33 10864176
>>10862
Никто не спорит с тем, что существуют алгоритмически неразрешимые задачи.
>никакие методы проверки, в том числе MLTT не выдадут на таком алгоритме никакого ответа, они просто зависнут.
Сам хуйню пишешь, а мне запрещаешь. Не зависнет ничего, в худшем случае просто не будет чекаться и все. Защита от такой хуйни есть во всех пруверах, подход разный, правда.
Аноним 12/02/17 Вск 19:50:09 10869177
>>10864
>Защита от такой хуйни есть во всех пруверах, подход разный, правда.
Охуеть защита - внешним образом прерывать процесс. Мы тут про основания математики, ты подался рассуждать про хаки в софте.
Аноним 13/02/17 Пнд 13:18:22 10916178
SDC116221.jpg 966Кб, 2592x1944
2592x1944
Умели же раньше книжки по основаниям писать. Читаю пикрелейтед, к слову, Френкель - тот самый, один из создателей ZFC. В главе про интуиционизм последний параграф - о том, как интуиционизм повлиял на различные разделы математики. Арифметику и алгебру вообще почти не затронул, анализ - поменялись методы в доказательствах некоторых теорем, от теории множеств в интуиционизме вообще почти камня на камне не осталось, лол. Т.е. что получилось - вычислимые разделы математики с некоторыми оговорками истинны как классически, так и конструктивно, а всякий аутизм и вера в невычислимую хуитку сразу же показывают свою несостоятельность. Арифметика, т.о. более адекватные основания математики, чем логика.
Аноним 06/03/17 Пнд 12:51:41 12688179
>>10795
Кстати, подумалось вдруг. А ведь постулат "всегда можно сделать ещё один шаг" прямо противоречит аксиоме выбора. В самом деле, рассмотрим множество возможных букв на листе бумаги и упорядочим его булеан по включению. Очевидно, любая цепь мажорируется своим объединением. Тогда по лемме Цорна есть максимальный элемент - должно существовать множество букв, к которому уже нельзя добавить ни одной буквы. Но ультрафинитисты говорят, что к любому множеству букв на листе можно, исхитрившись, дорисовать ещё одну букву. Противоречие. Аналогичное доказательство для шагающего человека оставим читателю в качестве упражнения.

Any комментс?
Аноним 07/03/17 Втр 14:14:22 12718180
>>12688
В частности, рассмотрим конечное множество, скажем, из 5 элементов и рассмотрим "шаг" обогащения подмножества множества одним элементом. Это неприменимо ко всему множеству. Шах и мат ультрафинитисты.
Аноним 07/03/17 Втр 19:15:28 12746181
>>12718
Это уже толстовато.
Аноним 11/03/17 Суб 07:44:05 12841182
>>12688
Если ты возьмёшь объединение всех букв, то добавить новую букву уже не получится (только одну из старых). Например, если к множеству букв {x,y,z} добавить букву x, всё равно будет множество {x,y,z}
Аноним 11/03/17 Суб 12:39:06 12843183
>>12841
Нет, тут под буквой понимается рисунок на листе бумаги, не пересекающийся с другими рисунками.
Аноним 27/03/17 Пнд 18:32:50 13694184
>>10852
H A L T I N G
P R O B L E M

Вообще, насколько нужно быть наивным, что веровать в то, что машина тьюринга - это неебаца вычислитель, который может вычислить всё что вообще можно вычислить. Ещё скажи что я на квантово-астрально-тёмноматериальном компьютере в 20 000 веке н.э. всё ещё не смогу решить проблему останова.
Аноним 27/03/17 Пнд 18:45:12 13696185
>>10852
Тупые транзистерные говна вообще дико примитивны. Тупая машина даже не догоняет что такое бесконечность, что блять нет смысла её строить, т.к. это займёт бесконечно времени. И даже если вместо самой бесконечности, ты просто даёшь ей конечный объект, но задашь ему свойства бесконечности, тупая машина решит доказать эти свойства и суко начнёт таки строить сраный бесконечный терм. Более того, даже нет возможности заставить одну тупую машину проследить за другой тупой машиной, чтоб та не строила бляцкий бесконечный терм. Быть констуктивистом, это значит верить в то, что вот этот вот примитив, типа МТ - это настолько серьёзный формализм, что на его основании можно кукарекать о глобальных вещах, типа существования/несуществования вообще. Даже гипервычисления преодолевают halting problem, но конструктивисту религия не позволит об него мараться.
Аноним 27/03/17 Пнд 19:21:02 13701186
Я ньюфаг, тред не читал. Раньше думал, что теория множеств это основание. Потом прочитал, что теория категорий. Теперь прочитал, что вообще теория типов и HoTT. Так кому верить? Что сейчас в моде у математиков? И когда будет окончательное решение оснований математики или я что-то пропустил и оно уже есть?

Также, менее интересно, но тоже интересно все-же основание геометрии. Ранее думал, что аксиомы Гильберта, но краем уха в википедии прочитал, что там еще какие-то есть после Гильберта.
Аноним 27/03/17 Пнд 19:23:37 13702187
>>13701
Проблема оснований математики успешно решена сто лет назад. Оказалось, что основания не нужны.
Аноним 27/03/17 Пнд 19:48:48 13704188
>>13702
Как же так? Я так вообще ничего не могу изучать, например.
Аноним 28/03/17 Втр 14:00:59 13745189
игнор.jpg 111Кб, 480x380
480x380
>>13694
>нужно быть наивным, что веровать в то, что машина тьюринга - это неебаца вычислитель, который может вычислить всё что вообще можно вычислить.
Машина тьюринга, как и любое равнообъемное ей уточнение понятия алгоритма (каноническая система Поста, лямбда-исчисление Черча, нормальный алгорифм Маркова и т.д.) - это именно неебаца вычислитель, которым можно вычислить все, что вообще в принципе вычислимо. То, что нельзя вычислить на машине Тьюринга, хуй ты вообще вычислишь.
>Ещё скажи что я на квантово-астрально-тёмноматериальном компьютере в 20 000 веке н.э. всё ещё не смогу решить проблему останова.
Нет, не сможешь. Тьюринг предлагал мысленный эксперимент - машина Тьюринга со встроенным оракулом, несуществующим всемогущим боженькой, который может решать алгоритмически неразрешимые задачи (пейпер: Turing, Alan (1938). Systems of Logic Based on Ordinals) Так вот, у такой машины с боженькой так же остается нерешенной проблема останова. Мораль? Проблема останова - это не проблема машины Тьюринга как таковой, а проблема существования в принципе невычислимых проблем.
>>13696
>Тупая машина даже не догоняет что такое бесконечность, что блять нет смысла её строить,
Будто ты догоняешь, умник. Или твое понимание бесконечности чем-то отличается от веры в нее. Брауэр именно об этом и писал, что проблема математики (кризис оснований н-р) в том, что там полно обобщений на общие, в т.ч. бесконечные случаи того, что работает на случаях конечных. Невычислимую же хуйню никак ты не вычислишь. Отказ от конструктивного подхода в данном случае манярешение уровня пикрелейтед, если проблему игнорировать - авось само как-нибудь рассосется. А хуй там плавал, не рассосется ничего.
Аноним 28/03/17 Втр 14:03:21 13746190
Конструктивный подход запрещает доказательство от противного?
Аноним 28/03/17 Втр 14:07:05 13747191
>>13746
Конструктивный подход запрещает неконструктивные доказательства. Т.е. доказательства, отличные от построимого объекта-доказательства. Отрицание должно быть построено, только тогда оно истинно констркутивно.
Аноним 28/03/17 Втр 14:27:53 13748192
>>13696
>Даже гипервычисления преодолевают halting problem, но конструктивисту религия не позволит об него мараться.
Гипервычисления - самая религия и есть. Полтора фрика уверовали, что можно объебать машину Тьюринга по вычислительным возможностям, при этом пока нет даже внятных теоретических обоснований, как это сделать. Все на уровне добрых намерений.
Аноним 28/03/17 Втр 18:01:50 13769193
>>13745
>>13748
Машина Тьюринга - тупое примитивное картофанское говно, а не формализм. Как и тезис Чёрча-Тьюринга, который любой здравомыслящий человек стесняется использовать в диалоге, усиляя его хотя бы до тезиса - Дойча.

>Нет, не сможешь.
Приплыли, умозаключение хуйзнает скольки летней давности лысой обезьяны с космической песчинки Земля - вершина теоретической вычислимости во Вселенной.
Любая МТ, что недетерменированная, что с оракулом - говно. И при чём тут боженька, если
Постулируется, что оракул способен решить определённые проблемы разрешимости за один такт машины Тьюринга.
что достаточно сильное ограничение.
Даже НМТ всё ещё обсирается работать с бесконечностями. Если Вселенная бесконечна, бесконечность нужно использовать для вычислений, МТ сосёт в них, следовательно МТ сосёт впринципе. Хотя причём тут бесконечности, она даже на квантмехе уже рыгает.

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

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

>Отказ от конструктивного подхода в данном случае манярешение
Маневрирование - это тупизм уровня древних греков, типа верю только в то что вижу, и числа чтоб перечислять существующие объекты. Не даром эти дауны застряли со своим ультрафинитизмом в жопе и площадь круга определить не могли, не говоря уже о пределах, производных и так далее. Кстати, иррациональные числа тоже не существуют? Напоминаю, что транзистерное говно зависнет, осторожно. Развитие в математике началось именно с момента, когда за неё взялись европейцы, которые любят бесконечность и не ссуца о ней размышлять, потмоу что она им естественна и интуитивно понятно. Быть конструктивным математиком = быть ссыклом из древней греции, где весь мир пластичен и точечен, и даже глядя в небо на звёзды нужно себя уверять, что это всего навсего отдельно стоящие исчислимые объекты, а не бесконечные неизмиримые и невычислимые дали.
Аноним 28/03/17 Втр 18:06:26 13773194
>>13748
Гипервычисления, это когда ты взял и перешагнул через манямирок про всемогущую МТ, не более.
Аноним 28/03/17 Втр 18:16:14 13778195
Brouwer.jpg 462Кб, 752x1083
752x1083
>>13773
>Гипервычисления, это когда ты взял и перешагнул через манямирок про всемогущую МТ, не более.
Но никто ведь не перешагнул. Как говорится, убьют - тогда и приходите.
>>13769
>Если Вселенная бесконечна,
А если не бесконечна? Насколько я понимаю, точного ответа на этот вопрос пока нет.
>Ну я не зависаю, когда ей оперирую, и мне хватает мозгов её не вычислять,
Ты так думаешь просто. Точнее, веруешь. Бесконечность невычислима, если ты нарисовал значок бесконечности и думаешь, что вычислил что-то - ты ебешь мозги самому себе. С таким же точно успехом можно пририсовать квантор существования к символу Аллаха и считать, что чего-то доказал.
>Тебе напомнить, почему этот говнтезис - всего лишь тезис?
Опровергнуть его все равно нечем, нравится тебе это или нет.
>Развитие в математике началось именно с момента, когда за неё взялись европейцы,
Которые ее и доразвивали до кризиса оснований, с которым уже больше 100 лет нихуя не могут поделать. Только один европеец (пикрелейтед) показал выход из этого тупика.
> А как оно может доказать - правильно, только построив.
А как можно доказать, не построив? Уверовать, что доказал? Расскажи.
Аноним 28/03/17 Втр 20:11:54 13790196
1489925894-f33f[...].png 21Кб, 400x382
400x382
Пенроуз привёл красивый пример. Пикрелейтед, ход белых. Человеку сразу ясно, что при правильной игре белых будет ничья. Но только лишь перебором это обосновать нельзя.
Аноним 28/03/17 Втр 20:20:41 13791197
>>13790
>Человеку сразу ясно, что при правильной игре белых будет ничья.
Человеку, знающему правила шахмат. И да, программы, умеющие в шахматы, перебором тоже не пользуются, там все сложнее. Так что пример вообще не в тему.
Аноним 28/03/17 Втр 20:38:28 13792198
>>13791
Пример иллюстрирует суть того, что под капотом бесконечности. Человеку ясно, почему будет так. Конструктивисты же - негодуют и требуют полного перебора.
Аноним 28/03/17 Втр 20:44:51 13793199
>>13792
>Пример иллюстрирует суть того, что под капотом бесконечности.
Пиздец. Шахматы - это не совсем бесконечность, во-первых. Во-вторых, это потенциально построимая бесконечность, т.к. есть правила ее построения (собственно, правила шахмат). Итого, шахматы со всеми возможными вариантами ходов - конструктивный объект. Что не имеет ничего общего с актуальной бесконечностью. Именно поэтому возможны программы, хорошо играющие в шахматы, более того, они совершенствуются, посколько суть таких алгоритмов - некоторая оптимизация выбора вариантов ходов. Хуйня пример, говорю же.
Аноним 28/03/17 Втр 21:12:12 13800200
Конструктивист и фанат нечеткой логики это один и тот же человек?
Аноним 28/03/17 Втр 21:27:45 13805201
>>13800
Какая разница?
Аноним 28/03/17 Втр 22:13:39 13812202
>>13793
>потенциально построимая бесконечность
Как машина убедиться в том, что этот конструктивный объект действительно обладает задаными свойствами (свойством бесконечности)?
Аноним 28/03/17 Втр 22:14:22 13813203
>>13812
>убедится

безграмотнофикс
Аноним 28/03/17 Втр 22:29:42 13816204
>>13812
А как ты сам убеждаешься в существовании у бесконечности свойства бесконечности (неограниченности/непрерывности)?
Аноним 28/03/17 Втр 23:24:52 13822205
>>13816
Начинаю строить эту бесконечность и зависаю, очевидно же.
Аноним 29/03/17 Срд 13:32:09 13834206
Снимок.PNG 55Кб, 715x544
715x544
>>13812
Конечность либо потенциальная бесконечность прямо следует из правил построения. Например, пикрелейтед правила построения множества N. Оно бесконечно в силу того, что для каждого a:N можно построить следующее за ним число через функцию следования succ(a):N.
Аноним 29/03/17 Срд 16:19:23 13839207
>>13702
>Проблема оснований математики успешно решена сто лет назад. Оказалось, что основания не нужны.
Чего? Это кто сказал, что основания не нужны?
Аноним 29/03/17 Срд 17:07:38 13842208
>>13839
Любой нормальный человек так скажет. Никаких нерешенных, острых проблем в основаниях сейчас нет. Всё закрыто.
Аноним 29/03/17 Срд 17:50:28 13845209
>>13842
>Никаких нерешенных, острых проблем в основаниях сейчас нет.
Да острых проблем нет. Но вовсе не оказалось, что "основания ненужны." Острых проблем нет потому что, фактически, произошла рецепция идей аксиоматической теории множеств в общематематическую культуру, разумеет, в сильно адаптированной форме. Аксиоматическая же теория множеств и была одним из подходов к преодолению кризису оснований начала 20-го века.
Аноним 29/03/17 Срд 18:02:22 13846210
>>13845
Острых проблем нет, да и вообще проблем нет, если не считать довольно странные исследования о всяких там континуумах Суслина и diamond-принципе.

Период, когда исследования в области оснований были важны и интересны буквально каждому математику, закончился ещё в первой половине двадцатого века. В наше время основания не нужны в том смысле, что новые статьи по основаниям не читает никто кроме трёх с половиной теоретиков оснований, а переписывания учебников на каком-то радикально новом языке в обозримом будущем вовсе не ожидается.
Аноним 29/03/17 Срд 18:24:01 13852211
>>13845
>кризис оснований
Как там теоретики оснований число один определили?
Аноним 29/03/17 Срд 19:07:40 13863212
Треда нет, спрошу тут: что почитать про automated theorem proving?
Аноним 29/03/17 Срд 19:18:09 13864213
>>13846
>странные исследования о всяких там континуумах Суслина и diamond-принципе.
Теория множеств и правда довольно выхолостилась на текущий момент.
> да и вообще проблем нет
Есть, конечно (я имею ввиду проблемы философии математики на которые потенциально могут пролить свет математические исследования). Например: 1. Что означает, что два доказательства по-существу одинаковые/разные? 2. Какие аксиомы на самом деле нужны в обычной математике (не логике)? 3. Какова правильная формализация теоретико-категорных построений?
Насколько я представляю ситуацию, по поводу 1. Ничего особенно убедительного до сих пор сделано не было. По вопросу 2. уже достигнут большой прогресс (см. обратная математика), тем не менее еще много чего можно сделать. По поводу более частного вопроса 3., некоторый прогресс безусловно имеется, но полностью удовлетворительной системы еще сформулировано не было.
>В наше время основания не нужны в том смысле, что новые статьи по основаниям не читает никто кроме трёх с половиной теоретиков оснований,
И собственно чем это отличается от многих других разделов математики? Ну и мода вещь приходящая - можно вспомнить, как недавно заметное количество алгебраических топологов потянулось заниматься теориями типов.
>а переписывания учебников на каком-то радикально новом языке в обозримом будущем вовсе не ожидается.
Ну собственно да, острой нужды в этом нет и не ожидается.

Аноним 29/03/17 Срд 20:00:55 13868214
>>13864
3. Вопрос неактуален. Очевидно, что для ∞-категорий оснований нет. Но они и не нужны никому, кроме сторонников веры, что у всего должно быть первопорядковое основание. Люди, которые пользуются инфинити-категориями, в основаниях не нуждаются.
Аноним 29/03/17 Срд 20:27:27 13869215
>>13868
>Люди, которые пользуются инфинити-категориями, в основаниях не нуждаются.
Учитывая, что вполне заметная их часть - это люди занимающиеся построениями моделей гомотопических теорий типов, тезис выглядит более чем сомнительно.
Аноним 29/03/17 Срд 22:08:24 13873216
>>3694 (OP)

Вопрос вообще простой. Есть у нас какая-то теория поля с лагранжианом $L = d_{\mu} \phi d^{\mu} \phi \ans - m|\phi|^2 - g|\phi|^4 $. Почему этот ебанный раздел все-еще не может в тех!?
Аноним 29/03/17 Срд 22:46:23 13876217
>>13791
>И да, программы, умеющие в шахматы, перебором тоже не пользуются
Схуяли? Да, там все сложнее, но в основе самый что ни на есть перебор.
Аноним 29/03/17 Срд 23:27:32 13877218
>>13873
[math] L = d_{\mu} \phi d^{\mu} \phi \ans - m|\phi|^2 - g|\phi|^4 [/math]
Аноним 29/03/17 Срд 23:54:40 13878219
latexmath.png 69Кб, 2105x627
2105x627
Аноним 29/03/17 Срд 23:56:47 13879220
Аноним 30/03/17 Чтв 00:25:00 13881221
>>13878
какой экстеншн ставить?
Аноним 30/03/17 Чтв 10:33:26 13914222
>>13881
>https://2ch.hk/faq/faq_sci.html
И замени строку
> // @include /^https?:\/\/2ch\.(hk|pm|re|tf|wj)/(sci|test)/
на
// @include /^https?:\/\/2ch\.(hk|pm|re|tf|wj)/(sci|math|test)/
Аноним 30/03/17 Чтв 12:42:36 13916223
Аноним 30/03/17 Чтв 14:26:27 13917224
>>13852
Никак. Кроме конструктивного определения других не завезли.
Аноним 30/03/17 Чтв 15:13:05 13918225
>>13917
Проорал с ко-ко-консруктивиста.
Аноним 31/03/17 Птн 05:13:53 13927226
>>13918
А что не так? N петух в свое время правильно говорил, что аксиомы Пеано исходят из того, что нам уже дано натуральное число. Формального определения нету. Не считая бурбаковского аутизма.
Аноним 31/03/17 Птн 15:29:57 13946227
>>13927
>аксиомы Пеано исходят из того, что нам уже дано натуральное число
Чушь.
Аноним 31/03/17 Птн 17:55:59 13953228
Снимок.PNG 50Кб, 1217x433
1217x433
>>13946
Схуяли чушь-то? Ты их читал? Давай разберем по частям.
- как видим, 1ая аксиома гласит, что 1 это натуральное число.
- далее определяется то, что в конструктивной математике называют функцией следования succ().
- далее некоторые свойства единицы, равенства и индукция.
Нигде нет определения, что такое единица, она просто вводится в 1ой аксиоме как готовый объект, в остальных аксиомах определяются некоторые ее свойства. Отсюда и вопрос - где формальное определение того, что есть 1? Нету его. Конструктивно я могу сказать, что по Маркову единица, как и любое натуральное число, является словом в алфавите |. Либо могу приплести нумералы Черча. Во всех этих случаях я даю конструктивное определение натуральному числу. Аксиомы же Пеано по-сути представляют собой правила построения N, не определяя явно, что есть натуральное число.
Аноним 31/03/17 Птн 20:59:35 13959229
Аноним 31/03/17 Птн 21:11:02 13961230
>>13953
>Ты их читал?
Более того, я могу их сформулировать по-человечески.
Непустое множество M называется множеством натуральных чисел, если:
1. Задана функция f:M→M.
2. Задана функция g:M→M.
3. Для любых x,y∈M верно, что f(x)=f(y).
4. Для любого m∈M верно, что g(m) ≠ f(m)
5. Для любых x,y∈M верно, что g(x)=g(y) → x=y.
6. Для любого X⊂M верно, что [f(M)⊂M ∧ ∀x [x∈X→g(x)∈X]]→X=M.

Функция f называется функцией выделения единицы. Единственный элемент множества f(M) обозначается 1.
Функция g называется функцией следования.
Аноним 31/03/17 Птн 22:58:33 13972231
>>13927
>N петух правильно говорил
Ясно.
Аноним 01/04/17 Суб 05:42:50 13991232
>>13961
Но твои правила с тем же успехом можно считать описанием множества вещественных чисел, конкретно N они не определяют. В отличие от моих конструктивгых определений конкретно множества N.
Аноним 01/04/17 Суб 05:45:41 13992233
>>13961
И да, единицу ты вводишь как уже предсуществующий объект, без определения его формально.
Аноним 01/04/17 Суб 11:20:13 13997234
>>13991
Нет, структуре вещественных чисел описанная мной структура не изоморфна.

>>13992
Структура Пеано - это то, чем могут обладать разные множества. Как структура группы. Ты же не жалуешься, что в аксиомы группы входит аксиома нейтрального элемента?
Я могу предъявить по крайней мере одно множество, обладающее структурой Пеано.
Аноним 01/04/17 Суб 12:08:12 14000235
>>13997
>Структура Пеано - это то, чем могут обладать разные множества.
Т.е. ты согласен, что это не определение конкретно N, а некие условия, под которые могут подпадать разные множества. Но тогда получается, что определения натурального числа из аксиом Пеано никак не следует.
>Нет, структуре вещественных чисел описанная мной структура не изоморфна.
А множеству дедекиндовых сечений?
Аноним 01/04/17 Суб 12:21:13 14004236
>>14000
>а некие условия, под которые могут подпадать разные множества
Именно так. Впрочем, в классе всех множеств, подпадающих под аксиомы Пеано, есть подкласс канонически выделенных множеств. Все такие множества изоморфны.

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

>множеству дедекиндовых сечений
Все множества со структурой вещественных чисел изоморфны.
Аноним 01/04/17 Суб 12:36:24 14005237
>>14004
>Натуральное число - это просто элемент некоторого множества со структурой Пеано,
Но если структурой Пеано могут обладать разные множества, а не только N, то твое заявление нуждается в пруфе изоморфности всех принципиально возможных множеств, обладающих структурой Пеано, согласись. Иначе опять же, формального определения нет.
Аноним 01/04/17 Суб 12:58:10 14006238
>>14005
Мы можем говорить о векторах, хотя не все векторные пространства изоморфны. Надо просто указывать пространство, которому принадлежит вектор. С натуральными числами точно так же - нельзя говорить о сферическом натуральном числе в вакууме, нужно указывать множество со структурой Пеано, элементом которого является это число.
Аноним 01/04/17 Суб 13:13:31 14007239
>>14006
>нужно указывать множество со структурой Пеано, элементом которого является это число.
Т.е. все то же множество N и его элемент - натуральное число. Определения которого у нас нет. Вот и пришли к тому, с чего начали.
>нельзя говорить о сферическом натуральном числе в вакууме,
Но ведь именно в этом суть формально-аксиоматического подхода. Из которого, в частности, следует истинность закона исключенного третьего - "А или не А", априори и безотносительно того, что есть "А" и "не А".
Аноним 01/04/17 Суб 13:17:50 14008240
>>14007
>Определения которого у нас нет.
Почему же? Есть определение канонического представителя класса изоморфных множеств со структурой Пеано, я могу его привести.
>именно в этом суть формально-аксиоматического подхода
Вот слово "вектор" для тебя законно?
Аноним 01/04/17 Суб 13:46:21 14011241
>>14008
>Есть определение канонического представителя класса изоморфных множеств со структурой Пеано, я могу его привести.
Но это не обязательно множество N или изоморфное ему, как мы выяснили выше, так? Сам же пишешь, что нужно явно указывать конкретное множество.
>Вот слово "вектор" для тебя законно?
Мы говорим об определении базового понятия - N. Вектор таковым не является, это просто подмножество векторного пространства, природа которого не конкретизируется его определением.
Аноним 01/04/17 Суб 13:56:21 14012242
>>14011
>или изоморфное ему
Почему же, обязательно. В стандартной теории множеств под натуральными числами, если не оговорено противное, понимается не просто какое-нибудь случайно выбранное множество со структурой Пеано, но одно вполне конкретное множество с такой структурой. Я могу его определить, если хочешь.
>подмножество
Опечатка?
>Вектор таковым не является
Термины "вектор" и "натуральное число" находятся на одном онтологическом уровне. Ни один из них не является более базовым, чем другой.
Аноним 01/04/17 Суб 14:48:23 14016243
>>14012
>В стандартной теории множеств под натуральными числами, если не оговорено противное, понимается не просто какое-нибудь случайно выбранное множество со структурой Пеано, но одно вполне конкретное множество с такой структурой. Я могу его определить, если хочешь.
Определи.
>Термины "вектор" и "натуральное число" находятся на одном онтологическом уровне. Ни один из них не является более базовым, чем другой.
Э, нет. Всю конструктивную математику можно свести к натуральным числам, т.к. к ним сводится любой конструктивный объект, как это показано у Мартин-Лёфа. Про вектор того же самого сказать нельзя, т.к. в общем случае это вообще почти все что угодно.
Аноним 01/04/17 Суб 15:38:31 14017244
>>14016
>Определи
Натуральными числами называется такое множество N, что
1. ∅∈N.
2. Если x∈N, то [x∪{x}]∈N.
3. В N нет собственных подмножеств со свойствами 1-2.

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

>вектор того же самого сказать нельзя
Вещественные числа - это векторное пространство, т.е. каждое вещественное число - вектор. Натуральные числа можно определить как подмножество вещественных чисел, см. анализ Зорича. Таким образом, всякое натуральное число - вектор, и всё, что сводится к натуральным числам, сводится и к векторам.
Аноним 01/04/17 Суб 15:43:09 14018245
>>14017
Что есть x∈N во второй аксиоме?
Аноним 01/04/17 Суб 15:48:26 14019246
Аноним 01/04/17 Суб 15:51:27 14020247
>>14019
Ну 0 понятно, пустое множество. А х что такое?
Аноним 01/04/17 Суб 15:53:10 14021248
>>14020
Кек. Ты тредом, похоже, ошибся.
Аноним 01/04/17 Суб 15:55:40 14022249
>>14019
Ну то есть, я что имею в виду. Твоя система аксиом в принципе повторяет >>13834 но там-то понятно, что a:N это натуральное число, которое к примеру есть нумерал Черча или хоть слово в алфавите | по Маркову. А у тебя х - это что? Определение его есть?
Аноним 01/04/17 Суб 15:56:40 14023250
>>14020
Всякий элемент N - это множество вида {∅, {∅}, {∅, {∅}}, {∅, {∅}, {∅, {∅}}}, ... }. Но вообще вторая аксиома - это просто формула ∀x[x∈N → [x∪{x}]∈N]. Ты ведь знаешь, что такое квантор, да?
Аноним 01/04/17 Суб 16:15:27 14024251
>>14023
Я знаю, что такое квантор. А это - {∅} у тебя что?
Аноним 01/04/17 Суб 16:19:47 14025252
>>14024
Множество, единственным элементом которого является пустое множество.

По определению,
0 := ∅
1 := {∅}
2 := {0,1} = {∅, {∅}}
3 := {0,1,2}
4 := {0,1,2,3}
5 := {0,1,2,3,4}
6 := {0,1,2,3,4,5}
7 := {0,1,2,3,4,5,6}
8 := {0,1,2,3,4,5,6,7}
9 := {0,1,2,3,4,5,6,7,8}
Чтобы определить остальные числа, удобно воспользоваться десятичной позиционной системой счисления.
Аноним 01/04/17 Суб 16:28:20 14026253
>>14025
Вот и до нумералов Черча добрались. Вместе с >>14017 правилами построения N. И что же во всем этом неконструктивного? Итого, пришли к >>13917
Аноним 01/04/17 Суб 16:31:04 14027254
>>14026
Это не нумералы Черча, это классическое определение по фон Нейману.
Аноним 01/04/17 Суб 16:32:36 14028255
>>14027
Но равнообъемное с нумералами Черча.
Аноним 01/04/17 Суб 16:33:28 14029256
>>14028
А также с кучей других вещей.
Аноним 01/04/17 Суб 17:04:37 14030257
>>14029
А значит, это конструктивное определение N.
Аноним 01/04/17 Суб 17:06:54 14032258
Аноним 01/04/17 Суб 17:09:14 14033259
>>14032
Потому что равнообъемно с конструктивным.
Аноним 01/04/17 Суб 17:10:08 14034260
>>14033
И разве это значит, что оно конструктивно?
Аноним 01/04/17 Суб 17:10:52 14035261
Аноним 01/04/17 Суб 17:12:15 14036262
>>14035
Ну хотелось бы пруф.
Аноним 01/04/17 Суб 17:36:44 14038263
>>14036
На каждой итерации ординалов фон Неймана и нумералов Черча получается одно и то же натуральное число.
Аноним 01/04/17 Суб 18:27:01 14041264
>>14038
У ординалов фон Неймана нет итераций.
Аноним 01/04/17 Суб 18:56:37 14044265
>>14025
Математики считают пустоту?
Аноним 01/04/17 Суб 19:08:48 14045266
>>14044
Её считают не только математики.
Аноним 01/04/17 Суб 19:36:59 14048267
Аноним 01/04/17 Суб 21:36:30 14056268
>>14044
Но ведь пустота это только Ø. Даже {Ø} это уже не пустое множество.
Аноним 01/04/17 Суб 22:02:21 14059269
>>14056
Тсс. Пусть думают, что мы умеем вычислять пустоты.
Аноним 02/04/17 Вск 05:31:00 14067270
>>14041
Не так назвал значит. Суть не меняется, пусть будет каждый последующий ординал фон Неймана равен каждому последующему нумералу Черча при условии отсчета их с нуля.
Аноним 02/04/17 Вск 23:22:46 14102271
>>14067
Окей. И как это влечет конструктивность?
Аноним 03/04/17 Пнд 19:08:07 14125272
>>14102
Элементарно. Есть две равнозначные системы. Одна из них конструктивная. Что можно сказать о второй?
Аноним 03/04/17 Пнд 20:23:17 14126273
>>14125
В общем случае - ничего. Иначе придётся признать конструктивным любое доказательство с использованием аксиомы выбора, для которого есть конструктивная альтернатива.
Аноним 03/04/17 Пнд 20:50:49 14128274
Снимок.PNG 80Кб, 565x650
565x650
>>14126
В общем случае - конструктивно все, что вычислимо/построимо и наоборот. Если что-то можно вычислить либо построить, или хотя бы дать правила для построения, то это что-то конструктивно.
Аноним 03/04/17 Пнд 21:06:44 14129275
Аноним 04/04/17 Втр 08:09:21 14140276
blob 5Кб, 227x115
227x115
Поясните нубу, допускает ли конструктивная математика пикрелейтед?
Аноним 04/04/17 Втр 15:19:50 14178277
>>14129
Выходит, ординалы фон Неймана конструктивны.
Аноним 04/04/17 Втр 16:04:40 14180278
>>14140
Сразу оговорюсь, что сам лично не стою на конструктивистских позициях.
Но насколько я понимаю, можно конструктивно показать, что данное бесконечное пересечение в самом деле описывает пустое множество, в том смысле что можно показать, что всякое число не принадлежит по крайней мере одному из пересекаемых множеств. При этом надо понимать, что с конструктивной точки зрения, нет причин полагать, что пересечение всякой последовательности допустимых совокупностей будет допустимо. Разумеется, в зависимости от сорта конструктивизма, здесь возможны разные уточнения.
Аноним 05/04/17 Срд 03:31:35 14217279
Аноним 05/04/17 Срд 04:24:23 14220280
>>14218
>(1,inf) intersect (2,inf) intersect (3,inf)
Да.
Аноним 05/04/17 Срд 08:24:13 14221281
>>14218
>>14140
Предположим, что бесконечное пересечение содержит точку А.
Тогда можно найти число m, такое что m > A, т.е. {A} ⊄ (m, ∞). Следовательно, пересечение пусто.
Аноним 05/04/17 Срд 08:32:24 14222282
>>14221
Это доказательство от противного. В конструктивной математике они запрещены.
Аноним 05/04/17 Срд 08:38:44 14223283
>>14222
Вопрос, как и ответ, со стакэксченджа. Интересует, как это доказывает конструктивная математика.
Аноним 07/04/17 Птн 14:56:45 14457284
blob 135Кб, 1527x749
1527x749
Как это всё соотносится с пикрелейтед?
Аноним 08/04/17 Суб 11:00:30 14511285
Вот Эвклид доказал, что множество простых чисел бесконечно от обратного. Конструктивная математика примет сие или потребует чего-то другого?
Аноним 08/04/17 Суб 17:01:50 14516286
>>14511
Его доказательство требует незначительной доработки напильником. В итоге получается программа, печатающая все простые числа.
База: напечатать 2.
Шаг: пусть напечатаны числа p1, ..., pn; проверяем все числа от pn + 1 до Пpi + 1 на простоту и печатаем наименьшее простое.

Выкладка Евклида выглядит теперь так: если все числа от pn+1 до Пpi составные, то Пpi + 1 простое. Это вполне себе конструктивно.
Аноним 08/04/17 Суб 17:03:18 14518287
Аноним 08/04/17 Суб 17:14:34 14520288
>>14140
а как конструктивно определить пересечение ряда множеств?
Аноним 08/04/17 Суб 17:19:42 14521289
>>14516
Затем, что в оригинальной формулировке разбирались случаи, является ли некоторое множество A конечным или бесконечным. Но это не конструктивно. Допустим, что множество A задается программой, которая по любому числу говорит "да" или "нет". Но в общем случае нельзя только по программе вычислить, конечно или бесконечно задаваемое ей множество.
Аноним 08/04/17 Суб 23:55:38 14527290
Аноним 17/04/17 Пнд 22:51:07 15180291
Selection027.png 94Кб, 929x837
929x837
Selection028.png 82Кб, 730x957
730x957
Вопрос по Coq. Только вкатился, начал читать туториал и не могу понять пример. Вот импликация лево- или правоассоциативна? A -> B -> C - это что означает?
Аноним 17/04/17 Пнд 22:58:53 15181292
>>15180
Все, уже понял.
Аноним 18/04/17 Втр 07:41:25 15201293
Я таки не понял. Теорема Геделя о неполноте не говорит, что конструктивная математика не работает?
Аноним 18/04/17 Втр 16:07:22 15309294
>>6020
>готовая спецификация для языка программирования с зависимыми типами, который может служить для доказательства теорем на компьютере.
Этот язык кто-то уже реализовал?
Аноним 18/04/17 Втр 17:54:30 15318295
deBruijn.gif 157Кб, 350x480
350x480
>>15201
>Теорема Геделя о неполноте не говорит, что конструктивная математика не работает?
Не говорит. В конструктивной математике всё выводимо, поскольку логические константы - это не просто буковы, которых много, а пруф-объекты, элементы своих типов/множеств. BHK-интерпретация логических констант и изоморфизм Карри-Говарда используются вместо абстрактной аксиоматики, в которой можно выразить недоказуемое в этой аксиоматике. Тогда как в случае конструктивной логики мы имеем дело только с построимыми объектами, доказуемыми, выводимыми и вычислимыми.
>>15309
>Этот язык кто-то уже реализовал?
Их полно в настоящее время, вышеупомянутый Coq >>15180 хотя бы. Проблема в том, что для работы с ними нужно понимание всей подноготной, лежащей в основе, иначе сложно оценить возможности, предоставляемые такими языками. Поэтому навыков быдлокодерства недостаточно. Первый успешный пример подобного языка - AUTOMATH де Брауна, это конец 60-х годов. Но там по факту всего лишь один из вариантов типизированной лямбды, MLTT, PTS, CoC, на которых основаны современные пруверы гораздо бодрее в этом плане.
Аноним 18/04/17 Втр 18:01:20 15319296
Как доказать проблему останова в конструктивной математике?
Аноним 18/04/17 Втр 18:02:11 15320297
>>15319
теорему об остановке

fix
Аноним 18/04/17 Втр 18:11:08 15321298
>>15319
Никак, это алгоритмически неразрешимая задача. Тьюринг это наглядно показал в примере машины Тьюринга с оракулом. Даже если у нас есть некий боженька, могущий в решение алгоритмически неразрешимых задач, проблема останова машины Тьюринга с встроенным боженькой все равно остается. Существуют алгоритмически неразрешимые, невычислимые задачи, это факт, с которым ничего не поделаешь.
Аноним 18/04/17 Втр 18:15:10 15322299
Это в неконструктивной математике принято веровать в т.н. "догму Гильберта" о том, что все задачи либо разрешимы, либо неразрешимы. В реальности же есть еще третий вариант "хуй его знает, разрешимо оно или нет по причине того, что в настоящее время решение неизвестно".
Аноним 18/04/17 Втр 18:20:27 15324300
>>15321
Как же Тьюринг доказал теорему об остановке? Он использовал неконструктивную математику для этого? В рамках конструктивной математики это сделать нельзя?
Аноним 18/04/17 Втр 18:23:40 15325301
>>15324
>Как же Тьюринг доказал теорему об остановке?
Он доказал, что это алгоритмически неразрешимая проблема.
Аноним 18/04/17 Втр 18:28:29 15326302
>>15325
Верно, он доказал, что проблема остановки - неразрешимая проблема. Меня интересует само доказательство. Оно везде приводися как доказательство от противного, что вроде бы недопустимо в конструктивной математике, так?
Аноним 18/04/17 Втр 18:28:52 15327303
>>15326
>алгоритмически неразрешимая проблема

fix
Аноним 18/04/17 Втр 18:30:49 15328304
Единственный на данный момент разумный вариант обойти проблему останова - не связываться с тьюринг-полными системами.
>>15327
А ты можешь предложить метод, не сводящийся к алгоритмическому, т.е. в общем случае к все той же машине Тьюринга?
Аноним 18/04/17 Втр 18:42:09 15335305
>>15328
Мой вопрос был лишь в том, является ли само доказательство теоремы об остановке конструктивным, и если нет - возможно ли построить его так, чтоб оно было конструктивным и если невозможно, то понять почему. Я конечно вообще нуб, но сейчас это выглядит так, как будто доказательство этой теоремы конструктивными методами невозможно по причинам, которые из этой же теоремы и выводятся. Т.е. во время доказательства теоремы, мы применяем следсвия из неё, что как бы странно, ведь мы её ещё не доказали.
Аноним 18/04/17 Втр 19:36:50 15386306
>>15318
Не существует конструктивного доказательства изоморфизма Карри-Говарда.
Аноним 18/04/17 Втр 19:46:31 15394307
>>15386
Чего несешь? Изоморфизм Карри-Говарда - построение множества конструктивных пруф-объектов. Наличие таких построений есть конструктивное доказательство возможности рассматривать пропозишены как множества пруф-объектов.
Аноним 18/04/17 Втр 19:57:35 15395308
>>15394
...при условии, что у нас доказан изоморфизм Карри-Говарда. Но именно его мы доказываем.
Аноним 18/04/17 Втр 22:23:44 15419309
То есть ответ на вопрос разрешима ли проблема останова на МТ в конструктивной математике - это "хуй знает"?
Аноним 19/04/17 Срд 01:17:21 15436310
Типизированность языка значит, что записать можно только корректные построения/доказательства, иначе “не компилируется”, а доказательства являются такими же объектами как и другие математические объекты (например, множества). Тот аспект, что непрерывность здесь выступает как правилом синтеза, так и обоснования получает выражение в гомеоморфной теории типов (Homotopy Type Theory, HoTT) и программе унивалентных оснований математики (UniMath) Владимира Воеводского (конец 2000-х годов). HoTT базируется на взаимосвязи между гомотопическими типами пространства (непрерывными отображениями) и типами в языках программирования. UniMath — программа построения средствами HoTT универсального формального языка, который обеспечивает возможность алгоритмической проверки правильности доказательств, и, одновременно, представляет собой конструктивные основания для современных разделов математики. Благодаря математическому содержанию, вложенному в теоретико-типовые понятия, на языке теории удается выразить и верифицировать результаты из абстрактных разделов математики, которые ранее считались не формализуемыми программными средствами.

HoTT и UniMath, таким образом, ― фреймворк для “делания математики” как программирования. Основное преимущество состоит в том, что он, буквально gets equality right. Т.е. понятие “равенства” впервые в истории математики описывает равенство объектов в настолько же сильном смысле, как оно используется на практике в неформальных доказательствах. Это преимущество достигается за счет использования топологического инструментария По-сути, Воеводский сводит все здание математики к топологическим операциям. Формальной основой для теории Воеводского явилась конструктивная теория типов Мартина-Лефа. Открытие Воеводского состояло в том, что он нашел геометрическую (гомотопическую) интерпретацию теории типов, позволившую исследовать богатую структуру отношений тождества, которая без этой интерпретации оставалась “невидимой”: тип a = b теперь интерпретируется не как тип доказательства равенства a и b, а как тип сохраняющих структуру обратимых переходов от a к b. При этом аксиома унивалентности Воеводского постулирует равенство объектов, между которыми может быть установлена эквивалентность, ― как равные рассматриваются изоморфные, гомеоморфные и другие гомотопически эквивалентные структуры.

Идея использования HoTT также в качестве математического основания физических и других естественно-научных теорий, мотивируется формальным характером теории типов и аксиомы унивалентности, что позволяет смотреть на HoTT и UniMath не только как на геометрическую теорию, но и как на своего рода геометризованную “логику” [Hartnet, 2015].
Аноним 19/04/17 Срд 11:03:18 15452311
Снимок.PNG 43Кб, 574x369
574x369
>>15395
Применимость = доказательство. Конструктивные системы вычислимы и выводимы сами из себя, без внешних дополнений. Именно это делает конструктивную логику полной по Геделю. Любая конструктивная аксиоматика - сама по себе конструктивный объект, правила вывода в ней - тоже. Поэтому корректность системы выводима из нее самой. Это азы, так-то. Именно подобные свойства конструктивных логик, того же изоморфизма Карри-Говарда, дают возможность строить проверяемые доказательства теорем, а интерпретация логических констант по Колмогорову - и писать абсолютно корректные программы на языках с зависимыми типами.
>>15436
Истину копипастишь. НоТТ - очень крутая вещь, но в зачаточном состоянии пока что.
Аноним 19/04/17 Срд 11:17:25 15453312
>>15452
Почему она в таком состоянии? Что там пока не так? Сколько это будет продолжаться?
Аноним 19/04/17 Срд 11:28:17 15455313
photoNormal.jpg 61Кб, 600x450
600x450
>>15453
Потому что это очень новое направление конструктивной математики. И сколько бы выдающихся умов над ней не работали, все равно за какие-то несколько лет невозможно проделать всю работу. В НоТТ книге описаны открытые проблемы. Радует, что с самого начала эту теорию пилили очень правильно - сразу в пруверах, чтобы поменьше аутизма, побольше фактического материала. Да и все доказательства с самого начала проверены, это значит, что в дальнейшем не вылезет никакой нежданчик, который просто не заметили сразу. По хорошему, нужны сразу пруверы с ядром на НоТТ, но такой пока что только один - LEAN.
Аноним 19/04/17 Срд 17:26:11 15490314
VOEVODSKIIVladi[...].jpg 661Кб, 1000x1334
1000x1334
Кому интересно, онлайн-версия библиотеки НоТТ для Coq на жабаскрипте - https://x80.org/rhino-hott/ можно гонять конструктивные основания прямо в браузере.
Аноним 19/04/17 Срд 19:18:11 15507315
>>15490
Быстрее окамл установить чем ждать пока оно загрузится.
Аноним 19/04/17 Срд 19:55:18 15511316
>>15455
>что в дальнейшем не вылезет никакой нежданчик, который просто не заметили сразу
А тут PA возьми и окажись противоречивой (а соответственно и все мало-мальски сильные теории типов). Или найдется ошибка в ядре Coq. Ну или, скажем, систематическая ошибка во всех процессорах архитектуры x86, что повлекло положительную проверку неверных доказательств. Последнее, положим, выглядит крайне маловероятно. Но тем не менее, формализация на компьютере не дает абсолютных гарантий.
Аноним 20/04/17 Чтв 00:10:28 15537317
В редукции математических доказательств Брауэр и Вейль доходят до интуитивного фундамента полной индукции и рассматривают ее как математическую "праинтуицию". Как математики, они имеют право поступать таким образом. Математики не обязаны исследовать вопрос о том, как получаются понятия, которые они кладут в основу доказательств математической науки в качестве исходных и недоказуемых. Но как философски мыслящие математики (а они сами себя считают такими) "интуиционисты" не имеют права на этом останавливаться. Они обязаны, дойдя до "праинтуиции" математики, вести свою редукцию дальше "назад". Они обязаны ответить на вопрос о генезисе самой этой "праинтуиции". Они обязаны точно и обстоятельно разъяснить, в чем состоят признаки "интуитивной ясности", на которую они постоянно ссылаются, но которая без соответствующих разъяснений легко может быть смешана с субъективной "оценкой" сознания, лишенной общезначимого и, следовательно, научного содержания.

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

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

Канторовская интуиция актуальной бесконечности лишена обязательности в глазах "интуиционистов". Они отказались признать за ней непосредственность и совершенную ясность внутреннего видения, на которые ссылался, как мы видели, Георг Кантор. Это разногласие существенно не только для математики, но и для гносеологии. Оно показывает, что в самом понятии интеллектуальной интуиции не было безусловной ясности и существовала возможность, а следовательно, и опасность субъективной иллюзии. И это не удивительно. Ссылка на непосредственность интеллектуальной интуиции используется в редукции математического обоснования. Но она не может быть последней инстанцией в философской редукции происхождения знания. Для гносеологического объяснения интеллектуальная интуиция не беспредпосылочное абсолютное начало знания, а его среднее звено. Его последующие звенья – положения, обосновывающиеся на интеллектуальной интуиции. Его первичное звено, составляющее предмет исследования уже не математики и вообще не специальных наук, а теории познания, – материальная практика общественного человека в ее историческом развитии. Интуиция как функция человеческого познания имеет свою историю. Корни этой истории глубоко уходят в почву практики. По верному разъяснению итальянского математика и логика Энрикеса, первоначальные математические интуиции, например в геометрии, "возникли путем идеализированного опыта, который неоднократно повторялся при состоянии интеллекта, предшествовавшем полному развитию сознания" (6, 16).

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

Их идеализм был не только догматичен и не только метафизичен по методу, неспособному применить генетическую точку зрения к самому явлению интуиции в человеческом мышлении. Он, кроме того, был агрессивен по своей направленности и нетерпим. Правильно утверждая, что построение в математике подчиняется логике решения проблем, отличной от классической, "интуиционисты" типа Брауэра и Вейля полагали, будто только эта логика имеет право на признание в математике. Вразрез с этой точкой зрения академик А.Н.Колмогоров показал, что между принципами классической логики и принципами "конструктивной" логики "интуиционизма" не существует отношения исключающего противоречия: "интуиционистская" логика есть логика новой и особой области исследования, ею не исключаются принципы доинтуиционистской логики; они лишь подвергаются ограничению там, и только там, где это ограничение вызывается своеобразием исследуемой области объектов.
Аноним 20/04/17 Чтв 01:38:47 15540318
>>15537
damn
Колмогоров bitchslapped Брауэра также как Лузина.
Аноним 20/04/17 Чтв 06:05:57 15546319
>>15544
Это не определения. Это нонсенс.
Когда в конструктивных исследованиях будут открыты новые интересные математические факты? Какие теоремы доказаны конструктивистами? Где интуиционистские теоремы Пуанкаре? Где интуиционистские интегральчики?
Аноним 20/04/17 Чтв 07:25:29 15548320
Errett Bishop, in his 1967 work Foundations of Constructive Analysis, worked to dispel these fears by developing a great deal of traditional analysis in a constructive framework.

Even though most mathematicians do not accept the constructivist's thesis, that only mathematics done based on constructive methods is sound, constructive methods are increasingly of interest on non-ideological grounds. For example, constructive proofs in analysis may ensure witness extraction, in such a way that working within the constraints of the constructive methods may make finding witnesses to theories easier than using classical methods. Applications for constructive mathematics have also been found in typed lambda calculi, topos theory and categorical logic, which are notable subjects in foundational mathematics and computer science. In algebra, for such entities as toposes and Hopf algebras, the structure supports an internal language that is a constructive theory; working within the constraints of that language is often more intuitive and flexible than working externally by such means as reasoning about the set of possible concrete algebras and their homomorphisms.

Physicist Lee Smolin writes in Three Roads to Quantum Gravity that topos theory is "the right form of logic for cosmology" (page 30) and "In its first forms it was called 'intuitionistic logic'" (page 31). "In this kind of logic, the statements an observer can make about the universe are divided into at least three groups: those that we can judge to be true, those that we can judge to be false and those whose truth we cannot decide upon at the present time" (page 28).
Аноним 20/04/17 Чтв 07:33:44 15549321
>>15547
Проинтегрируй sin конструктивно.
Аноним 20/04/17 Чтв 07:43:45 15550322
>>15547
Ясно все с вашим анализом.

... возможны и необычные с традиционной точки зрения функции: напр., построена к. ф., всюду определенная, непрерывная на единичном сегменте и не ограниченная на нем (см. [17]). Не имеет аналогов в традиционном анализе и теорема, согласно к-рой всякая к. ф. конструктивно непрерывна в любой точке, в к-рой она определена (см. [18]).
...

Так, доказана невозможность следующих алгоритмов (в смысле одного из уточнений понятия алгоритма): 1) распознающего для произвольного конструктивного действительного числа равно оно нулю или нет; 2) находящего для каждой сходящейся к. п. р. ч. то к. д. ч., к к-рому она сходится; 3) находящего для каждой совместной системы линейных уравнений (над полем к. д. ч.) какое-либо ее решение; 4) находящего для каждой непрерывной кусочно линейной знакопеременной функции корень этой функции; 5) находящего для всякой непрерывной кусочно линейной на единичном сегменте функции ее интеграл Римана по этому сегменту. К этому же кругу результатов принадлежит и следующая теорема, полностью решающая вопрос о возможности эффективного перехода от одной системы счисления к другой: алгоритм, находящий для всякой m-ичной конструктивной дроби равную ей n-ичную конструктивную дробь, возможен тогда и только тогда, когда множество простых делителей псодержится в множестве простых делителей т(см. [6]). (В частности, возможен алгоритм перехода от десятичной системы счисления к двоичной, но невозможен алгоритм перехода от двоичной системы к десятичной.)
Аноним 20/04/17 Чтв 11:56:11 15560323
>>15552
>Любой возможныц алгоритм изначально конструктивен
Незавершающийся тоже?
Аноним 20/04/17 Чтв 12:40:36 15566324
>>15552
Алгоритма перехода от двоичной системы к десятичной не существует.
Аноним 20/04/17 Чтв 13:10:52 15567325
>>15566
Для конечной двоичной дроби алгоритм очевиден.
Для периодической тоже.
Видимо там речь идёт о каких-то специфичных дробях.
Аноним 20/04/17 Чтв 13:16:23 15568326
>>15544
Актуальная бесконечность - ясная ментальная контрукция, мыслить её элементарно, если ты не инвалид с МТ вместо мозга, - это просто одновременное пребывание всех объектов, вроде бесконечной вселенной или бесконечности углубления в атом. При этом это одновременное существование само легко абстрагируется до объекта. Человеческий мозг не мыслит шагами и вычислениями, он мыслит зависимостями и отношениями. А ты просто даун-футуролух с машин лёрнингом головного мозга, которому бомбит что из транзистерных говен не сделать сознания, сколько мощностей не докидывай.

Но речь всего лишь о том, что ментальная конструкция "ещё один шаг", такая же идеалистическая: нет совершенно никаких причин считать её более обоснованной, чем актуальную бесконечность.
Аноним 20/04/17 Чтв 16:25:28 15596327
>>15544
>Брауэр совершенно точно определяет, что есть праинтуиция, на которой основаны все дальнейшие построения.
Будьте добры, приведите это определение.
Аноним 20/04/17 Чтв 16:59:05 15598328
>>15572
Ты не предлагаешь ничего конструктивного, простите за каламбур. Ты просто кукарекаешь, что актуальная бесконечность плохая, её пользователей надо репрессировать. По делу ничего не говоришь.

>>15596
inb4 кукареканье про акты интуиционизма на немецком
Аноним 20/04/17 Чтв 23:02:47 15644329
>>15598
Я нигде не говорил что пользователей актуальной бесконечности надо репрессировать. Что я говорил и буду говорить по этому поводу, так это то, что актуальная бесконечность это не математика, а религия, поскольку она не вычислима и в нее надобно веровать. Ок, веруйте. Но это не математика. По делу я как раз много говорю, просто не в коня корм, как говорится, что и взять с мейлру. В частности, сто раз объяснял, почему манядоказательства с актуальной бесконечностью это религия, а не математика. Но это и Брауэр объяснял еще в 1907 году.
Аноним 20/04/17 Чтв 23:05:42 15645330
>>15596
Я его приводил даже в виде картинок. Ну и цитаты самого Брауэра, разумеется. Толку'то хуй. Сложна слишком, наверное.
20/04/17 Чтв 23:48:57 15653331
>>15644
>поскольку она не вычислима и в нее надобно веровать
А разве вера только в вычислимое не является верой?
Аноним 21/04/17 Птн 01:05:32 15678332
>>15653
Вычислимость является математикой и работает без всякой веры, т.к просто вычтсляется. Вера начинается там, где заканчивается вычислимость и построимость. Построение, оно просто есть, без всякой дополнительной веры.
Аноним 21/04/17 Птн 15:51:15 15698333
>>15678
Построение на уровне "ещё один шаг" такое же умозрительное, т.е. такая же вера.
Аноним 21/04/17 Птн 16:51:03 15699334
>>15698
Еще раз. Абстракция потенциальной осуществимости по Маркову или трансфинитная индукция (конкретно по Мартин-Лёфу) - это бесконечность, взятая из правил построения объекта. Бесконечность, ассоциированная с правилами построения, о ней можно говорить только в контексте таких правил. Абстракция актуальной бесконечности - это бесконечность, не ассоциированная ни с чем, т.к. нет никаких общих правил ее получения. "Еще один шаг" построим в случае наличия правил построения, некая бесконечность сама по себе - вера уровня боженьки.
Аноним 21/04/17 Птн 18:13:31 15702335
>>15699
Но объект же нельзя построить используя его правила построения. Ты можешь только верить что потенциально это возможно.
Аноним 21/04/17 Птн 18:21:37 15703336
>>15702
>Но объект же нельзя построить используя его правила построения.
Тебе слово "абстракция" о чем-то вообще говорит? Или lazy evaluation?
Аноним 21/04/17 Птн 19:09:03 15707337
>>15703
Ещё раз, конструктивный объект [1, 2, ..] - нельзя построить. Он живёт только у тебя в голове. ∞ - тоже живёт только у тебя в голове, так в чём проблема?

∞ - это просто результат вычисления [1, 2, ..] на любом сверхтьюринговом вычислителе. ∞ - это, когда все шаги были сделаны.

Актуальную бесконесноть очень легко мыслить, для этого достаточно ощущать мир как безграничную протяжённость одновременно пребывающих объектов. Для потенциального 4хмерного существа наш 3хмерный мир с шагами выглядит как полностью развёрнутый, где нет никакого до, сейчас, дальше и ещё дальше, они прибывают все вместе.
Аноним 21/04/17 Птн 19:34:28 15710338
>>15707
>Актуальную бесконесноть очень легко мыслить
Все, что угодно очень легко мыслить. Однако, если мыслимое не имеет правил построения, то это не ментальная конструкция в смысле интуиционизма, не построимый объект (хотя бы в виде абстракции потенциальной осуществимости такого построения), а значит и не математика.
>на любом сверхтьюринговом вычислителе
Которые, как показал Тьюринг еще в 30-х годах, невозможны даже с оракулом, ага. Я тебя услышал.
Аноним 21/04/17 Птн 21:20:59 15729339
Конструктивные математики это просто люди с МТ головного мозга?
Аноним 21/04/17 Птн 21:32:29 15731340
quote-one-canno[...].jpg 71Кб, 850x400
850x400
>>15729
МТ, как и конструктивная логика Гейтинга, например, не формализует интуиционизм Брауэра. Гейтинг даже объяснял, почему. Но там не для мейлру объяснние, тут даже в разницу между актуальной и потенциальной бесконечностью не могут или в понимание пикрелейтед цитаты. С другой стороны ты все равно не назовешь ничего вычислимого, что не сводилось бы к машине Тьюринга. У тебя на этот счет нет ничего кроме веры, что МТ это что-то плохое.
Аноним 21/04/17 Птн 22:15:26 15733341
>>15710
>Однако, если мыслимое не имеет правил построения, то это не ментальная конструкция в смысле интуиционизма, не построимый объект
А у самих правил построения есть правила построения?
Аноним 21/04/17 Птн 22:21:29 15734342
>>15707
Ты бы лучше на палочках пояснял.
Взяли одну палочку | - конструктивный объект
Дорисовываем палочки | к |.. - конструктивный процесс.
В теории палочки можно дорисовывать бесконечно. Но лучше применять какое-то кодирование, вводить уже систему счисления и тд.

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

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

Но это я с дивана пишу. Я вообще больше мамин философ.
Аноним 21/04/17 Птн 22:21:44 15735343
>>15733
Твой вопрос тупой.
Все тупые вопросы я буду игнорировать.
(Автор этого поста был предупрежден.)
22/04/17 Суб 00:13:25 15738344
>>15735
А почему тупой? Тем, что тебе не нравится и ломает твою маня-идеологию?
>Все тупые вопросы я буду игнорировать.
Веруны тоже игнорируют доказтельство того, что в их книжках полная туфта.
(Автор этого поста был предупрежден.)
Аноним 22/04/17 Суб 05:05:47 15742345
>>15733
Есть. И я даже сто раз писал об этом с цитатами. Сами правила тоже конструктивный объект, как и результаты вывода по ним. Все выводимо и проверяемо, никакой веры.
Аноним 22/04/17 Суб 05:09:21 15743346
>>15738
Это какой'то подгоревший пишет. Про правила вывода сто раз все разжевано уже с цитатами, даже в этом треде выше. Суть в том, что все выводимо из самих конструктивных объектов.
Аноним 22/04/17 Суб 05:13:15 15744347
>>15734
Нет, ты не понял. Актуальная бесконечность это бесконечность сама по себе, не связанная ни с каким объектом, ни с какими правилами построения чего'либо.
Аноним 22/04/17 Суб 09:33:35 15745348
>>15742
>Все выводимо и проверяемо, никакой веры
Только в рамках аксиом, принятых в данной конкретной математической системе, и только по принятым в ней же правилам вывода из них.
Да и то. Обычно с периодическим маханием руками "да, вот тут у нас обнаружился неудобный парадокс, ну и хрен с ним, будем обходить это место".
Аноним 22/04/17 Суб 09:42:00 15746349
>>15745
Да ты и правда не очень умный. Тебе же говорят, сами правила тоже конструктивные объекты, как и вывод по ним. Корректность вывода в таких системах,, это так же конкретное построение.
Аноним 22/04/17 Суб 09:45:46 15747350
>>15745
И никаких парадоксов со времен самого Брауэра. Т.н парадокс Жирара фиксится элементарно введением иерархии вложенных универсумов вместо неконструктивного общего правила, который его и вызывал. Других антиномий вообще не завезли.
Аноним 22/04/17 Суб 10:13:42 15749351
>>15747
Ну и в чем тогда преимущество по надежности перед, "религией" (теорией множеств). И там и там, неаккуратная формализация приводила к парадоксам. И там и там все пофиксили переходом к предикативным построениям. Иными словами не видно, чтобы интуиция касательно интуиционистской математики давала меньше сбоев, чем интуиция касательно теоретико-множественной.
Аноним 22/04/17 Суб 10:50:39 15750352
>>15749
Очень важное, хотя и не единственное преимущество конструктивного подхода - его автоматизируемость, в частности, непосредственная реализуемость на комплюктере, без дополнительных костылей, прямо в соответствии с колмогоровской интерпретацией логических констант и изоморфизмом Карри-Говарда (программы как доказательства). С неконструктивными аксиоматиками так не выйдет, комплюктер ты веровать не заставишь, а невычислимое оно и в африке невычислимое, правил для его вычисления нет. Причем, как сказано выше, проверяемы на корректность и сами правила проверки на корректность, что означает тотальную корректность и выводимость той же MLTT. С ZFC ничего даже близко подобного не выйдет, хотя костыльные реализации и возможны, все через те же типы, н-р в Coq'е.
Аноним 22/04/17 Суб 10:55:22 15751353
>>15749
>И там и там, неаккуратная формализация приводила к парадоксам.
К слову, интуиционизм Брауэра не формализуем, о чем говорил в т.ч. создатель интуиционистской логики Гейтинг, и парадоксов там не было, нет и не может быть принципиально, поскольку это не какая-то там формальная система.
Аноним 22/04/17 Суб 11:08:37 15754354
>>15743
Я говорил о том, естил у консрктивного объекта правило построение правил построения? И правил построения есть ли правила построение правил построения правил построения?
Аноним 22/04/17 Суб 11:49:50 15757355
>>15750
>в частности, непосредственная реализуемость на комплюктере
Ну смотри, в теории множеств я могу доказать, например, что всякий фильтр расширяется до ультрафильтра, что вполне подходит под твое замечание про отсутствующую реализации на компьютере. В тоже время MLTT, и многих других естественных интуиционистских теориях, несложно доказать, что для всюду определена супер-экспоненциальная функция (supexp(0)=1, supexp(n+1)=2^{supexp(n)}). Но не то, чтобы вычисление supexp(10) могло быть реализовано на реальном компьютере. То есть эта реализуемость в общем случае носит совершенно абстрактный характер. Если же хочется реализуемость на реальном компьютере, то нужна вычислимость с адекватной сложностью. Но если хочется доказать, например, что некоторые объекты не просто существуют, а могут быть найдены за полиномиальное время, то дополнительные усилия потребуются и в конструктивных и в некоструктивных системах.
Аноним 22/04/17 Суб 13:03:30 15762356
>>15754
Все есть. Меня правда, несколько подзаебало пояснять в пустоту. Если бы ты понимал такие темы как интерпретация логических констант по Брауэру-Гейтингу-Колмогорову, натуральная дедукция Генцена-Правитца, изоморфизм Карри-Говарда, куб типизированных лямбда-исчислений а-ля Черч Барендрегта, наконец-таки MLTT, то м.б. что-то и вынес бы из моих объяснений. А так, все это выглядит как лекция в детском саду про мочидзукину теорию пространств Тейхмюллера.
>>15757
Закон исключенного третьего все равно придется выбросить, т.к. он невычислим. Но, если мы выкидываем из некоей аксиоматики невычислимую хуету, остается что-то более-менее заменимое на конструктивную логику.
Аноним 22/04/17 Суб 15:22:53 15775357
Как конструктивная математика может может формализировать некоторые невычислимые вещи, такие, как Spectral gap (важная вещь в физике)?
Аноним 22/04/17 Суб 16:18:48 15788358
Так что, кто-то запилит конструктивное доказательство теоремы остановки веруна Тьюринга? Или так дальше и придётся веровать что проблема остановки неразрешима на МТ?
Аноним 22/04/17 Суб 16:31:22 15790359
>>15788
Факт в том, что существуют алгоритмически неразрешимые проблемы.
Аноним 22/04/17 Суб 17:10:07 15796360
>>15790
Большинство алгоритмически неразрешимых проблем доказовались таковыми путём сведения к проблеме остановки, неразрешимость которой вроде как доказана. Но доказана она неконструтивно, вот в чём проблема.
Кстати, доказательство, что задача определения того, является ли частично рекурсивная функция с данным описанием общерекурсивной или нет, алгоритмически неразрешима - так же проведено неконструтивно.
Получается, что в рамках конструктивной логики вообще нет доказательств существования алгоритмически неразрешимых проблем?
Аноним 22/04/17 Суб 17:21:41 15797361
>>15796
Ты бы хоть погуглил, что вообще есть кончтруктивная математика. Конструктивное доказательство - это построение.
Аноним 22/04/17 Суб 19:54:35 15802362
>>15797
Ну и отказ от правила исключения третьего. Следовательно - отказ от доказательства от противного. Все доказательства того, что проблема алгоритмически неразрешима - проводятся от противного, как, например, доказательство теоремы останова у Тьюринга.
Мой вопрос, как в конструктивной математике доказать что та или иная проблема алгоритмически неразрешима? Это вообще возможно?
Аноним 23/04/17 Вск 01:33:00 15881363
>>15802
> отказ от доказательства от противного
Если у тебя есть утверждение вида "не А", например, "не (разрешимо что-то)", то ты имеешь полное конструктивное право сказать "предположим, что A, приведем к противоречию и вуаля". Это только с точки зрения классической математики может показаться, что тут что-то противное, а так вообще-то в любом варианте "не A" можно считать синонимом "если А, то ложь". А нельзя наоборот, A доказывать через приведение "не А" к противоречию.

Поэтому все утверждения о неразрешимости доказываются в конструктивной логике безо всяких проблем.
Аноним 23/04/17 Вск 04:46:59 15890364
>>15802
Я в каждом втором посте говорю о конструктивной интерпретации логических констант. Любое доказательство допустимо, если оно построимо, никто не против принципа исключенного третьего в случаях когда он доказуем. То же про конструктивное отрицание и т.д. есть отказ от веры в общие принципы без общего метода их построения, а вовсе не какие'то догмы уроынч 'отказа от принципа исключенного третьего потому что богородица не велит'.
Аноним 23/04/17 Вск 11:01:57 15901365
А можно меня, мимокрокодила, ввести в краткий курс дела. Чем примечательна конструктивная математика? Она примечательная только в основаниях математики или же это что-то типа "ко-ко-революции" в математике?
Аноним 23/04/17 Вск 11:23:14 15902366
>>15901
Конструктивная математика примечательна тем, что это настоящая математика, построимая и вычислимая. Без мутных верований в невычислимые вещи, от которых одни кризисы и неполнота.
Аноним 23/04/17 Вск 12:21:56 15906367
>>15901
Конструктивная математика примечательна тем, что доказательства и объекты строятся из одного и того же материала, а в классической математике они строго разделены.

Допустим, у тебя есть выражение sqrt (ln 1/x). Оно в программистских терминах выбрасывает исключения, то есть на самом деле оно в классической математике формально означает следующее:

case (case (if x != 0 then 1/x else \bot) of
| \bot -> \bot
| t -> if t > 0 then ln t else \bot
end) of
| \bot -> \bot
| t -> if t >= 0 then sqrt t else \bot
end
и к этому выражению еще нужно прицепить доказательство того, что оно не равно \bot для интересующих тебя x.

А в конструктивной математике sqrt (ln 1/x) означает let z <- div(1,x,доказательство x != 0),
y <- ln(z, доказательство z > 0)
in sqrt(y, доказательство y >= 0).

Вот поэтому большинство proof checker'ов основаны на конструктивной логике. Даже если пришить к ним пятую ногу закон исключенного третьего, они все равно по сути конструктивны.
Аноним 23/04/17 Вск 13:00:54 15912368
>>15906
Это не математика. Это быдлокод. Какая идея стоит за этим кодом? Да никакой.
Аноним 23/04/17 Вск 13:21:34 15924369
>>15906
Ну и чем принципиально отличается
if(x != 0) и if(t >= 0)
от
(доказательство x != 0) и (доказательство z > 0)
?

Из пустое в порожнее, ей богу.
Как раз однородность потеряна, вмето ондородной программы на термах, получили неоднородную с термами и типами (доказательствами).
Аноним 23/04/17 Вск 13:23:38 15929370
>>15912
Нет, это как раз математика. Быдлокод это невычислимые маняаксиомы, в которые по причине их невычислимости остается только веровать.
Аноним 23/04/17 Вск 13:31:27 15935371
>>15929
Математика > вычислимость.
Аноним 23/04/17 Вск 13:38:49 15946372
>>15935
Математика = вычислимость. Иначе это не математика.
Аноним 23/04/17 Вск 14:49:07 15972373
>>15929
Ты постишь в прямом смысле быдлокод и называешь его математикой. Быдлокод - не математика, поэтому ты вызываешь ненависть.
Аноним 23/04/17 Вск 20:36:57 16068374
>>15924
> Ну и чем принципиально отличается
> if(x != 0) и if(t >= 0)
> от
> (доказательство x != 0) и (доказательство z > 0)
> ?

Первому выражению еще недостает доказательства его корректности, а во второе выражение это доказательство уже встроено.

>>15920
> Нахуй тебе доказательтво
Нахуй тебе математика
Аноним 24/04/17 Пнд 12:49:40 16123375
дебилыматематика.jpg 60Кб, 600x433
600x433
>>16007
>бисконечность рабаты посчитать нимогут=(
Ты будто можешь, чучело. Еще раз, для самых одаренных математиков: пририсовывание квантора существования к символу Аллаха не является математическим доказательством Аллаха. Что тут непонятно-то? Дебилы, блядь. Думают, нарисовали значки бесконечности, закона исключенного третьего и т.д. и что-то этим доказали.
>>16029
Еще один гейний математики.
Аноним 24/04/17 Пнд 13:08:39 16132376
>>16123
Квантор существования не может быть пририсован к Аллаху, потому что Аллах - терм. А квантор существования может быть навешен только на соотношение.
Аноним 24/04/17 Пнд 13:19:35 16135377
Из дискуссии выше выведем интересный вопрос - вычислимо ли невычислимое? Некоторые ораторы кукарекают, что да. Каким же образом?
>>16132
Ок, вставив терм "Аллах" в любое соотношение с квантором существования, мы ничего не докажем.
Аноним 24/04/17 Пнд 13:28:29 16140378
>>16135
По какому правилу вставим? Нельзя просто так заменить связанную букву на произвольный терм. Под квантором вообще не может стоять терм, например.

Смотри, пусть у тебя есть слово, которое является соотношением, обозначим это слово значком f.
Пусть в слово f свободно входит буква, обозначаемая как x.
Так вот.
Ты не можешь просто так взять и написать (∃x)f.
Единственный законный способ получить соотношение (∃x)f - воспользоваться одним из правил вывода теории, в которой ты работаешь.
Аноним 24/04/17 Пнд 13:33:30 16146379
>>16140
>стоять терм
*не являющийся буквой
Аноним 24/04/17 Пнд 22:19:42 16237380
>>16226
>>16236
Не срите в тред. Тут интересная дискуссия о существовании в математике намечается. Кажется, конструктивист не понимает сути существования.
Аноним 24/04/17 Пнд 22:31:17 16239381
>>16237
Что есть существование?
Аноним 24/04/17 Пнд 23:19:38 16246382
>>16239
Ясно, что это не навешивание квантора на терм.
Аноним 25/04/17 Втр 00:03:21 16251383
А конструктивная математика случайно не отрицает существование иррациональных чисел и анализа?
Аноним 25/04/17 Втр 01:12:31 16253384
>>16251
> иррациональных чисел
с чего бы? sqrt(2), например, вполне вычислим (как система стягивающихся интервалов).

> анализа
По крайней мере с непрерывными функциями все хорошо.
Аноним 25/04/17 Втр 10:13:54 16278385
>>16237
Лучше Брауэра никто пока не определил что есть существование в математике. Более того, обычно ответом на этот вопрос являются жалкие оправдания, уровня "ито философия, а не математика!!111". С чего бы? О какой вообще математике можно говорить, если нет даже внятного определения, в каком именно случае мы можем сказать, что математический объект существует и в каком смысле следует понимать его существование? Это тот вопрос, с которого должна начинаться математика. Собственно, точку зрения Брауэра я уже приводил >>15731
Аноним 25/04/17 Втр 10:21:25 16279386
>>16278
Да, один момент. Это было написано Брауэром во времена, когда Гедель еще пешком под стол ходил, и никакой теоремы о неполноте сформулировано не было. Это уже позже было доказано, что работая с математикой как с языком ее представления (одним из возможных), так или иначе встает проблема двух стульев, на одном из которых противоречивость точеная, на другом - неполнота дроченая. Гильберт со своей программой формализации арифметики присел сразу на оба стула, бурбаки предпочли помереть (даже с официальным некрологом), т.к. со своим трактатом тоже рано или поздно приблизились бы к упомянутым стульям, что было отмечено даже в предисловии переводчика первого тома про теорию множеств.
Аноним 25/04/17 Втр 12:36:21 16280387
>>16278
Определение Брауэра неадекватно математической практике. Со времен Евклида математики успешно работали с объектами, которые не умели строить, и даже не пытались строить.
Аноним 25/04/17 Втр 12:40:13 16281388
>>16280
>Со времен Евклида математики успешно работали с объектами, которые не умели строить, и даже не пытались строить.
Например? Какие это объекты?
Аноним 25/04/17 Втр 15:31:53 16288389
lejb.jpg 31Кб, 489x471
489x471
Ладно, Брауэр для мейлру сложна. Давайте попроще.
- конструктивный объект - это всегда некое слово в некоем алфавите.
- конечные слова в конечных алфавитах можно прямо занумеровать натуральными числами, лексикографическим упорядочиванием, геделевской нумерацией, не суть.
- т.о. всю конструктивную математику можно напрямую свести к арифметике. Поэтому вся конструктивная математика вычислима, а единственными адекватными основаниями математики является арифметика. Не логика.
Вопрос, можно ли вычислить нечто, не сводимое вышеупомянутым либо каким-то другим способом к арифметике?
Аноним 25/04/17 Втр 16:53:34 16289390
>>16288
> это всегда некое слово в некоем алфавите.
Что такое алфавит и что такое слово?
>- т.о. всю конструктивную математику можно напрямую свести к арифметике. Поэтому вся конструктивная математика вычислима, а единственными адекватными основаниями математики является арифметика. Не логика.
Нельзя же доказать непротиворечимость арифметики её же соственными методами. Разве нет? И если каждая такая конструктивная математика сводится к арифметике, то нам остаёться верить в её непротеворичивость?
Аноним 25/04/17 Втр 16:56:27 16290391
>>16289
>Нельзя же доказать непротиворечимость арифметики её же соственными методами. Разве нет?
Формально-аксиоматически нельзя, у меня так программа Гильберта проебалась. Конструктивно можно.
>Что такое алфавит и что такое слово?
Писал не единожды, с примерами.
Аноним 25/04/17 Втр 16:57:45 16291392
>>16290
>Писал не единожды, с примерами.
Ещё раз напиши.
>Формально-аксиоматически нельзя, у меня так программа Гильберта проебалась. Конструктивно можно.
И как? Разве это не будет формальной системой?
Аноним 25/04/17 Втр 17:02:48 16292393
>>16291
>Ещё раз напиши.
Простейший пример: алфавит из одного знака |, слово в этом алфавите - натуральное число, н-р |||| = 4.
>Разве это не будет формальной системой?
Опять же, про интерпретации логических констант сто раз писано, и в чем разница между чисто формальным и конструктивным подходом на примере синтетических и аналитических кантовских суждений, даже лекцию Мартин-Лёфа приносил, тоже не один раз.
Аноним 25/04/17 Втр 17:06:41 16293394
>>16292
>Простейший пример: алфавит из одного знака |, слово в этом алфавите - натуральное число, н-р |||| = 4.
Я не понимаю, как это отличается от формального определения N? Мы говорим, что существует знак, который рассматриваем, как еденицу и вместо его сложения с другими знаками, как с числами рисует еденицы. Правда, как это отличается от формального определения?
>Опять же, про интерпретации логических констант сто раз писано, и в чем разница между чисто формальным и конструктивным подходом на примере синтетических и аналитических кантовских суждений, даже лекцию Мартин-Лёфа приносил, тоже не один раз.
Ты можешь привести конкретный пример, почему твоё определение N не формальная система? А не отсылать куда-то? Я хочу услышать твоё объяснение этому.
Аноним 25/04/17 Втр 17:07:37 16294395
>>16281
Например, с отрицательными числами. До XIX века об их существовании велись ожесточеннейшие споры. Даже Гаусс был вынужден отражать нападки философствующих околоматематиков, кричавших, что отрицательных чисел нет. Тем не менее, работать с отрицательными числами умели все. Речь именно об отрицательных, комплексные числа отдельная история. В XIX веке была предложена строгая теория отрицательных чисел, и спорщики заткнулись.
Аноним 25/04/17 Втр 17:13:10 16295396
>>16294
Отрицательное число - слово в алфавите - |. Это конструктивные объекты. Пример мимо.
>>16293
>Я не понимаю
В этом все дело. Разница в интерпретации логических констант. Чуть выше ИТТ уже выяснили, что единственным адекватным определением N можно считать ординалы фон Неймана, там же выяснили, что это те же нумералы Черча, вид сбоку. Т.е. конструктивная система.
Аноним 25/04/17 Втр 17:15:08 16297397
>>16295
>В этом все дело. Разница в интерпретации логических констант. Чуть выше ИТТ уже выяснили, что единственным адекватным определением N можно считать ординалы фон Неймана, там же выяснили, что это те же нумералы Черча, вид сбоку. Т.е. конструктивная система.
Ты не понял. Я хочу, чтобы ты объяснил, почему это не формальная система. Если ты говоришь, что выше дано такое объяснение, то приведи на него ссылки и прокоментируй его.
Аноним 25/04/17 Втр 18:01:02 16298398
>>16288
ЛЮБУЮ формальную систему можно рассмотреть как множество конечных слов в некотором алфавите - на которое наложено несколько дополнительных условий.

>>16292
ЛЮБУЮ формальную систему можно рассмотреть примерно таким же образом, разве что алфавит будет более богат.

>>16295
ЛЮБОЙ математический объект - слово в некотором алфавите. Теоретически достаточно всего одного символа, кстати. На практике используются более богатые алфавиты.
Аноним 25/04/17 Втр 18:06:29 16299399
>>16298
Я это уже писал >>14128 Вопрос был не в этом, а в том, как невычислимую хуитку типа закона исключенного третьего или актуальную бесконечность представить в такой же форме? Очевидно, что если знак бесконечности считать символом / термом / словом в некоем алфавите, то у него должны быть правила вычисления в канонический элемент множества или типа. Т.к. сам этот знак не является каноническим элементом. А таковых правил не существует. Вот и приплыли.
Аноним 25/04/17 Втр 18:08:40 16301400
>>16299
Открой для себя первую главу Бурбаки. Вопросы отпадут.
Аноним 25/04/17 Втр 18:12:09 16302401
>>16301
Читал я ваших бурбаков. У меня даже бумажная книшка есть. Ты расскажи, как ты неканонический элемент в канонический вычислять будешь, если правил вычисления нет? Значками играться можно сколько угодно, в итоге придем либо к противоречию, либо к неполноте, что есть свойства любой формальной системы, сводящейся к синтетическому суждению (опять же возвратимся к лекции Мартин-Лёфа).
Аноним 25/04/17 Втр 18:14:00 16303402
>>16302
Ты говоришь как человек, который не читал/не понял первую главу Бурбаки.
Давай разберемся вместе, если ты не против.
Аноним 25/04/17 Втр 19:38:17 16305403
>>16303
Судя по молчанию - против.
Аноним 25/04/17 Втр 22:01:28 16311404
Эта продвинутая типизация подойдет к клэйтронике?
Аноним 26/04/17 Срд 05:20:45 16324405
>>16305
Читал и понял. Я уже сто раз говорил в чем разница. В конструктивной системе выразимо только то что там доказуемо, отсюда геделевская полнота. В формальной системе можно выразит то, чего в ней нельзя доказать, т.к для доказательства требуется что'то помимо нее. Это прямое следствие интерпретации логических и др констант.
Аноним 26/04/17 Срд 06:59:00 16325406
Аноним 26/04/17 Срд 10:09:12 16329407
>>16324
К какому конкретно положению первой главы Бурбаки у тебя возникают претензии?
Аноним 26/04/17 Срд 10:41:44 16331408
>>16329
Тебе ж говорят, такой подход изначально ущербен, из'за геделевой неполноты либо противоречивости формальных систем, оторванных от построения. Самый простой пример, закон исключенного третьего, истинный с формально'аксиоматической точки зрения. Он невычислим в общем случае.
Аноним 26/04/17 Срд 11:08:28 16334409
>>16329
Ты вот з бурбаков поясняешь, а походу и предисловие даже не читал, где написано то , о чем я тебе толкую. Бурбаки даже не упомянули, что весь их подход в итоге в геделя и упирается.
Аноним 26/04/17 Срд 16:16:43 16356410
>>16331
Бурбаки предложили математику, в которой любой математический объект построим как конечное слово в некотором алфавите. То есть осуществили в точности твою мечту. Если тебя не устраивает их подход - назови первое же предложение первой главы Бурбаки, с которым ты не согласен.
Аноним 26/04/17 Срд 16:46:11 16359411
>>16356
Сейчас бы по сотому разу объяснять самые азы. Ты так и не понял что такое построение математического объекта. У бурбаков речь о построении вообще не идет, а язык рассматривается только как синтаксис. По бурбакам противоречие это синтаксическая ошибка. Выражение на бурбаковском языке не обязательно построимо, даже если и выразимо на нем. Пример все тот же, закон исключенного третьего. В нем нет ошибок по бурбакам, но он не вычислим и не построим. Я уже не знаю как проще объяснить, про интерпретации логических констант тцт вообще не воспринимают.
Аноним 26/04/17 Срд 16:58:36 16363412
>>16359
Математические объекты по Бурбаки и есть слова. Каждый математический объект построим точно в том же смысле, в каком натуральное число построимо из палочки |.
Аноним 27/04/17 Чтв 01:08:40 16398413
>>16363
Ты просто не понял. Знакосочеетания бурбаков это просто синтаксис. В котором выразима любая хуйня, сколь угодно непостроимая. Хоть знак бесконечности, хоть закон исключенного третьего. У них нет понятия выводимости, пруф'объектов, базиса и т.п. у Мартин'Лефа в лекции разница рассмотрена подробно, ссылку я сто раз давал и своими словами пояснял.
Аноним 27/04/17 Чтв 01:13:16 16399414
А вот если бурбаковский синтаксис рассмотреть через изоморфизм Карри'Говарда, то да, это будет конструктивной системой, но тогда в ней нельзя будет выразить непостроимых объектов.
Аноним 27/04/17 Чтв 02:30:00 16402415
Еще пример, чтобы было понятно. Знакосочетание 'Аллах' не является построением Аллаха, хотя и является когечным словом в конечном алфавите. Но, еще раз, у нас нет правил для вышеупомянутого построения.
Аноним 27/04/17 Чтв 04:32:17 16403416
>>16398
Нет ты. Палочки - это тоже просто синтаксис. Раз выразима - значит построима.

>>16402
Тогда и знакосочетание ||||| не является построением числа пять.
Аноним 27/04/17 Чтв 05:28:58 16404417
>>16398
>У них нет понятия выводимости
Лолчто.
Аноним 27/04/17 Чтв 05:30:39 16405418
>>16402
Аллах="Аллах". Аллах и есть слово в конечном алфавите. Это просто слово, никакого иного смысла в нём нет.
Аноним 27/04/17 Чтв 08:32:04 16408419
>>16403
В конструктивной математике кроме синтаксиса есть семантика, в т.ч номинальные дефиниции и правила вычисленичя неканонических объектов в канонические. Поэтому палочки и т.д можно вычислить в натуральные числа, а знакосочетания бурбаков вычислимы только когда выражают канонические объекты. Слово 'Аллах' невычислимо ни во что, так же как и закон исключенноно третьего, хотя и то и другое выразимо в бурбаковской нотации.