1,3 Мб, 3308x4679Решаем
Mendelson Elliott: Introduction to Mathematical Logic
http://rgho.st/7WHmFCSPM
По моему скромному разумению - уметь решать эти задачи максимально чётко должен уметь всякий уважающий себя математик, и неважно в какой сфере он работает.
Здесь я буду постить решения, до тех пор пока не прорешаю всё. Если кто хочет за компанию - присоединяйтесь, спрашивайте, предлагайте свои варианты, критикуйте.
Пикрелейтед включает в себя необходимые 13 аксиом(с галочками), которые составляют суть теории.
Чем крута NBG?
1) конечной аксиоматизируемостью(в отличие от ZFC)
2) отсутствием парадоксов (в отличие от наивной теории множеств)
3) наличием классов (в отличие от ZFC)
4) после её изучения - понятно о чём стандартные вузовские курсы
5) высокой скоростью доказывания, по сравнению с HoTT-ом, например, который собственно ещё очень сырой и совершенно невоспринимаем большинством математиков.
A про книгу - выдержала 6 изданий, что косвенно говорит о качестве. В подарок - определим таки наконец ординалы, и не только N.
Короче, в добрый путь!
Mendelson Elliott: Introduction to Mathematical Logic
http://rgho.st/7WHmFCSPM
По моему скромному разумению - уметь решать эти задачи максимально чётко должен уметь всякий уважающий себя математик, и неважно в какой сфере он работает.
Здесь я буду постить решения, до тех пор пока не прорешаю всё. Если кто хочет за компанию - присоединяйтесь, спрашивайте, предлагайте свои варианты, критикуйте.
Пикрелейтед включает в себя необходимые 13 аксиом(с галочками), которые составляют суть теории.
Чем крута NBG?
1) конечной аксиоматизируемостью(в отличие от ZFC)
2) отсутствием парадоксов (в отличие от наивной теории множеств)
3) наличием классов (в отличие от ZFC)
4) после её изучения - понятно о чём стандартные вузовские курсы
5) высокой скоростью доказывания, по сравнению с HoTT-ом, например, который собственно ещё очень сырой и совершенно невоспринимаем большинством математиков.
A про книгу - выдержала 6 изданий, что косвенно говорит о качестве. В подарок - определим таки наконец ординалы, и не только N.
Короче, в добрый путь!
1,2 Мб, 3308x4679p.s. также есть мнение, что NBG - хороша для изучения перед теорией категорий: ведь тогда не будет никаких вопросов типа "А что такое large category"? (которых и на dxdy хватает, с совершенно нелепыми ответами.)
Так, и да, если я что-то решил, это не значит, что я это не перерешаю с большей точностью суждений.
Так, и да, если я что-то решил, это не значит, что я это не перерешаю с большей точностью суждений.
1,2 Мб, 3308x4679>>9895 (OP)
ex. 4.1, 4.2, 4.4
ex. 4.1, 4.2, 4.4
1,3 Мб, 3308x4679>>9895 (OP)
Attention!
Собственно самое главное - решаем именно главы 4.1 и 4.2.
Указываем решенные на фото:
ex. 4.2, 4.5
Attention!
Собственно самое главное - решаем именно главы 4.1 и 4.2.
Указываем решенные на фото:
ex. 4.2, 4.5
1,2 Мб, 3308x4679(без номера, о том, что пустой класс - это множество)
Разумеется, в начале мои доказательства - будут хуже по качеству, чем в конце, поэтому - смело переписывайте начисто с дополнительными пояснениями.
Например - надо, чтобы были видны благодаря каким правилам логики предикатов осуществляются переходы между высказываниями о классах.
Разумеется, в начале мои доказательства - будут хуже по качеству, чем в конце, поэтому - смело переписывайте начисто с дополнительными пояснениями.
Например - надо, чтобы были видны благодаря каким правилам логики предикатов осуществляются переходы между высказываниями о классах.
121 Кб, 246x364Братишки, я вам почитать принес Введение в математическую логику Мендельсон Эллиот в пдф http://bookzz.org/md5/9FD88488C51AFEC4EB20D0279642D190 и в джву http://bookzz.org/md5/625FC8E6D627510F98E67C01A8EC3930
Бля, ты заебал, 3 треда про свою логику ебучую создал, у вас же есть тред про основания - там и паситесь.
Посмотрел по диагонали оглавление этого вашего Мендельсона, вот это http://bookzz.org/md5/1EC5F0DF018488D368BB3CB9D4EE279B посолиднее выглядит. Опять же, один из авторов - тот самый Френкель, который систему Цермело допилил.
>>9895 (OP)
Почему не взять книгу Манина, она интереснее.
Почему не взять книгу Манина, она интереснее.
>>9921
Так это другой анон алсо, это лучше, чем слушать нытье хорена про мочу в половине тредов на нулевой
Так это другой анон алсо, это лучше, чем слушать нытье хорена про мочу в половине тредов на нулевой
>>9923
Сначала ту, годнота же.
Сначала ту, годнота же.
Я вернулся, решил не просто доказывать это, а формально верифицировать(пока - всё утверждения до ex4.6). По скорости - лишь на процентов 10 медленнее получается, чем на бумаге.
>>10357
В Coq. Пока выкладывать не буду - не насчёт всего на 100% уверен. Но вроде получается, до 4.26 добрался. С гигантскими пропусками, разумеется.
В Coq. Пока выкладывать не буду - не насчёт всего на 100% уверен. Но вроде получается, до 4.26 добрался. С гигантскими пропусками, разумеется.
>>9895 (OP)
Ящик рассчитать поможет?
Ящик рассчитать поможет?
>>9895 (OP)
Вот моя имплементация
https://github.com/FirstLast1/nbg_in_coq/blob/master/NBG.v
Как что-нибудь обновлю - сразу напишу тут.
Критика, рекомендации и попытки самостоятельного решения нерешённых или решённых упражнений - приветствуются.
Вот моя имплементация
https://github.com/FirstLast1/nbg_in_coq/blob/master/NBG.v
Как что-нибудь обновлю - сразу напишу тут.
Критика, рекомендации и попытки самостоятельного решения нерешённых или решённых упражнений - приветствуются.
Стесняюсь спросить, если NBG представима в зависимых типах (оп жи ее на куке пишет), то зачем она вообще нужна, когда есть MLTT? Дополнительный набор костылей?
>>10423
Предлагаю тебе решить 5-10 упражнений подряд оттуда таким образом, который ты предлагаешь и выложить это, чтобы я понял, твой подход работает лучше и научился ему. Согласен?
Предлагаю тебе решить 5-10 упражнений подряд оттуда таким образом, который ты предлагаешь и выложить это, чтобы я понял, твой подход работает лучше и научился ему. Согласен?
>>9895 (OP)
Мне пояснили, что лучше либо готовые Ensembles в Coq, либо Mizar.
1) Я пока ещё не понял, есть ли там классы.
2) Установил Mizar, наверное надо на него переходить - вроде как самый распространённый язык формальных доказательств и обещали гигантскую стандартную библиотеку. Но пока даже ещё запустить не смог, есть какое-нибудь адекватное IDE? Если кто-нибудь пользует - как там минимальный хеллоуворлд написать и запустить?
Возможно просто уже ночь, но я в упор не вижу инструкции по первым шагам.
Мне пояснили, что лучше либо готовые Ensembles в Coq, либо Mizar.
1) Я пока ещё не понял, есть ли там классы.
2) Установил Mizar, наверное надо на него переходить - вроде как самый распространённый язык формальных доказательств и обещали гигантскую стандартную библиотеку. Но пока даже ещё запустить не смог, есть какое-нибудь адекватное IDE? Если кто-нибудь пользует - как там минимальный хеллоуворлд написать и запустить?
Возможно просто уже ночь, но я в упор не вижу инструкции по первым шагам.
>>10547
А почему не LEAN например http://leanprover.github.io/ ? Есть даже браузерный вариант https://leanprover.github.io/programming_in_lean/?live
>Coq, либо Mizar.
А почему не LEAN например http://leanprover.github.io/ ? Есть даже браузерный вариант https://leanprover.github.io/programming_in_lean/?live
>>10564
У Coq-а тоже есть браузерный вариант: https://x80.org/collacoq/
LEAN - это майкрософт с большинством ноунейм разработчиков.
А у Coq-а - открытый код, активное коммьюнити и тридцатилетняя история и известные авторы.
Ну я бы точно не стал доверять разработчикам Windows.
p.s. наверное всё-таки буду продолжать на Coq-е, но сначала надо выяснить, какую они там теорию множеств-то реализовали - это пока непонятно.
Благо, что при использовании Ensembles можно практически не менять доказательства.
Я пока не понял как там классы определяются, typeclass наверное?
У Coq-а тоже есть браузерный вариант: https://x80.org/collacoq/
LEAN - это майкрософт с большинством ноунейм разработчиков.
А у Coq-а - открытый код, активное коммьюнити и тридцатилетняя история и известные авторы.
Ну я бы точно не стал доверять разработчикам Windows.
p.s. наверное всё-таки буду продолжать на Coq-е, но сначала надо выяснить, какую они там теорию множеств-то реализовали - это пока непонятно.
Благо, что при использовании Ensembles можно практически не менять доказательства.
Я пока не понял как там классы определяются, typeclass наверное?
>>10561
Это ты заявляешь из идеологических соображений - предпочитая интуиционистскую теорию типов построениям на базе классической логики первого порядка? Или ты в самом деле всерьез пробовал и то и то и считаешь, что Coq удобнее в использование?
>>10547
Я сам сколь-нибудь всерьез не занимался формализацией доказательств в таких системах. Но из общих соображений я бы предположил, что тебе Mizar больше подходит. Coq - это система на основе Calculus of Inductive Constructions, который является вариантом интуиционистской теории типов. И формализацию математики, насколько я понимаю, они в норме делают именно за счет средств Cic, а не погружая в него теорию множеств и формализуя математику в этом погружение. В Mizar-е, насколько я понимаю ситуацию, напротив в норме используют более классический подход к формализации математики - Mizar проверяет доказательства в логике первого порядка, а стандартная библиотека сделана на основе теории множеств (ZFC + аксиома вселенных Гротендика). Судя по тому, что в Mizar-е уже очень много чего формализовано, думаю что пользоваться им в худшем случае не сильно более неудобно, чем Coq. В тоже время, Mizar ориентирован на случая гораздо более похожий на твой (формализацию доказательств в NGB).
Это ты заявляешь из идеологических соображений - предпочитая интуиционистскую теорию типов построениям на базе классической логики первого порядка? Или ты в самом деле всерьез пробовал и то и то и считаешь, что Coq удобнее в использование?
>>10547
Я сам сколь-нибудь всерьез не занимался формализацией доказательств в таких системах. Но из общих соображений я бы предположил, что тебе Mizar больше подходит. Coq - это система на основе Calculus of Inductive Constructions, который является вариантом интуиционистской теории типов. И формализацию математики, насколько я понимаю, они в норме делают именно за счет средств Cic, а не погружая в него теорию множеств и формализуя математику в этом погружение. В Mizar-е, насколько я понимаю ситуацию, напротив в норме используют более классический подход к формализации математики - Mizar проверяет доказательства в логике первого порядка, а стандартная библиотека сделана на основе теории множеств (ZFC + аксиома вселенных Гротендика). Судя по тому, что в Mizar-е уже очень много чего формализовано, думаю что пользоваться им в худшем случае не сильно более неудобно, чем Coq. В тоже время, Mizar ориентирован на случая гораздо более похожий на твой (формализацию доказательств в NGB).
>>10586
я это заявляю, потому что coq в 1000 раз популярнее и на нем уже все реализовали, сиди да и пользуйся.
>Это ты заявляешь из идеологических соображений - предпочитая интуиционистскую теорию типов построениям на базе классической логики первого порядка
я это заявляю, потому что coq в 1000 раз популярнее и на нем уже все реализовали, сиди да и пользуйся.
>>10598
Это, очевидно, не так. Например, в этом рейтинге по числу формализованных теорем он его просто обгоняет http://www.cs.ru.nl/~freek/100/ .
>в 1000 раз популярнее
Это, очевидно, не так. Например, в этом рейтинге по числу формализованных теорем он его просто обгоняет http://www.cs.ru.nl/~freek/100/ .
>>10598
А ничего, что там MLTT вместо логики первого порядка, и реализуя NBG поверх MLTT, ты занимаешься чем-то уровня натягивания совы на глобус?
>coq в 1000 раз популярнее
А ничего, что там MLTT вместо логики первого порядка, и реализуя NBG поверх MLTT, ты занимаешься чем-то уровня натягивания совы на глобус?
>>10600
хуйню несешь.
https://en.wikipedia.org/wiki/Calculus_of_constructions
https://coq.inria.fr/distrib/current/refman/Reference-Manual006.html
>>10599
зато по количеству кода на github, статей на arxiv.org и доказанных серьезных теорем coq уделывает эту поделку на паскале. В Coq даже есть mizar mode, настолько он развит.
>А ничего, что там MLTT вместо логики первого порядка
хуйню несешь.
https://en.wikipedia.org/wiki/Calculus_of_constructions
https://coq.inria.fr/distrib/current/refman/Reference-Manual006.html
>>10599
зато по количеству кода на github, статей на arxiv.org и доказанных серьезных теорем coq уделывает эту поделку на паскале. В Coq даже есть mizar mode, настолько он развит.
>>10603
Не проверял, вполне допускаю что правда несколько больше. Но если бы Coq был именно несравненно более популярен (что ты, фактически, пытался утверждать), чем Mizar, то он бы опережал везде и всегда. А если нет решительного перевеса по популярности, то адекватно выбирать инструмент более подходящий для конкретной цели.
>зато по количеству кода на github, статей на arxiv.org и доказанных серьезных теорем coq уделывает эту поделку на паскале
Не проверял, вполне допускаю что правда несколько больше. Но если бы Coq был именно несравненно более популярен (что ты, фактически, пытался утверждать), чем Mizar, то он бы опережал везде и всегда. А если нет решительного перевеса по популярности, то адекватно выбирать инструмент более подходящий для конкретной цели.
>>10606
Не уверен, но предполагаю, что mizar занимает лидирующую позицию по количеству теорем, так как именно близкая к ним тусовка начала https://en.wikipedia.org/wiki/QED_manifesto ?
Coq _выглядит_ более презентабельно по многим критериям.
И множества и классы - часть MLTT.
Натягивание совы на шар может пригодиться для построения модели NBG-теории в чём-то другом (для учебных целей онли). Да в том же MLTT/HoTT, положив 1-truncated типы как U в Ensembles (оно же - Var у меня). (Только предполагаю, офк)
На данную тему нужна серия лекций специалиста.
Не уверен, но предполагаю, что mizar занимает лидирующую позицию по количеству теорем, так как именно близкая к ним тусовка начала https://en.wikipedia.org/wiki/QED_manifesto ?
Coq _выглядит_ более презентабельно по многим критериям.
И множества и классы - часть MLTT.
Натягивание совы на шар может пригодиться для построения модели NBG-теории в чём-то другом (для учебных целей онли). Да в том же MLTT/HoTT, положив 1-truncated типы как U в Ensembles (оно же - Var у меня). (Только предполагаю, офк)
На данную тему нужна серия лекций специалиста.
p.s. честно говоря, не сильно яснее стало, что надо предпочесть Mizar, Coq или что-то ещё (почему бы не Isabelle?), придётся пробовать наудачу. В любом случае, спасибо за мнения, аноны.
>>10610
1) наличие на github
2) использование его авторами HoTT и серьезных теорем
3) наличие многих инструментов, экспорта в haskell
Мне кажется выбор стоит скорее между Coq и менее удобным, но переспективным Agda, чем между Coq и чем-то другим.
>Coq _выглядит_ более презентабельно по многим критериям.
1) наличие на github
2) использование его авторами HoTT и серьезных теорем
3) наличие многих инструментов, экспорта в haskell
Мне кажется выбор стоит скорее между Coq и менее удобным, но переспективным Agda, чем между Coq и чем-то другим.
10/10, мне вспомнился Джет Ли в костюме петуха
265 Кб, 600x849>>9895 (OP)
Посвежее есть что-нибудь с NBG? Пусть даже на английском.
Я просто чувствителен к качеству pdf-учебника, не могу в сканы.
А так бы попробовал прорешать что-нибудь по основаниям, всё хочу их осилить, но пока даже в ZFC строго не разобрался.
И тоже попробую верифицировать, только не в Coq, а в Agda, там синтаксис няшный.
>Mendelson Elliott: Introduction to Mathematical Logic
Посвежее есть что-нибудь с NBG? Пусть даже на английском.
Я просто чувствителен к качеству pdf-учебника, не могу в сканы.
А так бы попробовал прорешать что-нибудь по основаниям, всё хочу их осилить, но пока даже в ZFC строго не разобрался.
И тоже попробую верифицировать, только не в Coq, а в Agda, там синтаксис няшный.
686 Кб, 500x555Вот свежее (6-е), не шакальное издание того же учебника, что в ОП-посте:
https://my.mixtape.moe/tpcyzr.pdf
Жаль рашкинские издатели до сих пор не начали продавать электронные версии учебников, чтобы их можно было пиздить в нормальном качестве.
Так-то 4-е издание переводили, но в интернетах только шакальные сканы 2-го.
Блджад, как же плохо без уверенного инглиша.
https://my.mixtape.moe/tpcyzr.pdf
Жаль рашкинские издатели до сих пор не начали продавать электронные версии учебников, чтобы их можно было пиздить в нормальном качестве.
Так-то 4-е издание переводили, но в интернетах только шакальные сканы 2-го.
Блджад, как же плохо без уверенного инглиша.
>>10737
Не понимаю я вот такого школьничества и никогда не понимал. Посвежее, блядь. Как будто в NBG что-то изменилось со времен фон Неймана, Геделя и Бернайса, а в ZFC - со времен Цермело с Френкелем.
>Посвежее есть что-нибудь с NBG?
Не понимаю я вот такого школьничества и никогда не понимал. Посвежее, блядь. Как будто в NBG что-то изменилось со времен фон Неймана, Геделя и Бернайса, а в ZFC - со времен Цермело с Френкелем.
а на русише чо почитать?
>>9895 (OP)
А кто бабу не драл - не мужик.
А кто бабу не драл - не мужик.
>>10737
Есть 6th edition, в хорошем качестве, pdf, не скан. В самом вехнем посте ссылка на него.
Есть 6th edition, в хорошем качестве, pdf, не скан. В самом вехнем посте ссылка на него.
36 Кб, 400x366Ух, только заметил что я ебанулся на отличненько и учебник который я "доставил" в >>10738
и был в ОП-посте. Видимо я просмотрел >>9918 и почему-то думал что это он там был.
>>10740
Ты мой пост плохо понял?
Меня устраивают старые учебники содержательно.
Меня не устраивают электронные версии старых (изданий) учебников тем что они обычно представлены в виде хуёвых сканов. И нотация там иногда раздражает, вроде ⊃ в качестве импликации.
>>10758
Нет, не сидел там. Неприятное место, мало отличается от какого-нибудь /fag/
и был в ОП-посте. Видимо я просмотрел >>9918 и почему-то думал что это он там был.
>>10740
Ты мой пост плохо понял?
Меня устраивают старые учебники содержательно.
Меня не устраивают электронные версии старых (изданий) учебников тем что они обычно представлены в виде хуёвых сканов. И нотация там иногда раздражает, вроде ⊃ в качестве импликации.
>>10758
Нет, не сидел там. Неприятное место, мало отличается от какого-нибудь /fag/
>>10790
Но отношение подмножества в теории множеств это и есть импликация в логике. Так даже понятнее суть происходящего, чем какие-то стрелочки.
>вроде ⊃ в качестве импликации.
Но отношение подмножества в теории множеств это и есть импликация в логике. Так даже понятнее суть происходящего, чем какие-то стрелочки.
>>10794
А ты точно все учебники и на всех языках мира с 60-х перечитал?
А ты точно все учебники и на всех языках мира с 60-х перечитал?
90 Кб, 677x558Выписал сотню утверждений, часть доказал.
https://goo.gl/WViV5e
Модеру: давай сделаем этот тред модерируемым/тематическим - добавим в шапку ссылку "Мендельсона тред".
https://goo.gl/WViV5e
Модеру: давай сделаем этот тред модерируемым/тематическим - добавим в шапку ссылку "Мендельсона тред".
>>13225
>>9895 (OP)
По отзыву одного профессионального логика, у Мендельсона - лучшее изложение NBG.
(Опечатки, разумеется, есть, но нет небрежных выводов.)
>>9895 (OP)
По отзыву одного профессионального логика, у Мендельсона - лучшее изложение NBG.
(Опечатки, разумеется, есть, но нет небрежных выводов.)
>>9895 (OP)
>>19319 (OP)
Почему ты выбрал Metamath, а не Mizar? Только из-за живого коммьюнити? Мне вот ещё приглянулся Isabelle, кто-нибудь тут пользуется им? Стоит ли вообще останавливаться на Metamath/Mizar/Isabelle/etc? Может сразу использовать Coq? Вроде в Coq ZFC очень неестественным образом реализована — это меня смущает. Но правильно ли я понимаю, что для серьёзной математики больше подходит Coq, нежели ассистанты на простой теории типов/теории множеств?
>>19319 (OP)
Почему ты выбрал Metamath, а не Mizar? Только из-за живого коммьюнити? Мне вот ещё приглянулся Isabelle, кто-нибудь тут пользуется им? Стоит ли вообще останавливаться на Metamath/Mizar/Isabelle/etc? Может сразу использовать Coq? Вроде в Coq ZFC очень неестественным образом реализована — это меня смущает. Но правильно ли я понимаю, что для серьёзной математики больше подходит Coq, нежели ассистанты на простой теории типов/теории множеств?
>>9895 (OP)
А по моему скромному мнению, ты мудак
Будет он ещё решать, что я должен уметь, а что нет. Плюю тебе в твоё тупое ебало
>По моему скромному разумению - уметь решать эти задачи максимально чётко должен уметь всякий уважающий себя математик, и неважно в какой сфере он работает.
А по моему скромному мнению, ты мудак
Будет он ещё решать, что я должен уметь, а что нет. Плюю тебе в твоё тупое ебало
>>9939
Так ты не пустые рассматривай)0
Так ты не пустые рассматривай)0