Nxx писал(а):
Цитата:
Невычислимая биекция существует, так как её существование можно доказать в аксиоматической теории множеств.
Используется ли для этого аксиома выбора?
Нет.
Nxx писал(а):
Я признаю закон исключенного третьего и доказательства от противного. Значит, я - не конструктивист?
Да. Вы действительно не конструктивист.
Nxx писал(а):
Если бы у меня не было каши в голове после курса матана, я бы ничего тут не спрашивал.
Так, может, Вам стоит для начала повторить курс матана и попытаться разобраться в нём?

Хотя матан, собственно, здесь не при чём. Мы говорим о матлогике.
Давайте сделаем так. Пусть у нас есть некоторое (эффективное) перечисление (возможно, с повторениями) всех алгоритмов:

. Некоторые алгоритмы задают конструктивное действительное число (то есть генерируют последовательность рациональных чисел, сходящуюся к действительному числу с заданной оценкой скорости сходимости), а некоторые - нет. Пусть

--- некоторое число, такое что алгоритм

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

в

следующим образом:


равно минимальному натуральному числу

, такому что алгоритм

задаёт конструктивное действительное число, отличное от чисел, задаваемых алгоритмами

.
Тогда отображение, сопоставляющее каждому натуральному числу

конструктивное действительное число, задаваемое алгоритмом

, будет являться биекцией между множеством всех натуральных чисел и множеством всех конструктивных действительных чисел.
Функция

, естественно, не вычислима (это можно доказать. сведя к ней проблему остановки или проблему равенства конструктивных действительных чисел). Однако в рамках классической математики она построена совершенно законными методами (и даже без использования аксиомы выбора). Какие тут могут быть вопросы, не понимаю!
Добавлено спустя 4 минуты 15 секунд:PAV писал(а):
Да, полагаю что метод "от противного" там фигурирует. Пусть знатоки лучше ответят.
Метод "от противного" не фигурирует. А закон исключённого третьего фигурирует. Вот в том построении биекции, которое я привёл выше, мы используем то, что для любого

алгоритм

либо задаёт конструктивное действительное число, либо не задаёт
