Схемы можно вывести только из схем
Не знаю, никогда в такие детали не вникал. При
доказательстве несуществования бесконечной цепочки
используется аксиома подстановки. Построение бесконечной цепочки, исходя из предположения, что существует множество
, не обладающее свойством
, можно осуществить, используя определение по индукции. Вероятно, ещё аксиома выбора потребуется. Но у меня нет ни малейшего желания заниматься полной формализацией этого доказательства.
-- Чт май 11, 2017 15:40:50 --Напрямую там ничего не строится, там всё неэффективно.
Есть конструктивный унивёрсум.
Ну, там конструктивность понимается совершенно не так, как в конструктивизме. Это скорее не конструктивность, а определимость: сначала у нас ничего нет, а затем мы добавляем множества, которые можно определить, используя формулы теории множеств и ранее определённые множества.