Но ведь если мы знаем, что последовательность фундаментальная, то знаем, что она сходится.
Это разумеется, но в конструктивном анализе нужно вроде гораздо больше, чтобы каша сварилась повкуснее.
Someone рекомендовал в разных темах какую-то конкретную книгу по конструктивному анализу, где разбирались те три или четыре варианта конструктивных вещественных чисел, и утверждения там делаются часто, кажется, для двух самых приятных видов (из рассматриваемых). Не помню её автора.
Б. А. Кушнер. Лекции по конструктивному математическому анализу. "Наука", Москва, 1973.
Конструктивная последовательность рациональных чисел, фундаментальная в смысле классического математического анализа, может сходиться к невычислимому действительному числу, если под вычислимым понимать число, для которого существует алгоритм, вычисляющий это число с любой наперёд заданной точностью.
Про теоремы Гудстейна например я прочитал, что она эквивалентна непротиворечивости арифметики Пеано
В русскоязычной Википедии действительно так написано. В англоязычной Википедии я этого не нашёл. Более того, там и термин "consistency" отсутствует. При этом русскоязычная Википедия ссылается на статью Laurie Kirby и Jeff Paris, "Accessible Independence Results for Peano Arithmetic", Bulletin of the London Mathematical Society, (1982), 285-293.
Электронная копия этой статьи у меня есть. В ней термин "consistency" встречается ровно один раз в следующем контексте:
Цитата:
In proving the theorems we rely on work of Ketonen and Solovay [3] on ordinals below
, which in turn develops earlier work by the present authors, Harrington, Wainer, and others. Gentzen [1] showed that using transfinite induction on ordinals below
one can prove the consistency of
, and the Ketonen-Solovay machinery we use here can be viewed as illuminating in more detail the relationship between
and
.
(Note: Goodstein proved the following: if
is a non-decreasing function, define an
-Goodstein sequence
by letting
be the result of replacing every
in the base
representation of
by
, and subtracting
. Then the statement "for every non-decreasing
, every
-Goodstein sequence eventually reaches
" is equivalent to transfinite induction below
.)
Здесь
обозначает арифметику Пеано,
— натуральный ряд (с нулём),
— наименьший ординал, удовлетворяющий условию
; вероятно, подразумевается, что функция
должна удовлетворять условию
(
— наименьший бесконечный ординал, то есть, порядковый тип наименьшего индуктивного множества).
Здесь, как видим, нет ни малейшего намёка на эквивалентность теоремы Гудстейна и совместности (непротиворечивости) арифметики Пеано.