Существует ли биекция между вычислимыми числами и нат.?

[маткиб]

Nxx в сообщении #187264 писал(а):

По-моему, для доказательства данной теоремы достаточно доказать, что рано или поздно выражение превратится в последовательность единиц. Для этого, как мне кажется, достаточно доказать, что при вычитании единицы количество возведений в степень либо уменьшается, либо остается тем же.

А если оно всё время будет оставаться тем же?

[Nxx]

Цитата:

А если оно всё время будет оставаться тем же?

Когда все единицы в свободном члене закончатся, останутся только члены с возведением в степень, которые придется разбивать и уменьшать количество возведений в степень. Я сейчас не доказываю теорему, я просто обозначаю ход рассуждений.

[маткиб]

epros, я, конечно, не спорю с тем, что эту теорему можно доказать "мета-теоретическими" средствами на основе арифметики Пеано, но из Вашего доказательства я ничего не понял! Что значит "число x обнулится за конечное число шагов"? Ведь обнуление сильно зависит от того, на каком шаге у нас встретилось число x, потому что основание системы счисления у нас растёт с каждым шагом.
Поэтому, подобные рассуждения

epros писал(а):

Последняя формула очевидно истинная (ибо первый же шаг по числу $x+mk+1$ превращает его в число вида $x+mk$).

вообще говоря, бессмысленны.

Да и если бы Ваше доказательство было верно, то что мешает его формализовать в арифметике Пеано? Вашу последовательность формул без проблем можно записать одной формулой с параметром, типа $P(m,x)$, потом с помощью индукции (с Ваших слов) доказать, что

$$ (\forall x)P(m,x)\rightarrow(\forall x)P(m-1,x), $$

а потом, ещё раз применив индукцию, получить $(\forall m)(\forall x)P(m,x)$. Итого, всего 2 применения индукции (если не считать технических моментов) и никаких "мета-рассуждений". Короче говоря, формализуйте всё это дело более чётко.

А вопрос о конструктивности (не основанности на актуальной бесконечности) аксиомы индукции как был открытым, так и остаётся.

[epros]

маткиб писал(а):

epros, я, конечно, не спорю с тем, что эту теорему можно доказать "мета-теоретическими" средствами на основе арифметики Пеано, но из Вашего доказательства я ничего не понял!

Готов представить все необходимые пояснения, ибо в этом посте, естественно, всё сформулированно в максимально сжатом виде.

маткиб писал(а):

Что значит "число x обнулится за конечное число шагов"? Ведь обнуление сильно зависит от того, на каком шаге у нас встретилось число x, потому что основание системы счисления у нас растёт с каждым шагом.

Разумеется основание растёт с каждым шагом. На первом - это 2, на втором - 3 и т.д. В общем случае на шаге n-1 основание равно n. Поэтому рассматривается произвольный шаг последовательности (n-1-ый), а символом $n$ обозначено то основание, которое мы имеем на этом шаге.

Фраза "число x обнулится за конечное число шагов" означает:
Существует такое натуральное число k, что выполнив k шагов, начиная с текущего (n-1-ого), мы получим из этого числа (элемента последовательности $a_{n-1}$) нуль. Т.е. $a_{n-1+k} = 0$.

маткиб писал(а):

Поэтому, подобные рассуждения

epros писал(а):

Последняя формула очевидно истинная (ибо первый же шаг по числу $x+mk+1$ превращает его в число вида $x+mk$).

вообще говоря, бессмысленны.

Не согласен. Эти рассуждения строго формализуемы. Число $x+1$ на следующем шаге превратится в $s^{n+1}_n(x)$, где $s^{n+1}_n(...)$ обозначает операцию замены $n$ в $n$-ричном разложении числа на $n+1$. Естественно, формула разложения числа $x$ по старому основанию такая же, как формула разложения числа $s^{n+1}_n(x)$ по новому основанию.

маткиб писал(а):

Да и если бы Ваше доказательство было верно, то что мешает его формализовать в арифметике Пеано? Вашу последовательность формул без проблем можно записать одной формулой с параметром, типа $P(m,x)$, потом с помощью индукции (с Ваших слов) доказать, что

$$ (\forall x)P(m,x)\rightarrow(\forall x)P(m-1,x), $$

