Насколько я понимаю, у конструктивистов вообще нету ни множеств, ни элементов. Иначе говоря, "множество" - это у них синоним для формулы с 1 свободной переменной, а "элемент" - это синоним для терма, подстановка которого в эту самую формулу вместо ее единственной свободной переменной приводит к верной замкнутой формуле.
Я не говорил, что конструктивизм отрицает теории множеств. Есть энтузиасты, которые занимаются тем, что строят конструктивные аксиоматики теории множеств. Правда лично я не понимаю зачем это нужно. В слове "множество" самом по себе нет ничего особо ценного или содержательного, все интересные выводы появляются как раз при наличии достаточно сильной аксиоматики. Исторически наиболее сильные аксиоматики оказались привязаны именно к слову "множество", но никакого закона природы в этом нет: Можно привязать сильную аксиоматику к чему угодно другому.
Что касается конечности, в конструктивизме выделяют финитные, субфинитные, квазифинитные и неинфинитные "множества".
По-моему, вопрос определения конечности совершенно перпендикулярен конструктивизму. Он, конечно, важен, потому что от него зависит ключевое для конструктивизма понятие о наличии у алгоритма точки останова, но он и для неконструктивной математики важен.
Список - это у них терм особого вида.
Какого вида?
Финитность множества
известен способ построения списка, членами которого являются все элементы множества
и только они.
Не похоже на определение конечности. Я бы сказал, что возможны способы построения и бесконечных списков. Хотя, возможно, что собака зарыта в "особом" виде терма.
Субфинитность множества
известен способ построения списка, членами которого являются все элементы множества
но, возможно, не только они.
Аналогично.
Квазифинитность множества
известен способ построения натурального числа
, для которого будет опровергаться приведением к нелепости предположение о невозможности списка элементов множества
среди списков с не более чем
членами.
Хм. Двойное отрицание существования "списка с не более чем
членами". Это более похоже на определение конечности. Но оно как раз завязано на определение натурального числа.
Неинфинитность множества
невозможно привести к нелепости предположение о невозможности списка, членами которого являлись бы все элементы множества
и только они.
Я ослышался или здесь звучит тройное отрицание? Зачем? В конструктивизме тройное отрицание эквивалентно одинарному.
Если что, я ни разу не конструктивист, просто мне тоже было интересно, как у них конечность определяется.
Независимо от конструктивизма известно два определения конечности:
1) Возможность пронумеровать все объекты до некоторого натурального числа.
2) Упомянутая выше конечность "по Дедекинду".
Первое определение я полагаю естественным, ибо оно понятно любому, даже не слишком математически изощрённому уму. Второе я полагаю скорее "извращённым", чем "изящным". Ибо всё его изящество, насколько я понимаю, заключается в том, что в теории множеств с аксиомой выбора доказуема его эквивалентность первому определению.
Однако для теории множеств без аксиомы выбора можно построить модель, в которой первое и второе определения окажутся не эквивалентными.