Главная Юзердоски Каталог Трекер NSFW Настройки

Математика

Создать тред Создать тред

Тред закрыт.

Check this out!
<<
Назад | Вниз | Каталог | Обновить | Автообновление | 561 69 113
Оснований математики тред 2 Аноним 22/11/16 Втр 21:34:00 3694 1
npetuh.jpg 60Кб, 790x593
790x593
Аноним 22/11/16 Втр 21:40:09 3696 2
Решил научиться доказывать теоремы с помощью и 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 3701 3
>>3696
Там же дальше об этом говорится!
Аноним 22/11/16 Втр 22:34:12 3703 4
>>3701
Можно конкретное предложение?
Аноним 22/11/16 Втр 22:45:57 3705 5
>>3703
Ну, прямо следующий абзац же об этом... Или я твоего вопроса не понял? Если бы у пропозишнов не было типа, ты бы не смог доказывать никакие утверждения о пропозишнах. Он там и дает примеры: можно сказать "для всех натуральных чисел, если число меньше пяти, то меньше и шести", а можно сказать "для всех пропозишнов, если у нас есть пропозишн, то он у нас есть".
Аноним 22/11/16 Втр 22:57:54 3706 6
>>3705
> Или я твоего вопроса не понял?
Да. Мой вопрос: что такое тип?
Аноним 22/11/16 Втр 23:08:56 3707 7
Аноним 23/11/16 Срд 08:55:49 3733 8
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 3734 9
зт.png 225Кб, 1425x740
1425x740
>>3706
>что такое тип?
Тип - это конструктивный объект, который есть элемент самого себя. Да, в общем случае это приводит к парадоксу Жирара (по-сути, все тот жи парадокс Рассела), что было показано для первого варианта MLTT, поэтому сейчас там все немного хитрее - иерархия вложенных универсумов - U. Подробности опять же в вышеупомянутой книге, либо в учебнике по LEAN. Если не интересны философические объяснения - считай тип множеством, элементы которого определены заданными правилами.
Аноним 23/11/16 Срд 12:00:45 3739 10
т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 3742 11
>>3733
У тебя мания величия походу, бро.
Аноним 23/11/16 Срд 14:45:35 3744 12
>>3739
> полная и выводимая по Геделю
Что очевидно, ведь теорема Гёделя распространяется только на те системы, где можно построить PRA.
Аноним 24/11/16 Чтв 02:23:13 3777 13
Аноним 24/11/16 Чтв 14:06:03 3798 14
>>3739
>В итоге получается логическая система, полная и выводимая по Геделю
Ну сколько можно распространять дезинформацию?
>полная
Она не полна т.к. к ней вполне применимы теоремы Гёделя о неполноте, в частности, она не может ни доказать, ни опровергнуть утверждение о своей собственной непротиворечивости. Напомню, что полнота означает, что всякое предложений либо доказуемо, либо опровержимо. Если теория обладает таким свойством только для специального класса предложений, а не для всех предложений своего языка, то называть это полнотой некорректно.
>выводимая по Геделю
Не то, чтобы я прочел все работы Геделя, но я видел этот термин тоько у тебя, почти уверен, что ввел его вовсе не Гедель - ссылку на Геделя в студию, если придерживаешься другой точки зрения.

>>3744
>Что очевидно, ведь теорема Гёделя распространяется только на те системы, где можно построить PRA.
На самом деле теоремы Геделя о неполноте распространяются и на более слабые системы (1-ую так и вовсе можно доказать в арифметике Робинсона). Кроме того, эквациональная версия PRA (для которой тоже имеют место обе теоремы о неполноте) погружается в интуиционистскую теорию типов.
Аноним 25/11/16 Птн 09:02:23 3825 15
>>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 3826 16
Снимок.PNG 101Кб, 499x734
499x734
Да, MLTT не только сама по себе конструктивный объект, но исходя из интерпретации логических констант по Колмогорову, по-сути, готовая спецификация для языка программирования http://www.cse.chalmers.se/research/group/logic/book/book.pdf
Аноним 30/11/16 Срд 08:38:19 4265 17
1.gif 8Кб, 950x128
950x128
>>3694 (OP)
Шарящий в мат.логике анон, ответь.
Может ли теоретически получиться так, что ZFC непротиворечива, однако омега-противоречива, и если так, то возможно ли было бы эту омега-противоречивость некими метаматематическими методами (вроде тех, что использовал Гёдель) доказать?
Аноним 30/11/16 Срд 10:13:18 4269 18
>>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 4271 19
>>4269
Спасибо, анон!
Отсюда даже виден дальнейший ход того, как можно было бы доказать omega-Con(ZFC) - доказав неким образом верность арифметического выражения, эквивалентного not Con(ZFC+Con(ZFC+Сon(ZFC)))
Аноним 30/11/16 Срд 11:52:40 4272 20
>>4271
fix: доказать not omega-Con(ZFC)
Аноним 30/11/16 Срд 23:52:45 4303 21
>>4271
Я на самом деле переусложнил. Для ответа на твой вопрос нужно было лишь доказать непротиворечивость ZFC + Сon(ZFC) + not omega-Con(ZFC). Что требовало немного меньше усилий.
Аноним 03/12/16 Суб 15:25:14 4546 22
Анон, помоги доказать, что все тавтологии логики высказываний с 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 5929 23
73bb4bc1ea23e5b[...].png 271Кб, 1097x1221
1097x1221
Бамп божественным Вавиловым.
Аноним 21/12/16 Срд 09:13:33 5931 24
>>5929
Да никакой он не божественный. Мало того, что конструктивистов с кое-кем другим перепутал, так еще и ночью у него там кто-то символы дорисовывает. Теорем-пруверы, оказывается, опираются на тысячи неявных предположений - вот оно как! Просто черная магия и сильный ИИ какие-то.
Аноним 21/12/16 Срд 09:42:20 5932 25
>>5931
> Теорем-пруверы, оказывается, опираются на тысячи неявных предположений - вот оно как!
Вавилов тенденциозен, но собственно критика того, что конструктивность так называемой конструктивной математики довольно условна и опирается на то, что допускаются явно физически нереализуемые вычисления остается. В чем, в конце-концов, утверждение об обрывании последовательностей Гудстейна конструктивнее, чем утверждение о возможности удвоить шар путем перемещения конечного числа частей, учитывая, что ни одно из них не является физически реализуемым.
Аноним 21/12/16 Срд 12:22:23 5940 26
>>5931
>>5929
Да нормальный парень он, просто платонист. Так бывает, к сожалению. Но в остальном вкусы у него хорошие, литературу интересную цитирует. Можно же фильтровать информацию, правда? Пенроуз вон тоже отбитый платонист, но в остальном, исключая этот пункт, мне нравится его читать.
Аноним 21/12/16 Срд 14:08:25 5941 27
>>5940
>Да нормальный парень он, просто платонист.
Проблема не в том, что он платонист, а в том, что его заносит и он выдает мало адекватную аргументацию против несимпатичных ему позиций. Например теже "тысячи неявных аксиом" нужные конструктивной математике или что теорема Гёделя о неполноте говорит о "генерации некоторого специального вида текстов" (и ничего не говорит о математике).
Но, впрочем, пишет увлекательно (хотя, отчасти, это следствие того, что он выдвигает совершенно скандальные тезисы).
Аноним 21/12/16 Срд 14:54:22 5944 28
>>5941
Каждый математик в душе хотябы чуточку платонист. Даже ℕ-петух
Аноним 21/12/16 Срд 15:14:02 5946 29
>>5944
Да, видимо так, просто потому что сомнения в реальности математических объектов однозначно являются большой помехой, когда реально занимаешься доказательством теорем.
Хотя, разумеется, это касается только собственно математиков. Философы математики, не являющиеся, а тем более никогда не являвшиеся действующими математиками вполне могут не быть платонистами ни в какой степени.
Аноним 22/12/16 Чтв 14:40:51 6020 30
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 6067 31
Составьте, пожалуйста, список значимых работ по философии математики. Типа "Структуры" Куна, работ Поппера и Фейерабенда относительно философии науки. А также посоветуйте какое-то годное введение в мат. философию, можно на английском
Аноним 22/12/16 Чтв 20:54:32 6068 32
Аноним 23/12/16 Птн 07:09:21 6100 33
sosnoole.png 224Кб, 690x622
690x622
Аноним 23/12/16 Птн 08:38:03 6108 34
>>6067
>типа Куна и Фейерабенда
Harold Edwards
Gian-Carlo Rota
>>6068
Хуйня.
Аноним 23/12/16 Птн 09:57:08 6117 35
Снимок.PNG 163Кб, 972x232
972x232
инт3.png 488Кб, 1194x1269
1194x1269
инт4.png 579Кб, 1276x1257
1276x1257
>>6100
Ой, какая милота эта ваша грязноштанная математика. "Яскозал, что это буржуазная теория и вы так делайте". На самом же деле, а не в калмунистических манямирах, есть нейрофизиологические данные, доказывающие сводимость натурального числа к восприятию времени, о чем писал еще Брауэр. Т.н. модель ATOM Уолша. Ну, цитата Кронекера про бога хуета, конечно.
Аноним 23/12/16 Птн 10:07:03 6121 36
>>6117
>о чем писал еще Брауэр.
Ох и давно я этого не слышал.
>есть нейрофизиологические данные, доказывающие сводимость натурального числа к восприятию времени
Пруф?
Аноним 23/12/16 Птн 10:37:44 6127 37
23/12/16 Птн 21:35:44 6175 38
Аноним 24/12/16 Суб 10:28:28 6206 39
>>6175
Нейровизуализация - объективные данные, они не могут быть хуйней, они либо что-то показывают, либо нет. По этой теории, на которую ты ссылаешься, я тоже пояснял уже. Там авторы сами себе противоречат, результаты нейровизуализации у них показывают связь в обоих направлениях, но в одном меньше, чем в другом, из чего они от балды заключают, что то направление, по которому корелляция меньше - это метафора и его на самом деле не существует. Еще раз скажу, в их же статье показана реальная корелляция на реальной нейровизуализации. Т.е. исходя из их же данных, они просто дополнили результаты Уолша, показав несимметричность пространственно-временных отношений, т.е. фиолетовый, зеленый и розовый кружочки на втором пике >>6117 должны быть разных диаметров, чтобы точнее показывать реальную картину.
Аноним 26/12/16 Пнд 16:19:16 6393 40
Решил изучать математику с логики и оснований. Читаю Клини, все правильно делаю?
Аноним 01/01/17 Вск 14:30:16 6913 41
>>3694 (OP)
Поздравляю всех любителей кококатегорий с Новым Годом! Дорогие подгорающие и сотрудничающие с администрацией красные петушки, я очень рад, что вы есть:3

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

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

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

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

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

мимо кислота-архиватор-кун
Аноним 24/01/17 Втр 13:34:37 9315 66
>>8227
Тег для раздела вроде должен автоматом добавляться же. Или надо админа стукнуть, чтобы он его добавил?
Аноним 27/01/17 Птн 06:27:24 9466 67
Объясните мне, что значит "дать основания" и почему это всех так тревожит.
Аноним 27/01/17 Птн 06:50:06 9467 68
>>9466
Допустим, есть N утверждений, про которые известно, что они должны быть истинными. Требуется предоставить набор аксиом и определений такой, что в нём каждое из N утверждений будет теоремой, причем аксиомами будут далеко не все из этих N утверждений (желательно - ни одно).
Аноним 27/01/17 Птн 06:58:36 9468 69
>>9466
Допустим, есть N утверждений, про которые известно, что они должны быть истинными. Требуется предоставить набор аксиом и определений такой, что в нём каждое из N утверждений будет теоремой, причем аксиомами будут далеко не все из этих N утверждений (желательно - ни одно).
Аноним 27/01/17 Птн 22:24:42 9532 70
Поясните про полноту евклидовой/афинной/любой геометрии. В книгах обычно дается доказательство категоричности, но причем здесь полнота?
Аноним 28/01/17 Суб 06:36:24 9554 71
>>5929
А я ведь всю книгу прочёл, по совету с двача. В конце было ощущение, что меня протроллили. Хуже книги по логике я просто не встречал
Аноним 28/01/17 Суб 06:43:37 9555 72
>>9467
Разве об этом тред?
Аноним 28/01/17 Суб 06:57:24 9556 73
На самом деле спор об основаниях имеет сугубо психологически-невротическую природу, и вполне очевидно, что никогда не будет текста, который раз и навсегда удовлетворил бы всех. Все эти попытки свести множества к чисто синтаксической игре утверждений о множествах, или к конструктивным типам, или ещё к какому-то такому синтаксису очевидно не могут привести к какому-то удовлетворению. Вот кажется что синтаксические игры - это "более близкие" объекты чем множества, потому что они "более осязаемые", потому что это "финитарные средства", но это мысль чисто социально-культурологическая, это стереотип; если бы не было вот этого вот дискурса классической логики и попыток свести всю математику к формальным теориям, то никому бы не казалось, что абстракция алгоритма или конструктивного типа чем-то проще или сложнее, чем абстракция множества. Категорщики, кстати, это поняли уже и ебашут свои (\infty,1)-категории, зачастую, без всяких ремарок о том, как это всё можно свести к формальным первопорядковым теориям (хотя на начальном уровне всё же различие "больших и малых категорий" осталось, но я надеюсь, что всё же откажутся вскоре и от этого). Потому что ебать себе мозги по-поводу оснований в 2к17 это уже такая же пошлятина как и ебать себе мозги по поводу того, что первичнее - материализм или идеализм.
Аноним 28/01/17 Суб 12:15:58 9563 74
>>9556
>различие "больших и малых категорий" осталось, но я надеюсь, что всё же откажутся вскоре и от этого
Чистая педагогика же. Отказываться тут не получится, нужно новое поколение, которое со школы обучено категориям.
Аноним 28/01/17 Суб 23:29:36 9603 75
>>9556
>Потому что ебать себе мозги по-поводу оснований в 2к17 это уже такая же пошлятина как и ебать себе мозги по поводу того, что первичнее - материализм или идеализм.
Я тебя помню. У тебя подход к вопросу о том, что важно в математике - это что-то в духе отождествления важного с модным. Вполне понятно, почему с таким мировоззрением тебе претят основания, онтологические вопросы вообще, как и вероятно остальная философская проблематика. Но вообще, для остальных людей (более склонных к независимым суждениям) такого рода вопросы часто могут быть важнее.


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


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

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

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

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

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

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

Свободные векторы - классы множества ориентированных отрезков по этому отношению эквивалентности.
Аноним 31/01/17 Втр 19:21:08 9773 98
>>9761
ну и с какого хуя такой подход верный? эти определения не дают никакой интуиции: определи теперь сумму векторов, разнообразные произведения, получится вообще невыносимая поебень.
Аноним 31/01/17 Втр 19:39:47 9775 99
>>9749
Вот это проиграл с теоретико-множественных дидов, лил.
31/01/17 Втр 20:04:12 9778 100
>>9773
Что там определять? Правило треугольника очень простое. А "вектор это изотропия пространства" хуйня какая-то. Много векторов = много изотропий? Сумма векторов = сумма изотропий? Это тоже не даёт никакой интуиции. Поебень непонятная. Никогда школьник не вдуплит это.
31/01/17 Втр 20:18:04 9787 101
Во видал, даже я перепутал слова, школьники с ваших изометрий вообщей охуеют. Но тем, кто школьников ничему никогда не учил не понять.
>>9778-кун
Аноним 31/01/17 Втр 20:39:04 9791 102
Единственная реформа которая нужна школьному образованию - это укоротить его раза в 3, чтобы не мешать нормальным школьникам заниматься нормальными делами (ходить на кружки и заниматься самоподготовкой, например) и не ебать мозги всяким долбоёбам, которые всё равно ничего не выучат. Ну и, конечно же, не ебать мозги учителям, которые тоже школьной программы в полном объеме не знают.
Аноним 31/01/17 Втр 21:32:57 9795 103
>>9778
композиция изометрий - изометрия. Изометрии образуют группу Ли. все же просто.
31/01/17 Втр 21:36:58 9798 104
>>9795
Расскажи о своём опыте обучения 7-ми классников группам Ли.
Аноним 31/01/17 Втр 21:45:55 9800 105
>>9798
ну можно сказать просто "группа", это совсем простое понятие.
Аноним 31/01/17 Втр 22:16:08 9810 106
>>9773
Суммой ориентированного отрезка (ab) и ориентированного отрезка (bc) называется ориентированный отрезок (ac).

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

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