а потом, ещё раз применив индукцию, получить $(\forall m)(\forall x)P(m,x)$. Итого, всего 2 применения индукции (если не считать технических моментов) и никаких "мета-рассуждений".

Не знаю что мешает. Очевидно, если теорема о недоказуемости этого вывода в арифметике верна, то "мою последовательность формул" нельзя записать одной формулой с параметром. По крайней мере, мне не очевидно, что это можно, ибо эта последовательность формул весьма нетривиально зависит от $m$.

маткиб писал(а):

Короче говоря, формализуйте всё это дело более чётко.

Давайте я лучше подробно отвечу на все Ваши вопросы. И, надеюсь, тогда станет ясно, что в исходном посте всё изложено достаточно чётко (по крайней мере для того, кто готов вникнуть в тему).

маткиб писал(а):

А вопрос о конструктивности (не основанности на актуальной бесконечности) аксиомы индукции как был открытым, так и остаётся.

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

[маткиб]

epros писал(а):

маткиб писал(а):

Короче говоря, формализуйте всё это дело более чётко.

Давайте я лучше подробно отвечу на все Ваши вопросы. И, надеюсь, тогда станет ясно, что в исходном посте всё изложено достаточно чётко (по крайней мере для того, кто готов вникнуть в тему).

Как я могу задать вопросы, если я ВООБЩЕ ничего не понял из Вашего доказательства? В том числе обозначений. Например, я не понимаю этого

epros писал(а):

т.е. минимальное число этажности $m+1$ - это $n^{[m]2}$

А уж "очевидность" индуктивных переходов я вообще не осилил. Если Вы представляете доказательство, то сделать его читаемым - это целиком и полностью Ваша забота. Читатель не обязан домысливать, что Вы там на самом деле думали.

Я вникнуть в тему готов. Более того, я знаю доказательство этой теоремы, в том числе, говоря Вашими словами, в "мета(1)-расширении арифметики Пеано" (с некоторыми оговорками). Но я не считаю его конструктивным в том смысле, в котором это понимают конструктивисты.

epros писал(а):

маткиб писал(а):

А вопрос о конструктивности (не основанности на актуальной бесконечности) аксиомы индукции как был открытым, так и остаётся.

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

Этот вопрос очень важен. Потому что лично Ваш конструктивизм очень скользкий, Вы попросту называете конструктивным то, что Вам нравится, и это очень непоследовательно. С какой стати, например, вот такая

$$ (\forall x)(\exists y)P(x,y,0)\&(\forall n)((\forall x)(\exists y)P(x,y,n)\rightarrow(\forall x)(\exists y)P(x,y,n+1))\rightarrow(\forall n)(\forall x)(\exists y)P(x,y,n) $$

аксиома индукции конструктивна (кванторы понимаются в классическом смысле, а если их нет, то применим стандартный фокус с их моделированием)? Если никакого способа вычислить $(\forall x)(\exists y)P(x,y,n)$ для каждого $n$ нет (нужно бесконечное число раз запустить бесконечный перебор), то с какой стати это вообще для конструктивиста должно быть осмысленно? Это конечно хорошо - говорить, что это очевидно, а актуальная бесконечность, видите ли, не очевидна, но в этом случае Вы не имеете права называть себя конструктивистом.

[epros]

маткиб писал(а):

Как я могу задать вопросы, если я ВООБЩЕ ничего не понял из Вашего доказательства? В том числе обозначений. Например, я не понимаю этого

epros писал(а):

т.е. минимальное число этажности $m+1$ - это $n^{[m]2}$

Хм. Не похоже, что Вы готовы вникнуть. Там же написано (и, по-моему, вполне ясным образом):

epros писал(а):

под $n^{[m]1}$ понимается возведение числа $n$ в степень самого себя $m$ раз

Например, для $m=1$ имеем: $n^{[m]1} = n^n$.
И далее:

epros писал(а):

а под $n^{[m]k}$ - то же самое, но вместо $n$ в самой верхней позиции подставлено $n^k$

Т.е. для $m=1$ имеем: $n^{[m]k} = n^{n^k}$. Или, если $k=2$, то: $n^{[m]2} = n^{n^2}$
Таким образом, "минимальное число этажности 2" ($m+1 = 2$) - "это $n^{n^2}$" ($n^{[1]2} = n^{n^2}$).

