2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему
 
 ZFC in Coq, Jech's "Set Theory"
Сообщение19.01.2019, 13:58 


26/11/13
29
Предлагаю Вашему вниманию и обсуждению вот этот код для Coq. (it's self-contained, the standard library was only used.)
https://raw.githubusercontent.com/georg ... ter/Jech.v
Это сильно переделанный(как мне кажется, в лучшую сторону) и обильно дополненный вот этот репозиторий https://github.com/coq-contribs/zfc .

Если у Воеводского были "Унивалентные основания математики" на Coq-e, то почему бы не воплощать в коде "Классические основания математики"? :)

Да, из теоретико-множественного есть Metamath ( http://us.metamath.org/ ), есть Mizar ( http://mizar.org/ ).
Первый - сложен в обращении, написан на С++, некоторые знакомые логики говорят, что система не очень хорошая(точную их аргументацию не воспроизведу). Второй - просто мне не знаком.
Прорешенный первые главы Йеха есть в интернете. https://github.com/coq-contribs/zfc .
Деятельность, конечно, немного сектантская, но очень увлекательная и даже полезная. (многие, например, вообще не знают, чем отличаются, множества, классы, конгломераты,... и как с ними работать.)

p.s. есть слух, что где-то кто-то переводит Йеха на русский язык.

 Профиль  
                  
 
 Re: ZFC in Coq, Jech's "Set Theory"
Сообщение24.02.2019, 13:27 
Заслуженный участник


31/12/15
922
Это какой-то другой Йех?
http://lib1.org/_ads/3D3C0284720E62361EAC0D8B08E78BE8

 Профиль  
                  
 
 Re: ZFC in Coq, Jech's "Set Theory"
Сообщение24.02.2019, 21:17 
Заслуженный участник


15/05/05
3445
USA
george66 в сообщении #1378072 писал(а):
Это какой-то другой Йех?
http://lib1.org/_ads/3D3C0284720E62361EAC0D8B08E78BE8
ТС в своем коде ссылается на другую, более новую книгу: "Set Theory".(T.Jech, 2003)

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 3 ] 

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group