>>9926
>Существуют фс, которые могут подтвердить собственную непротиворечивость, именно этот факт и заставил гильберта верить.
Во времена Гильберта ничего такого известно не было. Современные же примеры совершенно экзотичны.
Аноним 01/02/17 Срд 19:33:12 9941 114
>>9930
Понятно. То есть, если грубо, этот аргумент в каком-то роде должен был быть социальным, а не метафизическим.
Аноним 01/02/17 Срд 19:33:32 9942 115
Аноним 01/02/17 Срд 19:42:37 9945 116
>>9941
Видимо так.
Но строго говоря, я Гильберта не читал (и не факт, что он непосредственно об этом пишет), а просто пересказываю интерпретации, которые слышал.
Аноним 03/02/17 Птн 11:50:19 10200 117
мэгумин.jpg 167Кб, 782x543
782x543
>>9924
У Гильберта получилось (и надо признать, годно получилось) аксиоматически построить геометрию. Этот успех заставил его уверовать, что и с арифметикой и вообще со всем остальным можно так же. Но реальность оказалось несколько сложнее, что прямо показывает нам сомнительную ценность таких экстраполяций от одного-пары частных случаев оптом и априори на все остальные как закон исключенного третьего, например. То же самое можно сказать про т.н. "догму Гильберта", это же чистая религия.
Аноним 03/02/17 Птн 12:33:39 10204 118
Аноним 03/02/17 Птн 14:46:20 10222 119
>>10200
> как закон исключенного третьего, например
и собственно модус поненс.
Аноним 03/02/17 Птн 14:55:14 10228 120
140542860164tnl[...].jpg 43Кб, 536x604
536x604
>>10222
>поненс.
С элиминатором импликации-то что не так?
Аноним 03/02/17 Птн 15:01:12 10229 121
>>10228
Все так, если веруешь.
Аноним 03/02/17 Птн 15:04:27 10230 122
Снимок.PNG 7Кб, 343x134
343x134
>>10229
>если веруешь.
Во что?
Аноним 03/02/17 Птн 15:10:17 10232 123
>>10230
В правила резолюции.
Аноним 03/02/17 Птн 15:12:53 10233 124
>>10228
Если начать применять этот принцип
>прямо показывает нам сомнительную ценность таких экстраполяций от одного-пары частных случаев оптом и априори на все остальные
последовательно (т.е. отказываться от индукции вообще), то и от модус поненс нужно отказаться.
Аноним 03/02/17 Птн 15:23:09 10234 125
>>10232
Ну вот я тебе принес это правило, покажи что там не так.
>>10233
Но у нас пропозишен - это всегда множество пруф-объектов, его доказывающих. Только конструктивные объекты, только хардкор.
Аноним 03/02/17 Птн 15:27:09 10238 126
>>10234
>Только конструктивные объекты, только хардкор.
Ну это вера из двух частей:
- вера в тезис черча, так что любая математическая задача может быть сведена к алгоритму
- вера в непогрешимость вычислительной техники (тот же модус поненс по сути)
Аноним 03/02/17 Птн 15:28:18 10239 127
>>10238
О какой вере ты говоришь применительно к вычислимым объектам?
Аноним 03/02/17 Птн 15:36:18 10241 128
>>10239
о вере в функциональные типы. Еще разок: у нас есть эмпирический закон, что транзисторы ведут себя определенным образом. Остается только верить, что они будут вести себя так и дальше. Согласно этой вере вычисление всегда предсказуемо. А дальше по изоморфизму карри-говарда модус поненс может быть сведен к функциональным типам.

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

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

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

Пока что я могу судить, что ты до сих пор не удосужился открыть HoTT и почитать, раз я должен вычитывать правильные определения за тебя.
Аноним 03/02/17 Птн 17:10:42 10265 140
>>9940
>>9941
Я хотел бы переделать свой ответ. Мне кажется ты говоришь не про то, ибо если бы программа Гильберта действительно бы заключалась в
>всякое теоретико-множественное доказательство финитного факта преобразуется в финитное доказательство того же факта.
то, естественно, она была бы успешной. Ведь есть тупо теорема о том, что ZFC доказывает те же самые арифметические утверждения, что и PA (я её запомнил как "теорема об элиминации"), значит дело тут не в том.
Аноним 03/02/17 Птн 17:11:54 10266 141
>>10260
>HoTT не нужны никакие пререквизиты
Ой, все. Там самая первая глава - изложение MLTT. Для MLTT не нужны пререквизиты? И как, много ты там понял?
Аноним 03/02/17 Птн 17:43:53 10273 142
>>10265
> Ведь есть тупо теорема о том, что ZFC доказывает те же самые арифметические утверждения, что и PA (я её запомнил как "теорема об элиминации"), значит дело тут не в том.
Такой теоремы нет. В силу второй теоремы Гёделя о неполноте, предполагая непротиворечивость PA, верно обратное. В ZFC несложно доказать, что PA непротиворечива (рассмотреть натуральные числа с функциями сложения, умножения и следования и показать, что это модель PA), но по второй теореме Гёделя о неполноте PA не доказывает собственную непротиворечивость.
Аноним 03/02/17 Птн 18:11:31 10275 143
>>10273
Извиняюсь, перепутал с другой теоремой о том, что ZFC+CH доказывает те же самые арифм. утверждения, что и ZFC.
Аноним 03/02/17 Птн 18:28:08 10276 144
>>10266
Мне всю книгу скринить надо, чтобы ты ее тут прочитал? Книга начинается с пояснения, что такое тип, что такое теория типов, что такое суждение. Кому нужны такие пояснения? Вестимо, что математикам, кому знакомы общие понятия наивной теории множеств и гомотопической алгебры. Далее идет сравнение с классическими основаниями.
Читателю, знакомому с MLTT, рекомендуют вообще читать первую главу по диагонали.
Аноним 03/02/17 Птн 21:11:07 10289 145
поехал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 10308 146
проиграл.webm 2778Кб, 480x360
480x360
>>10289
Ты в моих постах триггеры выискиваешь, чтобы потом гореть с них? Зачем? Это же обычная терминология.
Аноним 04/02/17 Суб 19:14:43 10338 147
Аноним 04/02/17 Суб 19:19:40 10339 148
Аноним 04/02/17 Суб 22:53:30 10348 149
>>10339
А ты хорош. Но интуиционизм тоже неплох
Аноним 05/02/17 Вск 13:20:37 10358 150
>>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 10364 151
>>10358
миллионы книг и статей - харам
@
халяль - полторы книжки
Аноним 11/02/17 Суб 18:36:39 10795 152
пахомматематика2.jpg 82Кб, 782x550
782x550
p0008.png 194Кб, 2889x4500
2889x4500
Почитал тута за ультраинтуиционизм Есенина-Вольпина пикрелейтед, это разве серьезная математическая точка зрения? Он отвергает марковскую абстракцию потенциальной осуществимости, но тут же предлагает "гипотезу осуществимости следующего шага", что то же самое, вид сбоку. Далее, говорит, что функция следования - это не закон, а только намек на закон (хотя по факту это конструктивная функция, конструктивный объект, т.е. именно совершенно конкретная формулировка закона). Потом вообще какой-то аутизм уровня того анекдота:
-Дохуя-это сколько?
- Иди вдоль рельсов и считай шпалы. Когда досчитаешь до "а ну его
нахуй"-это будет как раз половина.
Аноним 11/02/17 Суб 19:09:11 10796 153
>>10795
На твоем пикрелейтеде же вполне четко и понятно даны ответы на твои вопросы. Не очень понятно, что именно непонятно. Вот он говорит: пусть у нас есть ребенок и функция следования для него, которая берет ребенка и дает ребенка в следующий момент времени. То есть р, р', р''- это все ребенки, но интуитивно ясно, что после некоторого (неопределенного) количества применений этой операции результат уже никак ребенком быть не может. Это он и постулирует утверждением под номером три. Я просто пересказываю текст еще раз, да.

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

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

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

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

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

4. Пользуясь случаем, передаю привет чернильной дыре.
Аноним 12/02/17 Вск 13:09:52 10821 157
>>10810
>1. Если убрать с головы волосатого человека один волосок, он не станет лысым. Начнём убирать с головы человека волосы по одной штучке за раз; через некоторое время получим лысого человека. Таким образом, имеем антиномию. Объекты, обладающие такой антиномией, будем называть собственно ультрафинитистскими.
Тут нет никакой антиномии, просто бинарная логика неприменима к подобным задачам, т.к. мы не можем в точности указать, с какого конкретно количества волос считать человека лысым. Непрерывная функция принадлежности вопрос снимает полностью, т.к. появляется возможность считать человека лысым и волосатым в какой-то степени от 0 до 1. Не понимаю, зачем тащить в такие задачи какой-то ультрафинитизм, когда все элементарно сводится к нечетким множествам.
>>10808
>Это не определение.
А что это? 0:N, if a:N then succ(a):N, закон построения (функция следования).
Аноним 12/02/17 Вск 14:45:05 10823 158
>>10821
А где гарантия, что "бинарная логика" применима к основным умозрительным объектам метаматематики, таким как строка символов, алфавит, возможность в любой момент времени ввести новую, не использованную ранее букву?
Аноним 12/02/17 Вск 15:55:44 10825 159
>>10823
В случае конечных объектов можно проверить непосредственно, применима или нет. В общем случае, безотносительно возможности построения, никакой гарантии, только вера.
12/02/17 Вск 16:10:27 10827 160
>>10825
Тогда получается мы не можем нормально работать с натуральными числами?
Аноним 12/02/17 Вск 16:10:35 10828 161
>>10825
А ультрафинитисты вот не веруют, но доказывают.
Аноним 12/02/17 Вск 16:17:23 10829 162
>>10827
С какими-то можем, с какими-то нет. Так-то 10^100^1000^10000 тоже натуральное число.
>>10828
На эту тему вообще есть что почитать интересного? Я вот гуглил, на русском языке одну статью нашел, которую и процитировал, на английском тоже почти ничего.
12/02/17 Вск 16:19:13 10830 163
>>10829
>С какими-то можем, с какими-то нет. Так-то 10^100^1000^10000 тоже натуральное число.
Выходит, конструктивная математика основанна на вере ?
Аноним 12/02/17 Вск 16:23:58 10831 164
>>10830
Я уже столько раз писал про марковскую абстракцию потенциальной осуществимости, что даже не помню сколько раз конкретно. И чем конструктивный объект отличается от потенциально существующего, писал не меньше. С себя начни, если такие простые вещи понять не можешь.
Аноним 12/02/17 Вск 16:30:18 10832 165
>>10831
проговаривать название != писать
12/02/17 Вск 16:32:27 10833 166
>>10831
Ну у тебя и пичот.
>марковскую абстракцию потенциальной осуществимости
Вера. Обычная вера в то, что алгоритм может работать верно и выдавать нужные результаты, при этом не останавливаясь. Раз можно проверить потенциальное сущствование только конечное количество объектов, в нашем случае чисел, то как проверить, что алгоритм верен?
> С себя начни, если такие простые вещи понять не можешь.
Ты опять берёшь и уходишь от ответа, мань.
Аноним 12/02/17 Вск 18:09:48 10842 167
>>10830
>Выходит, конструктивная математика основанна на вере ?
Мозг конструирует для нас реальность. И мы в нее верим, а что ещё остается делать?
Аноним 12/02/17 Вск 18:13:55 10845 168
Аноним 12/02/17 Вск 18:45:46 10852 169
>>10833
В алгоритмы веровать не нужно. Алгоритм либо работает правильно и выдает правильный результат, либо он работает неправильно и выдает результат, доказывающий абсурдность предположения, что алгоритм работает правильно. Любой алгоритм сводится к типизированной лямбде, корректность его можно проверить методами MLTT, опять же, про интерпретацию логических констант и изоморфизм Карри-Говарда я писал достаточно, чтобы тут у какого-то кловна жопа горела с этой терминологии.
12/02/17 Вск 18:48:37 10853 170
>>10852
>Алгоритм либо работает правильно и выдает правильный результат, либо он работает неправильно и выдает результат, доказывающий абсурдность предположения, что алгоритм работает правильно.
Разве это не закон исключённого третьего? Ты берёшь и веруешь в то, что твой алгоритм работет либо правильно либо неправильно? Чем эта вера отличается от веры в аллаха?
Аноним 12/02/17 Вск 18:59:57 10855 171
>>10853
>Разве это не закон исключённого третьего? Ты берёшь и веруешь в то, что твой алгоритм работет либо правильно либо неправильно? Чем эта вера отличается от веры в аллаха?
Пиздец. А я ведь специально сформулировал отрицание именно в интуиционистском смысле. Но что можно объяснить школьнику на батрушке. Закон исключенного третьего это "А или не А". "А" в данном случае означает "у нас есть пруф-объект, подтверждающий, что А не пусто, а:А". "не А" можно представить в двух вариантах: "у нас есть пруф-объект, доказывающий, что построение А неосуществимо, б:Б" и "у нас нет нихуя". В классическом смысле оба этих случая равнозначны. В интуиционизме допустимо только доказательство через конкретное построение, т.е. только первый вариант. Тогда как второй не доказывает ничего, т.к. это не построение. В интуиционизме закон исключенного третьего не принимается как общее правило по простой причине - у нас нет построений А или построений, отрицающих А на все возможные случаи. Поэтому закон исключенного третьего, принимаемый априори - чистая вера.
Аноним 12/02/17 Вск 19:18:23 10858 172
Поясните за New Foundations. Что это?
Аноним 12/02/17 Вск 19:22:33 10859 173
>>10852
Охуенный у тебя манямирок, в котором все алгоритмы всегда выдают результат. Нам бы всем не помешал такой.
Аноним 12/02/17 Вск 19:25:50 10860 174
p0180.png 207Кб, 2811x4481
2811x4481
p0181.png 209Кб, 2811x4481
2811x4481
p0182.png 211Кб, 2811x4481
2811x4481
>>10858
Пикрелейтед.
>>10859
>все алгоритмы всегда выдают результат.
Пустой тип как результат проверки на корректность - тоже построенный результат.
Аноним 12/02/17 Вск 19:32:29 10862 175
>>10860
> Пустой тип как результат проверки
> результат
Ты так говоришь, будто проблема остановки решена. Я не против твоих ХоТТов, да и в споре не участвую, но никогда не пиши хуйню вроде
>Алгоритм либо работает правильно и выдает правильный результат, либо он работает неправильно и выдает результат
Алгоритм может начать работу и никогда не завершиться, и никакие методы проверки, в том числе MLTT не выдадут на таком алгоритме никакого ответа, они просто зависнут.
Аноним 12/02/17 Вск 19:38:33 10864 176
>>10862
Никто не спорит с тем, что существуют алгоритмически неразрешимые задачи.
>никакие методы проверки, в том числе MLTT не выдадут на таком алгоритме никакого ответа, они просто зависнут.
Сам хуйню пишешь, а мне запрещаешь. Не зависнет ничего, в худшем случае просто не будет чекаться и все. Защита от такой хуйни есть во всех пруверах, подход разный, правда.
Аноним 12/02/17 Вск 19:50:09 10869 177
>>10864
>Защита от такой хуйни есть во всех пруверах, подход разный, правда.
Охуеть защита - внешним образом прерывать процесс. Мы тут про основания математики, ты подался рассуждать про хаки в софте.
Аноним 13/02/17 Пнд 13:18:22 10916 178
SDC116221.jpg 966Кб, 2592x1944
2592x1944
Умели же раньше книжки по основаниям писать. Читаю пикрелейтед, к слову, Френкель - тот самый, один из создателей ZFC. В главе про интуиционизм последний параграф - о том, как интуиционизм повлиял на различные разделы математики. Арифметику и алгебру вообще почти не затронул, анализ - поменялись методы в доказательствах некоторых теорем, от теории множеств в интуиционизме вообще почти камня на камне не осталось, лол. Т.е. что получилось - вычислимые разделы математики с некоторыми оговорками истинны как классически, так и конструктивно, а всякий аутизм и вера в невычислимую хуитку сразу же показывают свою несостоятельность. Арифметика, т.о. более адекватные основания математики, чем логика.
Аноним 06/03/17 Пнд 12:51:41 12688 179
>>10795
Кстати, подумалось вдруг. А ведь постулат "всегда можно сделать ещё один шаг" прямо противоречит аксиоме выбора. В самом деле, рассмотрим множество возможных букв на листе бумаги и упорядочим его булеан по включению. Очевидно, любая цепь мажорируется своим объединением. Тогда по лемме Цорна есть максимальный элемент - должно существовать множество букв, к которому уже нельзя добавить ни одной буквы. Но ультрафинитисты говорят, что к любому множеству букв на листе можно, исхитрившись, дорисовать ещё одну букву. Противоречие. Аналогичное доказательство для шагающего человека оставим читателю в качестве упражнения.

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

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

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

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

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

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

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

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

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

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