В этом можно легко убедиться если вычесть из $n^{n^2}$ единицу. Получим:
$a \cdot n^{b_1} + a \cdot n^{b_2} + a \cdot n^{b_3} + ... + a \cdot n + a$, где $a = n-1$, $b_1 = n^2-1$, $b_2 = n^2-2$ и т.д. При этом $a$ меньше основания разложения ($n$), а числа $b_1$, $b_2$ и т.д. имеют нулевую "этажность", т.е. представляются как $i \cdot n + j$, где $i$ и $j$ - меньше основания разложения. Так что, как видите, "этажей" в формуле разложения этого числа по основанию $n$ стало на один меньше.

По этому вопросу ещё что-то разжёвывать нужно?

маткиб писал(а):

А уж "очевидность" индуктивных переходов я вообще не осилил.

Например, берём формулу (3):

epros писал(а):

(3) Если любое число меньше $n^{[m-1]n^{m1}+m2}$ обнулится за конечное количество шагов, то любое число меньше $n^{[m-1]n^{m1}+m2+1}$ обнулится за конечное количество шагов.

Индукцией по $m2$, полагая предпосылку верной для $m2 = 0$, получаем, что для любого $m2$ число меньше $n^{[m-1]n^{m1}+m2}$ обнулится за конечное количество шагов. В частности, это верно для $m2 = (n-1) n^{m1}$. Но $n^{[m-1]n^{m1}+(n-1) n^{m1}} = n^{[m-1]n \cdot n^{m1}} = n^{[m-1] n^{m1+1}} = n^{[m] (m1+1)}$ Таким образом, если верна предпосылка формулы (2):

epros писал(а):

(2) Если любое число меньше $n^{[m] m1}$ обнулится за конечное количество шагов, то любое число меньше $n^{[m] (m1+1)}$ обнулится за конечное количество шагов.

то верно и её следствие.

маткиб писал(а):

Если Вы представляете доказательство, то сделать его читаемым - это целиком и полностью Ваша забота. Читатель не обязан домысливать, что Вы там на самом деле думали.

Ну, извиняюсь. Это всё-таки не научный журнал. Вы спросили доказательство - я ответил (насколько мог кратко).

Но ещё одну вещь я бы во избежание недоразумений всё-таки уточнил: расстановку кванторов. По переменным $m1, m2, ...$ кванторы всеобщности стоят перед соответствующими формулами: (2), (3) и т.д. Это соответствует формулировке аксиомы индукции. По переменной $n$ кванторы всеобщности стоят в обоих частях каждой импликации, т.е. отдельно квантифицировано и то, что идёт после "если", и то, что идёт после "то" (вот это и могло бы вызвать недоразумения). Переменная $m$ на уровне формул арифметики не квантифицируется (индукция по ней выполняется на уровне мета-теории). В принципе, её может и не быть в явном виде в приведённых формулах.

Пффф. На всё сразу просто физически не успеваю отвечать. Относительно конструктивности индукции давайте начнём с предыдущего вопроса:

маткиб писал(а):

P.S. Остался в подвешенном состоянии вопрос о конструктивности аксиомы индукции. Например, с чего бы

$$ P(0)\&(\forall n)(P(n)\rightarrow P(n+1))\rightarrow(\forall n)P(n) $$

верна для неразрешимого $P(n)$?

Очевидно, что если верны предпосылки индукции, то $P(n)$ просто не может быть неразрешимым. Ибо один из способов его разрешения (для конкретного n) - это выполнить алгоритм, который пройдёт по очереди все шаги индукции вплоть до n включительно.

[Nxx]

epros, такая фигня называется "итерированная экспонента" и записывается $\exp_n^m(k)$

[epros]

Nxx писал(а):

epros, такая фигня называется "итерированная экспонента" и записывается $\exp_n^m(k)$

Что Вы имеете в виду? Замену в $n$-ричном разложении числа $k$ основания $n$ на $m$? Буду знать.

[Nxx]

epros писал(а):

Nxx писал(а):

epros, такая фигня называется "итерированная экспонента" и записывается $\exp_n^m(k)$

Что Вы имеете в виду? Замену в $n$-ричном разложении числа $k$ основания $n$ на $m$? Буду знать.

