(Это связано с основаниями математики, но не спешите отчаиваться)
В данном треде я постараюсь ответить на все возникшие у анонов вопросы. Его вроде надо сделать модерируемым.
FAQ:
1)Что это?
Это теория типов для формального доказательств первопорядковых языков. Ну то есть язык программирования для ZFC, NBG, геометрии (Тарского) и ещё много чего первопорядкового.
Всё это доступно онлайн в удобном гипертекстовом виде.
2)Какие профиты?
а) Очень большая библиотека доказательств, легко читается. Имеет достаточно долгую историю - с девяностых.
б) Пруфассистант: два режима, как в Coq: либо конструируешь доказательство, либо интерактивный режим.
в) Непосредственно прилагается самоучитель.
г) Простой (300 строк на питоне) верификатор доказательств.
д) Имеет модель в ZFC. (самая мякотка, смотри пункт 3)
е) Живое коммьюнити.
3) Какие задачи?
Есть такая статья: http://us.metamath.org/ocat/model/model.pdf
Не знаю как анону, но мне было бы очень любопытно в ней разобраться.
4) Почему "лучше" чем HoTT, Coq, HOL и т.д.?
Да потому что ZFC и логика предикатов - это математический стандарт де-факто, поэтому знание metamath может помочь вам понимать беглую речь преподавателей в институте. (А не страдать по крайностям "это очевидно" и "ничерта не понятно".)
Смело задавайте вопросы и высказывайте мнения.
> знание metamath может помочь вам понимать беглую речь преподавателей в институте
Ну а что, предикат калкулус для того и нужен, чтобы понимать логические переходы.
4ый пункт улыбнул. Я тебе даже поясню, в чем ты не прав:
1) вот смотри, 1ый вариант куба Барендрегта это типизированные лямбда-исчисления, связанные между собой отношением включения (т.е. правый верхний дальний угол - самый упакованный вариант, он соответствует CoC, calculus of construction, это исчисление является основой Кока).
2) 2ой куб - соответствующие первому логические системы, которые представимы в соответствующей лямбде из 1го куба. Первичная логика предикатов соответствует правому нижнему переднему углу куба и т.о. лямбда-Р исчислению, предложенному независимо де Брауном и Говардом, в нем выразим т.н. изоморфизм Карри-Говарда.
3) из вышесказанного очевидно, что исчисление предикатов и ZFC легко и просто выразимо в Коке, ценители могут даже исключенное третье использовать. Собственно, ZFC в Коке давно есть https://github.com/coq-contribs/zfc
Посмотрел по диагонали статью http://us.metamath.org/ocat/model/model.pdf синтаксис этого прувера (пик1) напоминает AUTOMATH де Брауна (пики 2 и 3). Для подобных языков лямбда - то что доктор прописал, что-то лучше и проще придумать нереально.
>синтаксис этого прувера (пик1) напоминает AUTOMATH де Брауна
Добавлю, что с той разницей, что де Браун не ограничивал себя какой-то конкретной логической системой.
1) И где сейчас AUTOMATH? Почему он не используется широко?(риторический вопрос)
2) Какое средство верификации всяких домашек на доказательство теорем, по-твоему, следует использовать? А то с этим проблемы постоянно.
Моя цель - проверка домашек на доказательство. (Без стогости формальной системы - беда, плыву). ДЗ - из всяких классических учебников типа Зорича, Шеня, Шварца и т.д.
Что лучше всего использовать, чтобы быть уверенным в истинности своих утверждений?
Множества, в том же Coq - искуственно сконструированы в Ensembles чёрт ногу сломит и нет обширной библиотеки.
HoTT - слишком инновационно и никто другой не будет понимать.
Mizar - выглядит подозрительно, не разбирался в нём.
Metamath - вроде ОК же, разве не лучший вариант?
Что взамен предлагаешь? (Буду признателен.)
>И где сейчас AUTOMATH? Почему он не используется широко?(риторический вопрос)
Да нет, не риторический. Причина в том, что там слишком много ручной работы, перевести книгу в этот формат это очень трудозатратно, на примере Grundlagen Ландау можно увидеть, что это пиздецки тяжелый труд. https://www.cs.ru.nl/~freek/aut/
>Какое средство верификации всяких домашек на доказательство теорем, по-твоему, следует использовать? А то с этим проблемы постоянно.
Кок жи. Единственный нормальный кроссплатформенный прувер с человеческим лицом, годящийся для всего от домашек до сколь угодно серьезной математики.
Метаматематика - не математика, а бесплодная мастурбация. И этим всё сказано.
> http://us.metamath.org/index.html
> A Java applet that demonstrates simple proofs.
Эх, вернул себе свой 1996!..
Выглядит как-то заброшено. Неудивительно, что все кок вместо этого советуют. Но тебе же не статьи на нем писать, тебе надо свою вполне конкретную задачу решить, так что не вижу смысла тебе следовать этим советам. К тому же когда надо будет - перекатишься без проблем: все-таки между любыми двумя пруферами гэп намного меньше, чем между пруфером и доказательствами на бумаге.
Кстати, а что с мендельсонотредом? Забросил или не взлетел?
Чем больше я думаю по этому поводу, тем больше мне кажется, что математика определяется основополагающими принципами и источниками человеческого разума, на стыке их производной в виде рассудочной деятельности и той части реальности, которая доступна для познания через органы чувств.
Математика - это заложенный самим Богом способ более глубокого, чем обыденное, познания окружающей действительности. Или случайно образованное продолжение обычного языка, расширенного для мышления отвлеченных, но естественным образом ставшими полезными/подвластными человеку свойств чувственно наблюдаемых объектов.
Во! Математика это короче духовность, а вы со своим онанизмом и бездушными вычислениями на мертвых машинах всё портите! DEUS VULT!
Ага, двачую, только я вот стыжусь почему-то об этом писать.
>Чем больше я думаю по этому поводу, тем больше мне кажется, что математика определяется основополагающими принципами и источниками человеческого разума, на стыке их производной в виде рассудочной деятельности и той части реальности, которая доступна для познания через органы чувств.
Было уже. Причем, подобные взгляды довольно подробно были разобраны Кантом, Брауэром, Маннури. Вот только они ничем не отличаются от бездушных вычислений, это как в той притче про слона и слепых. Один описывает уши, другой залупу. Поэтому описания фундаментально разные. А сам слон при этом один.
Разумеется, я лишь merely компиляю-пересказываю того же Канта.
>слон
Так говоришь, будто ты со стороны видишь всю математику, и подшучиваешь над слепцами, которые то доказывают что-то с помощью ЭВМ, то рассуждают интуитивно.
Но это наверняка не так, и вполне уместен вопрос: а имеет ли смысл говорить о «слоне» вообще?
>>19371
>Стыд
Самое глупое из человеческих чувств.
> Так говоришь, будто ты со стороны видишь всю математику, и подшучиваешь над слепцами, которые то доказывают что-то с помощью ЭВМ, то рассуждают интуитивно.
> Но это наверняка не так, и вполне уместен вопрос: а имеет ли смысл говорить о «слоне» вообщ
Я как раз думаю, что нашел нечто интересное, позволяющее связать эти подходы. Нет, не узоры с разрывами.
>Самое глупое из человеческих чувств.
Ну это интимное ведь, ты же голым не ходишь по улице.
Я переключился на библиотеку ZFC в Metamath. NBG тоже вполне можно лаконично на метамаф реализовывать. (пока нет такой задачи, не нужно)
Встроенный пруфассистант не сильно удобен в силу совместимости и возраста, однако наловчиться вполне можно.
Но простота базовых принципов - подкупает.
В целом - потрясающей красоты вещь, я в восторге.
Безусловно, за каким-нибудь hott-ом - будущее, но, для понимания уже существующей математики и математиков, метамаф - хороший инструмент для самообучения.
про пункт 3)
да, выразимо.
Но теорию стоящую за коком тоже надо как-то обосновать. В чём-то простом.
Как раз metamath подходит.
Ого, тред еще живой.
> теорию стоящую за коком тоже надо как-то обосновать. В чём-то простом.
Лямбда же. Ну и изоморфизм Карри-Говарда. В конечном счёте все обоснование упирается в вычислимость. Как и MLTT.
Если ты из Москвы, то давай увидимся в НМУ 20го января в 13:00 ? Там книжный хороший, тебе понравится, как раз туда собираюсь.
>Математика - это заложенный самим Богом способ более глубокого, чем обыденное, познания окружающей действительности.
Вы сильно преувеличиваете. Математика — это просто описание некоторых аспектов реальности, вот и всё. Нет никакого "более глубокого" познания. Всё познание одинаковое.
тред же про метамаф... не надо тут, я хотел бы, чтобы последним постом было следующее заключение:
1) там очень сомнительная и некрасивая теория типов.
2) Язык слишком бедный
3) В такого рода системах можно легко нарваться на противоречие. ( из-за того, что там замены без нормального вывода типа)
4) Морока с "различностью переменных" - излишняя грузящая синтаксис вещь.
Поэтому пусть этот тред утонет: есть куда более красивые и полезные аналогичные классические вещи - элементарные теории первого порядка.
ОП