V
Там, правда, используется функциональная и пропозициональная экстенсиональность.
Size: a a a
2019 November 15
KV
Не могу понять, как в итоге строятся прообразы для сюръекции. Откуда они берутся?
V
Собственно, пропозициональная экстенсиональность есть аналог классификатора подобъектов в теории типов.
МБ
Ну, да. Но чтобы к этому подвести людей без бэкграунда, надо всю категорную логику рассказать. Это долго. Если бы была дорожка покороче к чисто категорному доказательству, было бы, конечно, отлично.
V
Не могу понять, как в итоге строятся прообразы для сюръекции. Откуда они берутся?
Они не строятся, только доказывается их существование. Это разные вещи без AC.
KV
Они не строятся, только доказывается их существование. Это разные вещи без AC.
Так доказательство конструктивное или нет?
V
Так доказательство конструктивное или нет?
Да, но это не означает, что есть функция, которая их выбирает.
МБ
Не могу понять, как в итоге строятся прообразы для сюръекции. Откуда они берутся?
Ну. Они не строятся. У нас просто есть классификаторы. А, ну выше уже написали.
V
Т.е. мы доказали, что для каждого элемента B существует прообраз, но не сконструировали его. Чтобы перейти от первого ко второму, нужна AC.
KV
Стало быть, я не знаю, что такое "конструктивное доказательство"
V
Стало быть, я не знаю, что такое "конструктивное доказательство"
В конструктивной математике есть две интерпретации слова "существует": сильное и слабое. Сильное означает, что у нас есть явная конструкция, а слабое только что доказательство существования. Если есть AC, то эти две интерпретации становятся эквивалентны.
V
Я выше использовал слово "существует" в слабом смысле.
KV
Это интересно, что конструктивное доказательство можно получить без конструирования...
V
Ну да, есть теории, такие как голая MLTT, где невозможно сформулировать слабое существование, поэтому люди, привыкшие к ней, могут про это не догадываться.
МБ
Ну, мы конструируем, но у нас есть некие базовые сущности "из воздуха", и мы их неким образом интерпретируем, возможно, не жёстко конструктивно. Можно считать это аксиомами.
KV
Ну, мы конструируем, но у нас есть некие базовые сущности "из воздуха", и мы их неким образом интерпретируем, возможно, не жёстко конструктивно. Можно считать это аксиомами.
И как это отличается от неконструктивной математики?
CE
И как это отличается от неконструктивной математики?
Что такое неконструктивная математика?
KV
Что такое неконструктивная математика?
Математика, которую нельзя назвать конструктивной и более того, можно назвать классической
CE
Математика, которую нельзя назвать конструктивной и более того, можно назвать классической
То есть lem+ac?
KV
То есть lem+ac?
Грубо говоря, да