То, что вы обозначаете $n^{[m]k}$.

[маткиб]

epros писал(а):

маткиб писал(а):

P.S. Остался в подвешенном состоянии вопрос о конструктивности аксиомы индукции. Например, с чего бы

$$ P(0)\&(\forall n)(P(n)\rightarrow P(n+1))\rightarrow(\forall n)P(n) $$

верна для неразрешимого $P(n)$?

Очевидно, что если верны предпосылки индукции, то $P(n)$ просто не может быть неразрешимым. Ибо один из способов его разрешения (для конкретного n) - это выполнить алгоритм, который пройдёт по очереди все шаги индукции вплоть до n включительно.

Ладно, займёмся таким вопросом: с чего Вы взяли, что формула $P(n)$ вообще имеет какой-то смысл? Например, если $P(n)\equiv(\forall x)(\exists y)Q(x,y,n)$, то $P(n)$ может быть не просто неразрешима, но и бессмысленна, ведь придавать смысл (определять понятие истинности) формулам арифметики Вы отказываетесь.

А аксиома индукции - это не то же самое, что "доказали $P(0)$, доказали $(\forall n)(P(n)\rightarrow P(n+1))$, поэтому можем доказать и $P(n)$", аксиома индукции - это тоже формула арифметики. Именно формула, а не процесс и не правило вывода (и если заменить её на правило вывода, то она сильно ослабнет, пусть кто поправит, если не прав). В этой формуле нигде не записано, что формула $P(n)$ разрешима хотя бы для какого-то $n$, а аксиома индукции обязана работать и быть разрешимой для любой формулы $P(n)$, в том числе не разрешимой ни при каком $n$. И нет никакой гарантии, что она вообще имеет смысл. Если из формулы для $P(n)$ сразу виден разрешающий алгоритм для любого $n$, то смысл, понятное дело, есть, а вот если алгоритма нет, то чёрт его знает.

С доказательством теоремы Гудстейна потом разберусь (если не лень будет).

Добавлено спустя 22 минуты 11 секунд:

epros, сначала нужно определиться с аксиомами, которые Вы используете при "конструктивном" доказательстве теоремы, а потом уже копаться в доказательстве, чтобы можно было придраться по поводу неконструктивности той или иной аксиомы. Пока что я не вижу никакой конструктивности даже в обычной аксиоме индукции.

[epros]

Nxx писал(а):

epros писал(а):

Nxx писал(а):

epros, такая фигня называется "итерированная экспонента" и записывается $\exp_n^m(k)$

...

То, что вы обозначаете $n^{[m]k}$.

Вообще-то в этом доказательстве потребуется не такая функция, а другая, которую можно рекурсивно определить следующим образом:
$\Lambda_k(n,m_1,...,m_k) = n^{\Lambda_{k-1}(n,m_1,...,m_{k-1})}+m_k$ где переменная $m_k$ определена в диапазоне $(0 \leqslant m_k \leqslant (n-1) n^{\Lambda_{k-1}(n,m_1,...,m_{k-1})})$
$\Lambda_1(n,m_1) = m_1$ где переменная $m_1$ определена в диапазоне $(2 \leqslant m_1 \leqslant n^2)$

Тогда первая формула запишется так:
(0)

$$\forall n (Z_n(\Lambda_{m+2}(n,2,0,...,0))) \to \forall n (Z_n(\Lambda_{m+3}(n,2,0,...,0)))$$

А каждая следующая формула с номером $k$ $(1 \leqslant k \leqslant m+2)$ запишется так:
(k)

$$\forall m_1,..., m_k (\forall n (Z_n(\Lambda_{m+2}(n,m_1,..., m_k, 0,..., 0))) \to \forall n (Z_n(\Lambda_{m+2}(n,m_1,..., m_{k-1}, m_k+1, 0,..., 0))))$$

Здесь $Z_n(x)$ - это предикат: "Любое число $y < x$ обнулится через конечное количество шагов, начиная с $n$-того". Для маткиба: Только не просите меня формализовать запись этого предиката. Очевидно, что это возможно в такой же мере, в какой возможно дать формальное определение последовательности.

Добавлено спустя 1 час 58 минут 40 секунд:

