Насколько я помню, это все про чистые системы типов. Если у тебя есть well-founded иерархия вселенных, и тебе разрешено задавать функции, у которых результат живет во вселенной ниже вселенной аргумента, но не самой нижней, то получится логически неконсистентная система. Ну и они там начиная с Жирарда строят такие термы, которые приводят к противоречиям, а потом объясняют, что они значат. В последнее я никогда не мог толком врубится. Думаю, что надо пару недель посидеть с карандашом над статьей Харкенса и/или заимплементить U- и U.
У меня студенты лямбда-куб делают в качестве финальной лабораторки, надо будет заставить их еще и PTS заимплементить.
У Жирара все просто, на уровне парадокса Рассела - на то, как я понял, и завели люди различие между types и kinds. А тут что-то хитренькое... для меня, в смысле.
Студенты классные. У меня все хреново в этом смысле. Для формального доказательства ассоциативности объединения множеств в ZFC берут три множества в качестве premises... дальше в таком же духе.
Жирар доказал более тонкую штуку про неконсистентность U и U-. А отсюда, задавая стирающее отображение, заменяющее все (три) вселенные на одну (Type или *), неконстстентность системы с Type:Type получается прямым следствием.
List = Set -> Set -- so now you can have List Int, List Bool, etc; in Haskell you can't express that as a type expression, so you end up talking about kinds, * -> *, so at least one can talk about parameterising on some of them, or matching the parameters.
Read literally, this means that given a type (Set), List produces a type (Set). But is it possible to have a List List? (Hence paradox akin to Russel)
The solution is to have towers of types. In Agda, Set implies Set 1. So List = Set 1 -> Set 1. But the type (Set 1 -> Set 1) is itself a Set 2 - next level universe of types. Although List is in a different universe, List Int is in the same universe as Int. Then at type level it is impossible to have List List, because List accepts an argument of type from universe 1 (Set 1), not universe 2 (Set 2, such as List).
It is possible to generalize List, though, by capturing the universe from which the argument is: List = Set a -> Set a. Now it is possible to express something like List List, but the two Lists are from two different universes.
"результат живет во вселенной ниже вселенной аргумента," Вот отсюда все ваши парадоксы логики и другая хрень с множествами. Типа давайте пусть не будет геометрии, тогда будут парадоксы. Геометрию убрать невозможно. Это моя аксиома. Шо там думают предшественники? Думаю, согласны в основном.
Кто и куда убрал геометрию? Евклидова геометрия - почетная разрешимая теория первого порядка с равенством, это Тарский еще в 50-ые годы прошлого столетия показал.
Мы с Тарским незнакомы, но то, что геометрия и парадоксы несовместимы, у меня лично нет ни каких сомнений. Речь о чём, когда вы вводите любые понятия и рассуждаете о них, это всегда происходит в трёхмерном пространстве. Невозможно создать понятие без этого.
Ну это из серии "в огороде бузина". Понятия всё равно все в пространстве. (И во времени). И что это доказывает? Когда доказывается теорема Пифагора, там нет никаких логических парадоксов. Более того, когда есть парадоксы, это значит неверная геометрическая модель: "Множество которое содержит само себя своим членом" Ну, нарисуйте, расскажите что вы нарисовали. И сразу понятно, что просто модель неверна. Это просто сухая вода и масло-масляное. Отрицание высказывания "множество, которое не содержит себя своим членом" может быть разным в зависимости от контекста. Напишите отрицание высказывания "не Земля".Отрицание - одно из самых сложных понятий. Сводить это к какой-то "простоте" это значит противоречить фактам.
Отрицание - самая сложная логическая операция. Она всегда имеет контекст. Без контекста она не имеет смысла. Когда я учился, нам сказали - вот закорючка, она называется "отрицание". А в чём смысл операции никто толком не объяснял. Это сложнейшее понятие, которые многие совершенно неправильно понимают. Во всяких википедиях дурачки пишут, что это обратное значение. Когда спрашиваешь, что такое обратное значение, уточняют что это обратное значение всего к чему стоит отрицание. Слово "контекст" им не знакомо. Примеров нет. Типа шо тут говорить, это "тупым токо не понятно". Начну с того, что отрицание может просто не существовать.
Я так понимаю, что вы с топологией и геометрией не очень так, правда? И зависимость топологии от аксиоматики, скажем, теории множеств тоже не вполне идет, так?
Ну так всё гипотеза. но это не аргумент. А вот что скажет суд, куда делся труп? Если есть чудеса, то труп может воскреснуть, и на небо улететь, но суд в эти сказки не верит. И я тоже. Это я вам Эвклид Эвклиду говорю.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2018-12-13 07:59 pm (UTC)У меня студенты лямбда-куб делают в качестве финальной лабораторки, надо будет заставить их еще и PTS заимплементить.
no subject
Date: 2018-12-13 08:11 pm (UTC)Студенты классные. У меня все хреново в этом смысле. Для формального доказательства ассоциативности объединения множеств в ZFC берут три множества в качестве premises... дальше в таком же духе.
no subject
Date: 2018-12-13 09:50 pm (UTC)no subject
Date: 2018-12-13 10:13 pm (UTC)no subject
Date: 2018-12-14 07:14 pm (UTC)Like,
List = Set -> Set -- so now you can have List Int, List Bool, etc; in Haskell you can't express that as a type expression, so you end up talking about kinds, * -> *, so at least one can talk about parameterising on some of them, or matching the parameters.
Read literally, this means that given a type (Set), List produces a type (Set). But is it possible to have a List List? (Hence paradox akin to Russel)
The solution is to have towers of types. In Agda, Set implies Set 1. So List = Set 1 -> Set 1. But the type (Set 1 -> Set 1) is itself a Set 2 - next level universe of types. Although List is in a different universe, List Int is in the same universe as Int. Then at type level it is impossible to have List List, because List accepts an argument of type from universe 1 (Set 1), not universe 2 (Set 2, such as List).
It is possible to generalize List, though, by capturing the universe from which the argument is: List = Set a -> Set a. Now it is possible to express something like List List, but the two Lists are from two different universes.
Геометрия трёхмерна
Date: 2018-12-14 10:31 am (UTC)Re: Геометрия трёхмерна
Date: 2018-12-14 12:14 pm (UTC)Re: Геометрия трёхмерна
Date: 2018-12-14 12:22 pm (UTC)Re: Геометрия трёхмерна
Date: 2018-12-14 12:43 pm (UTC)Re: Геометрия трёхмерна
Date: 2018-12-14 01:45 pm (UTC)Когда доказывается теорема Пифагора, там нет никаких логических парадоксов. Более того, когда есть парадоксы, это значит неверная геометрическая модель: "Множество которое содержит само себя своим членом" Ну, нарисуйте, расскажите что вы нарисовали. И сразу понятно, что просто модель неверна. Это просто сухая вода и масло-масляное.
Отрицание высказывания "множество, которое не содержит себя своим членом" может быть разным в зависимости от контекста. Напишите отрицание высказывания "не Земля".Отрицание - одно из самых сложных понятий. Сводить это к какой-то "простоте" это значит противоречить фактам.
Re: Геометрия трёхмерна
Date: 2018-12-14 10:44 pm (UTC)Re: Геометрия трёхмерна
Date: 2018-12-15 07:39 am (UTC)Re: Геометрия трёхмерна
Date: 2018-12-15 10:11 am (UTC)Re: Геометрия трёхмерна
Date: 2018-12-14 01:05 pm (UTC)Re: Геометрия трёхмерна
Date: 2018-12-14 01:46 pm (UTC)Re: Геометрия трёхмерна
Date: 2018-12-14 01:06 pm (UTC)Нет.
Аксиома - это гипотеза.
Re: Геометрия трёхмерна
Date: 2018-12-14 04:54 pm (UTC)