Вопрос вообще простой. Есть у нас какая-то теория поля с лагранжианом $L = d_{\mu} \phi d^{\mu} \phi \ans - m|\phi|^2 - g|\phi|^4 $. Почему этот ебанный раздел все-еще не может в тех!?
Аноним 29/03/17 Срд 22:46:23 13876 217
>>13791
>И да, программы, умеющие в шахматы, перебором тоже не пользуются
Схуяли? Да, там все сложнее, но в основе самый что ни на есть перебор.
Аноним 29/03/17 Срд 23:27:32 13877 218
>>13873
[math] L = d_{\mu} \phi d^{\mu} \phi \ans - m|\phi|^2 - g|\phi|^4 [/math]
Аноним 29/03/17 Срд 23:54:40 13878 219
latexmath.png 69Кб, 2105x627
2105x627
Аноним 29/03/17 Срд 23:56:47 13879 220
Аноним 30/03/17 Чтв 00:25:00 13881 221
>>13878
какой экстеншн ставить?
Аноним 30/03/17 Чтв 10:33:26 13914 222
>>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 13916 223
Аноним 30/03/17 Чтв 14:26:27 13917 224
>>13852
Никак. Кроме конструктивного определения других не завезли.
Аноним 30/03/17 Чтв 15:13:05 13918 225
>>13917
Проорал с ко-ко-консруктивиста.
Аноним 31/03/17 Птн 05:13:53 13927 226
>>13918
А что не так? N петух в свое время правильно говорил, что аксиомы Пеано исходят из того, что нам уже дано натуральное число. Формального определения нету. Не считая бурбаковского аутизма.
Аноним 31/03/17 Птн 15:29:57 13946 227
>>13927
>аксиомы Пеано исходят из того, что нам уже дано натуральное число
Чушь.
Аноним 31/03/17 Птн 17:55:59 13953 228
Снимок.PNG 50Кб, 1217x433
1217x433
>>13946
Схуяли чушь-то? Ты их читал? Давай разберем по частям.
- как видим, 1ая аксиома гласит, что 1 это натуральное число.
- далее определяется то, что в конструктивной математике называют функцией следования succ().
- далее некоторые свойства единицы, равенства и индукция.
Нигде нет определения, что такое единица, она просто вводится в 1ой аксиоме как готовый объект, в остальных аксиомах определяются некоторые ее свойства. Отсюда и вопрос - где формальное определение того, что есть 1? Нету его. Конструктивно я могу сказать, что по Маркову единица, как и любое натуральное число, является словом в алфавите |. Либо могу приплести нумералы Черча. Во всех этих случаях я даю конструктивное определение натуральному числу. Аксиомы же Пеано по-сути представляют собой правила построения N, не определяя явно, что есть натуральное число.
Аноним 31/03/17 Птн 20:59:35 13959 229
Аноним 31/03/17 Птн 21:11:02 13961 230
>>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 13972 231
>>13927
>N петух правильно говорил
Ясно.
Аноним 01/04/17 Суб 05:42:50 13991 232
>>13961
Но твои правила с тем же успехом можно считать описанием множества вещественных чисел, конкретно N они не определяют. В отличие от моих конструктивгых определений конкретно множества N.
Аноним 01/04/17 Суб 05:45:41 13992 233
>>13961
И да, единицу ты вводишь как уже предсуществующий объект, без определения его формально.
Аноним 01/04/17 Суб 11:20:13 13997 234
>>13991
Нет, структуре вещественных чисел описанная мной структура не изоморфна.

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

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

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

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

>вектор того же самого сказать нельзя
Вещественные числа - это векторное пространство, т.е. каждое вещественное число - вектор. Натуральные числа можно определить как подмножество вещественных чисел, см. анализ Зорича. Таким образом, всякое натуральное число - вектор, и всё, что сводится к натуральным числам, сводится и к векторам.
Аноним 01/04/17 Суб 15:43:09 14018 245
>>14017
Что есть x∈N во второй аксиоме?
Аноним 01/04/17 Суб 15:48:26 14019 246
Аноним 01/04/17 Суб 15:51:27 14020 247
>>14019
Ну 0 понятно, пустое множество. А х что такое?
Аноним 01/04/17 Суб 15:53:10 14021 248
>>14020
Кек. Ты тредом, похоже, ошибся.
Аноним 01/04/17 Суб 15:55:40 14022 249
>>14019
Ну то есть, я что имею в виду. Твоя система аксиом в принципе повторяет >>13834 но там-то понятно, что a:N это натуральное число, которое к примеру есть нумерал Черча или хоть слово в алфавите | по Маркову. А у тебя х - это что? Определение его есть?
Аноним 01/04/17 Суб 15:56:40 14023 250
>>14020
Всякий элемент N - это множество вида {∅, {∅}, {∅, {∅}}, {∅, {∅}, {∅, {∅}}}, ... }. Но вообще вторая аксиома - это просто формула ∀x[x∈N → [x∪{x}]∈N]. Ты ведь знаешь, что такое квантор, да?
Аноним 01/04/17 Суб 16:15:27 14024 251
>>14023
Я знаю, что такое квантор. А это - {∅} у тебя что?
Аноним 01/04/17 Суб 16:19:47 14025 252
>>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 14026 253
>>14025
Вот и до нумералов Черча добрались. Вместе с >>14017 правилами построения N. И что же во всем этом неконструктивного? Итого, пришли к >>13917
Аноним 01/04/17 Суб 16:31:04 14027 254
>>14026
Это не нумералы Черча, это классическое определение по фон Нейману.
Аноним 01/04/17 Суб 16:32:36 14028 255
>>14027
Но равнообъемное с нумералами Черча.
Аноним 01/04/17 Суб 16:33:28 14029 256
>>14028
А также с кучей других вещей.
Аноним 01/04/17 Суб 17:04:37 14030 257
>>14029
А значит, это конструктивное определение N.
Аноним 01/04/17 Суб 17:06:54 14032 258
Аноним 01/04/17 Суб 17:09:14 14033 259
>>14032
Потому что равнообъемно с конструктивным.
Аноним 01/04/17 Суб 17:10:08 14034 260
>>14033
И разве это значит, что оно конструктивно?
Аноним 01/04/17 Суб 17:10:52 14035 261
Аноним 01/04/17 Суб 17:12:15 14036 262
>>14035
Ну хотелось бы пруф.
Аноним 01/04/17 Суб 17:36:44 14038 263
>>14036
На каждой итерации ординалов фон Неймана и нумералов Черча получается одно и то же натуральное число.
Аноним 01/04/17 Суб 18:27:01 14041 264
>>14038
У ординалов фон Неймана нет итераций.
Аноним 01/04/17 Суб 18:56:37 14044 265
>>14025
Математики считают пустоту?
Аноним 01/04/17 Суб 19:08:48 14045 266
>>14044
Её считают не только математики.
Аноним 01/04/17 Суб 19:36:59 14048 267
Аноним 01/04/17 Суб 21:36:30 14056 268
>>14044
Но ведь пустота это только Ø. Даже {Ø} это уже не пустое множество.
Аноним 01/04/17 Суб 22:02:21 14059 269
>>14056
Тсс. Пусть думают, что мы умеем вычислять пустоты.
Аноним 02/04/17 Вск 05:31:00 14067 270
>>14041
Не так назвал значит. Суть не меняется, пусть будет каждый последующий ординал фон Неймана равен каждому последующему нумералу Черча при условии отсчета их с нуля.
Аноним 02/04/17 Вск 23:22:46 14102 271
>>14067
Окей. И как это влечет конструктивность?
Аноним 03/04/17 Пнд 19:08:07 14125 272
>>14102
Элементарно. Есть две равнозначные системы. Одна из них конструктивная. Что можно сказать о второй?
Аноним 03/04/17 Пнд 20:23:17 14126 273
>>14125
В общем случае - ничего. Иначе придётся признать конструктивным любое доказательство с использованием аксиомы выбора, для которого есть конструктивная альтернатива.
Аноним 03/04/17 Пнд 20:50:49 14128 274
Снимок.PNG 80Кб, 565x650
565x650
>>14126
В общем случае - конструктивно все, что вычислимо/построимо и наоборот. Если что-то можно вычислить либо построить, или хотя бы дать правила для построения, то это что-то конструктивно.
Аноним 03/04/17 Пнд 21:06:44 14129 275
Аноним 04/04/17 Втр 08:09:21 14140 276
blob 5Кб, 227x115
227x115
Поясните нубу, допускает ли конструктивная математика пикрелейтед?
Аноним 04/04/17 Втр 15:19:50 14178 277
>>14129
Выходит, ординалы фон Неймана конструктивны.
Аноним 04/04/17 Втр 16:04:40 14180 278
>>14140
Сразу оговорюсь, что сам лично не стою на конструктивистских позициях.
Но насколько я понимаю, можно конструктивно показать, что данное бесконечное пересечение в самом деле описывает пустое множество, в том смысле что можно показать, что всякое число не принадлежит по крайней мере одному из пересекаемых множеств. При этом надо понимать, что с конструктивной точки зрения, нет причин полагать, что пересечение всякой последовательности допустимых совокупностей будет допустимо. Разумеется, в зависимости от сорта конструктивизма, здесь возможны разные уточнения.
Аноним 05/04/17 Срд 03:31:35 14217 279
Аноним 05/04/17 Срд 04:24:23 14220 280
>>14218
>(1,inf) intersect (2,inf) intersect (3,inf)
Да.
Аноним 05/04/17 Срд 08:24:13 14221 281
>>14218
>>14140
Предположим, что бесконечное пересечение содержит точку А.
Тогда можно найти число m, такое что m > A, т.е. {A} ⊄ (m, ∞). Следовательно, пересечение пусто.
Аноним 05/04/17 Срд 08:32:24 14222 282
>>14221
Это доказательство от противного. В конструктивной математике они запрещены.
Аноним 05/04/17 Срд 08:38:44 14223 283
>>14222
Вопрос, как и ответ, со стакэксченджа. Интересует, как это доказывает конструктивная математика.
Аноним 07/04/17 Птн 14:56:45 14457 284
blob 135Кб, 1527x749
1527x749
Как это всё соотносится с пикрелейтед?
Аноним 08/04/17 Суб 11:00:30 14511 285
Вот Эвклид доказал, что множество простых чисел бесконечно от обратного. Конструктивная математика примет сие или потребует чего-то другого?
Аноним 08/04/17 Суб 17:01:50 14516 286
>>14511
Его доказательство требует незначительной доработки напильником. В итоге получается программа, печатающая все простые числа.
База: напечатать 2.
Шаг: пусть напечатаны числа p1, ..., pn; проверяем все числа от pn + 1 до Пpi + 1 на простоту и печатаем наименьшее простое.

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

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

