[
Это нужна противоречивость
Size: a a a
Типы в языках программирования, моделирования, представления знаний и жизни
505 membersпожаловаться на группу
2021 November 23
E
ненаселенные теории это противоречивые теории
[
Тогда теории с юнитом
E
да, наверное я был неправ
E
мы или не выводим теорем, или нужно добавить аксиому, которая потом создаст противоречие
E
я путал выводимость (во всех моделях, sic!) и существование модели
[
В общем, проблем с добавлением новых аксиом не будет
[
Пока те не противоречат друг другу
s
Как минимум можно добавлять выводимые теоремы в аксиомы.
2021 November 24
AC
Вот на этом месте можно было бы остановиться и подумать. Лобачевский заменил одну аксиому другой, а не просто добавил ещё одну. О чём я и говорю. Кстати, по ссылке на пост Бауэра есть упоминание "нейтральной геометрии", с чего и началось обсуждение.
AC
Точно? А то между алеф-нуль и алеф-один может быть сколько угодно промежуточных вариантов в зависимости от. До алеф-нуль это не работает?
NR
а "построить" множество мощности континуум это как
AC
Наоборот. Противоречивость даёт населённость всем. А ненаселённые (с пустой моделью) можно.
s
AC
Написано, что она независима от ZFC (по крайней мере), то есть можно добавить к ZFC и её отрицание, тогда промежуточные мощности хотя бы будут существовать (декларативно). Но я не знаю, что Вы имели в виду под "построить"... 😁
s
Да, если добавить аксиому, то такое множество будет существовать.
s
Но без дополнительных аксиом ты не можешь вывести доказательство существования подобного множества.
AC
А теперь Вы перепутали выводимость и общезначимость (истинность во всех моделях). 😉