Теория множеств

Нужно сказать несколько слов о теории множеств. Широко распространено мнение, что интуиционисты допускают лишь разрешимые множества, такие как множество четных чисел или множество простых; но это не является интуиционистской точкой зрения, это слишком ограничительно. Нет причин не допускать произвольное свойство математических сущностей в качестве определения множества. Брауэр называет такое множество видом, но это лишь вопрос терминологии. К примеру, я могу говорить о виде $S$ цифр, встречающихся бесконечно много раз в десятичном разложении $\pi$. Хотя я не могу предъявить элемент $S$, я знаю, что $S$ не может быть пустым. Таким образом, если $NE$ — вид непустых видов натуральных чисел, то $S \in NE$.

Теория видов строго предикативна в том смысле, что элементы вида должны определяться независимо от самого вида. Мы начинаем с натуральных чисел; следующий уровень образован последовательностями выбора натуральных чисел и потоками, котрые можно рассматривать как виды последовательностей выбора. Виды натуральных чисел и потоки видов суть виды типа $0$. Такой вид, как $NE$, относится к типу $1$, и т. д. Кванторы по видам допустимы, но они ограничиваются на элементы заданного вида или потока.