fix
Аноним 18/04/17 Втр 18:30:49 15328 304
Единственный на данный момент разумный вариант обойти проблему останова - не связываться с тьюринг-полными системами.
>>15327
А ты можешь предложить метод, не сводящийся к алгоритмическому, т.е. в общем случае к все той же машине Тьюринга?
Аноним 18/04/17 Втр 18:42:09 15335 305
>>15328
Мой вопрос был лишь в том, является ли само доказательство теоремы об остановке конструктивным, и если нет - возможно ли построить его так, чтоб оно было конструктивным и если невозможно, то понять почему. Я конечно вообще нуб, но сейчас это выглядит так, как будто доказательство этой теоремы конструктивными методами невозможно по причинам, которые из этой же теоремы и выводятся. Т.е. во время доказательства теоремы, мы применяем следсвия из неё, что как бы странно, ведь мы её ещё не доказали.
Аноним 18/04/17 Втр 19:36:50 15386 306
>>15318
Не существует конструктивного доказательства изоморфизма Карри-Говарда.
Аноним 18/04/17 Втр 19:46:31 15394 307
>>15386
Чего несешь? Изоморфизм Карри-Говарда - построение множества конструктивных пруф-объектов. Наличие таких построений есть конструктивное доказательство возможности рассматривать пропозишены как множества пруф-объектов.
Аноним 18/04/17 Втр 19:57:35 15395 308
>>15394
...при условии, что у нас доказан изоморфизм Карри-Говарда. Но именно его мы доказываем.
Аноним 18/04/17 Втр 22:23:44 15419 309
То есть ответ на вопрос разрешима ли проблема останова на МТ в конструктивной математике - это "хуй знает"?
Аноним 19/04/17 Срд 01:17:21 15436 310
Типизированность языка значит, что записать можно только корректные построения/доказательства, иначе “не компилируется”, а доказательства являются такими же объектами как и другие математические объекты (например, множества). Тот аспект, что непрерывность здесь выступает как правилом синтеза, так и обоснования получает выражение в гомеоморфной теории типов (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 15452 311
Снимок.PNG 43Кб, 574x369
574x369
>>15395
Применимость = доказательство. Конструктивные системы вычислимы и выводимы сами из себя, без внешних дополнений. Именно это делает конструктивную логику полной по Геделю. Любая конструктивная аксиоматика - сама по себе конструктивный объект, правила вывода в ней - тоже. Поэтому корректность системы выводима из нее самой. Это азы, так-то. Именно подобные свойства конструктивных логик, того же изоморфизма Карри-Говарда, дают возможность строить проверяемые доказательства теорем, а интерпретация логических констант по Колмогорову - и писать абсолютно корректные программы на языках с зависимыми типами.
>>15436
Истину копипастишь. НоТТ - очень крутая вещь, но в зачаточном состоянии пока что.
Аноним 19/04/17 Срд 11:17:25 15453 312
>>15452
Почему она в таком состоянии? Что там пока не так? Сколько это будет продолжаться?
Аноним 19/04/17 Срд 11:28:17 15455 313
photoNormal.jpg 61Кб, 600x450
600x450
>>15453
Потому что это очень новое направление конструктивной математики. И сколько бы выдающихся умов над ней не работали, все равно за какие-то несколько лет невозможно проделать всю работу. В НоТТ книге описаны открытые проблемы. Радует, что с самого начала эту теорию пилили очень правильно - сразу в пруверах, чтобы поменьше аутизма, побольше фактического материала. Да и все доказательства с самого начала проверены, это значит, что в дальнейшем не вылезет никакой нежданчик, который просто не заметили сразу. По хорошему, нужны сразу пруверы с ядром на НоТТ, но такой пока что только один - LEAN.
Аноним 19/04/17 Срд 17:26:11 15490 314
VOEVODSKIIVladi[...].jpg 661Кб, 1000x1334
1000x1334
Кому интересно, онлайн-версия библиотеки НоТТ для Coq на жабаскрипте - https://x80.org/rhino-hott/ можно гонять конструктивные основания прямо в браузере.
Аноним 19/04/17 Срд 19:18:11 15507 315
>>15490
Быстрее окамл установить чем ждать пока оно загрузится.
Аноним 19/04/17 Срд 19:55:18 15511 316
>>15455
>что в дальнейшем не вылезет никакой нежданчик, который просто не заметили сразу
А тут PA возьми и окажись противоречивой (а соответственно и все мало-мальски сильные теории типов). Или найдется ошибка в ядре Coq. Ну или, скажем, систематическая ошибка во всех процессорах архитектуры x86, что повлекло положительную проверку неверных доказательств. Последнее, положим, выглядит крайне маловероятно. Но тем не менее, формализация на компьютере не дает абсолютных гарантий.
Аноним 20/04/17 Чтв 00:10:28 15537 317
В редукции математических доказательств Брауэр и Вейль доходят до интуитивного фундамента полной индукции и рассматривают ее как математическую "праинтуицию". Как математики, они имеют право поступать таким образом. Математики не обязаны исследовать вопрос о том, как получаются понятия, которые они кладут в основу доказательств математической науки в качестве исходных и недоказуемых. Но как философски мыслящие математики (а они сами себя считают такими) "интуиционисты" не имеют права на этом останавливаться. Они обязаны, дойдя до "праинтуиции" математики, вести свою редукцию дальше "назад". Они обязаны ответить на вопрос о генезисе самой этой "праинтуиции". Они обязаны точно и обстоятельно разъяснить, в чем состоят признаки "интуитивной ясности", на которую они постоянно ссылаются, но которая без соответствующих разъяснений легко может быть смешана с субъективной "оценкой" сознания, лишенной общезначимого и, следовательно, научного содержания.

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

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

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

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

Их идеализм был не только догматичен и не только метафизичен по методу, неспособному применить генетическую точку зрения к самому явлению интуиции в человеческом мышлении. Он, кроме того, был агрессивен по своей направленности и нетерпим. Правильно утверждая, что построение в математике подчиняется логике решения проблем, отличной от классической, "интуиционисты" типа Брауэра и Вейля полагали, будто только эта логика имеет право на признание в математике. Вразрез с этой точкой зрения академик А.Н.Колмогоров показал, что между принципами классической логики и принципами "конструктивной" логики "интуиционизма" не существует отношения исключающего противоречия: "интуиционистская" логика есть логика новой и особой области исследования, ею не исключаются принципы доинтуиционистской логики; они лишь подвергаются ограничению там, и только там, где это ограничение вызывается своеобразием исследуемой области объектов.
Аноним 20/04/17 Чтв 01:38:47 15540 318
>>15537
damn
Колмогоров bitchslapped Брауэра также как Лузина.
Аноним 20/04/17 Чтв 06:05:57 15546 319
>>15544
Это не определения. Это нонсенс.
Когда в конструктивных исследованиях будут открыты новые интересные математические факты? Какие теоремы доказаны конструктивистами? Где интуиционистские теоремы Пуанкаре? Где интуиционистские интегральчики?
Аноним 20/04/17 Чтв 07:25:29 15548 320
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 15549 321
>>15547
Проинтегрируй sin конструктивно.
Аноним 20/04/17 Чтв 07:43:45 15550 322
>>15547
Ясно все с вашим анализом.

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

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

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

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

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

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

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

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

Но это я с дивана пишу. Я вообще больше мамин философ.
Аноним 21/04/17 Птн 22:21:44 15735 343
>>15733
Твой вопрос тупой.
Все тупые вопросы я буду игнорировать.
(Автор этого поста был предупрежден.)
22/04/17 Суб 00:13:25 15738 344
>>15735
А почему тупой? Тем, что тебе не нравится и ломает твою маня-идеологию?
>Все тупые вопросы я буду игнорировать.
Веруны тоже игнорируют доказтельство того, что в их книжках полная туфта.
(Автор этого поста был предупрежден.)
Аноним 22/04/17 Суб 05:05:47 15742 345
>>15733
Есть. И я даже сто раз писал об этом с цитатами. Сами правила тоже конструктивный объект, как и результаты вывода по ним. Все выводимо и проверяемо, никакой веры.
Аноним 22/04/17 Суб 05:09:21 15743 346
>>15738
Это какой'то подгоревший пишет. Про правила вывода сто раз все разжевано уже с цитатами, даже в этом треде выше. Суть в том, что все выводимо из самих конструктивных объектов.
Аноним 22/04/17 Суб 05:13:15 15744 347
>>15734
Нет, ты не понял. Актуальная бесконечность это бесконечность сама по себе, не связанная ни с каким объектом, ни с какими правилами построения чего'либо.
Аноним 22/04/17 Суб 09:33:35 15745 348
>>15742
>Все выводимо и проверяемо, никакой веры
Только в рамках аксиом, принятых в данной конкретной математической системе, и только по принятым в ней же правилам вывода из них.
Да и то. Обычно с периодическим маханием руками "да, вот тут у нас обнаружился неудобный парадокс, ну и хрен с ним, будем обходить это место".
Аноним 22/04/17 Суб 09:42:00 15746 349
>>15745
Да ты и правда не очень умный. Тебе же говорят, сами правила тоже конструктивные объекты, как и вывод по ним. Корректность вывода в таких системах,, это так же конкретное построение.
Аноним 22/04/17 Суб 09:45:46 15747 350
>>15745
И никаких парадоксов со времен самого Брауэра. Т.н парадокс Жирара фиксится элементарно введением иерархии вложенных универсумов вместо неконструктивного общего правила, который его и вызывал. Других антиномий вообще не завезли.
Аноним 22/04/17 Суб 10:13:42 15749 351
>>15747
Ну и в чем тогда преимущество по надежности перед, "религией" (теорией множеств). И там и там, неаккуратная формализация приводила к парадоксам. И там и там все пофиксили переходом к предикативным построениям. Иными словами не видно, чтобы интуиция касательно интуиционистской математики давала меньше сбоев, чем интуиция касательно теоретико-множественной.
Аноним 22/04/17 Суб 10:50:39 15750 352
>>15749
Очень важное, хотя и не единственное преимущество конструктивного подхода - его автоматизируемость, в частности, непосредственная реализуемость на комплюктере, без дополнительных костылей, прямо в соответствии с колмогоровской интерпретацией логических констант и изоморфизмом Карри-Говарда (программы как доказательства). С неконструктивными аксиоматиками так не выйдет, комплюктер ты веровать не заставишь, а невычислимое оно и в африке невычислимое, правил для его вычисления нет. Причем, как сказано выше, проверяемы на корректность и сами правила проверки на корректность, что означает тотальную корректность и выводимость той же MLTT. С ZFC ничего даже близко подобного не выйдет, хотя костыльные реализации и возможны, все через те же типы, н-р в Coq'е.
Аноним 22/04/17 Суб 10:55:22 15751 353
>>15749
>И там и там, неаккуратная формализация приводила к парадоксам.
К слову, интуиционизм Брауэра не формализуем, о чем говорил в т.ч. создатель интуиционистской логики Гейтинг, и парадоксов там не было, нет и не может быть принципиально, поскольку это не какая-то там формальная система.
Аноним 22/04/17 Суб 11:08:37 15754 354
>>15743
Я говорил о том, естил у консрктивного объекта правило построение правил построения? И правил построения есть ли правила построение правил построения правил построения?
Аноним 22/04/17 Суб 11:49:50 15757 355
>>15750
>в частности, непосредственная реализуемость на комплюктере
Ну смотри, в теории множеств я могу доказать, например, что всякий фильтр расширяется до ультрафильтра, что вполне подходит под твое замечание про отсутствующую реализации на компьютере. В тоже время MLTT, и многих других естественных интуиционистских теориях, несложно доказать, что для всюду определена супер-экспоненциальная функция (supexp(0)=1, supexp(n+1)=2^{supexp(n)}). Но не то, чтобы вычисление supexp(10) могло быть реализовано на реальном компьютере. То есть эта реализуемость в общем случае носит совершенно абстрактный характер. Если же хочется реализуемость на реальном компьютере, то нужна вычислимость с адекватной сложностью. Но если хочется доказать, например, что некоторые объекты не просто существуют, а могут быть найдены за полиномиальное время, то дополнительные усилия потребуются и в конструктивных и в некоструктивных системах.
Аноним 22/04/17 Суб 13:03:30 15762 356
>>15754
Все есть. Меня правда, несколько подзаебало пояснять в пустоту. Если бы ты понимал такие темы как интерпретация логических констант по Брауэру-Гейтингу-Колмогорову, натуральная дедукция Генцена-Правитца, изоморфизм Карри-Говарда, куб типизированных лямбда-исчислений а-ля Черч Барендрегта, наконец-таки MLTT, то м.б. что-то и вынес бы из моих объяснений. А так, все это выглядит как лекция в детском саду про мочидзукину теорию пространств Тейхмюллера.
>>15757
Закон исключенного третьего все равно придется выбросить, т.к. он невычислим. Но, если мы выкидываем из некоей аксиоматики невычислимую хуету, остается что-то более-менее заменимое на конструктивную логику.
Аноним 22/04/17 Суб 15:22:53 15775 357
Как конструктивная математика может может формализировать некоторые невычислимые вещи, такие, как Spectral gap (важная вещь в физике)?
Аноним 22/04/17 Суб 16:18:48 15788 358
Так что, кто-то запилит конструктивное доказательство теоремы остановки веруна Тьюринга? Или так дальше и придётся веровать что проблема остановки неразрешима на МТ?
Аноним 22/04/17 Суб 16:31:22 15790 359
>>15788
Факт в том, что существуют алгоритмически неразрешимые проблемы.
Аноним 22/04/17 Суб 17:10:07 15796 360
>>15790
Большинство алгоритмически неразрешимых проблем доказовались таковыми путём сведения к проблеме остановки, неразрешимость которой вроде как доказана. Но доказана она неконструтивно, вот в чём проблема.
Кстати, доказательство, что задача определения того, является ли частично рекурсивная функция с данным описанием общерекурсивной или нет, алгоритмически неразрешима - так же проведено неконструтивно.
Получается, что в рамках конструктивной логики вообще нет доказательств существования алгоритмически неразрешимых проблем?
Аноним 22/04/17 Суб 17:21:41 15797 361
>>15796
Ты бы хоть погуглил, что вообще есть кончтруктивная математика. Конструктивное доказательство - это построение.
Аноним 22/04/17 Суб 19:54:35 15802 362
>>15797
Ну и отказ от правила исключения третьего. Следовательно - отказ от доказательства от противного. Все доказательства того, что проблема алгоритмически неразрешима - проводятся от противного, как, например, доказательство теоремы останова у Тьюринга.
Мой вопрос, как в конструктивной математике доказать что та или иная проблема алгоритмически неразрешима? Это вообще возможно?
Аноним 23/04/17 Вск 01:33:00 15881 363
>>15802
> отказ от доказательства от противного
Если у тебя есть утверждение вида "не А", например, "не (разрешимо что-то)", то ты имеешь полное конструктивное право сказать "предположим, что A, приведем к противоречию и вуаля". Это только с точки зрения классической математики может показаться, что тут что-то противное, а так вообще-то в любом варианте "не A" можно считать синонимом "если А, то ложь". А нельзя наоборот, A доказывать через приведение "не А" к противоречию.

Поэтому все утверждения о неразрешимости доказываются в конструктивной логике безо всяких проблем.
Аноним 23/04/17 Вск 04:46:59 15890 364
>>15802
Я в каждом втором посте говорю о конструктивной интерпретации логических констант. Любое доказательство допустимо, если оно построимо, никто не против принципа исключенного третьего в случаях когда он доказуем. То же про конструктивное отрицание и т.д. есть отказ от веры в общие принципы без общего метода их построения, а вовсе не какие'то догмы уроынч 'отказа от принципа исключенного третьего потому что богородица не велит'.
Аноним 23/04/17 Вск 11:01:57 15901 365
А можно меня, мимокрокодила, ввести в краткий курс дела. Чем примечательна конструктивная математика? Она примечательная только в основаниях математики или же это что-то типа "ко-ко-революции" в математике?
Аноним 23/04/17 Вск 11:23:14 15902 366
>>15901
Конструктивная математика примечательна тем, что это настоящая математика, построимая и вычислимая. Без мутных верований в невычислимые вещи, от которых одни кризисы и неполнота.
Аноним 23/04/17 Вск 12:21:56 15906 367
>>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 15912 368
>>15906
Это не математика. Это быдлокод. Какая идея стоит за этим кодом? Да никакой.
Аноним 23/04/17 Вск 13:21:34 15924 369
>>15906
Ну и чем принципиально отличается
if(x != 0) и if(t >= 0)
от
(доказательство x != 0) и (доказательство z > 0)
?

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

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

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

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

> анализа
По крайней мере с непрерывными функциями все хорошо.
Аноним 25/04/17 Втр 10:13:54 16278 385
>>16237
Лучше Брауэра никто пока не определил что есть существование в математике. Более того, обычно ответом на этот вопрос являются жалкие оправдания, уровня "ито философия, а не математика!!111". С чего бы? О какой вообще математике можно говорить, если нет даже внятного определения, в каком именно случае мы можем сказать, что математический объект существует и в каком смысле следует понимать его существование? Это тот вопрос, с которого должна начинаться математика. Собственно, точку зрения Брауэра я уже приводил >>15731
Аноним 25/04/17 Втр 10:21:25 16279 386
>>16278
Да, один момент. Это было написано Брауэром во времена, когда Гедель еще пешком под стол ходил, и никакой теоремы о неполноте сформулировано не было. Это уже позже было доказано, что работая с математикой как с языком ее представления (одним из возможных), так или иначе встает проблема двух стульев, на одном из которых противоречивость точеная, на другом - неполнота дроченая. Гильберт со своей программой формализации арифметики присел сразу на оба стула, бурбаки предпочли помереть (даже с официальным некрологом), т.к. со своим трактатом тоже рано или поздно приблизились бы к упомянутым стульям, что было отмечено даже в предисловии переводчика первого тома про теорию множеств.
Аноним 25/04/17 Втр 12:36:21 16280 387
>>16278
Определение Брауэра неадекватно математической практике. Со времен Евклида математики успешно работали с объектами, которые не умели строить, и даже не пытались строить.
Аноним 25/04/17 Втр 12:40:13 16281 388
>>16280
>Со времен Евклида математики успешно работали с объектами, которые не умели строить, и даже не пытались строить.
Например? Какие это объекты?
Аноним 25/04/17 Втр 15:31:53 16288 389
lejb.jpg 31Кб, 489x471
489x471
Ладно, Брауэр для мейлру сложна. Давайте попроще.
- конструктивный объект - это всегда некое слово в некоем алфавите.
- конечные слова в конечных алфавитах можно прямо занумеровать натуральными числами, лексикографическим упорядочиванием, геделевской нумерацией, не суть.
- т.о. всю конструктивную математику можно напрямую свести к арифметике. Поэтому вся конструктивная математика вычислима, а единственными адекватными основаниями математики является арифметика. Не логика.
Вопрос, можно ли вычислить нечто, не сводимое вышеупомянутым либо каким-то другим способом к арифметике?
Аноним 25/04/17 Втр 16:53:34 16289 390
>>16288
> это всегда некое слово в некоем алфавите.
Что такое алфавит и что такое слово?
>- т.о. всю конструктивную математику можно напрямую свести к арифметике. Поэтому вся конструктивная математика вычислима, а единственными адекватными основаниями математики является арифметика. Не логика.
Нельзя же доказать непротиворечимость арифметики её же соственными методами. Разве нет? И если каждая такая конструктивная математика сводится к арифметике, то нам остаёться верить в её непротеворичивость?
Аноним 25/04/17 Втр 16:56:27 16290 391
>>16289
>Нельзя же доказать непротиворечимость арифметики её же соственными методами. Разве нет?
Формально-аксиоматически нельзя, у меня так программа Гильберта проебалась. Конструктивно можно.
>Что такое алфавит и что такое слово?
Писал не единожды, с примерами.
Аноним 25/04/17 Втр 16:57:45 16291 392
>>16290
>Писал не единожды, с примерами.
Ещё раз напиши.
>Формально-аксиоматически нельзя, у меня так программа Гильберта проебалась. Конструктивно можно.
И как? Разве это не будет формальной системой?
Аноним 25/04/17 Втр 17:02:48 16292 393
>>16291
>Ещё раз напиши.
Простейший пример: алфавит из одного знака |, слово в этом алфавите - натуральное число, н-р |||| = 4.
>Разве это не будет формальной системой?
Опять же, про интерпретации логических констант сто раз писано, и в чем разница между чисто формальным и конструктивным подходом на примере синтетических и аналитических кантовских суждений, даже лекцию Мартин-Лёфа приносил, тоже не один раз.
Аноним 25/04/17 Втр 17:06:41 16293 394
>>16292
>Простейший пример: алфавит из одного знака |, слово в этом алфавите - натуральное число, н-р |||| = 4.
Я не понимаю, как это отличается от формального определения N? Мы говорим, что существует знак, который рассматриваем, как еденицу и вместо его сложения с другими знаками, как с числами рисует еденицы. Правда, как это отличается от формального определения?
>Опять же, про интерпретации логических констант сто раз писано, и в чем разница между чисто формальным и конструктивным подходом на примере синтетических и аналитических кантовских суждений, даже лекцию Мартин-Лёфа приносил, тоже не один раз.
Ты можешь привести конкретный пример, почему твоё определение N не формальная система? А не отсылать куда-то? Я хочу услышать твоё объяснение этому.
Аноним 25/04/17 Втр 17:07:37 16294 395
>>16281
Например, с отрицательными числами. До XIX века об их существовании велись ожесточеннейшие споры. Даже Гаусс был вынужден отражать нападки философствующих околоматематиков, кричавших, что отрицательных чисел нет. Тем не менее, работать с отрицательными числами умели все. Речь именно об отрицательных, комплексные числа отдельная история. В XIX веке была предложена строгая теория отрицательных чисел, и спорщики заткнулись.
Аноним 25/04/17 Втр 17:13:10 16295 396
>>16294
Отрицательное число - слово в алфавите - |. Это конструктивные объекты. Пример мимо.
>>16293
>Я не понимаю
В этом все дело. Разница в интерпретации логических констант. Чуть выше ИТТ уже выяснили, что единственным адекватным определением N можно считать ординалы фон Неймана, там же выяснили, что это те же нумералы Черча, вид сбоку. Т.е. конструктивная система.
Аноним 25/04/17 Втр 17:15:08 16297 397
>>16295
>В этом все дело. Разница в интерпретации логических констант. Чуть выше ИТТ уже выяснили, что единственным адекватным определением N можно считать ординалы фон Неймана, там же выяснили, что это те же нумералы Черча, вид сбоку. Т.е. конструктивная система.
Ты не понял. Я хочу, чтобы ты объяснил, почему это не формальная система. Если ты говоришь, что выше дано такое объяснение, то приведи на него ссылки и прокоментируй его.
Аноним 25/04/17 Втр 18:01:02 16298 398
>>16288
ЛЮБУЮ формальную систему можно рассмотреть как множество конечных слов в некотором алфавите - на которое наложено несколько дополнительных условий.

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

>>16295
ЛЮБОЙ математический объект - слово в некотором алфавите. Теоретически достаточно всего одного символа, кстати. На практике используются более богатые алфавиты.
Аноним 25/04/17 Втр 18:06:29 16299 399
>>16298
Я это уже писал >>14128 Вопрос был не в этом, а в том, как невычислимую хуитку типа закона исключенного третьего или актуальную бесконечность представить в такой же форме? Очевидно, что если знак бесконечности считать символом / термом / словом в некоем алфавите, то у него должны быть правила вычисления в канонический элемент множества или типа. Т.к. сам этот знак не является каноническим элементом. А таковых правил не существует. Вот и приплыли.
Аноним 25/04/17 Втр 18:08:40 16301 400
>>16299
Открой для себя первую главу Бурбаки. Вопросы отпадут.
Аноним 25/04/17 Втр 18:12:09 16302 401
>>16301
Читал я ваших бурбаков. У меня даже бумажная книшка есть. Ты расскажи, как ты неканонический элемент в канонический вычислять будешь, если правил вычисления нет? Значками играться можно сколько угодно, в итоге придем либо к противоречию, либо к неполноте, что есть свойства любой формальной системы, сводящейся к синтетическому суждению (опять же возвратимся к лекции Мартин-Лёфа).
Аноним 25/04/17 Втр 18:14:00 16303 402
>>16302
Ты говоришь как человек, который не читал/не понял первую главу Бурбаки.
Давай разберемся вместе, если ты не против.
Аноним 25/04/17 Втр 19:38:17 16305 403
>>16303
Судя по молчанию - против.
Аноним 25/04/17 Втр 22:01:28 16311 404
Эта продвинутая типизация подойдет к клэйтронике?
Аноним 26/04/17 Срд 05:20:45 16324 405
>>16305
Читал и понял. Я уже сто раз говорил в чем разница. В конструктивной системе выразимо только то что там доказуемо, отсюда геделевская полнота. В формальной системе можно выразит то, чего в ней нельзя доказать, т.к для доказательства требуется что'то помимо нее. Это прямое следствие интерпретации логических и др констант.
Аноним 26/04/17 Срд 06:59:00 16325 406
Аноним 26/04/17 Срд 10:09:12 16329 407
>>16324
К какому конкретно положению первой главы Бурбаки у тебя возникают претензии?
Аноним 26/04/17 Срд 10:41:44 16331 408
>>16329
Тебе ж говорят, такой подход изначально ущербен, из'за геделевой неполноты либо противоречивости формальных систем, оторванных от построения. Самый простой пример, закон исключенного третьего, истинный с формально'аксиоматической точки зрения. Он невычислим в общем случае.
Аноним 26/04/17 Срд 11:08:28 16334 409
>>16329
Ты вот з бурбаков поясняешь, а походу и предисловие даже не читал, где написано то , о чем я тебе толкую. Бурбаки даже не упомянули, что весь их подход в итоге в геделя и упирается.
Аноним 26/04/17 Срд 16:16:43 16356 410
>>16331
Бурбаки предложили математику, в которой любой математический объект построим как конечное слово в некотором алфавите. То есть осуществили в точности твою мечту. Если тебя не устраивает их подход - назови первое же предложение первой главы Бурбаки, с которым ты не согласен.
Аноним 26/04/17 Срд 16:46:11 16359 411
>>16356
Сейчас бы по сотому разу объяснять самые азы. Ты так и не понял что такое построение математического объекта. У бурбаков речь о построении вообще не идет, а язык рассматривается только как синтаксис. По бурбакам противоречие это синтаксическая ошибка. Выражение на бурбаковском языке не обязательно построимо, даже если и выразимо на нем. Пример все тот же, закон исключенного третьего. В нем нет ошибок по бурбакам, но он не вычислим и не построим. Я уже не знаю как проще объяснить, про интерпретации логических констант тцт вообще не воспринимают.
Аноним 26/04/17 Срд 16:58:36 16363 412
>>16359
Математические объекты по Бурбаки и есть слова. Каждый математический объект построим точно в том же смысле, в каком натуральное число построимо из палочки |.
Аноним 27/04/17 Чтв 01:08:40 16398 413
>>16363
Ты просто не понял. Знакосочеетания бурбаков это просто синтаксис. В котором выразима любая хуйня, сколь угодно непостроимая. Хоть знак бесконечности, хоть закон исключенного третьего. У них нет понятия выводимости, пруф'объектов, базиса и т.п. у Мартин'Лефа в лекции разница рассмотрена подробно, ссылку я сто раз давал и своими словами пояснял.
Аноним 27/04/17 Чтв 01:13:16 16399 414
А вот если бурбаковский синтаксис рассмотреть через изоморфизм Карри'Говарда, то да, это будет конструктивной системой, но тогда в ней нельзя будет выразить непостроимых объектов.
Аноним 27/04/17 Чтв 02:30:00 16402 415
Еще пример, чтобы было понятно. Знакосочетание 'Аллах' не является построением Аллаха, хотя и является когечным словом в конечном алфавите. Но, еще раз, у нас нет правил для вышеупомянутого построения.
Аноним 27/04/17 Чтв 04:32:17 16403 416
>>16398
Нет ты. Палочки - это тоже просто синтаксис. Раз выразима - значит построима.

>>16402
Тогда и знакосочетание ||||| не является построением числа пять.
Аноним 27/04/17 Чтв 05:28:58 16404 417
>>16398
>У них нет понятия выводимости
Лолчто.
Аноним 27/04/17 Чтв 05:30:39 16405 418
>>16402
Аллах="Аллах". Аллах и есть слово в конечном алфавите. Это просто слово, никакого иного смысла в нём нет.
Аноним 27/04/17 Чтв 08:32:04 16408 419
>>16403
В конструктивной математике кроме синтаксиса есть семантика, в т.ч номинальные дефиниции и правила вычисленичя неканонических объектов в канонические. Поэтому палочки и т.д можно вычислить в натуральные числа, а знакосочетания бурбаков вычислимы только когда выражают канонические объекты. Слово 'Аллах' невычислимо ни во что, так же как и закон исключенноно третьего, хотя и то и другое выразимо в бурбаковской нотации.
Аноним 27/04/17 Чтв 11:06:08 16418 420
>>16408
Эти термины даже не гуглятся.
Аноним 27/04/17 Чтв 11:27:59 16419 421
PerMartin-Lofbig.jpg 24Кб, 329x400
329x400
>>16418
Так я уж на пальцах пытаюсь объяснить, зачем нужен изоморфизм Карри-Говарда и конструктивные интерпретации логических констант. И что ты хочешь на русском языке нагуглить? Лекция Мартин-Лёфа на английском, как и термины типа canonical, non-canonical constants, nominal definition и т.д. Ты главное пойми - если бы все было так просто, как тебе кажется, то изначальная программа Гильберта по формализации арифметики не провалилась бы. А метаматематика, которую ты у бурбаков в первой главе увидел - это уже шаг к конструктивизации математики. Отсюда и некоторое сходство типа наличия алфавитов, знаков, знакосочетаний. Но без вышеупомянутых вещей типа BHK-интерпретации и изоморфизма Карри-Говарда, такой подход мало чем интересен, опять же сто раз писал почему - возможны синтаксические выражения, не имебщие под собой объектов-построений, типа закона исключенного третьего. Я про эту лекцию говорю 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
Аноним 27/04/17 Чтв 11:41:17 16420 422
>>16419
Допустим. Определи BHK-интерпретацию и изоморфизм Карри-Говарда, о которых ты так много говоришь. И сделай это, пожалуйста, корректно, без утверждений о навешивании квантора существования на Аллаха. По твоей ссылке какой-то Кант с тучками вместо определений.
Аноним 27/04/17 Чтв 11:46:45 16422 423
Аноним 27/04/17 Чтв 15:16:52 16430 424
>>16408
Подожди, то есть палочки - это не натуральные числа? А что такое "натуральные числа" тогда?
Аноним 27/04/17 Чтв 17:59:22 16458 425
Аноним 28/04/17 Птн 05:25:02 16491 426
>>16430
Натуральные числа - это мощности конечных множеств.
Аноним 28/04/17 Птн 12:27:10 16501 427
>>16491
Что, серьёзно? Мощности? Не ординалы?
Аноним 28/04/17 Птн 13:07:50 16503 428
aleph-null2.jpg 13Кб, 300x269
300x269
>>16491
>>16501
Свидетели теории множеств приехали :3 Давайте-ка, раскидайте за вашу веру. Континуум непостроим же, с каких хуев вы веруете, что его мощность = алеф1? И если алеф0 - это мощность N, чему равно число алеф0 минус 1?
Аноним 28/04/17 Птн 14:25:00 16504 429
>>16503
Как свидетель теории множеств замечу, что
1. Нельзя говорить о сферической построимости в вакууме.
2. В стандартной аксиоматике (ZFC плюс-минус классы) нельзя доказать, что мощность континуума равна алеф1. Опровергнуть это также нельзя. Поэтому тот, кто говорит, что мощность континуума равна алеф-1, не разбирается в современной дефолтной теории множеств.
Однако мы ввели специальные числа бет (вторая буква еврейского алфавита). Легко доказать, что мощность континуума равна бет-1.
3. Зависит от того, как ты определяешь минус. Аналогия с натуральными числами здесь не работает, и определение должно быть ясным, внятным.
Аноним 28/04/17 Птн 14:37:59 16505 430
>>16504
>Нельзя говорить о сферической построимости в вакууме.
Что значит "сферической в вакууме"? Построимость полностью определяется правилами построения, которые так же являются конструктивным объектом, и т.д., я об этом сто раз писал.
>Легко доказать, что мощность континуума равна бет-1.
Вот так маневр, не слыхал. Судя по педивикии, бет1 это булеан алеф0 (2^алеф0), или я не так понял?
>Аналогия с натуральными числами здесь не работает, и определение должно быть ясным, внятным.
А что работает? Так-то сложнее придумать что-то внятнее и яснее арифметики. Если речь об алеф0, который есть кардинал N, то почему для работы с ним нельзя использовать натуральные числа? Шаманство какое-то, не?
Аноним 28/04/17 Птн 15:06:01 16506 431
>>16505
1. Определения на бочку.
2. Бет1 - это 2^ℵ0. Мощность булеана счетного множества, если угодно.
3. Сложение кардиналов вполне естественно. Вычитание не настолько интуитивно и потому должно быть определено строго.
Аноним 28/04/17 Птн 16:28:05 16513 432
>>16506
>Определения на бочку.
Определение чего? Построения? Сто раз уже обсуждали, тут так никому и не зашло. И через акты интуиционизма Брауэра, и через BHK интерпретацию и изоморфизм карри-Говарда. Бесполезно ж, как в том анекдоте "и унитаз приносил, и жопу показывал, все равно бумагу не продали".
>Сложение кардиналов вполне естественно. Вычитание не настолько интуитивно и потому должно быть определено строго.
Вопрос в том, есть ли изоморфизм между кардиналами и натуральными числами. Если есть, то какой число соответствует кардиналу алеф0? Если нету, то о чем тут вообще говорить.
Аноним 28/04/17 Птн 17:09:38 16516 433
>>16513
1. Да, определение построения.
4. Об изоморфизме в какой категории идёт речь?
Аноним 28/04/17 Птн 17:19:17 16518 434
>>16516
1. написал же в посте даже.
2. ну, скажем, соответствие между кардиналами и соотв. им натуральными числами. Оно есть?
Аноним 28/04/17 Птн 18:04:17 16521 435
>>16518
1. "Построение - это ...". Где у тебя написаны такие слова? Не вижу.
2. Класс кардиналов настолько велик, что даже не является множеством. Натуральные числа можно отождествить с точками ℵ0.
Аноним 29/04/17 Суб 01:30:16 16565 436
>>16501
Множество кардиналов конечных множеств изоморфно множеству ординалов конечных множеств. Для натуральных чисел Card(n) = Ord(n)
Аноним 29/04/17 Суб 01:35:30 16566 437
>>16503
Операцию вычитания можно ввести не всегда. Даже на множестве натуральных чисел ты не можешь вычесть большее из меньшего. Множество кардиналов также не образует группу по сложению, поэтому вычитание в общем случае на множестве кардиналов ввести нельзя. Впрочем, поскольку из x + 1 = алеф0 следует, что x = алеф0, то можно сказать, что алеф0 - 1 = алеф0. А вот однозначно определить алеф0 - алеф0 нельзя, также как нельзя, например, делить на 0.
Аноним 29/04/17 Суб 05:26:57 16585 438
>>16565
Вот не изоморфно, структуры там всё же разные.
Аноним 30/04/17 Вск 00:26:42 16693 439
IcJM5p2nwIo.jpg 50Кб, 448x448
448x448
Сап гайз

Подскажите пожалуйста какие из теорий учитывают время.

Ну типа:
a = 1; a is 1
a =? 2; a will be 2
a ?= 0; a was 0

А то чет после знакомства с хаскелем, изучая английский я понял что там никак особо не учитывается время. Ну и в прологе вроде тоже.
Аноним 30/04/17 Вск 01:51:38 16699 440
>>16585
Нет, структуры совершенно изоморфны!
Аноним 30/04/17 Вск 03:53:43 16707 441
>>16693
Это ты сам придумал?
Аноним 30/04/17 Вск 05:57:47 16709 442
>>16693
Темпоральные логики.
Аноним 30/04/17 Вск 08:47:57 16710 443
>>16693
Ну раз уж ты знаком с хаскелем, то наверняка знаешь, что переменные можно замутить через state-монаду.
Аноним 30/04/17 Вск 12:04:57 16714 444
Screenshot2017-[...].png 385Кб, 1600x2560
1600x2560
Screenshot2017-[...].png 332Кб, 1600x2560
1600x2560
>>16707
Да. Ну это само в глаза бросилось после пролога, хаскеля и инглиша.

>>16709
Спасибо, это то что нужно похоже.

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



А сейчас мне хочется какой нибудь работающий язык программирования пощупать на LTL или CTL. Ну или/и книжек годных по ним. Но я не математик, просто программирование немного знаю.

Плюс может знаете куда оно все нынче развилось, может что новее есть, включающее TL в себя. Типа помеси нечеткой и темпоральной логики, такое что то.
Аноним 30/04/17 Вск 16:59:04 16738 445
инт7.png 969Кб, 1388x1738
1388x1738
Brouwer4.jpeg 6Кб, 241x326
241x326
>>16693
>>16714
Весь интуиционизм Брауэра построен на восприятии человеком времени. До Брауэра похожие идеи высказывал Кант, но у Брауэра все максимально доведено до ума в 1 акте интуиционизма. То, что у тебя на пике, по-сути частный случай того, что у Брауэра называется two-ity,...,n-ity.
Аноним 01/05/17 Пнд 22:36:28 16878 446
>>16738
Я не особо шарю, но судя по этому треду его теория как то не очень программируется. Ну и мне не осилить чистый матан, вот то что можно потыкать в coq, agda или lean еще может быть как нибудь когда нибудь, а то что сильно оторвано от программирования уже сложновато.

Ну и я еще инглиш не выучил сильно дальше элементарной повседневности.
Аноним 02/05/17 Втр 04:21:53 16908 447
>>16699
я имею в виду структуру (<,+). Там изоморфизм один-в-один
Аноним 02/05/17 Втр 05:34:02 16911 448
>>16878
Чистый неоинтуиционизм Брауэра программируется только на мозгах создающего субъекта, это да. Но его формализации типа конструктивной математики уже программируются запросто, т.к есть ВНК интерпретация логических крюонстант и изоморфизм Карри'Говарда, на которых основаны перечимленные тобой пруверы. Кому как, конечно, лично мне проще понимать что'то когда представляешь, откуда растут ноги, зачем это ыообще было нужно и т.д
Аноним 02/05/17 Втр 18:55:38 16956 449
>>16738
Он построен на восприятии человеком простарнства, т.е. ставшего, но не времени, т.е. становления.
Аноним 02/05/17 Втр 23:00:59 16970 450
>>16956
Ты читать не умеешь? Я вполне определенно написал про время, столь же определенно об этом написано и у Брауэра, н'р первый акт интуиционизма
Аноним 03/05/17 Срд 14:58:02 16989 451
14918396085760.webm 633Кб, 1280x720
1280x720
>>16911
Ну не могу я прочитать даже ту страницу текста что ты мне скинул. Кинешь упрощенный вариант на русском - прочитаю.

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

Ща погуглил эту математику и:

>Абстрактность конструктивной математики проявляется в систематическом применении двух основных отвлечений: абстракции отождествления и абстракции потенциальной осуществимости.

>Абстракция отождествления состоит в предположении о возможности однозначного и не вызывающего сомнений решения вопроса о (графическом) равенстве или различии любых двух рассматриваемых нами конструктивных объектов, а также о возможности полного отвлечения от мелких различий, имеющихся между графически равными объектами. Случаи, когда указанные предположения не выполняются, заранее исключаются из рассмотрения. Так, при рассмотрении слов в кириллическом алфавите мы исключаем из рассмотрения случаи, когда не можем прочитать слово (вследствие неразборчивости почерка или, например, вследствие повреждения запоминающего устройства ЭВМ, в которое слово было занесено).

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

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

> В связи со сказанным, в конструктивной математике под «существованием» конструктивного объекта понимается его потенциальная осуществимость — то есть наличие в нашем распоряжении метода, позволяющего воспроизводить этот объект любое потребное число раз. Такое понимание резко расходится с пониманием существования объекта, принятым в теоретико-множественной математике. В теории множеств факт постоянного рождения и исчезновения конструктивных объектов не находит никакого выражения: с её точки зрения, подвижные реальные объекты являются лишь «тенями» вечно существующих в некотором фантастическом мире статичных «идеальных объектов» (и только эти «идеальные объекты» и следует якобы рассматривать в математике).
Тут мне не совсем ясно. Но мне надо что бы один объект был фактически чем то не одним и тем же во времени. Т.е. сегодня А = 1, завтра все то же А = 2 уже, ну и вообще всему что я захожу, лол.

Ну и что бы выражение А = А + 1 могло быть верным. Типа что бы новое А стало равно старому А плюс единице.

Короче связь с реально работающими, эффективными(!) по ресурсам системами очень и очень важна мне.
Аноним 03/05/17 Срд 15:37:09 16991 452
>>16989
>Она вообще же не подходит для работы с чем то реальным. Первый абзац отметает всякие там нейронные сети и нечеткие логики.
Начнем с того, что это не так. Во-первых, любая нейросеть это в любом случае конструктивный объект, иначе ее невозможно было бы реализовать, тем более на капплюктере. Про нечеткую логику могу сказать, что существует конструктивная нечеткая логика, разработанная Атанассовым, есть даже крайне годная книжка http://gen.lib.rus.ec/book/index.php?md5=6503D14B49A5ED76608DB72793718885 если ты вообще в курсе, что такое нечеткая логика, то главная разница с конструктивным вариантом в том, что в последнем используется конструктивное отрицание, т.е. явно заданное и построимое. Это значит, что для нечеткого множества должна быть явно задана не только функция принадлежности, но и функция непринадлежности, которая в обычной нечеткой логике считается равной 1-функция принадлежности. Функция принадлежности + функция непринадлежности не должны в сумме превышать единицу, естественно. Но могут быть меньше единицы, что невозможно в обычной нечеткой логике.
>Тут мне не совсем ясно.
Это уже дебри какие-то. Речь о требовании, чтобы конструктивный объект всегда был одним и тем же построением, единица должна быть единицей вчера и через 100 лет. С классической точки зрения странное требование, да.
>Ну и что бы выражение А = А + 1 могло быть верным. Типа что бы новое А стало равно старому А плюс единице.
Суть в том, чтобы один и тот же конструктивный объект был одним и тем же. Никто не запрещает присваивать новые значения переменной.
>с реальной точки зрения оно никогда не будет эффективно работать на пк, а мне это важно.
С реальной точки зрения, это вообще единственное, что может работать на пк. Т.к. на пк возможны только построимые объекты. Любая программа на любом языке программирования - это конструктивный объект и тривиально сводится к типизированному лямбда-исчислению. Большинство вещей не называются конструктивными, хотя и являются таковыми. Таблица умножения конструктивный объект, однако никто и никогда не называет ее конструктивной таблицей умножения.
Аноним 03/05/17 Срд 16:59:37 16992 453
>>16991
>любая нейросеть это в любом случае конструктивный объект, иначе ее невозможно было бы реализовать, тем более на капплюктере
Wrong. Компьютер не может даже в бесконечные десятичные дроби. Реализация на компьютере - просто приближение. Если на компьютере получилось приблизить какой-то объект, этот объект не становится конструктивным.
>всегда был одним и тем же построением
Причем в общем случае невозможно проверить, являются ли или не являются два построения одним и тем же построением. Так что требование заведомо невыполнимое.
Аноним 03/05/17 Срд 17:09:10 16993 454
>>16992
>Если на компьютере получилось приблизить какой-то объект, этот объект не становится конструктивным.
Зато конструктивно его приближение. А если сам этот объект непостроим в силу бесконечности или еще чего-то невычислимого, то он и не существует. Хотя, можно и веровать что существует, но тогда встает вопрос, в каком смысле.
>в общем случае невозможно проверить, являются ли или не являются два построения одним и тем же построением.
Чего несет. Есть правила построения, есть методы проверки равенства конструктивных объектов, есть наконец объект построенный по правилам. Проверка т.о. тривиальна.
Аноним 03/05/17 Срд 17:59:25 16996 455
>>16993
>есть методы проверки равенства конструктивных объектов
В общем случае даже невозможно выяснить, равны ли два конструктивных вещественных числа.
Аноним 03/05/17 Срд 18:15:45 16997 456
>>16996
Потому что ты так сказал, я же правильно понимаю?
Аноним 03/05/17 Срд 18:35:04 16998 457
>>16991
Блин, да мне конкретная реализация нужна на компьютере что бы её тыкать.

И пока я свой путь вижу так: haskell -> agda -> lean/coq

Либо это книга должна быть где решаются более менее конкретные задачи через вот это вот твое. А голую теорию мне не на что наматывать и никак я её не могу воспринимать, увы.
Аноним 03/05/17 Срд 18:38:54 16999 458
>>16997
Потому что такому алгоритму придётся работать бесконечно долго - пока не построит оба числа и не сравнит их посимвольно. А алгоритм должен давать ответ за конечное время.
Аноним 03/05/17 Срд 18:44:17 17000 459
>>16999
Можно просто сравнить алгоритмы для получения этих чисел.
Аноним 03/05/17 Срд 18:44:33 17001 460
>>16998
А хаскель и агда тебе зачем? Тыкай сразу кок, там все нужное есть. Книги, опять же по коку никто не отменял.
>>16999
>Потому что такому алгоритму придётся работать бесконечно долго - пока не построит оба числа и не сравнит их посимвольно. А алгоритм должен давать ответ за конечное время.
То, что континуум непостроим, еще Брауэр показал на примере актов интуиционизма. Это верующие придумали специальную ебулду - бет1, и написали, что она типа имеет мощность континуума. А я типа прочитал и должен уверовать, потому что проверить все равно невозможно, т.к. даже правил построения этой специальной ебулды нет. Вот тебе и неконструктивная математика.
Аноним 03/05/17 Срд 19:00:33 17002 461
>>17000
Нельзя. Если алгоритм рекурсивен (а обычно так и есть), то он на каждом последующем шаге использует результат вычислений на предыдущем шаге. И просто так нельзя сказать, дают ли два алгоритма один и тот же результат или не дают, - нужно проделать вычисления. В конструктивной математике вещественное число - это алгоритм, который принимает на вход натуральное n и печатает первые n цифр вещественного числа; такой алгоритм должен быть определен для любого n. Такой алгоритм работает конечное время, и всё хорошо. Но чтобы сравнить два вещественных числа, в общем случае нужно запустить два соответствующих алгоритма бесконечно много раз - по одному разу для каждого натурального n - и сравнить результаты. Что требует бесконечного времени.

>>17001
Хватит кривляться. Жалко смотрится.
Аноним 03/05/17 Срд 19:18:39 17003 462
>>17002
Нет, не нужно. Достаточно сравнить алгоритмы. Существуют системы типов, в которых несравнимые из-за проблемы останова алгоритмы не могут быть типизированы.
Аноним 03/05/17 Срд 19:29:32 17004 463
>>17003
Возьми алгоритм, который каким-нибудь образом считает корень из 2.
Возьми итерационную формулу Герона для корня из 2.
Как ты будешь выяснять, равны ли два числа, определяемые этими алгоритмами?
Аноним 03/05/17 Срд 19:39:04 17005 464
>>17001
Хаскелл нужен хотя бы затем что он еще язык программирования. Агда вроде некст лвл от него. А ну еще ща Идрис же. А петушка и лен, по хотту который, мне пока наверно не осилить.

У меня кароч очень все плохо с математическим бэграундом, но что то если по тихому если кодить от простого к сложному, то со временем идеи доходят.
Аноним 03/05/17 Срд 21:02:58 17017 465
какие пререквизиты нужны для хотт? алгебры абстрактной навернуть?
Аноним 03/05/17 Срд 21:36:01 17026 466
>>17017
MLTT, котягории, гомотопии.
Аноним 03/05/17 Срд 22:26:48 17029 467
>>17026
А можно книжек по этим штукам? По 2-3 на каждую из тем. Одну для совсем конченых дебилов которые математики не нюхали толком, ну научпоп какой нибудь интересный. Вторую уже 50/50 человеческую/сверхчеловеческую математическую. А третью уже совсем для конченых сверхлюдей.

Ну и русский язык пока в приоритете, к сожалению.
Аноним 03/05/17 Срд 22:43:12 17031 468
Сам нашел:

Между первыми курсами и более крутой алгеброй можно почитать Ю. А. Бахтурин «Основные структуры современной алгебры» или Paolo Aluffi "Algebra: Chapter 0", чтобы настроиться. И любую книгу для программистов по теории типов (тот же Пирс).

Тут: http://maxim.livejournal.com/479716.html
Аноним 03/05/17 Срд 23:03:23 17036 469
Мда, Алуффи понятнее Бахтурина, хотя написан на языке который я толком не знаю.
Аноним 03/05/17 Срд 23:44:58 17051 470
Аноним 04/05/17 Чтв 04:06:16 17121 471
>>16997
"" Следует отметить, что проблема распознавания равенства двух произвольных вещественных чисел является алгоритмически неразрешимой, а потому при конструктивном понимании математических суждений утверждение

«любые два вещественных числа или равны, или не равны»

оказывается ложным. Соответственно, теоретико-множественное представление об атомарности континуума (его составленности из чётко отделённых друг от друга точек) не переносится в конструктивную математику ""
Аноним 04/05/17 Чтв 10:42:30 17125 472
>>17121
Я уже сто раз написал, что континуум непостроим. Еще Брауэру это было известно. И уж континуум точно не сводится ко всякой религии типа алефов и бетов1. Однако, если мы рассматриваем вещественные числа с конечным числом знаков, проблемы нет никакой вообще.
>при конструктивном понимании математических суждений утверждение «любые два вещественных числа или равны, или не равны» оказывается ложным.
В тех случаях, когда это утверждение непосредственно доказуемо построением, то оно не может быть ложным конструктивно, как и закон исключенного третьего.
Аноним 04/05/17 Чтв 11:14:57 17126 473
>>17125
>если мы рассматриваем вещественные числа с конечным числом знаков
Конструктивисты не рассматривают вещественные числа с конечным числом знаков. Даже сраные ультрафинитисты так не делают. У тебя уже совсем какой-то радикализм.
Аноним 05/05/17 Птн 01:38:25 17242 474
>>17005
Хаскель - это прекрасно, научишься жить без переменных, зато с монадами. Опыт весьма полезный для кока и прочего, будешь, например, фолдить налево и направо вместо того, чтобы пытаться писать циклы.

Но! собственно к доказыванию чего бы то ни было хаскель не имеет никакого отношения. Изучи хотя бы для начала классическую пропозициональную логику (она и в конструктивной математике для булевских значений точно так же работает).
Аноним 05/05/17 Птн 05:57:31 17259 475
>>17242
Но в хаскеле же выразимо исчисление конструкций, СоС? Где'то видел даже реализацию млтт на нем.
Аноним 05/05/17 Птн 07:55:43 17260 476
>>17125
"вещественные числа с конечным числом знаков" - это рациональные числа. Но ты же не запретишь конструктивистам рассматривать такие числа, как корень из двух?
Аноним 05/05/17 Птн 09:40:34 17261 477
>>17260
В таком случае мы опять упираемся в абстракцию потенциальной осуществимости, от которой у местной школуйни непрекращающаяся батрушка из'за непонимания в чем разница с актуальной бесконечностью.
Аноним 05/05/17 Птн 09:53:41 17263 478
>>17259
Не совсем, в хаскеле нету dependent types, а попытки их присобачить через typeclasses - то еще извращение.
См. https://wiki.haskell.org/Dependent_type

Но даже если какие-то индуктивные конструкции в хаскеле есть, то это еще не значит, что про них что-то доказывать можно, так же как далеко не всякий язык с типом boolean содержит проверялку доказательств пропозициональной логики.
Аноним 05/05/17 Птн 10:16:58 17265 479
>>17261
Есть абстракция потенциальной осуществимости - нет алгоритма для проверки равенства двух чисел.
Аноним 05/05/17 Птн 10:35:02 17266 480
>>17265
Ну и что? Можно подумать, эта проблема разрешима с неконструктивным подходом. Алгоритмически неразрешимые задачи не разрешимы ничем другим тоже.
Аноним 05/05/17 Птн 11:12:46 17268 481
>>17242
Для hott надо tapl, для tapl надо иметь опыт программирования хоть на каком нибудь функциональном языке.

>>17263
В 8 версии что то вроде добавили такое, но может путаю.
Аноним 05/05/17 Птн 11:25:18 17269 482
>>17268
Ты, наверно, имеешь в виду TypeInType. Это прикольно, но все-таки не dependent types.
Аноним 05/05/17 Птн 12:39:18 17270 483
>>17269
А почему средствами самого языка не сделать? В зависимых типах нет никакого волшебства, только лямбда термы.
Аноним 05/05/17 Птн 13:46:48 17271 484
>>17266
У нас есть полноценный предельный переход, использующий няшненькую актуальную бесконечность. А у вас нету, азаза.
Аноним 05/05/17 Птн 13:53:19 17272 485
>>17271
Придумали очередную хуйню в надежде исправить ситуацию с невычислимой проблемой и рады. Сама'то проблема никуда не денется, если ее подкрасить пердельным переходом, а по факту заниматься самым махровым финитизмом с ограниченным числом знаков после запятой.
Аноним 05/05/17 Птн 14:29:10 17273 486
>>17272
Это называется не хуйня, а математика.
У твоей секты даже вменяемых книжек нет с доказательствами.
Аноним 05/05/17 Птн 14:34:45 17274 487
>>17273
Невычислимая хуйня называется 'хуйня' а не математика. Секта это когда веруют, что в математикке можно и без вычислимости. Книжки ты все равно не осилишь, хотя я сто раз ссылки давал.
Аноним 05/05/17 Птн 18:13:13 17278 488
>>17274
Ты давал ссылки на гуманитарные манярассуждения. Ни разу на что-то серьёзное.
Аноним 05/05/17 Птн 21:22:03 17314 489
>>17270
Волшебство как раз есть, и вот оно в чем.

Почему "массив длины 120" и "массив длины 5!" - это один и тот же тип? Потому что (компилятор запускает рекурсивную функцию) 5!=5432=120. Ура?

Пока еще не ура. Есть две проблемы. Первая в том, что типы могут зависеть от параметров, значение которых на этапе компиляции неизвестно. Почему "массив длины 120n" - тот же тип, что "массив длины n
5!"? А вот компилятор и не знает, почему. Значит, где-то рядом должно лежать доказательство.

Вторая проблема в том, что тип "массив длины f(x)" может быть вообще не определен, если f зависает.

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

Аноним 05/05/17 Птн 21:30:25 17315 490
Tapl.PNG 142Кб, 628x685
628x685
>>17269
Угу, наверно, тут кажется смотрел и там нету.

https://www.linux.org.ru/news/opensource/12611764

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

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


Ну вон предисловие к tapl'y годно отражает философию такого подхода.

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

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

И смешивать их пока не стоит, имхо. Цели у них разные достаточно.
Аноним 05/05/17 Птн 21:40:12 17316 491
Наконец-то запостили ссылку на лор. Теперь /матх официально стал филиалом раздела "девелопмент".

Оп, ты пилишь перекат? Как думаешь, есть ли смысл про х-ли и теорию категорий отдельный тред создать?
Аноним 06/05/17 Суб 00:23:18 17323 492
>>17278
Можещь рассказать, почему труды Мартин'Лефа это гуманитарные манярассуждения, а твои кукареканья на мейлру нет?
Аноним 06/05/17 Суб 00:33:26 17324 493
>>17323
Есть овер дофига разных теорий множеств.
Пользы для математики от большинства из них нет.
Аноним 06/05/17 Суб 00:39:45 17325 494
>>17324
Ты так и не ответил, что гуманитарного у Мартин'Лефа в млтт. А неконструктивные теории множеств и правда бесполезны из'за невычислимых аксиом типа исключенного третьего
Аноним 06/05/17 Суб 00:47:05 17326 495
>>17325
Твои теории - это не математика. Это воинствующая философия, это ультиматум математикам. Ты пытаешься заставить всех превратиться в конструктивистов, но не аргументируешь это никак. Если бы твои теории были бы полезны и мощны, то математики бы сами стали на твою точку зрения. Но твои теории бестолковы, а твои требования вздорны. Ты не можешь обогатить математику. Более того, ты и не хочешь её обогащать. Ты требуешь от неё отказаться.
Аноним 06/05/17 Суб 00:51:48 17327 496
>>17326
Проблема только в том, что ты кукарекаешь вместо того, чтобы попытаться понять, что единственный мой тезис в том, что математика должна быть вычислимой, иначе это не математика, что доказал кризис основпний. Так и бывает, когда в математику тащат всякую религию. Ну а то, что ты Мартин'Лефа не осилил не говоря о Брауэре, это чисто твои сложности.
Аноним 06/05/17 Суб 00:54:56 17329 497
>>17327
К математике твои безумные идеи никакого отношения не имеют. Ни сам Брауэр, ни его культисты никакой математики (не то что интересной математики, а вообще хоть какой-нибудь математики) создать не смогли.
Аноним 06/05/17 Суб 01:27:56 17334 498
>>17329
Ты уже какой раз свое незнание используешь как доказательство. Если лично ты чего'то не понимаешь, это ничего не доказывает.
Аноним 06/05/17 Суб 01:51:40 17335 499
>>17334
Допустим, я чего-то не знаю и скрытая, потаённая конструктивистская математика действительно есть. Ну так покажи же её.
inb4 очередная философия
Аноним 06/05/17 Суб 10:47:13 17340 500
Есть учебники для самых маленьких по конструктивной теории множеств, конструктивной логике, конструктивной чего-то-там-ещё?
Аноним 06/05/17 Суб 11:58:27 17344 501
14807225247060.jpg 47Кб, 600x450
600x450
Аноним 06/05/17 Суб 12:00:13 17345 502
>>17340
Эту тему почти никто и никогда не пытался популяризовать, практически все что есть это не для начинающих, более того, на английском. Вон, предыдущий оратор так нихуя и не понял. Но, немного годноты из области "по-проще" все же есть. Во-первых, переводная книжка создателя конструктивной логики и ученика Брауэра, Гейтинга http://gen.lib.rus.ec/book/index.php?md5=EF2FA380D0496F56F759C39EAA1A5459 во-вторых, конструктивный подход к основаниям крайне годно описан у Френкеля, того самого, который один из создателей ZFC, http://gen.lib.rus.ec/book/index.php?md5=1EC5F0DF018488D368BB3CB9D4EE279B 4ая глава. Хотя и заметно, что Френкель не сторонник (мягко говоря) этих идей, таки его уровень как математика сказывается - очень грамотно пояснил.
Аноним 06/05/17 Суб 12:00:16 17346 503
Аноним 06/05/17 Суб 12:03:11 17347 504
Аноним 06/05/17 Суб 12:06:58 17348 505
SDC115941.jpg 979Кб, 2592x1944
2592x1944
>>17347
А, ну еще Марков, "Нормальные алгорифмы" и есть книжка даже для младших школьников, Успенский "Машина Поста". Пикрелейтед тоже весьма годная книжка, но я бы не назвал ее "попроще".
Аноним 06/05/17 Суб 13:45:22 17369 506
>>17340
> конструктивной теории множеств
А что это? Если ты представляешь себе ZFC без закона исключенного третьего, так это совсем не то.

Конструктивно множества можно определить как функции (по объекту возвращают да или нет) или предикаты (каждому объекту соответствует утверждение). И это абсолютно разные вещи! С классической точки зрения это примерно как вычислимые и перечислимые множества.

А дальше можно развести какую-никакую теорию, но так как вся вселенная счётна, то кардинально не повыпендриваешься.
Аноним 06/05/17 Суб 14:35:16 17375 507
Философские взгляды древнегреческих ученых заключались в том, что все объекты в мире исчисляемы, по крайней мере, с помощью целых чисел. Существует исторический анекдот: ученики Пифагора были настолько обескуражены открытием, что число √2 иррационально, что даже убили одного из пифагорейцев, когда он попытался обнародовать это открытие.
Аноним 06/05/17 Суб 17:55:36 17402 508
>>17369
>Конструктивно множества можно определить как функции (по объекту возвращают да или нет) или предикаты (каждому объекту соответствует утверждение).
Конструктивно множества определяется через правила построения всех его элементов. Множество, определенное через функцию принадлежности (характеристическую) элементов - это самый что ни на есть классический подход.
Аноним 06/05/17 Суб 18:29:50 17403 509
>>17375
Любые теоретические основания приходится строить на непроверяемых утверждениях. Современным аналогом утверждения пифагорейцев о том, что всё строится из целых чисел, является тезис Чёрча-Тьюринга о том, что любое вычисление в принципе может быть проделано машиной Тьюринга. Если когда-нибудь будут изобретены способы совершать сверхтьюринговые вычисления, то для большинства современных математиков (занимающихся основаниями) это станет таким же шоком, как для пифагорейцев - иррациональность числа √2
Аноним 06/05/17 Суб 18:44:12 17404 510
>>17403
>Если когда-нибудь будут изобретены способы совершать сверхтьюринговые вычисления, то для большинства современных математиков (занимающихся основаниями) это станет таким же шоком, как для пифагорейцев - иррациональность числа √2
С какой стати?
>Любые теоретические основания приходится строить на непроверяемых утверждениях.
Не любые. Брауэр как раз от такого подхода и отказался.
Аноним 06/05/17 Суб 19:34:47 17407 511
>>17402
То, что ты написал, эквивалентно предикату принадлежности. А именно, если есть предикат P, то можно перечислить все элементы, перечислив все доказательства и проверяя, доказывают ли они утверждения вида P(x). Обратно, если есть перечисляющая функция, то можно написать предикат P(x)="существует шаг, на котором эта функция выдаёт x".
Аноним 06/05/17 Суб 19:42:57 17409 512
https://www.youtube.com/watch?v=YRmteHY-TYI

Вот вроде неплохой курс для самых маленьких от основ лямбда-исчисления к теме "12. Генценовское (секвенциальное) исчисление для интуиционистской логики высказываний. Теорема об устранении сечения." Я начал смотреть вроде неплохо, нет проклятия знаний. Но почему-то есть только 12 лекций из 15, не хватает следующих:
13. Интуиционистская логика первого порядка. Система естественного вывода и генценовское (секвенциальное) исчисление.
14. Введение в теорию типов. Зависимое произведение типов и соответствие (по Карри–Говарду) с интуиционистским квантором всеобщности. Исчисление индуктивных конструкций (CIC); система Coq для формализации математических доказательств на ЭВМ.
15. Применение λ-исчисления в языкознании: категориальные грамматики, семантика Монтегю.
Аноним 06/05/17 Суб 20:00:34 17411 513
Снимок.PNG 289Кб, 459x441
459x441
>>17409
Что-то он сходу за типизированную лямбду пояснять начал, толком не рассказав про апплиацию, абстракцию, альфа и бета редукции как явления вообще. Думаю у самых маленьких по ходу этих лекций полно вопросов будет.
Аноним 06/05/17 Суб 20:23:23 17412 514
сложно.jpg 30Кб, 480x360
480x360
>>17409
Короче, посмотрел минут 15, нахуй. Если уже знаешь о чем речь, то зайдет. В противном случае скорее всего будет пикрелейтед. Лучше уж сразу вот над этим медитировать http://ttic.uchicago.edu/~dreyer/course/papers/barendregt.pdf
Аноним 06/05/17 Суб 21:55:16 17416 515
14874669791260.jpg 140Кб, 920x960
920x960
>>17412
Ну так надо haskell/(o)caml/idris(?) -> tapl -> потом языки которые сможешь хотя бы неполноценно осилить зная tapl: agda/coq/lean/может еще варианты какие -> потом добираешь нужный математический бэкграунд в hott, mltt и книжках которые нужны что бы их осилить.

Перед этим можно попердолиться в scheme и sicp'om если хаскелл сложна.

Ну это мой план такой, лол.
Аноним 06/05/17 Суб 22:09:32 17419 516
ikzWVysfds.jpg 31Кб, 600x206
600x206
>>17416
Более подходящий пик.
Аноним 07/05/17 Вск 00:16:06 17424 517
>>17404
А ты сам что про тезис Чёрча-Тьюринга думаешь?
Аноним 07/05/17 Вск 12:39:08 17432 518
>>17411
Это в следующей лекции.
Аноним 08/05/17 Пнд 09:45:26 17458 519
Neural Networks, Types, and Functional Programming

https://colah.github.io/posts/2015-09-NN-Types-FP/

Вот, думаю тому парню с конструктивной математикой будет интересно. Автор рассматривает нейросети с помощью функционального программирования, теории типов и мельком вспоминает, что хорошо было бы рассмотреть с точки зрения гомотипической теории типов. Там есть и другие интересные статьи, в частности, нейросети и топология, но я до них еще не дошел.
Аноним 08/05/17 Пнд 20:09:22 17491 520
>>17455
Уже дополнили.Тезис Чёрча — Тьюринга — Дойча
08/05/17 Пнд 21:05:36 17493 521
Я уже давно матешей сам занимаюсь, даже год в НМУ ходил, но мне не понравилось, в тред забрел впервые,
у меня вопрос:
вы тут что против платонического мира идей?
Аноним 08/05/17 Пнд 21:06:21 17494 522
>>17493
сорян за сажу, если против хотелось бы услышать доводы, да и за тоже хотелось бы услышать
Аноним 08/05/17 Пнд 22:56:33 17506 523
>>17493
Хоть скопипасти что это.
Аноним 08/05/17 Пнд 23:21:04 17509 524
>>17506
ну ебана, тред оснований математики, а ты не знаешь в чем разница между платоном и аристотелем?
Просто с беглого чтения треда я понял что тут в целом натсроены против платона.
Аноним 09/05/17 Втр 00:05:56 17512 525
>>17493
>>17509
Да, конструктивисты наезжают на Платона, конкретно - на идею существования математических объектов независимо от наших построений. Доводов в обе стороны тут полный тред.
Аноним 09/05/17 Втр 00:41:40 17513 526
>>17509
Да я только залез сюда.
Аноним 09/05/17 Втр 01:28:54 17518 527
>>17514
Анон, ты мне друг, но истина дороже: оба имеют самое прямое отношение к основаниям классической математики. Платон сформулировал, где находятся и как существуют невычислимые числа - в мире идей, конечно же. Аристотель создал первую формальную логику, дожившую до Ренессанса без изменений. Не фиг тут, короче.
Аноним 09/05/17 Втр 02:20:53 17523 528
>>17519
> В мир идей, конечно же, нужно уверовать.
Еще в душу вселенной, какой же платонист без мировой души.

> А аристотелева логика для математики бесполезна, это Гильберт доказал.
Ну это все равно что сказать, что интегральное исчисление показало бесполезность методов Евклида для вычисления площадей и объемов. Теперь-то они, конечно, не нужны, а всё-таки Евклид красава. А аристотелева логика в современном варианте - это примерно содержимое детской книжки "Логическая игра" Кэрролла. Конечно, когда у тебя есть нормальное исчисление предикатов, оно уже не надо; но ведь кто-то переиздает же Кэрролла для детишек, значит, нужно.
Аноним 09/05/17 Втр 04:55:11 17528 529
>>17491
>Тезис Чёрча — Тьюринга — Дойча
Довольно смутная гипотеза. Из того, что мы знаем о квантовой физике в настоящий момент, следует, что любое вычисление, которое делает квантовый компьютер, может сделать и машина Тьюринга (хотя для некоторых вычислений ей и потребуется для этого гораздо больше времени).
Аноним 09/05/17 Втр 05:13:47 17529 530
>>17512
Однако теория множеств не предполагает существование "платоновского мира идей". Напротив, если, например, почитать "Теорию множеств" Бурбаки (классический теоретико-множественный трактат), то они там ясно дают понять, что не признают никакого другого понятия математической истины кроме как выводимости формулы определённого вида в определённой формальной математической системе. При этом разные формальные системы будут доказывать разные (возможно, даже противоположные) формулы, которые в рамках соответствующих формальных систем будут "истинными". Можно сказать, что формализм в математике - это противоположность платоновского идеализма, так как формалистов совершенно не интересуют вопросы "реального существования" математических объектов. Вопросы же эти интересуют как раз интуиционистов и конструктивистов, для которых математический объект "реально существует", если его можно конструктивно построить. Грамотные конструктивисты критикуют классическую теорию множеств не за мнимый "идеализм", а напротив, за то, что доказываемые в формальной теории множеств формулы оказываются совсем оторванными от какого бы то ни было реального содержания (например, в теории множеств доказывается формула существует множество A, обладающее определёнными свойствами, при этом о том, как построить такое множество нам остаётся неизвестно). Таким образом, формальная теория множеств строит излишние цепочки силлогизмов, которые можно рассматривать как чистую схоластику. Ну и у некоторых остаётся подозрение, что кроме излишних схоластических выводов могут оказаться построены и совсем уж некорректные (например, ZFC может оказаться омега-противоречивой), хотя пока никаких явных некорректных выводов в ZFC не выявлено.
Аноним 09/05/17 Втр 07:56:46 17533 531
Сводить критику платонизма у уверованию в душу это конечно хорошая демагогия, но
"даже с точки зрения формалиста, есть
нечто, что оказывает большее влияние на направления математической
мысли, нежели человеческий разум."
Аноним 09/05/17 Втр 08:14:51 17534 532
>>17533
да, и это нечто - реальный физический мир
Аноним 09/05/17 Втр 08:16:27 17535 533
>>17534
так это и есть платонизм
Аноним 09/05/17 Втр 08:24:16 17536 534
>>17527
Логики, поясните за одну вещь (сам я не логик, поэтому прошу прощения за возможно некорректные термины).
Можно ли в формальной арифметике 1-го порядка (с классической логикой, включающей закон исключения третьего и проч.) доказать существование числа, обладающего неким свойством, которое мы конструктивно не можем построить?
Или более общий вопрос. Допустим, у нас есть теория 1-го порядка, для которой существует конструктивная модель, и все аксиомы в этой теории могут быть подтверждены конструктивными построениями в этой модели. Есть подозрение, что, если мы можем доказать в этой теории существование объекта n, то мы можем его в нашей модели и конструктивно построить.
Как кажется, в теориях первого порядка классическая логика полностью согласуется с воззрением конструктивистов "существовать значит быть построенным", и менять для этого логику (например, убирая закон исключения третьего) необходимости нет.
Так ли это или я ошибаюсь?
Аноним 09/05/17 Втр 08:25:36 17537 535
>>17535
Нет, платонизм - это когда на нас влияет реальный нефизический мир, а не реальный физический мир
Аноним 09/05/17 Втр 08:29:52 17538 536
>>17537
Во времена платона не было разницы, а сейчас есть. Суть в том что мы открываем, а не изобретаем.
Аноним 09/05/17 Втр 08:39:11 17539 537
>>17538
Возможно, это слишком искусственное разграничение. Ведь даже конструктивисты согласятся, что мы открываем свойства конструктивных объектов (даже если сами объекты мы изобрели). В то же время приведённая цитата из Роббинса говорит о том, что физический мир влияет на то, что определённые математические конструкции оказываются более ценными, чем другие, так как, например, более помогают нам в науке. Однако тот же инструментарий математического анализа можно строить разными способами (как строили его по разному Ньютон и Лейбниц). Поэтому открыли мы математический анализ или изобрели? И какие именно его аспекты открыли, а какие изобрели?
Аноним 09/05/17 Втр 08:48:00 17540 538
Аноним 09/05/17 Втр 08:52:35 17541 539
>>17539
Не только разными способами, а, наверное, бесконечным количеством разных способов. Суть в том что единого понятия мат. анализа. нет. И какие бы мы способы не избрали, принципы будут открываться одни и те же(и базироваться на одних и тех же). Так же как например уже в самих операциях сложения и т.д. действительных чисел заложена конепция комплексных чисел.
Можно вот еще что сказать, представь что нам нужно проверить инопланетян на разумность, не логично ли выдать им информацию о натуральных числах и ожидать иррациональных и вообще всего остального.
Вся суть платонизма в современных терминах сводится именно к материализму, не взирая на многие элементы идеализации, понятно что точка в геометрии не соответствует ей в физике, но понятие точки в нас взялось именно из физической.
Аноним 09/05/17 Втр 08:54:58 17542 540
>>17541
Дополню: арнольд, например, понимал математику как часть физики, не знаю конечно на сколько весь остальной его треп правдив.
Аноним 09/05/17 Втр 09:00:14 17543 541
>>17541

Ну в такой трактовке, думаю, платонистами в той или иной мере являются все математики - и конструктивисты, и формалисты.

Однако, как я заметил здесь >>17529
главная претензия конструктивистов к теории множеств заключается вовсе не в платонизме последних, а в схоластичности выводов классической теории множеств.
Аноним 09/05/17 Втр 09:34:01 17544 542
>>17536
> доказать существование числа, обладающего неким свойством, которое мы конструктивно не можем построить?

Да. Например, мы не можем конструктивно решить проблему остановки. Рассмотрим следующее свойство числа:
P(x) = x = 2^k, где k - останавливающаяся программа или x = 3^k, где k - зависающая программа
Это свойство невычислимо. Тем не менее, в зависимости от того, что делает программа номер 0, либо 2, либо 3 обладает этим свойством.

> то мы можем его в нашей модели и конструктивно построить.
Это правда в следующем смысле: если ExP(x) - теорема интуиционистской арифметики без свободных переменных, то также теоремой является P(t) для некоторого терма t. Если в P нет кванторов, то ExP(x) может быть даже и теоремой классической арифметики. Но вот если в P есть кванторы...

> менять для этого логику (например, убирая закон исключения третьего) необходимости нет.
Ну вот допустим ты привел предположение Ax~P(x) к противоречию, то есть доказал ~Ax~P(x). Что дальше? Классическая математика подсказывает, что ExP(x), а где ты этот x конструктивно возьмёшь?
Аноним 09/05/17 Втр 10:52:18 17547 543
>>17528
Да, я, если честно, тоже там думаю. На данный момент квантовые компьютеры, которые хотят сделать, не способны на сверхтьюринговые вычислениями. Да и вообще, объяснять одну загадку (возможность сверхтьюринговых вычислений) другой загадкой (квантовые компьютеры) не очень умно. Просто решил закинуть этот тезис, хоть и самому он не очень нравится
Аноним 09/05/17 Втр 11:34:56 17548 544
>>17544
>Например, мы не можем конструктивно решить проблему остановки
Зато неконструктивно можем, сведя ее у исключенному третьему, "или остановится или нет)))". И почему-то никого не беспокоит, что это "решение"-то уровня /б, никакого значения не имеющее, ни теоретического ни тем более практического.
Аноним 09/05/17 Втр 11:38:33 17549 545
>>17547
>>17528
Но тут же есть какой-то верующий, кукарекующий что Тьюринг петух и его машина ненужна, т.к. квантовые вычисления бла-бла-бла. Мне вот тоже этот момент не очень понятен, что есть такого в квантовых вычислениях, не сводящегося к вычислениям неквантовым. Вычисления, они и в африке вычисления, безотносительно метода, разве нет?
Аноним 09/05/17 Втр 22:54:16 17609 546
Можно объяснить, что такое вычислимость и почему закон исключающего третьего невычислим?
Аноним 10/05/17 Срд 07:13:47 17628 547
>>3694 (OP)
Почему на правила вывода в формальных системах накладывают такое ограничение, что число их должно быть конечно? По-моему, как и в случае с аксиомами, достаточно, чтобы правила вывода составляли перечислимое множество, которое даже не обязательно должно быть эффективно разрешимым.
Ведь вся суть формальных систем - в том, чтобы множество теорем составляли перечислимое множество. Думаю, что и должно быть общим определением формальной системы, а уж с помощью каких алгоритмов это множество определяется (в частности, введение самих таких понятий как аксиомы и правила вывода) - это уже частности.
Аноним 10/05/17 Срд 10:00:29 17631 548
>>17628
>в том, чтобы множество теорем составляли перечислимое множество
Чушь.
Аноним 10/05/17 Срд 10:31:02 17632 549
>>17630
А чего ты привязался к классикам насчет неполноты, разве интуиционистская арифметика может доказать собственную непротиворечивость?
Аноним 10/05/17 Срд 12:04:44 17636 550
>>17632
Арифметика Гейтинга - это конструктивный объект, как и все другие конструктивные объекты, служащий в т.ч. контекстом для всех возможных построимых выводов из него. И как для любого другого конструктивного объекта, любой такой вывод можно сделать не обращаясь к чему-то внешнему. В конструктивной системе заведомо непостроимо то, что из нее не выводимо и наоборот - нельзя вывести то, что нельзя построить. Это классически можно нарисовать закон исключенного третьего, а дальше как знаешь, никого не ебет, как ты его будешь доказывать в случае, когда построимое доказательство невозможно. Насчет непротиворечивости, любая конструктивная система непротиворечива, поскольку в таковой невозможно построить что-то и одновременно свести возможность такого построения к абсурду.
Аноним 10/05/17 Срд 13:40:40 17641 551
>>17636
> И как для любого другого конструктивного объекта, любой такой вывод можно сделать не обращаясь к чему-то внешнему.

Ты, кажется, плохо понимаешь, что такое неполнота. Для того, чтобы сформулировать теорему о неполноте, нужно две системы - "маленькая" и "большая", большая - это наш обычный язык (скажем, арифметика), а маленькая - это модель большой, реализованная в ней самой (погугли coq-in-coq, например). Теорема Гёделя говорит, что большая система не может доказать непротиворечивость маленькой, и для арифметики Гейтинга эту теорему никто не отменял. Твои попытки избавиться от обращения к внешнему (к большой системе с точки зрения маленькой) неубедительны, поскольку большая и маленькая система изоморфны.

> любая конструктивная система непротиворечива,
Сферическая логика в вакууме непротиворечива, потому что любой терм типа ложь можно доредуцировать до конструкторов, а их в типе ложь нет. Но арифметика - ни разу не сферическая логика в вакууме, оттого и неполнота.
Аноним 10/05/17 Срд 13:54:42 17643 552
>>17641
Но если система выводима из себя, как из контекста, то и противоречивость ее так же выводима непосредственно, т.е. построима.
Аноним 10/05/17 Срд 13:56:48 17644 553
Аноним 10/05/17 Срд 14:12:19 17645 554
>>17631
Допустим, у меня есть алгоритм, с помощью которого я получаю бесконечную последовательность формул, и каждую такую формулу я считаю теоремой. Чем плоха такая формальная система?
Аноним 10/05/17 Срд 18:49:58 17657 555
>>17645
Не в каждой формальной системе возможен алгоритм, выдающий все теоремы и только теоремы.
Аноним 10/05/17 Срд 22:07:32 17670 556
>>17643
Что такое "выводима из себя, как из контекста"?
"Противоречивость построима" - в смысле ложь доказуема?
Ты о чем вообще?
Аноним 11/05/17 Чтв 02:32:08 17692 557
>>17657
Теорема - это по определению и есть то, что выдаёт алгоритм формальной системы. Ты путаешь "теорему" с "истинным высказыванием". Действительно, не все формальные системы полны - в сильных формальных системах не каждое "истинное высказывание" является "теоремой".
Аноним 11/05/17 Чтв 03:19:00 17694 558
>>17692
Объясни, пожалуйста, что ты понимаешь под алгоритмом формальной системы. В моём представлении формальная система - это ориентированный граф, в котором вершинами являются формулы, и стрелка из вершины A в вершину B есть тогда и только тогда, когда [тут описываются т.н. "правила вывода"]. Некоторые формулы называются аксиомы (между прочим, из любой вершины есть стрелка в каждую аксиому). Пути, начинающиеся в аксиомах, называются доказательствами. Формула называется теоремой, если ею оканчивается какое-нибудь доказательство.
Аноним 11/05/17 Чтв 07:50:28 17702 559
>>17694
Каждое доказательство формальной системы может быть верифицировано алгоритмом (который проверит это доказательство по строчкам и скажет - да, действительно, это доказательство корректно). Из этого следует, что и все аксиомы, и правила вывода тоже должны быть проверяемы алгоритмом. Поэтому мы, например, не можем сказать "возьмём в качестве аксиом нашей формальной системы все истинные предложения о натуральных числах". Просто потому, что нет такого алгоритма, который мог бы проверить истинность или ложность каждого предложения.

А поскольку множество доказательств счётно (каждое доказательство - конечная последовательность символов), то мы можем запустить алгоритм, который будет последовательно продуцировать корректные доказательства таким образом, что каждое корректное доказательство на каком-то этапе будет выведено. А значит, можно запустить алгоритм, который будет продуцировать теоремы, причём все теоремы (каждая теорема будет иметь некий конечный номер n). Естественно, имея формулу, сказать заранее, является ли она теоремой, то есть будет ли она выведена нашим алгоритмом или не будет, нельзя. Более того, этого нельзя в общем случае эффективно проверить, так как наш алгоритм работает бесконечно долго.

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

По-моему, именно такая, алгоритмическая точка зрения, даёт наиболее общее понятие формальной системы и теорем (всякие аксиомы, правила вывода - это частности; на самом деле, не так уж и важно, как именно наш алгоритм работает).
Аноним 11/05/17 Чтв 08:13:42 17703 560
Аноним 12/05/17 Птн 17:19:29 17773 561
Создать тред Создать тред

Check this out!

Настройки X
Стикеры X
Избранное / Топ тредов