nya,
iifatЕсли хочется
абсолютно конструктивного, надо ещё показать что
можно выразить непереодичной десятичной дробью. Возможно это можно сделать правильно группируя соответст. разложения в ряды.
Ничего подобного не требуется. Я сколько-нибудь подробно знаком только с советским направлением конструктивизма, в котором конструктивные действительные числа задаются парой алгоритмов, один из которых выдаёт фундаментальную последовательность рациональных чисел, а другой называется регулятором сходимости и по заданному натуральному
указывает номер, начиная с которого члены последовательности отличаются от предела меньше, чем на
. Для чисел
и
такие алгоритмы, естественно, существуют.
Кстати, разложение произвольного конструктивного действительного числа в десятичную дробь, вообще говоря, не конструктивно. Также не существует алгоритма, который проверял бы равенство любых двух конструктивных действительных чисел.
Но я не в курсе, как там обстоят дела с доказательством иррациональности. Подозреваю, что всё в порядке, но примеров таких доказательств не видел.