Математика

Тред закрыт.

Check this out!
Metamath Аноним 28/05/17 Вск 16:43:32 193191
800px-AdolfAbra[...].jpg 132Кб, 800x1122
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 может помочь вам понимать беглую речь преподавателей в институте. (А не страдать по крайностям "это очевидно" и "ничерта не понятно".)

Смело задавайте вопросы и высказывайте мнения.
Аноним 28/05/17 Вск 19:49:00 193382
PeMT7qdw.png 127Кб, 512x382
512x382
>>19319 (OP)
> знание metamath может помочь вам понимать беглую речь преподавателей в институте
Аноним 28/05/17 Вск 20:05:51 193403
>>19338
Ну а что, предикат калкулус для того и нужен, чтобы понимать логические переходы.
харе лямбда, харе барендрехт Аноним 29/05/17 Пнд 13:40:47 193554
Снимок.PNG 20Кб, 524x437
524x437
Снимок1.PNG 26Кб, 562x448
562x448
ZFC.png 246Кб, 736x732
736x732
>>19319 (OP)
4ый пункт улыбнул. Я тебе даже поясню, в чем ты не прав:
1) вот смотри, 1ый вариант куба Барендрегта это типизированные лямбда-исчисления, связанные между собой отношением включения (т.е. правый верхний дальний угол - самый упакованный вариант, он соответствует CoC, calculus of construction, это исчисление является основой Кока).
2) 2ой куб - соответствующие первому логические системы, которые представимы в соответствующей лямбде из 1го куба. Первичная логика предикатов соответствует правому нижнему переднему углу куба и т.о. лямбда-Р исчислению, предложенному независимо де Брауном и Говардом, в нем выразим т.н. изоморфизм Карри-Говарда.
3) из вышесказанного очевидно, что исчисление предикатов и ZFC легко и просто выразимо в Коке, ценители могут даже исключенное третье использовать. Собственно, ZFC в Коке давно есть https://github.com/coq-contribs/zfc
Аноним 29/05/17 Пнд 14:18:18 193565
Снимок.PNG 57Кб, 706x565
706x565
Снимок1.PNG 119Кб, 809x708
809x708
Снимок2.PNG 21Кб, 442x270
442x270
>>19319 (OP)
Посмотрел по диагонали статью http://us.metamath.org/ocat/model/model.pdf синтаксис этого прувера (пик1) напоминает AUTOMATH де Брауна (пики 2 и 3). Для подобных языков лямбда - то что доктор прописал, что-то лучше и проще придумать нереально.
Аноним 29/05/17 Пнд 14:26:05 193576
Снимок.PNG 72Кб, 870x293
870x293
>>19356
>синтаксис этого прувера (пик1) напоминает AUTOMATH де Брауна
Добавлю, что с той разницей, что де Браун не ограничивал себя какой-то конкретной логической системой.
Аноним 29/05/17 Пнд 19:06:50 193597
>>19357
1) И где сейчас AUTOMATH? Почему он не используется широко?(риторический вопрос)
2) Какое средство верификации всяких домашек на доказательство теорем, по-твоему, следует использовать? А то с этим проблемы постоянно.

Моя цель - проверка домашек на доказательство. (Без стогости формальной системы - беда, плыву). ДЗ - из всяких классических учебников типа Зорича, Шеня, Шварца и т.д.
Что лучше всего использовать, чтобы быть уверенным в истинности своих утверждений?

Множества, в том же Coq - искуственно сконструированы в Ensembles чёрт ногу сломит и нет обширной библиотеки.

HoTT - слишком инновационно и никто другой не будет понимать.

Mizar - выглядит подозрительно, не разбирался в нём.

Metamath - вроде ОК же, разве не лучший вариант?
Что взамен предлагаешь? (Буду признателен.)

Аноним 29/05/17 Пнд 20:45:28 193628
>>19359
>И где сейчас AUTOMATH? Почему он не используется широко?(риторический вопрос)
Да нет, не риторический. Причина в том, что там слишком много ручной работы, перевести книгу в этот формат это очень трудозатратно, на примере Grundlagen Ландау можно увидеть, что это пиздецки тяжелый труд. https://www.cs.ru.nl/~freek/aut/
>Какое средство верификации всяких домашек на доказательство теорем, по-твоему, следует использовать? А то с этим проблемы постоянно.
Кок жи. Единственный нормальный кроссплатформенный прувер с человеческим лицом, годящийся для всего от домашек до сколь угодно серьезной математики.
Аноним 29/05/17 Пнд 21:03:06 193649
Я вот думаю, что вы, господа, занимаетесь формализмом, логикой, онанизмом - в общем, чем угодно, только не реальной математикой.
Метаматематика - не математика, а бесплодная мастурбация. И этим всё сказано.
Аноним 29/05/17 Пнд 21:24:04 1936610
>>19319 (OP)
> http://us.metamath.org/index.html
> A Java applet that demonstrates simple proofs.
Эх, вернул себе свой 1996!..

Выглядит как-то заброшено. Неудивительно, что все кок вместо этого советуют. Но тебе же не статьи на нем писать, тебе надо свою вполне конкретную задачу решить, так что не вижу смысла тебе следовать этим советам. К тому же когда надо будет - перекатишься без проблем: все-таки между любыми двумя пруферами гэп намного меньше, чем между пруфером и доказательствами на бумаге.

