E
я про геометрии как множество точек, множество прямых из них, и аксиомы про них.
Size: a a a
Типы в языках программирования, моделирования, представления знаний и жизни
505 membersпожаловаться на группу
2021 November 23
E
такой игрушечный пример для формальных систем
E
типа геометрия из 16 точек и 8 прямых
K
Про такие геометрии я ничего не знаю, так что заберу слова про кривизну назад
AC
Значит, если мы оставим обе аксиомы, то теория окажется противоречивой. Это не является контрпримером к изначальному утверждению. 😊
E
она непротиворечива, потому что сцществуют модели для нее – проективная плоскость
[
Линейные типы это, проводя аналогию со стековым языком, когда запрещены операции dup и drop
AC
Там же указано, что это перевод the HoTT book. Если перевод хотя бы адекватный — то "вранья" там, конечно, не будет.
AC
Я не сомневаюсь, что проективная геометрия сама по себе непротиворечива. Я указываю на то, что оставив аксиому 1 и просто добавив аксиому 2 Вы получаете противоречивую теорию. Видимо, проективная геометрия строится не так. 😊
E
да нет там противоречая
E
первая аксиома утверждает что есть один из двух вариантов, вторая оставляет только один
E
иногда надо спускаться с абстрактных вершин до простых конкретных примеров ))
AC
Если из подмножества аксиом мы можем вывести утверждение, которое противоречит другой аксиоме, то система аксиом противоречива — по-моему, так. 🤷♀️
E
но ведь нет, и вот пример. конкретный.
AB
аксиома1: x=1
аксиома2: x=1 or x=2
аксиома2: x=1 or x=2
E
только с геометриями пример содержательный, потому что и там, и там развитая теория: классическая геометрия и проективная геометрия.
AC
Пойдём спросим Brenoritvrezorkre? 😁
AC
В https://ru.wikipedia.org/wiki/%D0%9F%D1%80%D0%BE%D0%B5%D0%BA%D1%82%D0%B8%D0%B2%D0%BD%D0%B0%D1%8F_%D0%B3%D0%B5%D0%BE%D0%BC%D0%B5%D1%82%D1%80%D0%B8%D1%8F
проективная геометрия определяется с аксиомой 2, но без аксиомы 1, как я и предполагал. 🤷♀️
проективная геометрия определяется с аксиомой 2, но без аксиомы 1, как я и предполагал. 🤷♀️
E
но аксиома1 логически не мешает аксиоме2, то есть не создает противоречия