В принципе, спор ни о чём, посколько
утверждение об истинности ZF равносильно
существованию вполне отделимого элементарного топоса с объектом
натуральных чисел.
Так что на самом деле все теоремы в ZF следует
воспринимать так: если T — вполне отделимый
элементарный топос с объектом натуральных чисел,
то тогдка верно следующее: …
Этот факт устраняет сам предмет спора и делает всё яснее.
Кстати, веровать при этом ни во что не надо.
В частности, следует осознать, что в математике
нет никаких «аксиом»
(утверждений, принимаемых без доказательств
— глупость-то какая!), а есть определения.
В частности, у нас есть определение некоторого
объекта (теории множеств ZFC, или в современном
варианте, вполне отделимого элементарного
топоса с объектом натуральных чисел и аксиомой выбора) и для этого
объекта выполняются определённые свойства
(наличие алгебраического замыкания
у любого поля, построенного внутри этого объекта).
В частности, в математики не существует абсолютных
конструкций, всё делается относительно чего-либо.

Другое дело, что ZFC (или топосы, кому как
больше нравится) приняты настолько повсеместно,
что это принято не упоминать. И правильно, нечего
засорять тексты повторениями.

А для конструктивной математики вместо
топоса ZFC используется эффективный топос.
Вот, например, что я нашёл:
http://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-208/
И теоремы в нём, конечно другие.

(Reply to this) (Parent) (Thread)

> если T — вполне отделимый
> элементарный топос с объектом натуральных чисел,
> то тогдка верно следующее: …
> Этот факт устраняет сам предмет спора и делает всё яснее.
> Кстати, веровать при этом ни во что не надо.

Кирпич можно взять и положить на стол. Конструктивное вещественное число — тоже (в виде распечатки соответствующей программы или дискеты, на которую эта программа записана). Можно положить на стол элементарный топос? Если нет — то в его существование остаётся именно веровать.

> А для конструктивной математики вместо
> топоса ZFC используется эффективный топос.

В конструктивной математике используется только то, что можно положить на стол. А то, что говорите Вы — это попытка понимания результатов конструктивной математики "классиками", к собственно конструктивной математике отношения не имеющая.

С уважением,
Гастрит

(Reply to this) (Parent) (Thread)

>Можно положить на стол элементарный топос?

Эффективный топос можно положить на стол в виде
распечатки программы, реализующей его операции.

>В конструктивной математике используется только то, что можно положить на стол.

Для этого сначала надо определить, что такое
объект, который можно положить на стол.

(Reply to this) (Parent)