МБ
Brenoritvrezorkre
А если отказаться от доказательств от противного?
Без отпротивного легко доказывается.
Size: a a a
2019 November 15
B
Тут уже написали нечто
МБ
Ага. Увидел. Но это требует доказательства того, что Set - это топос. Что не является тривиальным. Можно просто доказать прямо в терминах множеств. Там в какую сторону нужно?
KV
Ага. Увидел. Но это требует доказательства того, что Set - это топос. Что не является тривиальным. Можно просто доказать прямо в терминах множеств. Там в какую сторону нужно?
Из эпиморфизма в сюръекцию
KV
Вот ещё интересно, есть ли там выбор или это меня переклинило опять.
МБ
МммМм... Возможно. Я знаю доказательство такое: возьмём g = характеристическую функцию dom(f), g : Y -> {0, 1}. Будет верно, что (g после f) = ((const 1) после f), следовательно g = const 1, то есть dom(f) совпадает с Y. Для характеристических функций, наверное, аксиома выбора нужна.
V
Вот ещё интересно, есть ли там выбор или это меня переклинило опять.
Не нужна. Иначе это бы не было конструктивным доказательством.
V
МммМм... Возможно. Я знаю доказательство такое: возьмём g = характеристическую функцию dom(f), g : Y -> {0, 1}. Будет верно, что (g после f) = ((const 1) после f), следовательно g = const 1, то есть dom(f) совпадает с Y. Для характеристических функций, наверное, аксиома выбора нужна.
Это то же самое доказательство, что я приводил. Только здесь используется тот факт, что Prop = {0,1}, что эквивалентно закону исключенного третьего.
МБ
А то, что я написал конструктивно? Там же утверждается, что такая g существует. А не факт.
МБ
Ну, да... Наверное.
МБ
Но так студентам проще объяснять, imho. Топосы у нас на второй семестр оставлены.
V
Здесь нужно только множество утверждений.
V
Без него я подозреваю это не доказуемо. Можно попробовать найти LCCC без классификатора подобъектов, где это неверно.
МБ
Ну... А как его по-быстрому рассказать? Эпи/моно-морфизмы у нас же прям на первой лекции.
V
Но так студентам проще объяснять, imho. Топосы у нас на второй семестр оставлены.
Это в общем зависит от конструктивного фреймворка, в котором это доказывается. Если в категориях, то нужно определить классификатор подобъектов и регулярные категории.
МБ
Ну, да. Но это довольно абстрактное изложение. А у нас курс "для программистов", то есть, всякие привязки к конкретным вычислениям.
МБ
Ну, то есть, не хочется, чтобы это было только про Coq и типы.
V
Хотя речь же про доказательство именно в Set. Обычно под Set подразумевают категорию классических множеств, т.е. и с LEM, и с AC. При наличии LEM всё доказывается в Set напрямую без проблем. Если же работать в конструктивной теории множеств, то, чтобы формально это доказать, нужно сначала выбрать собственно конструктивную теорию множеств, где это будет доказываться.
V
Ну, то есть, не хочется, чтобы это было только про Coq и типы.
А, ну в теории типов это легко
V
Собственно, доказательство, которое я написал, уже на языке теории типов написано. Практически.