маткиб писал(а):

с чего Вы взяли, что формула $P(n)$ вообще имеет какой-то смысл?

Насколько я понимаю понятие "смысл", оный заключается в возможностях применения той конструкции, о "смысле" которой мы говорим. Соответственно, "смысл" в арифметике заключается в возможностях выполнения соответствующих операций над объектами арифметики, то бишь - над числами. А то, какие операции могут выполняться над числами, как раз определяется аксиомами арифметики.

маткиб писал(а):

Например, если $P(n)\equiv(\forall x)(\exists y)Q(x,y,n)$, то $P(n)$ может быть не просто неразрешима, но и бессмысленна, ведь придавать смысл (определять понятие истинности) формулам арифметики Вы отказываетесь.

Если у Вас есть какая-то возможность вычислить $(\forall x)(\exists y)Q(x,y,0)$ и к тому же Вам откуда-то известно, что $(\forall x)(\exists y)Q(x,y,n) \to (\forall x)(\exists y)Q(x,y,n+1)$ для любого $n$, то "смысл" в $(\forall x)(\exists y)Q(x,y,n)$ для любого $n$ заключается именно в том, что Вы можете его найти с помощью индукции. Весь вопрос только в этих "если" и "откуда известно".

маткиб писал(а):

А аксиома индукции - это не то же самое, что "доказали $P(0)$, доказали $(\forall n)(P(n)\rightarrow P(n+1))$, поэтому можем доказать и $P(n)$", аксиома индукции - это тоже формула арифметики.

Разумеется, в рамках арифметики индукция - это аксиома для соответствующего предиката.

маткиб писал(а):

Именно формула, а не процесс и не правило вывода (и если заменить её на правило вывода, то она сильно ослабнет, пусть кто поправит, если не прав).

Я, по крайней мере, поправлять не буду.
Правило вывода действительно слабее, поскольку оно работает на уровне мета-теории, а аксиома - на уровне теории. Например, в теории $T$ может быть недоказуемо $(\forall n) P(n)$, но доказуемо $P(n)$ для каждого $n$. Т.е., как Вы где-то выразились, "доказательство для каждого $n$ требует индивидуального и творческого подхода". А если выразиться точнее, то: В теории $T$ есть доказательства $P(n)$ для каждого $n$, но нет одного общего доказательства для всех $n$. Кстати, живой пример - это приведённое мной доказательство теоремы Гудстейна: Для каждой конкретной "этажности" $m$ доказательство в арифметике есть, а общего для всех $m$ доказательства нет - оно есть только в мета-теории.

Утверждение о том, что "мы можем выполнить алгоритм, который пройдёт все шаги индукции до $n$" на самом деле является утверждением о существовании индукции на мета-уровне:
$(T \vdash P(0)) \wedge (\forall n) (T \vdash P(n) \to P(n+1)) \to (\forall n) (T \vdash P(n))$

А индукция на уровне теории такова:
$T \vdash P(0) \wedge (\forall n) (P(n) \to P(n+1)) \to (\forall n) P(n)$

Понятное дело, первое ещё не означает второго. Откуда же возьмётся второе? А очень просто: Второе отличается от первого только тем, что этот алгоритм (который "пройдёт все шаги индукции до $n$") определён в рамках теории $T$.

маткиб писал(а):

Если из формулы для $P(n)$ сразу виден разрешающий алгоритм для любого $n$, то смысл, понятное дело, есть, а вот если алгоритма нет, то чёрт его знает.

Не знаю уж, "сразу" или не "сразу", но если предпосылки для индукции доказаны в рамках теории $T$, то смысл в индукции в рамках теории $T$ есть. Например, в случае с приведённым мной доказательством теоремы Гудстейна первая формула доказана только для конкретно заданной "этажности" $m$, т.е. у нас есть $P(m) \to P(m+1)$. Но в арифметике, очевидно, нельзя доказать формулу $(\forall m) (P(m) \to P(m+1))$, поэтому в арифметике предпосылка индукции не доказана.

маткиб писал(а):

epros, сначала нужно определиться с аксиомами, которые Вы используете при "конструктивном" доказательстве теоремы, а потом уже копаться в доказательстве, чтобы можно было придраться по поводу неконструктивности той или иной аксиомы. Пока что я не вижу никакой конструктивности даже в обычной аксиоме индукции.

