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