>У Георга Кантора возникла прекрасная идея расширить рамки логики первого порядка, чтобы была возможность рассуждать о самих утверждениях. Это реализуется через принцип рефлексии - мы хотим, чтобы для каждого утверждения-с-параметром At у нас возникла его “внутренняя реализация” {t | A(t
( ... )
Так. Видимо, пост надо временно закрыть и переработать. Главным образом потому, что потребность в теории, где невыводимо V ∈ V для Кантора была мотивирована вовсе не парадоксом Рассела, а парадоксом Кантора
( ... )
Александр, а можно задать Вам вопрос про диагональный метод Кантора? Точнее, про доказательство этим методом несчётности отрезка [0,1]. Я никак не могу понять, почему это доказательство правильно, ведь, по-моему, оно ломается в два счёта...
Доказательство такое: - допустим, у нас есть последовательность всех точек отрезка - мы записываем эти точки в виде двоичной дроби. - далее мы строим двоичную дробь, отличающуюся от дроби первой точки в первой позиции, от дроби второй точки во второй позиции и т.д. - на этом основании заключают, что вновь построенная дробь не присутствует в списке.
Однако есть такой факт: дроби 1.00000... и 0.111111... обозначают одно и то же число. И несложно составить последовательность дробей, на первом месте которой стоит 1.00000..., а в результате применения диагональной процедуры получается 0.111111...
Приведённое доказательство действительно неверно. Для того, чтобы доказательство работало, нужно использовать как минимум троичные дроби. Можно десятичные.
Перечитал пост и понял, что стоит задать ещё один вопрос:
>Принцип рефлексии позволяет для любого множества X сформировать множество всех его подмножеств P(X), и Кантор доказал (используя схему преобразования - тоже частный случай неограниченного принципа рефлексии), что это множество строго больше исходного множества XВот, кроме шуток, не понимаю, что такое "множество всех подмножеств". Вроде бы, сначала, это очевидно... но потом начинаешь не понимать: как переносится понятие "множества всех подмножеств" на бесконечные множества И ПРИ ЭТОМ сохраняется "это множество строго больше исходного множества X". Все известные мне бесконечные множества строятся путём конечного числа "конструкторов" (0 и s для нат. чисел), т.е. допускают конечное описание. Любое подмножество либо тоже допускает конечное описание, либо... я не понимаю, о чём идёт речь (т.к. не понимаю, как мы определяем, что это именно подмножество X), когда говорят об этом подмножестве. А тогда множество подмножеств тоже должно, кажется, быть не более, чем счётным
( ... )
А можешь рассказать (лучше со ссылками) про то, как соотносятся теория множеств, теория категорий и HoTT -- что из этого годится как основания математики, что на чём строится, что без чего может существовать?
На спасение приходит понятие слабой категории, она же weak (∞,1) -category. Это ослабление категорий в том смысле, что теперь ассоциативность композиции морфизмов требуется не в строгом смысле, а с точностью до изоморфизма. На этом пути рождается понятие ∞-топоса. Так вот в ∞-топосах нам, судя по всему, уже не нужно wellpointedness и аксиомы выбора, чтобы работать
( ... )
Далее, HoTT внутри HoTT есть интерпретация конструктивной теории множеств CZF. Если в HoTT постулировать аксиому выбора для 1-типов, то эта интерпретация интерпретирует всю ZFC. Саму же HoTT можно проинтерпретировать в терминах симплициальных множеств в рамках ZFC, причём эта модель удовлетворяет аксиоме выбора для 1-типов. Для доказательства корректности модели, однако, требуется вариант аксиомы о непротиворечивости ZFC - аксиома о существовании сильно недостижимого кардинала (т.е. множества являющегося полноценной моделью самой ZFC). Вопрос о консервативности HoTT+AC над ZFC является открытым. Красивым способом решения было бы показать, что интерпретаций теории множеств внутри HoTT внутри модели внутри ZFC и есть внутренняя модель ZFC. Авторы публикации про симплициальную модель говорят что это так и должно быть, но детали не проработаны и сейчас этим вопросом всерьёз никто, насколько я знаю, не занимается, т.к. подозревают, что модель ещё будет немножко развита в ближайшие годы и тогда доказательство в любом случае придётся менять.
Интересно, а каких ещё клёвых штук можно на грудах наформализовывать? Я никогда всерьёз не интересовался грудами, привык думать о них как “те же торсоры, только в профиль”, а тут вот пример, когда использование груд очень украшает аксиоматику.
1) Вы не пробовали записать удобную аксиоматику для иных геометрий, основываясь на грудах? Наверное, для афинной напрашивается, а вот как со сферической, эвклидовой, гиперболической, проективной и конформной - априори непонятно.
2) А вы что-нибудь знаете про Planar ternary rings? Они могут быть описаны как equational theories, или они ближе к полям и соответственно слишком “жесткие”, чтобы быть алгебраическими теориями?
Не пробовал, но вот человек пробовал для аффинной и у него не получилось https://dxdy.ru/topic122315.html Там ведь не только сдвиги, там гомотетии нужны. В эллиптическом пространстве любое движение (сохраняющее ориентацию) есть композиция левого и правого сдвигов. Я это всё (написание программы) затеял с тройной целью: 1) Поучиться программировать; 2) Разобраться в геометрии (что с детства хотел сделать, но всё никак); 3) В перспективе написать пруфчекер, чтобы понять, как пишутся пруфчекеры. Соответственно, выбрал самую простую геометрию. Аксиоматика из книги Бахмана, если её расшифровать (а это нелегко было, посмотрите стр. 165-170, из которых я выжал доказательства), сбывает вековую мечту - свести геометрию к алгебре и доказательства к тупым вычислениям! В результате научился рисовать OpenGL и сейчас учусь сглаживать края, а до пруфчекера дойду ещё не скоро.
Comments 46
Reply
Reply
Точнее, про доказательство этим методом несчётности отрезка [0,1].
Я никак не могу понять, почему это доказательство правильно, ведь, по-моему, оно ломается в два счёта...
Reply
Reply
- допустим, у нас есть последовательность всех точек отрезка
- мы записываем эти точки в виде двоичной дроби.
- далее мы строим двоичную дробь, отличающуюся от дроби первой точки в первой позиции, от дроби второй точки во второй позиции и т.д.
- на этом основании заключают, что вновь построенная дробь не присутствует в списке.
Однако есть такой факт: дроби 1.00000... и 0.111111... обозначают одно и то же число. И несложно составить последовательность дробей, на первом месте которой стоит 1.00000..., а в результате применения диагональной процедуры получается 0.111111...
Reply
Reply
>Принцип рефлексии позволяет для любого множества X сформировать множество всех его подмножеств P(X), и Кантор доказал (используя схему преобразования - тоже частный случай неограниченного принципа рефлексии), что это множество строго больше исходного множества XВот, кроме шуток, не понимаю, что такое "множество всех подмножеств". Вроде бы, сначала, это очевидно... но потом начинаешь не понимать: как переносится понятие "множества всех подмножеств" на бесконечные множества И ПРИ ЭТОМ сохраняется "это множество строго больше исходного множества X". Все известные мне бесконечные множества строятся путём конечного числа "конструкторов" (0 и s для нат. чисел), т.е. допускают конечное описание. Любое подмножество либо тоже допускает конечное описание, либо... я не понимаю, о чём идёт речь (т.к. не понимаю, как мы определяем, что это именно подмножество X), когда говорят об этом подмножестве. А тогда множество подмножеств тоже должно, кажется, быть не более, чем счётным ( ... )
Reply
Reply
Reply
Reply
Reply
https://dxdy.ru/topic135617.html
Reply
Интересно, а каких ещё клёвых штук можно на грудах наформализовывать? Я никогда всерьёз не интересовался грудами, привык думать о них как “те же торсоры, только в профиль”, а тут вот пример, когда использование груд очень украшает аксиоматику.
Reply
2) А вы что-нибудь знаете про Planar ternary rings? Они могут быть описаны как equational theories, или они ближе к полям и соответственно слишком “жесткие”, чтобы быть алгебраическими теориями?
Reply
https://dxdy.ru/topic122315.html
Там ведь не только сдвиги, там гомотетии нужны. В эллиптическом пространстве любое движение (сохраняющее ориентацию) есть композиция левого и правого сдвигов. Я это всё (написание программы) затеял с тройной целью:
1) Поучиться программировать;
2) Разобраться в геометрии (что с детства хотел сделать, но всё никак);
3) В перспективе написать пруфчекер, чтобы понять, как пишутся пруфчекеры.
Соответственно, выбрал самую простую геометрию. Аксиоматика из книги Бахмана, если её расшифровать (а это нелегко было, посмотрите стр. 165-170, из которых я выжал доказательства), сбывает вековую мечту - свести геометрию к алгебре и доказательства к тупым вычислениям! В результате научился рисовать OpenGL и сейчас учусь сглаживать края, а до пруфчекера дойду ещё не скоро.
Reply
Leave a comment