Давайте тогда просто исходить из того, что конструктивисты признаЮт индукцию, как из "общепризнанного факта".

[epros]

Да, маткиб, если Вы уже готовы принять моё доказательство теоремы Гудстейна, то я готов продемонстрировать, что недоказуемость теоремы в арифметике обусловлена именно недостаточностью выразительных средств языка арифметики. И даже могу указать, каких именно средств не хватает в стандартном синтаксисе арифметики.

[naiv1]

epros в сообщении #187905 писал(а):

я готов продемонстрировать, что недоказуемость теоремы в арифметике обусловлена именно недостаточностью выразительных средств языка арифметики.

Продемонстрируйте, было бы интересно ознакомиться.

epros в сообщении #187905 писал(а):

И даже могу указать, каких именно средств не хватает в стандартном синтаксисе арифметики.

Если Вас не затруднит, укажите, пожалуйста, эти средства.

[kpierre]

Droog_Andrey писал(а):

Nxx писал(а):

Кстати, интересный вопрос, что такое причинность. Как бы вы на него ответили? Причинность - понятие математическое или физическое? Может ли вообще быть причинность в математике?

Если рассматривать физику как науку о материи и материальных объектах, а математику - как науку об информации и информационных объектах, то причинность - понятие математическое и представляет собой преобразование информации.

Хорошей аналогией может служить оператор любого преобразования: он связывает образ и прообраз (следствие и причину). Только с абстрактными информационными объектами интереснее. Но пока без какой-либо теории. Все, увы, зациклились на шенноновской теории связи.

Это все жутко интересно, на мой взгляд напрямую относится вот к этой теме: http://dxdy.ru/topic17894.html . Очень хочется копать дальше, может быть вам известны какие-нибудь места математики непосредственно сюда относящиеся?

[маткиб]

epros писал(а):

Да, маткиб, если Вы уже готовы принять моё доказательство теоремы Гудстейна,

Я готов принять Ваше доказательство теоремы Гудстейна, с учётом того, что оно не противоречит моим представлениям. Если Вы принимаете аксиому индукции в арифметике Пеано без всяких ограничений, то и проблем никаких нет, т.е., добавив к арифметике Пеано схему аксиом $(\forall x)((\mathrm{PA}\vdash\Phi(x))\rightarrow\Phi(x))$ (т.е. равномерную схему рефлексии), получим теорему Гудстейна. На каком основании конструктивисты принимают аксиому индукции в таком "общем" виде, я, естественно, не понял. Мне кажется, что такое принятие автоматически зачисляет конструктивиста в ряды классических математиков.

Проверить Ваше доказательство я не готов, ибо это тяжкий труд (на который я не способен), поэтому я верю Вам на слово.

epros писал(а):

то я готов продемонстрировать, что недоказуемость теоремы в арифметике обусловлена именно недостаточностью выразительных средств языка арифметики. И даже могу указать, каких именно средств не хватает в стандартном синтаксисе арифметики.

Продемонстрируйте, и укажите эти средства, потом я скажу своё мнение на этот счёт.

Добавлено спустя 19 минут 14 секунд:

epros писал(а):

Утверждение о том, что "мы можем выполнить алгоритм, который пройдёт все шаги индукции до $n$" на самом деле является утверждением о существовании индукции на мета-уровне:
$(T \vdash P(0)) \wedge (\forall n) (T \vdash P(n) \to P(n+1)) \to (\forall n) (T \vdash P(n))$

А индукция на уровне теории такова:
$T \vdash P(0) \wedge (\forall n) (P(n) \to P(n+1)) \to (\forall n) P(n)$

Понятное дело, первое ещё не означает второго. Откуда же возьмётся второе? А очень просто: Второе отличается от первого только тем, что этот алгоритм (который "пройдёт все шаги индукции до $n$") определён в рамках теории $T$.

Последний абзац не осилил. Сначала нужно придумать правдоподобные аксиомы для теории T, а потом уже рассуждать о том, что из них что-то там следует. У Вас же первая формула не определяет никаких аксиом T, ни даже правил вывода, но Вы почему-то делаете вывод, что аксиомы индукции оттуда следуют как теоремы. Каков смысл?