AC
Так у Вас очень быстро окажется противоречивый набор аксиом. 😉
Size: a a a
Типы в языках программирования, моделирования, представления знаний и жизни
505 membersпожаловаться на группу
2021 November 23
AB
ПС
Ну, я плохо перефразировал тезис из лирического отступления в этом блогопосте
http://math.andrej.com/2021/05/18/computing-an-integer-using-a-sheaf-topos/
http://math.andrej.com/2021/05/18/computing-an-integer-using-a-sheaf-topos/
E
возьмем конечные геометрии в качестве примера. и аксиму 1: любые две прямые либо не пересекаются, либо пересекаются ровно в одной точке. добавим аксиому 2: любые две прямые пересекаются ровно в одной точке. это две разных геометрии, и обе непротиворечивы
AC
Аксиома 1 же поглощает (subsumes) аксиому 2 — или я не понял что Вы имеете в виду?
ПС
(Со мной обсуждать результаты статьи бесполезно, я за топосы не шарю, извините)
E
аксиома 2 сильнее аксиомы 1
AC
Да, именно это и значит, что 1 поглощает 2. 😊
2 implies 1E
ну можно вторую аксиому сделать: любые две прямые пересекаются, и тогда не будет поглащения, а суть та же
AC
А можно первую аксиому разбить на две: 1а) любые две прямые либо пересекаются, либо нет; 1б) если две прямые пересекаются, то только в одной точке. Тогда окажется, что 1а) — первое, является инстанцированием LEM, и второе — поглощает модифицированную вторую аксиому. 😊
В общем, Вы приводите пример когда мы усиливаем (сужаем) теорию введением новой аксиомы. Мне просто пока не очевидно, что это доказывает.
В общем, Вы приводите пример когда мы усиливаем (сужаем) теорию введением новой аксиомы. Мне просто пока не очевидно, что это доказывает.
E
доказывает, что с введением новых аксиом прежние теоремы могут оказаться неверны
E
то есть "мешают", даже в непротиворечивых системах
AC
Приведите пример, пожалуйста? Я с ходу не могу придумать.
E
теорема, что через точку вне прямой можно провести параллельную прямую -- в евклидовой геометрии верна (аксиома 1), а в проективной нет (аксиома 1+2)
K
Так это не аксиома, а метрика пространства
DK
смотрю отсюда, вроде адекватный вариант
https://henrychern.wordpress.com/2017/11/03/гомотопическая-теория-типов/
https://henrychern.wordpress.com/2017/11/03/гомотопическая-теория-типов/
E
конечные геометрии вообще без метрики живут
K
Ну, 5 аксиома геометрии рушится, когда пространство искривлено.
K
Я имел ввиду кривизну