Кстати, а что с мендельсонотредом? Забросил или не взлетел?
Аноним 29/05/17 Пнд 21:26:31 1936711
>>19364
А математика тогда что?
Аноним 29/05/17 Пнд 23:26:54 1936812
>>19367
Чем больше я думаю по этому поводу, тем больше мне кажется, что математика определяется основополагающими принципами и источниками человеческого разума, на стыке их производной в виде рассудочной деятельности и той части реальности, которая доступна для познания через органы чувств.

Математика - это заложенный самим Богом способ более глубокого, чем обыденное, познания окружающей действительности. Или случайно образованное продолжение обычного языка, расширенного для мышления отвлеченных, но естественным образом ставшими полезными/подвластными человеку свойств чувственно наблюдаемых объектов.

Во! Математика это короче духовность, а вы со своим онанизмом и бездушными вычислениями на мертвых машинах всё портите! DEUS VULT!
Аноним 30/05/17 Втр 01:08:03 1937113
>>19368
Ага, двачую, только я вот стыжусь почему-то об этом писать.
Аноним 30/05/17 Втр 10:54:21 1937714
elephantpic.jpg 71Кб, 590x374
590x374
>>19368
>Чем больше я думаю по этому поводу, тем больше мне кажется, что математика определяется основополагающими принципами и источниками человеческого разума, на стыке их производной в виде рассудочной деятельности и той части реальности, которая доступна для познания через органы чувств.
Было уже. Причем, подобные взгляды довольно подробно были разобраны Кантом, Брауэром, Маннури. Вот только они ничем не отличаются от бездушных вычислений, это как в той притче про слона и слепых. Один описывает уши, другой залупу. Поэтому описания фундаментально разные. А сам слон при этом один.
Аноним 30/05/17 Втр 15:07:47 1938715
>>19371
И правильно делаешь
Аноним 31/05/17 Срд 00:31:05 1940516
>>19377
Разумеется, я лишь merely компиляю-пересказываю того же Канта.
>слон
Так говоришь, будто ты со стороны видишь всю математику, и подшучиваешь над слепцами, которые то доказывают что-то с помощью ЭВМ, то рассуждают интуитивно.
Но это наверняка не так, и вполне уместен вопрос: а имеет ли смысл говорить о «слоне» вообще?

>>19371
>Стыд
Самое глупое из человеческих чувств.
Аноним 31/05/17 Срд 16:19:21 1945317
>>19405
> Так говоришь, будто ты со стороны видишь всю математику, и подшучиваешь над слепцами, которые то доказывают что-то с помощью ЭВМ, то рассуждают интуитивно.
> Но это наверняка не так, и вполне уместен вопрос: а имеет ли смысл говорить о «слоне» вообщ
Я как раз думаю, что нашел нечто интересное, позволяющее связать эти подходы. Нет, не узоры с разрывами.
Аноним 01/06/17 Чтв 18:00:10 1953418
>>19405
>Самое глупое из человеческих чувств.
Ну это интимное ведь, ты же голым не ходишь по улице.
Аноним 02/06/17 Птн 10:35:42 1958119
>>19366

Я переключился на библиотеку ZFC в Metamath. NBG тоже вполне можно лаконично на метамаф реализовывать. (пока нет такой задачи, не нужно)

Встроенный пруфассистант не сильно удобен в силу совместимости и возраста, однако наловчиться вполне можно.
Но простота базовых принципов - подкупает.

В целом - потрясающей красоты вещь, я в восторге.

Безусловно, за каким-нибудь hott-ом - будущее, но, для понимания уже существующей математики и математиков, метамаф - хороший инструмент для самообучения.
Аноним 16/01/18 Втр 02:30:18 3499020
>>19355

про пункт 3)
да, выразимо.
Но теорию стоящую за коком тоже надо как-то обосновать. В чём-то простом.
Как раз metamath подходит.
Аноним 16/01/18 Втр 06:53:48 3499421
Аноним 16/01/18 Втр 22:23:15 3514422
>>34990
> теорию стоящую за коком тоже надо как-то обосновать. В чём-то простом.
Лямбда же. Ну и изоморфизм Карри-Говарда. В конечном счёте все обоснование упирается в вычислимость. Как и MLTT.
Аноним 17/01/18 Срд 13:44:57 3517723
>>35144
Если ты из Москвы, то давай увидимся в НМУ 20го января в 13:00 ? Там книжный хороший, тебе понравится, как раз туда собираюсь.
Аноним 26/06/18 Втр 21:31:47 4102524
>>19368
>Математика - это заложенный самим Богом способ более глубокого, чем обыденное, познания окружающей действительности.
Вы сильно преувеличиваете. Математика — это просто описание некоторых аспектов реальности, вот и всё. Нет никакого "более глубокого" познания. Всё познание одинаковое.
Аноним 26/06/18 Втр 22:33:56 4103225
>>41025
пиздец ты некрофил
27/06/18 Срд 11:11:38 4103826
>>41025
тред же про метамаф... не надо тут, я хотел бы, чтобы последним постом было следующее заключение:

1) там очень сомнительная и некрасивая теория типов.
2) Язык слишком бедный
3) В такого рода системах можно легко нарваться на противоречие. ( из-за того, что там замены без нормального вывода типа)
4) Морока с "различностью переменных" - излишняя грузящая синтаксис вещь.

Поэтому пусть этот тред утонет: есть куда более красивые и полезные аналогичные классические вещи - элементарные теории первого порядка.

ОП
Настройки X
Стикеры X
Избранное / Топ тредов