Предыдущий
Решил научиться доказывать теоремы с помощью и 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.
Поясните, как у утверждения может быть тип? В чем смысл?
>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.
Поясните, как у утверждения может быть тип? В чем смысл?
Там же дальше об этом говорится!
Можно конкретное предложение?
Ну, прямо следующий абзац же об этом... Или я твоего вопроса не понял? Если бы у пропозишнов не было типа, ты бы не смог доказывать никакие утверждения о пропозишнах. Он там и дает примеры: можно сказать "для всех натуральных чисел, если число меньше пяти, то меньше и шести", а можно сказать "для всех пропозишнов, если у нас есть пропозишн, то он у нас есть".
> Или я твоего вопроса не понял?
Да. Мой вопрос: что такое тип?
http://adam.chlipala.net/cpdt/html/Universes.html
https://coq.inria.fr/refman/Reference-Manual006.html#Cic
По второй ссылке определение: получается, что "тип" - это сорт, а сорт - это Проп, Сет или Тип_ай для натурального ай.
Кук не нужон, зашквар же. Есть няшный 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 страницы
>что такое тип?
Тип - это конструктивный объект, который есть элемент самого себя. Да, в общем случае это приводит к парадоксу Жирара (по-сути, все тот жи парадокс Рассела), что было показано для первого варианта MLTT, поэтому сейчас там все немного хитрее - иерархия вложенных универсумов - U. Подробности опять же в вышеупомянутой книге, либо в учебнике по LEAN. Если не интересны философические объяснения - считай тип множеством, элементы которого определены заданными правилами.
Да, есть еще важный момент. Даже в классической логике логические операции можно рассматривать как операции над множествами. "или" соответствует операции объединения множеств, "и" - пересечение, импликация - подмножество и т.д., пик2. Эта хуйня просто расширяется дальше - пик1, плюс используется интерпретация логических констант по Брауэру-Гейтингу-Колмогорову. В итоге получается логическая система, полная и выводимая по Геделю, поскольку опирается не на синтетическое суждение, оторванное от конструктивного построения, а на аналитическое. Подробнее, на пальцах и с примерами тута http://archive-pml.github.io/martin-lof/pdfs/Martin-Lof-Analytic-and-Synthetic-Judgements-in-Type-Theory.pdf
У тебя мания величия походу, бро.
> полная и выводимая по Геделю
Что очевидно, ведь теорема Гёделя распространяется только на те системы, где можно построить PRA.
https://arhivach.org/thread/216774/
Предыдущий тред.
Предыдущий тред.
>В итоге получается логическая система, полная и выводимая по Геделю
Ну сколько можно распространять дезинформацию?
>полная
Она не полна т.к. к ней вполне применимы теоремы Гёделя о неполноте, в частности, она не может ни доказать, ни опровергнуть утверждение о своей собственной непротиворечивости. Напомню, что полнота означает, что всякое предложений либо доказуемо, либо опровержимо. Если теория обладает таким свойством только для специального класса предложений, а не для всех предложений своего языка, то называть это полнотой некорректно.
>выводимая по Геделю
Не то, чтобы я прочел все работы Геделя, но я видел этот термин тоько у тебя, почти уверен, что ввел его вовсе не Гедель - ссылку на Геделя в студию, если придерживаешься другой точки зрения.
>Что очевидно, ведь теорема Гёделя распространяется только на те системы, где можно построить PRA.
На самом деле теоремы Геделя о неполноте распространяются и на более слабые системы (1-ую так и вовсе можно доказать в арифметике Робинсона). Кроме того, эквациональная версия PRA (для которой тоже имеют место обе теоремы о неполноте) погружается в интуиционистскую теорию типов.
>в частности, она не может ни доказать, ни опровергнуть утверждение о своей собственной непротиворечивости.
Для этого есть проверка типов, ведь по изоморфизму Карри-Говарда все утверждения в конструктивной логике соответствуют своим типам. Т.е. такая система как 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
>Напомню, что полнота означает, что всякое предложений либо доказуемо, либо опровержимо.
Спасибо, я знаю что такое полнота. Интерпретация логических констант по Брауэру-Гейтингу-Колмогорову полна именно в этом смысле, поскольку любое суждение в ней либо построимо, либо абсурдно и т.о. соответствует пустому множеству своих пруфов (типу по изоморфизму Карри-Говарда).
Да, MLTT не только сама по себе конструктивный объект, но исходя из интерпретации логических констант по Колмогорову, по-сути, готовая спецификация для языка программирования http://www.cse.chalmers.se/research/group/logic/book/book.pdf
Шарящий в мат.логике анон, ответь.
Может ли теоретически получиться так, что ZFC непротиворечива, однако омега-противоречива, и если так, то возможно ли было бы эту омега-противоречивость некими метаматематическими методами (вроде тех, что использовал Гёдель) доказать?
Если кратко, то может. Будучи точным, вопрос о том, что значит "может ли теоретически получиться" довольно тонкий.
Например, используя вторую теорему Гёделя о неполноте можно показать, что если непротиворечива 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).
Спасибо, анон!
Отсюда даже виден дальнейший ход того, как можно было бы доказать omega-Con(ZFC) - доказав неким образом верность арифметического выражения, эквивалентного not Con(ZFC+Con(ZFC+Сon(ZFC)))
fix: доказать not omega-Con(ZFC)
Я на самом деле переусложнил. Для ответа на твой вопрос нужно было лишь доказать непротиворечивость ZFC + Сon(ZFC) + not omega-Con(ZFC). Что требовало немного меньше усилий.
Анон, помоги доказать, что все тавтологии логики высказываний с 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.
-(-(-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.
Бамп божественным Вавиловым.
Да никакой он не божественный. Мало того, что конструктивистов с кое-кем другим перепутал, так еще и ночью у него там кто-то символы дорисовывает. Теорем-пруверы, оказывается, опираются на тысячи неявных предположений - вот оно как! Просто черная магия и сильный ИИ какие-то.
> Теорем-пруверы, оказывается, опираются на тысячи неявных предположений - вот оно как!
Вавилов тенденциозен, но собственно критика того, что конструктивность так называемой конструктивной математики довольно условна и опирается на то, что допускаются явно физически нереализуемые вычисления остается. В чем, в конце-концов, утверждение об обрывании последовательностей Гудстейна конструктивнее, чем утверждение о возможности удвоить шар путем перемещения конечного числа частей, учитывая, что ни одно из них не является физически реализуемым.
Да нормальный парень он, просто платонист. Так бывает, к сожалению. Но в остальном вкусы у него хорошие, литературу интересную цитирует. Можно же фильтровать информацию, правда? Пенроуз вон тоже отбитый платонист, но в остальном, исключая этот пункт, мне нравится его читать.
>Да нормальный парень он, просто платонист.
Проблема не в том, что он платонист, а в том, что его заносит и он выдает мало адекватную аргументацию против несимпатичных ему позиций. Например теже "тысячи неявных аксиом" нужные конструктивной математике или что теорема Гёделя о неполноте говорит о "генерации некоторого специального вида текстов" (и ничего не говорит о математике).
Но, впрочем, пишет увлекательно (хотя, отчасти, это следствие того, что он выдвигает совершенно скандальные тезисы).
Каждый математик в душе хотябы чуточку платонист. Даже ℕ-петух
Да, видимо так, просто потому что сомнения в реальности математических объектов однозначно являются большой помехой, когда реально занимаешься доказательством теорем.
Хотя, разумеется, это касается только собственно математиков. Философы математики, не являющиеся, а тем более никогда не являвшиеся действующими математиками вполне могут не быть платонистами ни в какой степени.
>Философы математики, не являющиеся, а тем более никогда не являвшиеся действующими математиками вполне могут не быть платонистами ни в какой степени.
Но кого ебёт судьба унтерменшей?
>пик
Какой же этот клоун неосилятор, господи. Он бы хоть попытался разобраться в том, что критикует. Вместо того, чтобы мазать калом математиков, до которых ему как до Луны пешком и всё лесом. Впрочем, наверное, я слишком многого хочу от рашкованского быдлана. Сто раз уже было сказано об абстракции потенциальной осуществимости, общей для всей математики, но нет. Дебилы будут кукарекать про чернильные дыры. Дебил, он на то и дебил, чтобы не понимать очевидного. В частности, что число 10^10^10^...^10 относится к натуральным исходя из конструктивно определенных правил построения N. В частности, у этого числа есть предваряющее его 10^10^10^...^10-1 и следущее за ним 10^10^10^...^10+1 Т.о., хотя данное число физически и непостроимо, о его свойствах (принадлежности к N) мы можем судить из вышесказанного. И еще раз - абстракция потенциальной осуществимости, она общая для всей математики, какого хуя за нее предъявляют только конструктивизму? Если об этом еще Евклид писал? Вот этой своей обличающей писаниной этот ваш вавилов вообще что и кому доказал? Практическое применение у нее какое? С MLTT все ясно, при интерпретации логических констант по Колмогорову это по факту готовая спецификация для языка программирования с зависимыми типами, который может служить для доказательства теорем на компьютере. При интерпретации этих же логических констант по Брауэру-Гейтингу MLTT может служить конструктивными основаниями математики. А вот эта ваша вавиловщина, какие у нее задачи? Парашу тралить?
>критика того, что конструктивность так называемой конструктивной математики довольно условна и опирается на то, что допускаются явно физически нереализуемые вычисления остается.
Он просто про MLTT не слышал, если слышал, то не читал, если читал, то не понял, если понял, то не так.
>>6044
Заебывает просто все это школотунство уровня Рыбникова и прочих катющиков, "все пидорасы, а я - Дартаньян, яскозал" без чего-то даже отдаленно напоминающего вменяемую аргументацию. Яскозал и все. Вавилов этот ваш, он бы так читал Мартин-Лёфа, как потом отчитывает, и большинство претензий отпало бы само собой. Хотя опять же, возможно, я просто много хочу от мамкина траля.
Заебывает просто все это школотунство уровня Рыбникова и прочих катющиков, "все пидорасы, а я - Дартаньян, яскозал" без чего-то даже отдаленно напоминающего вменяемую аргументацию. Яскозал и все. Вавилов этот ваш, он бы так читал Мартин-Лёфа, как потом отчитывает, и большинство претензий отпало бы само собой. Хотя опять же, возможно, я просто много хочу от мамкина траля.
Составьте, пожалуйста, список значимых работ по философии математики. Типа "Структуры" Куна, работ Поппера и Фейерабенда относительно философии науки. А также посоветуйте какое-то годное введение в мат. философию, можно на английском
>типа Куна и Фейерабенда
Harold Edwards
Gian-Carlo Rota
Хуйня.
Ой, какая милота эта ваша грязноштанная математика. "Яскозал, что это буржуазная теория и вы так делайте". На самом же деле, а не в калмунистических манямирах, есть нейрофизиологические данные, доказывающие сводимость натурального числа к восприятию времени, о чем писал еще Брауэр. Т.н. модель ATOM Уолша. Ну, цитата Кронекера про бога хуета, конечно.
>о чем писал еще Брауэр.
Ох и давно я этого не слышал.
>есть нейрофизиологические данные, доказывающие сводимость натурального числа к восприятию времени
Пруф?
>Пруф?
Пишу жи
>Т.н. модель ATOM Уолша.
Ссылочка на РТ пабмед - https://www.ncbi.nlm.nih.gov/pubmed/14585444
Нейровизуализация - объективные данные, они не могут быть хуйней, они либо что-то показывают, либо нет. По этой теории, на которую ты ссылаешься, я тоже пояснял уже. Там авторы сами себе противоречат, результаты нейровизуализации у них показывают связь в обоих направлениях, но в одном меньше, чем в другом, из чего они от балды заключают, что то направление, по которому корелляция меньше - это метафора и его на самом деле не существует. Еще раз скажу, в их же статье показана реальная корелляция на реальной нейровизуализации. Т.е. исходя из их же данных, они просто дополнили результаты Уолша, показав несимметричность пространственно-временных отношений, т.е. фиолетовый, зеленый и розовый кружочки на втором пике должны быть разных диаметров, чтобы точнее показывать реальную картину.
Решил изучать математику с логики и оснований. Читаю Клини, все правильно делаю?
Поздравляю всех любителей кококатегорий с Новым Годом! Дорогие подгорающие и сотрудничающие с администрацией красные петушки, я очень рад, что вы есть:3
Спасибо.
любитель кокотегорий :3
Советую пик-релейтед. Книжка посовременнее, и изложено всё яснее и компактнее.
Там, например, вся логика высказываний строится на основе всего 3 схем аксиом.
Британские ученые смоделировали существо, которое хуже червя-пидора.
Перед вами прикладной конструктивист-картофанщик, ему дали временное наименование "Сиплый спермоглот".
Команда математиков во главе с Мишей Вербицким уже доказала, что "Сиплый спермоглот" - это абсолютно непробиваемое дно, хуже которого уже быть не может.
В ближайшее время научное сообщество попытается воссоздать живую копию Сиплоглота для дальнейшего исследования.
Многие считают, что существо будет получено при помощи метаморфоза Хорена - ближайшего аналога Сиплоглота.
Перед вами прикладной конструктивист-картофанщик, ему дали временное наименование "Сиплый спермоглот".
Команда математиков во главе с Мишей Вербицким уже доказала, что "Сиплый спермоглот" - это абсолютно непробиваемое дно, хуже которого уже быть не может.
В ближайшее время научное сообщество попытается воссоздать живую копию Сиплоглота для дальнейшего исследования.
Многие считают, что существо будет получено при помощи метаморфоза Хорена - ближайшего аналога Сиплоглота.
Ну блядь, создай отдельный тред про сиплоглота, а то модерация с каникул вернется и всех поубивает итт
Он питается останками Фихтенгольцев и Гурс, запивая водкой.
Кстати, а что по поводу учебников Гурсы можно сказать?
>В ближайшее время научное сообщество попытается воссоздать живую копию Сиплоглота для дальнейшего исследования.
Результат воссоздания всех шокировал! Сиплый спермаглот мутировал в новый вид! Произошло скрешенивая спермаглота и мистического модуля над кольцом! Спермаглом ебал модуля прямо в анальное кольцо, после чего тот заразился математическим спидом и умер. После смерти Мистик опорожнил кишечник и высрал яичко, которое отнесли в инкубатор. Повадки нового вида очень странные, он любит абстракции, говорит, что R^n не нужно, всем советует читать Бурбаки и закидывается наркатой почти каждый день. Также это существо считает себя свободным человеком, хотя и сидит весь день в клетке.
Когда проводили экскремент никто и подумать не мог, что из таких посевов вырастет такой урожай!
Результат воссоздания всех шокировал! Сиплый спермаглот мутировал в новый вид! Произошло скрешенивая спермаглота и мистического модуля над кольцом! Спермаглом ебал модуля прямо в анальное кольцо, после чего тот заразился математическим спидом и умер. После смерти Мистик опорожнил кишечник и высрал яичко, которое отнесли в инкубатор. Повадки нового вида очень странные, он любит абстракции, говорит, что R^n не нужно, всем советует читать Бурбаки и закидывается наркатой почти каждый день. Также это существо считает себя свободным человеком, хотя и сидит весь день в клетке.
Когда проводили экскремент никто и подумать не мог, что из таких посевов вырастет такой урожай!
Выглядит нажористо, там больше картофана, чем в Фихтенгольце?
Я бы сказал, что вместе со всякими Позняками эта книга - эталон картофана.
Открыл, посмотрел, там сразу идёт анализ в C. Там что, это книга немного концептуальна. Её ещё Арнульд хвалил.
Можно создать отдельный трэд для вборса математических мемесов, но уж никак не про сиплоглота.
Однако, создав такое, мы умышленно сформируем очередную метастазу на недавно оправившейся от Хорена и ЛЖР-трэда доске. Уж не убьем ли?
>"modus ponens"
>вместо "элиминатор импликации"
Не читал, но...
1) часть серии из десятков книг
2) в названии серии "applied"
3) в названии "an introduction"
4) ОДИН АВТОР
5) в аксиомах ниже - символ точки поставлен так, что совершенно непонятно, что же он обозначает. НИКОГДА такое не встречал.
Предполагаю, что книга - говно, перехожу к дегустации.
Фу, буэ, действительно говно. Ты откуда такой выполз, что советуешь это? Сам что-ли нашёл. Небось первокур ВУЗ-а с непрофильной математикой?
Сделаем ещё несколько замечаний относительно аксиоматического метода в математической логике. Термин «аксиоматический методы» используется в различных смыслах, что иногда ведёт к недоразумениям.
Прежде всего это содержательно-аксиоматический метод. Он употребляется, когда изучается род структур, удовлетворяющих одному и тому же списку свойств. Например, один род структур составляют группы, другой род структур — кольца, третий род структур — структуры Пеано и т.п. Под аксиомами при этом понимаются просто конкретные условия, которым должна удовлетворять любая из структур изучаемого рода. Эти условия понимаются содержательно и записываются на рабочем математическом языке, например на русском или английском. Впрочем, часто аксиомы какого-либо рода структур записывают и на точном логико-математическом языке, но понимают содержательно как утверждения о структурах; для одних структур эти аксиомы могут быть истинны, а для других — ложны.
И где же тут вера кокококонсруктивист?
Прежде всего это содержательно-аксиоматический метод. Он употребляется, когда изучается род структур, удовлетворяющих одному и тому же списку свойств. Например, один род структур составляют группы, другой род структур — кольца, третий род структур — структуры Пеано и т.п. Под аксиомами при этом понимаются просто конкретные условия, которым должна удовлетворять любая из структур изучаемого рода. Эти условия понимаются содержательно и записываются на рабочем математическом языке, например на русском или английском. Впрочем, часто аксиомы какого-либо рода структур записывают и на точном логико-математическом языке, но понимают содержательно как утверждения о структурах; для одних структур эти аксиомы могут быть истинны, а для других — ложны.
И где же тут вера кокококонсруктивист?
>И где же тут вера
Сейчас бы веруну за веру пояснять на подтираче. Ты ж очевидных вещей не видишь, что такому объяснишь. Самый очевидный пример веры - как раз матлогика. Вот есть логические константы, например А. Есть их комбинации. Например "А или не А". Последнее, например, считается истиной, невзирая ни на что. А если подумать головой, а не как обычно, то с каких хуев-то? Если у нас нет конкретного построения, на основании которого мы можем показать свойства А или не А, то надо веровать что все равно это правило истинно для всех возможных случаев априори. Отсюда и неполнота по Геделю - мы делаем предположение, недоказуемое в общем случае. Простейший пример - расеянский автопром. Пусть А будет высказыванием "дверь закрыта", не А - соответственно "дверь открыта". Так есть еще вариант "дверь не закрыта", не сводящееся к открытой двери, т.к. формально-то она выглядит закрытой, но она и не закрыта, т.к. если прислониться - вывалишься из таза к хуям. Но формально у нас только 2 варианта - "А или не А". Совсем другое дело - интерпретация логических констант по Гейтингу. В этом случае мы можем принять А только в случае наличия доказательства А (наличия пруф-объекта, принадлежащего к множеству А и т.о. доказывающего, что множество А ненулевое). Так же и с "не А", мы это принимаем только в случае доказательства того, что множество А пустое (т.е. не содержит никаких объектов). Никакой веры не требуется, требуется только построение. Собственно, к матлогике как формальным правилам еще при Гильберте были большие претензии, отсюда и необходимость создания других подходов к вопросу ощущалась еще в начале 20 века, что н-р привело к созданию натуральной дедукция Генценом и т.д. Аксиоматическая матлогика была фейлом уже во времена ее создания, просто Гильберт яскозал что можно вот так формализовать все, потому что до этого у него получилось формализовать геометрию. Ну и догма Гильберта, конечно. Тут уже чистая религия.
Приведи пример в математике, когда закон исключающего третьего не выполняется. Без теоремы генделя о неполноте.
Во всех случаях, когда нет построения, доказывающего свойства "А" или "не А", остается только веровать, что этот закон выполняется (т.к. непосредственно мы не можем этого заключить). Это вообще не математический закон, а онтологический. Аристотель в него веровал, и ты так делай.
Закон исключенного третьего утверждает, что для любого A верно A или не A.
Отрицание закона исключенного третьего утверждает, что существует такое A, что верно A и не A.
Предъяви такое A.
>мам, вот они веруны, ну скажи
Наличие в формальной системе каких-либо законов регулируется только правилами вывода.
То есть ты не можешь привести такое А?
В твоём вопросе ошибка, ведь при сокращении двойного отрицания ты неявно подразумеваешь, что верен закон исключения третьего.
Отрицание закона исключенного третьего - это утверждение, что верно не(А или неА) = неА и ненеА.
Отрицанием "неB" я обозначаю то, что определена вычислимая функция из пустого множества в множество B.
В такой формулировке на роль А подходит пустое множество.
Это и есть искомый контрпример существования интерпретации интуиционисткой логики, которую нельзя расширить до интерпретации классической логики.
p.s.
(ну и да, под верностью С я понимаю существование вычислимой функции из одноэлементного множества - в С)
(ну и да, под верностью С я понимаю существование вычислимой функции из одноэлементного множества - в С)
p.p.s. "понимаю" именно в той интерпретации, офк.
Ты же, скорее всего, говоришь, что "Пропозициональная логика лучше, чем логика предикатов!", что весело. Ведь если проводить аналогию с молотком и микроскопом, то ты предлагаешь смотреть на инфузорий в молоток.
Однако - спасибо за провокационный вброс, мне понравилось.
Ты же, скорее всего, говоришь, что "Пропозициональная логика лучше, чем логика предикатов!", что весело. Ведь если проводить аналогию с молотком и микроскопом, то ты предлагаешь смотреть на инфузорий в молоток.
Однако - спасибо за провокационный вброс, мне понравилось.
>Отрицание закона исключенного третьего утверждает, что существует такое A, что верно A и не A.
Хуйню не неси, пожалуйста. Прочитай, что ты написал и подумай головой. Ты же даже дизъюнкцию не понимаешь, о каком интуиционизме с тобой говорить вообще? Сам написал хуйню, сам опроверг, ахаха кококонструктивисты соснули. Детский сад блядь, штаны на лямках.
p.p.p.s. - я не он, и хз что он там насчёт Аристотеля и онтологий говорил. Не могу утверждать, что он сказал либо верно, либо неверно. Может он сказал, что он лжёт. И как тогда решить - верно или неверно? Надо мне было именно так, по-Антисфенофски возразить.
Вы не тралите? Вчера написал здесь один единственный пост, и он удалён. Гениально, охуенный раздел, всем спасибо
Итак, создадим две параллельных вселенные, где у нас А равно одному и тому же значению. Равно ли А самому себе в другой вселенной?
Шапку раздела прочитай, ньюфажик. Написал небось какую-нибудь нерелейтед хуйню - вот и потерли. И этот пост тоже потрут.
Не, всё было абсолютно по теме. Абсолютно. А щас вот херня идёт здесь и не трётся, как ни странно. Вероятно от моего поста просто кому-то в очередной раз бомбануло, его репортнули и, как следствие - потёрли, так часто бывает. Что поделаешь, 2017, свобода слова, да.
У тебя образование математическое есть? Ты уверен, что можешь судить, что по теме, а что - нет? Написал один-еединственный пост, а уже про свободу слова рассуждаешь, лол. Есть же прикрепленный тред для начинающих, all your posts are belong to that. И вот теперь ето у нас уже точно офтоп, репортнул, нехуй хоренщину тут разводить
другие аксиомы логики тоже онтологические. Уверуем же.
>Так есть еще вариант "дверь не закрыта", не сводящееся к открытой двери, т.к. формально-то она выглядит закрытой, но она и не закрыта, т.к. если прислониться - вывалишься из таза к хуям
Эх щас бы естественным языком формальную логику опровергать...
Приходит к конструктивисту мамка и спрашивает: тебе суп или котлеты? А он такой: мать ты че охуела такое спрашивать ты че под гильберта легла...
>Аксиоматическая матлогика была фейлом уже во времена ее создания
кто б создателям HoTT рассказал, они еще новые аксиомы придумали, дебичи
В шапке раздела не написано что требуется предъявление ИНН, паспорта, диплома и других идентификаторов личности, а также нигде прямым текстом не сказано что любые посты обязательно должны быть в пределах темы оп поста и никак иначе.
Тупое следование правилам вроде как называется итальянской забастовкой, насколько эффективно работать в таком режиме, да и хоть что-то обсуждать? По моему ответ очевиден.
> Щитпостинг в тематических модерируемых тредах будет жестко пресекаться. Не пишите в тематические треды, если не уверены, что вам есть что сказать.
ДОБАВЛЯЙТЕ ТЭГИ, КОГДА АРХИВИРУЕТЕ
мимо кислота-архиватор-кун
Тег для раздела вроде должен автоматом добавляться же. Или надо админа стукнуть, чтобы он его добавил?
Объясните мне, что значит "дать основания" и почему это всех так тревожит.
Допустим, есть N утверждений, про которые известно, что они должны быть истинными. Требуется предоставить набор аксиом и определений такой, что в нём каждое из N утверждений будет теоремой, причем аксиомами будут далеко не все из этих N утверждений (желательно - ни одно).
Допустим, есть N утверждений, про которые известно, что они должны быть истинными. Требуется предоставить набор аксиом и определений такой, что в нём каждое из N утверждений будет теоремой, причем аксиомами будут далеко не все из этих N утверждений (желательно - ни одно).
Поясните про полноту евклидовой/афинной/любой геометрии. В книгах обычно дается доказательство категоричности, но причем здесь полнота?
А я ведь всю книгу прочёл, по совету с двача. В конце было ощущение, что меня протроллили. Хуже книги по логике я просто не встречал
Разве об этом тред?
На самом деле спор об основаниях имеет сугубо психологически-невротическую природу, и вполне очевидно, что никогда не будет текста, который раз и навсегда удовлетворил бы всех. Все эти попытки свести множества к чисто синтаксической игре утверждений о множествах, или к конструктивным типам, или ещё к какому-то такому синтаксису очевидно не могут привести к какому-то удовлетворению. Вот кажется что синтаксические игры - это "более близкие" объекты чем множества, потому что они "более осязаемые", потому что это "финитарные средства", но это мысль чисто социально-культурологическая, это стереотип; если бы не было вот этого вот дискурса классической логики и попыток свести всю математику к формальным теориям, то никому бы не казалось, что абстракция алгоритма или конструктивного типа чем-то проще или сложнее, чем абстракция множества. Категорщики, кстати, это поняли уже и ебашут свои (\infty,1)-категории, зачастую, без всяких ремарок о том, как это всё можно свести к формальным первопорядковым теориям (хотя на начальном уровне всё же различие "больших и малых категорий" осталось, но я надеюсь, что всё же откажутся вскоре и от этого). Потому что ебать себе мозги по-поводу оснований в 2к17 это уже такая же пошлятина как и ебать себе мозги по поводу того, что первичнее - материализм или идеализм.
>различие "больших и малых категорий" осталось, но я надеюсь, что всё же откажутся вскоре и от этого
Чистая педагогика же. Отказываться тут не получится, нужно новое поколение, которое со школы обучено категориям.
>Потому что ебать себе мозги по-поводу оснований в 2к17 это уже такая же пошлятина как и ебать себе мозги по поводу того, что первичнее - материализм или идеализм.
Я тебя помню. У тебя подход к вопросу о том, что важно в математике - это что-то в духе отождествления важного с модным. Вполне понятно, почему с таким мировоззрением тебе претят основания, онтологические вопросы вообще, как и вероятно остальная философская проблематика. Но вообще, для остальных людей (более склонных к независимым суждениям) такого рода вопросы часто могут быть важнее.
>хотя на начальном уровне всё же различие "больших и малых категорий" осталось, но я надеюсь, что всё же откажутся вскоре и от этого
Эта дурацкая терминология - это последствие неудачного выбора подразумеваемого метода формализации в теории множеств на основе классов. Но изначально это все было весьма полезно т.к. не было хорошей независимой интуиции о категориях и допустимых рассуждениях о них так что апелляция к разработанному аппарату теории множеств была полезна. Хотя стоит отметить, что если, например, подразумевать формализацию в теории множеств на основе принципа отражений, то все выходит существенно более гладко (хотя здесь есть недостаток в виде относительно больших требований к знаниям теории множеств). С другой стороны, разумеется, все это было важно в основном на начальном этапе разработки теории категорий, сейчас, когда неформальные представления о том, какого рода рассуждения корректны хорошо разработаны, заморачиваться вопросом о формализации куда менее важно.
>если бы не было вот этого вот дискурса классической логики и попыток свести всю математику к формальным теориям, то никому бы не казалось, что абстракция алгоритма или конструктивного типа чем-то проще или сложнее, чем абстракция множества.
Нет, конечно. Алгоритм на текущий день (исторически это, разумеется, было скорее наоборот) можно считать непосредственной абстракцией от программы на компьютере. Это гораздо боле приближенно к обычной жизни, чем множества или конструктивные типы (я бы сказал, что лишь немного сложнее понятия натурального числа).
>Я тебя помню.
Ты меня не можешь помнить.
>Но вообще, для остальных людей (более склонных к независимым суждениям)
>Это гораздо боле приближенно к обычной жизни, чем множества или конструктивные типы
Самая большая загадка на свете: почему люди, позицианирующие себя как рационально-мыслящие-с-независимыми-суждениями упорнее всего талдычат одни и те же догмы? Не загадка никакая, конечно, примерно понятно из какого желания ноги у независимо-судящих растут.
Ты меня не можешь помнить.
>Но вообще, для остальных людей (более склонных к независимым суждениям)
>Это гораздо боле приближенно к обычной жизни, чем множества или конструктивные типы
Самая большая загадка на свете: почему люди, позицианирующие себя как рационально-мыслящие-с-независимыми-суждениями упорнее всего талдычат одни и те же догмы? Не загадка никакая, конечно, примерно понятно из какого желания ноги у независимо-судящих растут.
>Ты меня не можешь помнить.
Технически я не могу исключать, что ошибаюсь, но определенно у меня был небольшой диалог с аноном с явно родственной позицией и похожим стилем.
>позицианирующие себя как рационально-мыслящие-с-независимыми-суждениями
Да бог с тобой, я лишь подчеркивал то, что идея о сведение ценности исключительно к моде - это, в сущности, радикальная позиция состоящая в полном отказе от самостоятельных суждений (по данному вопросу).
> талдычат одни и те же догмы
Если у тебя все-таки есть аргументы почему это довольно очевидно наблюдение несостоятельно, то можешь поделиться.
>Отказываться тут не получится, нужно новое поколение, которое со школы обучено категориям.
Думаю, что в любом случае учить сразу категориям, в обход множеств, неэффективный подход. Дело в том, что очень похоже, что основной набор интуиций касательно категорий (в независимом от теории множеств контексте) заметно сложнее чем набор интуиций для самих множеств. В пользу этого явно говорит то, что набор формальных аксиом для теории множеств более-менее вразумителен, а вопрос о аксиоматизации категории Cat, если мне не изменяет память, провисел открытым полтора десятилетия, в итоге был решен, но аксиоматизация оказалась весьма сложной и в итоге никакой заметной популярностью не пользуется.
>Если у тебя все-таки есть аргументы почему это довольно очевидно наблюдение несостоятельно, то можешь поделиться.
Аргументы должны быть у тебя почему оно состоятельно. (Бремя доказательства) Сразу скажу, что аргумент эта же ачивидно - не очень сильный.
>Да бог с тобой, я лишь подчеркивал то, что идея о сведение ценности исключительно к моде - это, в сущности, радикальная позиция состоящая в полном отказе от самостоятельных суждений (по данному вопросу).
Я ни к чему "ценность" не сводил, так как не понимаю, что слово "ценность" значит.
Аргументы должны быть у тебя почему оно состоятельно. (Бремя доказательства) Сразу скажу, что аргумент эта же ачивидно - не очень сильный.
>Да бог с тобой, я лишь подчеркивал то, что идея о сведение ценности исключительно к моде - это, в сущности, радикальная позиция состоящая в полном отказе от самостоятельных суждений (по данному вопросу).
Я ни к чему "ценность" не сводил, так как не понимаю, что слово "ценность" значит.
Точки, стрелочки, композиция, идентичность. Охуеть как сложно.
>набор формальных аксиом для теории множеств более-менее вразумителен
Объясни, пожалуйста, чем мотивированы
а) аксиома подстановки
б) аксиома регулярности
Это простая часть. Проблема состоит в том, чтобы очертить допустимые методы формации новых категорий, не опираясь на аппарат теории множеств. И если доводить дело до честного выписывания набора аксиом, то выходит сложно (сложнее чем с множествами).
a) если некоторая коллекция является множеством, то всякая коллекция того же или меньшего размера тоже множество;
б) множества и вселенная фон Неймана - это одно и тоже.
Но строго говоря, это аксиомы, которые были добавлены на позднем этапе разработки теории множеств и если их выбросить, то получится теория вполне подходящая для погружения обычной математики, но плохо подходящая для собственно теоретико-множественных исследований. В силу этого они отражают боле "продвинутые" интуиции.
Ладно, у меня нет особенного желания ввязываться в пустой спор с человеком, который в основном занимается словесной эквелибристикой, а не содержательной аргументацией своей позиции.
>Ачивидно, что алгоритм понятнее и проще, чем множество
>Почему?
>А почему нет?
>Ты сделал утверждение, ты и обосновывай
>Пропало всякое желание с тобой разговаривать, эквилибрист словесный
yaasno
>Это простая часть. Проблема состоит в том, чтобы очертить допустимые методы формации новых категорий
Вот у меня два вопроса всегда
1) Зачем их очерчивать?
2) Почему останавливаются только на первой итерации и не очерчивают допустимые методы очерчивания допустимых методов образования новых категорий?
1)Чтобы различать корректные рассуждения и некорректные. Для практики обычного математика аксиоматизация, как правило, здесь избыточна и в подавляющем большинстве случаев понимания получаемого из разбора большого числа допустимых построений и нескольких приводящих к парадоксам вполне достаточно. Хотя, конечно, не исключено, что например однажды может прийти на рецензию статья, где ошибка кроется в построение парадоксальность которого не ясна из рассмотренных примеров.
2)Без комментариев.
Почему без комментариев? Почему корректность важна, а корректность корректности "без комментариев"? Что это за фашизм такой?
Я же говорю, тебе прежде всего хочется заниматься словесной эквилибристикой. Речь шла о обучении теории категорий, ты же для полемических целей акцентируешь внимание на совершенно очевидно иррелевантном здесь вопросе.
https://2ch.hk/sci/res/402946.html
Конструктивный выблядок ворвался в тред по ВАЛЕОЛОГИИ!!! Эта шваль осталась в /sci или же она тут обитает? Какой-то новый уровень шитпоста прям.
Конструктивный выблядок ворвался в тред по ВАЛЕОЛОГИИ!!! Эта шваль осталась в /sci или же она тут обитает? Какой-то новый уровень шитпоста прям.
>Проблема состоит в том, чтобы очертить допустимые методы формации новых категорий, не опираясь на аппарат теории множеств.
Таки да. Но тут такая штука , что просто так взять и раз и навсегда очертить математику и успокоится ( как хотел Гильберт, например) ведь не получится. Точнее, оно может и получится, только смысла тогда особого в категориях нет - тут теория множеств как раз лучше послужит, как статичная система.
Как по мне, весь смак категорий в том, чтобы не мешать творческой ( а для упоротых платонистов - исследовательской) составляющей процесса. Т.е. да - ты можешь наворотить лютейшую хуйню не оглядываясь ни на кого, лишь бы ты сам видел в этом смысл. Тогда вопрос корректности выходит за рамки формализма - это уже вопрос того, как другие относятся к твоей работе.
Ну а прелесть еще в том, что по сути даже школьную программу менять не надо. Просто математика должна начинаться с показа объектов и морфизмов и слов типа "ну вот в целом это и есть математика". Дети сначала нихуя не поймут, конечно. И дальше все пусть идет по старому, но каждая пройденная тема, хоть в алгебре, хоть в геометрии, должна кончаться показом соответствующей категории. И вот так постепенно к концу школы до некоторых действительно дойдет, что значит абстракция и конструирование. А это уже будет лютейшим вином, как по мне.
Почему каждый хуй мечтает отреформировать школьную программу? Т.е. вообще каждый, поголовно.
Потому что фундамент
Ну я всегда рад поссать за шиворот гуманитарному быдлу. Ты, собственно, к чему возгорел? Неудобный вопрос про фальсифицируемость критерия Поппера не понравился?
потому что хочется как-то связать ее с математикой, а так они лишь имеют одинаковое название. Почему бы просто не переименовать школьный предмет в "практические вычислительные навыки".
Проблема есть. Но исправить это далек не просто, особенно если говорить об общеобразовательной школе и тем более, если заходить с позиций математика с ограниченным/отсутствующим опытом преподавания рядовым школьникам. Например, уверен, что план
>Просто математика должна начинаться с показа объектов и морфизмов и слов типа "ну вот в целом это и есть математика". Дети сначала нихуя не поймут, конечно. И дальше все пусть идет по старому, но каждая пройденная тема, хоть в алгебре, хоть в геометрии, должна кончаться показом соответствующей категории. И вот так постепенно к концу школы до некоторых действительно дойдет, что значит абстракция и конструирование.
полностью провалится и просто никто ничего не поймет (включая преподавателей математики). Думаю, что это провалится и в матшколах.
Можно вспомнить колмогоровскую реформу школьного курса геометрии в рамках которой например простая замена термина "равенство фигур" на более корректный "конгруэнтность фигур" привела к большим проблемам с пониманием содержания школьниками.
Из своего ограниченного опыта преподавания в кружках школьникам 5-7 классов могу сказать, что навык восприятия абстрактных конструкций находится на низком уровне и развивается медленно. Например, задачи которые сводятся к тому или иному разбору конкретных случаев даются школьникам куда легче, чем задачи где нужно дать, пусть и тривиальное, но общее рассуждение.
Колмогоровская реформа была гораздо более радикальной, нежели просто замена термина "равенство" на термин "конгруэнтность". Например, он определил вектор как изометрию плоскости/пространства, буквально такими словами. Естественно, что учителя его не поняли.
>то чувство, когда искренне не понимаешь, что не так
как вектор то определять правильно? как стрелочку с хвостиком?
Столбец.
Неориентированный отрезок - это неупорядоченная пара точек плоскости.
Ориентированный отрезок - это упорядоченная пара точек плоскости.
Два ориентированных отрезка называются эквивалентными, если совмещаются параллельным переносом.
Свободные векторы - классы множества ориентированных отрезков по этому отношению эквивалентности.
ну и с какого хуя такой подход верный? эти определения не дают никакой интуиции: определи теперь сумму векторов, разнообразные произведения, получится вообще невыносимая поебень.
Вот это проиграл с теоретико-множественных дидов, лил.
Что там определять? Правило треугольника очень простое. А "вектор это изотропия пространства" хуйня какая-то. Много векторов = много изотропий? Сумма векторов = сумма изотропий? Это тоже не даёт никакой интуиции. Поебень непонятная. Никогда школьник не вдуплит это.
Во видал, даже я перепутал слова, школьники с ваших изометрий вообщей охуеют. Но тем, кто школьников ничему никогда не учил не понять.
-кун
-кун
Единственная реформа которая нужна школьному образованию - это укоротить его раза в 3, чтобы не мешать нормальным школьникам заниматься нормальными делами (ходить на кружки и заниматься самоподготовкой, например) и не ебать мозги всяким долбоёбам, которые всё равно ничего не выучат. Ну и, конечно же, не ебать мозги учителям, которые тоже школьной программы в полном объеме не знают.
композиция изометрий - изометрия. Изометрии образуют группу Ли. все же просто.
Расскажи о своём опыте обучения 7-ми классников группам Ли.
ну можно сказать просто "группа", это совсем простое понятие.
Суммой ориентированного отрезка (ab) и ориентированного отрезка (bc) называется ориентированный отрезок (ac).
Пусть x и y - свободные векторы. Выберем в x представителя (pq). Найдем в y ориентированный отрезок (qr), начало которого равно q. Суммой x и y называется класс эквивалентности отрезка (pq)+(qr). Определение не зависит от выбора представителя, очевидно.
Пусть векторы определены как изометрии плоскости. Ну и как определить тогда сумму?
>Пусть векторы определены как изометрии плоскости.
Это неправильное определение - хочется отождествить вектора с параллельными переносами, а кроме них изометриями являются еще повороты и отражения.
Как композицию биекций, но не мат. школьникам такое будет очень сложно переварить. Им ещё придётся строить заново геометрическую интуицию. Ещё школьнику понятно будет что такое параллельный перенос конкретных фигур и векторов, но преобразования всей плоскости будет сложнее понять.
В общем всем реформаторам предлагаю пойти в обычную школу, взять там обычных школьников и попытаться им рассказать что-то на вашем любимом языке. в рамках факультатива
А на вопрос мой так никто и не ответил - почему тот же Гильберт был дико заинтересован в том, что бы дать "непротиворечивые финитарные основания для математики", но тот факт, что "непротиворечивые финитарные основания" сами оставались без "непротиворечивых финитарных оснований" его нисколько не смущал? Неужто он не видел, что он просто смещает "стартовую точку", но никакого принципиального парадигмального сдвига не происходит? Не понимаю этот момент серьезно.
Существуют фс, которые могут подтвердить собственную непротиворечивость, именно этот факт и заставил гильберта верить.
Но ведь они доказывают не собственную непротиворечивость, а непротиворечивость "маленькой модели самой себя", то есть тут происходит расщепление на "большую ФС" и "маленькую ФС внутри большой ФС" и "большая ФС" не может, вообще говоря, провести отождествление "маленькой ФС" с самой собой. То есть тут размахивают руками и говорят о какой-то "эффективной непротиворечивости", дескать да, формально не можем отождествить, но мы-то понимаем как оно на самом деле. Ну так мы и раньше понимали как оно на самом деле, без программ Гильберта всяких.
У Гильберта не стояло задачи обосновать корректность финитных методов - они как раз и были очерчены таким образом, чтобы быть куском математики, который признается всеми математиками (не уверен, были ли в те времена ультрафинитисты, которые и с этим были не согласны, но в любом случае они никогда не были чем-то большим, чем незначительное меньшинство). Была проблема с более абстрактными теоретико-множественными методами в свете парадоксов теории множеств и вполне заметного числа математиков, которые эти методы отвергали. Гильберт хотел защитить теоретико-множественные методы от этих нападок, сведя их к финитным. Насколько я понимаю, Гильберт не был точен в формулировках целей так как в силу ошибочных предположений считал, что можно достичь "всего и сразу". Тем не менее, видимо главным здесь было доказать финитными средствами, что всякое теоретико-множественное доказательство финитного факта преобразуется в финитное доказательство того же факта.
>Существуют фс, которые могут подтвердить собственную непротиворечивость, именно этот факт и заставил гильберта верить.
Во времена Гильберта ничего такого известно не было. Современные же примеры совершенно экзотичны.
Понятно. То есть, если грубо, этот аргумент в каком-то роде должен был быть социальным, а не метафизическим.
Видимо так.
Но строго говоря, я Гильберта не читал (и не факт, что он непосредственно об этом пишет), а просто пересказываю интерпретации, которые слышал.
Чё там на сходосе порешили по поводу а=0.9999999(9)?
Что такое иррациональное число? Это просто те вещественные числа, которые не являются рациональными. Всё. Аксиоматика построена.
В этом треде каждый анон знает все тонкости определения вещественных чисел по Стевину-Вейерштрассу. Попробуй что-нибудь другое.
Чё значит попробуй? Я вопрос задал вообще-то
Доказательства на уровне
>Что такое иррациональное число? Это просто те вещественные числа, которые не являются рациональными.
Это то что уничтожит любой софист, причём самый нубский
Тут нужно задавать более тонкие вопросы. Например, требовать предъявить явно заданный полный порядок на R. Оставь 0.(9)=1 школьникам.
Ой всё, иди нахуй, мог тыкнуть в статью и заткнуть меня легко и просто, но ты почему-то решил тут заняться флудом.
Вынужден признать что и здесь используется софистика уровня "Ну ты понел". Ноль у них положительный и отрицательный, всё сделают чтобы убедительно друг друга так наебать чтобы ещё и самим себе поверить
У Гильберта получилось (и надо признать, годно получилось) аксиоматически построить геометрию. Этот успех заставил его уверовать, что и с арифметикой и вообще со всем остальным можно так же. Но реальность оказалось несколько сложнее, что прямо показывает нам сомнительную ценность таких экстраполяций от одного-пары частных случаев оптом и априори на все остальные как закон исключенного третьего, например. То же самое можно сказать про т.н. "догму Гильберта", это же чистая религия.
>эуклид
> как закон исключенного третьего, например
и собственно модус поненс.
>поненс.
С элиминатором импликации-то что не так?
Все так, если веруешь.
>если веруешь.
Во что?
В правила резолюции.
Если начать применять этот принцип
>прямо показывает нам сомнительную ценность таких экстраполяций от одного-пары частных случаев оптом и априори на все остальные
последовательно (т.е. отказываться от индукции вообще), то и от модус поненс нужно отказаться.
Ну вот я тебе принес это правило, покажи что там не так.
Но у нас пропозишен - это всегда множество пруф-объектов, его доказывающих. Только конструктивные объекты, только хардкор.
>Только конструктивные объекты, только хардкор.
Ну это вера из двух частей:
- вера в тезис черча, так что любая математическая задача может быть сведена к алгоритму
- вера в непогрешимость вычислительной техники (тот же модус поненс по сути)
О какой вере ты говоришь применительно к вычислимым объектам?
о вере в функциональные типы. Еще разок: у нас есть эмпирический закон, что транзисторы ведут себя определенным образом. Остается только верить, что они будут вести себя так и дальше. Согласно этой вере вычисление всегда предсказуемо. А дальше по изоморфизму карри-говарда модус поненс может быть сведен к функциональным типам.
Теперь у нас есть такой же закон исключенного третьего. Эмпирически он всегда выполнен для вычислимых объектов. В чем же дело? Почему нельзя в него верить?
>у нас есть эмпирический закон, что транзисторы ведут себя определенным образом. Остается только верить, что они будут вести себя так и дальше.
Именно что эмпирически. Зачем верить, если есть факты?
>закон исключенного третьего. Эмпирически он всегда выполнен для вычислимых объектов. В чем же дело? Почему нельзя в него верить?
Потому что он невычислим в общем случае. А на конечных множествах его и Брауэр не отрицал.
>Зачем верить, если есть факты?
Математик и физик доказывают теорему о том, что все нечетные числа - простые. Математик: - 1 - простое, 3 - простое, 5 - простое, 7 - простое, 9 - не простое. Это контрпример, значит теорема неверна. Физик: - 3, 5 и 7 - простые, 9 - ошибка эксперимента, 11 - простое и т.д. Возьмем ещё несколько случайно выбранных нечетных чисел. 17 - простое, 19 - простое, 23 - простое... Теорема доказана.
>Потому что он невычислим в общем случае
Это доказанный факт?
Но вернемся к >Зачем верить, если есть факты
На 2017 год закон исключенного третьего всегда работал для любых математических объектов.
Высказывание - моя мамка старше меня и моложе, например. Вообще, логика времени нужна, а не пространства.
Невыводимая формула, конечно, отличный пример.
>На 2017 год закон исключенного третьего всегда работал для любых математических объектов.
Для любых, на которых его можно показать непосредственно. Т.е. на любых построимых, вычислимых, в общем случае - конструктивных объектах. Хватит тупить уже, самому тебе не надоело нести хуйню?
Я сказал просто для любых. Утверждение, доказанное в классической логике, всегда может быть доказано в интуитивистской. (эмпирический факт)
Классическая логика - это просто синтаксические правила. Считается, что они истинны для всех случаев оприори. Конструктивная - манипуляции с конструктивными объектами, действие правил распространяется только на конструктивные объекты.
Ты оперируешь какими-то бредовыми определениями. Классическая логика это интуитивистская + LEM. Собственно, нахера я опять пересказываю HoTT?
>Ты оперируешь какими-то бредовыми определениями.
Ты не слышал про интуиционстскую логику Гейтинга, интерпретацию логических констант по Брауэру-Гейтингу-Колмогорову, изоморфизм Карри-Говарда, раз уж называешь "мои" определения бредовыми. Видимо, и про MLTT мало что знаешь. Но при этом лезешь в НоТТ. Это напоминает школьников из треда про машинное обучение и нейросети в /пр - не зная даже азов уровня учебников Вентцель и Зорича/Фихтенгольца, лезут читать ISLR и т.д. Итог закономерен.
HoTT не нужны никакие пререквизиты, она предназначена для математиков, желающих изучить новые основания. Читателю не нужно знать даже, что такое теория типов, а все твои исторические термины он может изучить в википедии.
Пока что я могу судить, что ты до сих пор не удосужился открыть HoTT и почитать, раз я должен вычитывать правильные определения за тебя.
Я хотел бы переделать свой ответ. Мне кажется ты говоришь не про то, ибо если бы программа Гильберта действительно бы заключалась в
>всякое теоретико-множественное доказательство финитного факта преобразуется в финитное доказательство того же факта.
то, естественно, она была бы успешной. Ведь есть тупо теорема о том, что ZFC доказывает те же самые арифметические утверждения, что и PA (я её запомнил как "теорема об элиминации"), значит дело тут не в том.
>HoTT не нужны никакие пререквизиты
Ой, все. Там самая первая глава - изложение MLTT. Для MLTT не нужны пререквизиты? И как, много ты там понял?
> Ведь есть тупо теорема о том, что ZFC доказывает те же самые арифметические утверждения, что и PA (я её запомнил как "теорема об элиминации"), значит дело тут не в том.
Такой теоремы нет. В силу второй теоремы Гёделя о неполноте, предполагая непротиворечивость PA, верно обратное. В ZFC несложно доказать, что PA непротиворечива (рассмотреть натуральные числа с функциями сложения, умножения и следования и показать, что это модель PA), но по второй теореме Гёделя о неполноте PA не доказывает собственную непротиворечивость.
Извиняюсь, перепутал с другой теоремой о том, что ZFC+CH доказывает те же самые арифм. утверждения, что и ZFC.
Мне всю книгу скринить надо, чтобы ты ее тут прочитал? Книга начинается с пояснения, что такое тип, что такое теория типов, что такое суждение. Кому нужны такие пояснения? Вестимо, что математикам, кому знакомы общие понятия наивной теории множеств и гомотопической алгебры. Далее идет сравнение с классическими основаниями.
Читателю, знакомому с MLTT, рекомендуют вообще читать первую главу по диагонали.
Хотя прозвучали кодовые слова...
Ты в моих постах триггеры выискиваешь, чтобы потом гореть с них? Зачем? Это же обычная терминология.
которые кроме тебя никто не употребляет.
https://www.google.ru/?gfe_rd=cr&ei=ev2VWIOMNoqBZI_LlcgF#newwindow=1&q=%22%D0%B8%D0%BD%D1%82%D0%B5%D1%80%D0%BF%D1%80%D0%B5%D1%82%D0%B0%D1%86%D0%B8%D1%8E+%D0%BB%D0%BE%D0%B3%D0%B8%D1%87%D0%B5%D1%81%D0%BA%D0%B8%D1%85+%D0%BA%D0%BE%D0%BD%D1%81%D1%82%D0%B0%D0%BD%D1%82%22
Не, ну серьезно. "Общепринятые термины", употребляющиеся в одной книжке и ссылающихся на эту книжку статьях.
https://www.google.ru/?gfe_rd=cr&#newwindow=1&q=%22%D0%B0%D0%BA%D1%82+%D0%B8%D0%BD%D1%82%D1%83%D0%B8%D1%86%D0%B8%D0%BE%D0%BD%D0%B8%D0%B7%D0%BC%D0%B0%22
https://www.google.ru/?gfe_rd=cr#newwindow=1&q=%22%D0%91%D1%80%D0%B0%D1%83%D1%8D%D1%80%D1%83-%D0%B3%D0%B5%D0%B9%D1%82%D0%B8%D0%BD%D0%B3%D1%83%22
https://www.google.ru/?gfe_rd=cr&#newwindow=1&q=%22%D0%B0%D0%BA%D1%82+%D0%B8%D0%BD%D1%82%D1%83%D0%B8%D1%86%D0%B8%D0%BE%D0%BD%D0%B8%D0%B7%D0%BC%D0%B0%22
https://www.google.ru/?gfe_rd=cr#newwindow=1&q=%22%D0%91%D1%80%D0%B0%D1%83%D1%8D%D1%80%D1%83-%D0%B3%D0%B5%D0%B9%D1%82%D0%B8%D0%BD%D0%B3%D1%83%22
А ты хорош. Но интуиционизм тоже неплох
Пиздец. А ниче, что по этой теме на русском языке полторы книжки и есть? Мне, может быть, использовать термин 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? Ты правда аутист какой-то, сам себе придумываешь триггеры, чтобы потом с них на батрушку высаживаться.
миллионы книг и статей - харам
@
халяль - полторы книжки
Почитал тута за ультраинтуиционизм Есенина-Вольпина пикрелейтед, это разве серьезная математическая точка зрения? Он отвергает марковскую абстракцию потенциальной осуществимости, но тут же предлагает "гипотезу осуществимости следующего шага", что то же самое, вид сбоку. Далее, говорит, что функция следования - это не закон, а только намек на закон (хотя по факту это конструктивная функция, конструктивный объект, т.е. именно совершенно конкретная формулировка закона). Потом вообще какой-то аутизм уровня того анекдота:
-Дохуя-это сколько?
- Иди вдоль рельсов и считай шпалы. Когда досчитаешь до "а ну его
нахуй"-это будет как раз половина.
-Дохуя-это сколько?
- Иди вдоль рельсов и считай шпалы. Когда досчитаешь до "а ну его
нахуй"-это будет как раз половина.
На твоем пикрелейтеде же вполне четко и понятно даны ответы на твои вопросы. Не очень понятно, что именно непонятно. Вот он говорит: пусть у нас есть ребенок и функция следования для него, которая берет ребенка и дает ребенка в следующий момент времени. То есть р, р', р''- это все ребенки, но интуитивно ясно, что после некоторого (неопределенного) количества применений этой операции результат уже никак ребенком быть не может. Это он и постулирует утверждением под номером три. Я просто пересказываю текст еще раз, да.
Ну а про "и так далее" и вовсе говорить нечего. Определим натуральные числа: 1, 2, 3 и так далее. Ну ты понял.
Пример с ребенком дурной какой-то, что-то уровня парадокса лысого или парадокса кучи. Такое решается с помощью нечеткой логики, функция следования и потенциальная осуществимость тут вообще не при чем.
>Ну а про "и так далее" и вовсе говорить нечего. Определим натуральные числа: 1, 2, 3 и так далее. Ну ты понял.
И что тут не так?
> что тут не так
Это не определение.
> тут вообще не при чем
Ну как они не при чем, если он об этом и говорит? Никто же не спорит, что эти ситуации можно смоделировать в рамках дефолтной модели. Это у него просто философский аргумент такой: вот, посмотрите - понятие, которые мы принимаем за интуитивно ясное, на самом деле работает совсем не так, а эдак.
Не более дурной, чем пример с брадобреем в кое-какой другой некогда популярной теории.
1. Если убрать с головы волосатого человека один волосок, он не станет лысым. Начнём убирать с головы человека волосы по одной штучке за раз; через некоторое время получим лысого человека. Таким образом, имеем антиномию. Объекты, обладающие такой антиномией, будем называть собственно ультрафинитистскими.
2. К собственно ультрафинитистским объектам не применима абстракция потенциальной осуществимости. Они обладают тем свойством, что по ходу итеративного процесса перестают быть равными себе, какими они были до начала процесса.
3. Не существует доказательств, что объекты, используемые в метаматематических построениях, не являются собственно ультрафинитистскими.
4. Пользуясь случаем, передаю привет чернильной дыре.
>1. Если убрать с головы волосатого человека один волосок, он не станет лысым. Начнём убирать с головы человека волосы по одной штучке за раз; через некоторое время получим лысого человека. Таким образом, имеем антиномию. Объекты, обладающие такой антиномией, будем называть собственно ультрафинитистскими.
Тут нет никакой антиномии, просто бинарная логика неприменима к подобным задачам, т.к. мы не можем в точности указать, с какого конкретно количества волос считать человека лысым. Непрерывная функция принадлежности вопрос снимает полностью, т.к. появляется возможность считать человека лысым и волосатым в какой-то степени от 0 до 1. Не понимаю, зачем тащить в такие задачи какой-то ультрафинитизм, когда все элементарно сводится к нечетким множествам.
>Это не определение.
А что это? 0:N, if a:N then succ(a):N, закон построения (функция следования).
А где гарантия, что "бинарная логика" применима к основным умозрительным объектам метаматематики, таким как строка символов, алфавит, возможность в любой момент времени ввести новую, не использованную ранее букву?
В случае конечных объектов можно проверить непосредственно, применима или нет. В общем случае, безотносительно возможности построения, никакой гарантии, только вера.
Тогда получается мы не можем нормально работать с натуральными числами?
А ультрафинитисты вот не веруют, но доказывают.
С какими-то можем, с какими-то нет. Так-то 10^100^1000^10000 тоже натуральное число.
На эту тему вообще есть что почитать интересного? Я вот гуглил, на русском языке одну статью нашел, которую и процитировал, на английском тоже почти ничего.
>С какими-то можем, с какими-то нет. Так-то 10^100^1000^10000 тоже натуральное число.
Выходит, конструктивная математика основанна на вере ?
Я уже столько раз писал про марковскую абстракцию потенциальной осуществимости, что даже не помню сколько раз конкретно. И чем конструктивный объект отличается от потенциально существующего, писал не меньше. С себя начни, если такие простые вещи понять не можешь.
проговаривать название != писать
Ну у тебя и пичот.
>марковскую абстракцию потенциальной осуществимости
Вера. Обычная вера в то, что алгоритм может работать верно и выдавать нужные результаты, при этом не останавливаясь. Раз можно проверить потенциальное сущствование только конечное количество объектов, в нашем случае чисел, то как проверить, что алгоритм верен?
> С себя начни, если такие простые вещи понять не можешь.
Ты опять берёшь и уходишь от ответа, мань.
>Выходит, конструктивная математика основанна на вере ?
Мозг конструирует для нас реальность. И мы в нее верим, а что ещё остается делать?
Познакомьтесь немного с сабжем, прежде чем спорить https://plato.stanford.edu/entries/mathematics-constructive/
В алгоритмы веровать не нужно. Алгоритм либо работает правильно и выдает правильный результат, либо он работает неправильно и выдает результат, доказывающий абсурдность предположения, что алгоритм работает правильно. Любой алгоритм сводится к типизированной лямбде, корректность его можно проверить методами MLTT, опять же, про интерпретацию логических констант и изоморфизм Карри-Говарда я писал достаточно, чтобы тут у какого-то кловна жопа горела с этой терминологии.
>Алгоритм либо работает правильно и выдает правильный результат, либо он работает неправильно и выдает результат, доказывающий абсурдность предположения, что алгоритм работает правильно.
Разве это не закон исключённого третьего? Ты берёшь и веруешь в то, что твой алгоритм работет либо правильно либо неправильно? Чем эта вера отличается от веры в аллаха?
>Разве это не закон исключённого третьего? Ты берёшь и веруешь в то, что твой алгоритм работет либо правильно либо неправильно? Чем эта вера отличается от веры в аллаха?
Пиздец. А я ведь специально сформулировал отрицание именно в интуиционистском смысле. Но что можно объяснить школьнику на батрушке. Закон искл