> Для конструирования моделей используется теория множеств, точнее два семейства теорий множеств
Любопытно, а почему не теоркат или какой-то из вариантов теории типов? И почему именно эта аксиоматика, а не NBD например? Так просто привычнее или ZFC(n)/CZF(n) позволяют получить результаты, принципиально недостижимые с помощью теории типов и проч.?
1) Потому что для конструирования моделей сперва используются теории, в которых все уверены и сила которых откалибрована за многие десятилетия. И уже потом можно для других целей использовать другие теории.
2) Почему NBG, а не ZFC? На самом деле NBG консервативна относительно ZFC, так что это “та же” аксиоматика.
3) Конструирование моделей внутри самих теорий типов - отдельная отросль, и собственно модель кубической теории типов BCH была (на языке NuPRL) построена в экстенциональной теории типов. Ну и сейчас несколько групп независимо ведёт работу по такому общему фреймворку, чтобы было удобно строить модели самых разных теорий типов в рамках некоторой удобной фиксированной теории типов (по выразительности между HoTTMin и HoTTMax(1)), и доказывать с комфортом всякие их свойства. Вот самый сок: http://www.cs.cmu.edu/~cangiuli/papers/xtt.pdf... )
Большой спасибо за ссылки. А есть некий обзор/ликбез современного состояния теорий типов (зависимые, экстенсиональные, кубические, интенсиональные...) и того, как они применяются (Coq, Agda, NuPRL, RedPRL...)?
В стародавние времена у нас матан начинался как раз с теории множеств и ZFC. Интересно, будет-ли в будущем использоваться та же XTT в качестве базиса. А может где-то уже так преподают?
1) Область настолько динамично развивается, что up-to-date обзора в целом нет.
2) Я думаю, рано или поздно теория типов войдёт в стандартную математическую программу, но сейчас до этого далеко. Для начала там должно всё стабилизироваться и должны выйти реально удобные и обкатанные инструменты (мы в JetBrains вот работаем над языком https://github.com/JetBrains/Arend, майкрософт на Lean, люди развивают Cubical Agda и Coq, RedPRL, но все они пока не идеал).
Оффтопик. Александр, можно Вам задать элементарынй вопрос по Hott Book? Что-то, я впал в ступор (. Не могли бы Вы пояснить в двух словах, почему окружность (circle, раздел 6.4) не подходит в качестве контрпримера утверждения Lemma 3.3.4. Every mere proposition is a set. Ведь все элементы circle равны между собой, поэтому, circle - mere proposition. Заранее, спасибо.
Основная проблема, как я ее вижу, не в том, что в определение 3.3.1. закралась ошибка, которую не устранили за почти 8 лет тщательной верификации текста. Исходя из этого явно ошибочного определения формально доказана Lemma 3.3.4. Every mere proposition is a set. с определением Definition 3.3.1. Hott Book эта лемма, очевидно, ложна. А из того факта, что ее "доказательство" было как-бы формально верифицировано, неизбежно следует неприятный вывод, что ложное утверждение притаилось в базовой схеме доказательств Hott Book. Это ложное утверждение позволяет доказать любое утверждение (в том числе, и ложное).
Comments 16
Любопытно, а почему не теоркат или какой-то из вариантов теории типов? И почему именно эта аксиоматика, а не NBD например?
Так просто привычнее или ZFC(n)/CZF(n) позволяют получить результаты, принципиально недостижимые с помощью теории типов и проч.?
Reply
2) Почему NBG, а не ZFC? На самом деле NBG консервативна относительно ZFC, так что это “та же” аксиоматика.
3) Конструирование моделей внутри самих теорий типов - отдельная отросль, и собственно модель кубической теории типов BCH была (на языке NuPRL) построена в экстенциональной теории типов. Ну и сейчас несколько групп независимо ведёт работу по такому общему фреймворку, чтобы было удобно строить модели самых разных теорий типов в рамках некоторой удобной фиксированной теории типов (по выразительности между HoTTMin и HoTTMax(1)), и доказывать с комфортом всякие их свойства. Вот самый сок: http://www.cs.cmu.edu/~cangiuli/papers/xtt.pdf... )
Reply
В стародавние времена у нас матан начинался как раз с теории множеств и ZFC. Интересно, будет-ли в будущем использоваться та же XTT в качестве базиса. А может где-то уже так преподают?
Reply
2) Я думаю, рано или поздно теория типов войдёт в стандартную математическую программу, но сейчас до этого далеко. Для начала там должно всё стабилизироваться и должны выйти реально удобные и обкатанные инструменты (мы в JetBrains вот работаем над языком https://github.com/JetBrains/Arend, майкрософт на Lean, люди развивают Cubical Agda и Coq, RedPRL, но все они пока не идеал).
Reply
Александр, можно Вам задать элементарынй вопрос по Hott Book? Что-то, я впал в ступор (.
Не могли бы Вы пояснить в двух словах, почему окружность (circle, раздел 6.4) не подходит в качестве контрпримера утверждения Lemma 3.3.4. Every mere proposition is a set. Ведь все элементы circle равны между собой, поэтому, circle - mere proposition.
Заранее, спасибо.
Reply
Reply
Да, это первое, что мне пришло в голову. Проблема в том что в определении в d Hott Book этого условия нет:
Definition 3.3.1. A type P is a mere proposition if for all x, y : P we have x = y.
Reply
Исходя из этого явно ошибочного определения формально доказана
Lemma 3.3.4. Every mere proposition is a set.
с определением Definition 3.3.1. Hott Book эта лемма, очевидно, ложна.
А из того факта, что ее "доказательство" было как-бы формально верифицировано, неизбежно следует неприятный вывод, что ложное утверждение притаилось в базовой схеме доказательств Hott Book. Это ложное утверждение позволяет доказать любое утверждение (в том числе, и ложное).
Reply
Leave a comment