Трансфинитная индукция - основана ли она только на интуиции?

[Someone]

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

Хм. Где "там"? Если Вы имеете в виду вот эту фразу из статьи про Epsilon-induction:
"$\in$-induction is a special case of well-founded induction",
то, очевидно, она не про аксиому регулярности, а про то, что эпсилон-индукция является частным случаем трансфинитной индукции:

Корнечно, очевидно. Поэтому я это писать не стал, решил, что Вы сами догадаетесь.

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

"Частность" это случая заключается в том, что в качестве отношения полного порядка используется отношение принадлежности, а не что-то иное.

Отношение принадлежности не является отношением полного порядка (за исключением ординалов).

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

Если же посмотреть по другой ссылке - на статью про аксиому регулярности, то там как раз сказано:
"Given the other ZF axioms, the axiom of regularity is equivalent to the axiom of induction".

Точнее, axiom of $\in$-induction". Это не то же самое, что трансфинитная индукция по вполне упорядоченному множеству или индукция по натуральным числам, которая прекрасно обходится без аксиомы регулярности.

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

Может быть оно и так, только это меня бы очччень удивило. Ибо в последовательностях Гудстейна нет ничего бесконечного: и все элементы последовательности конечны, и их количество конечно.

Дык, последнее как раз и есть утверждение теоремы Гудстейна. Если Вы заранее знаете, что "их количество конечно", то зачем ещё какую-то теорему Гудстейна доказывать?

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

Поэтому совершенно непонятно, какое отношение ко всему этому может иметь утверждение о существовании бесконечности.

Аксиомы индукции в арифметике формулируются для натурального ряда - бесконечного множества натуральных чисел. Если Вы хотите эти аксиомы доказывать, то Вы должны иметь возможность говорить о натуральном ряде (и о его подмножествах) как о едином объекте. Тут аксиома бесконечности и вылезет.

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

Доказательство теоремы 4 на стр. 234 Куратовского-Мостовского мне понятно. И мне кажется очевидным, что его можно повторить без упоминания понятия "множества", оперируя только "свойствами" $\varphi(x)$ - формулами языка логики первого порядка. Всё что нужно - это иметь под рукой для объектов рассматриваемой теории отношение полного порядка.

В арифметике эта теорема превращается в (очевидное) утверждение, что, взяв произвольное натуральное число $n$, мы можем провести индукцию до этого натурального числа. Как из этого получить полную форму аксиомы индукции - не знаю. Скорее всего, это невозможно (не зря же есть отдельные понятия непротиворечивости и $\omega$-непротиворечивости).

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

Например, в случае последовательностей Гудстейна они прямо следуют из определения последовательностей. А вот с утверждением о существовании минимального объекта, удовлетворяющего любому заданному свойству, всё гораздо сложнее. По крайней мере, я не знаю откуда его можно взять. Уж не из аксиом арифметики - это точно.

Возможно, именно поэтому теорема Гудстейна и недоказуема в арифметике. Кстати, это не единственное недоказуемое в арифметике утверждение.

[epros]

Someone в сообщении #471400 писал(а):

Если Вы заранее знаете, что "их количество конечно", то зачем ещё какую-то теорему Гудстейна доказывать?

Я знаю, что это доказывается трансфинитной индукцией до ординала $\varepsilon_0$. И мне не очевидно, что для этого необходимо утверждение о существовании бесконечности.

Someone в сообщении #471400 писал(а):

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

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

Someone в сообщении #471400 писал(а):

Как из этого получить полную форму аксиомы индукции - не знаю.

Не из этого. Полную форму аксиомы индукции, как я понял, можно получить из аксиом полного порядка. Схема такая же, как у Куратовского-Мостовского, только без упоминания "множеств":
Рассматриваем формулу $\neg \varphi(x)$, если ей удовлетворяет хотя бы один объект, то в силу аксиом полного порядка есть минимальный $\tilde{x}$, удовлетворяющий $\neg \varphi(\tilde{x})$. Значит для любого $y < \tilde{x}$ имеем $\varphi(y)$, а в силу предпосылки индукции это влечёт за собой $\varphi(\tilde{x})$, что противоречит $\neg \varphi(\tilde{x})$. Значит исходное предположение неверно: формуле $\neg \varphi(x)$ не удовлетворяет ни один объект.

Вопрос в том, откуда взять утверждение о существовании минимального объекта, удовлетворяющего формуле. Похоже, что иначе как из интуиции неоткуда.

[migmit]

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

поскольку Вы пренебрегли кванторами.

Нет. Там написано "при всех" - это словесный эквивалент квантора $\forall$.

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

это самое индукционное предположение $X$ оказалось воткнутым в предпосылку импликации

Это когда я стал показывать, как сделать закат солнца вручную. А нормальный путь - добавить $X$ как аксиому и доказывать, фактически, его же, только для $m+1$.

[epros]

migmit в сообщении #471461 писал(а):

Там написано "при всех" - это словесный эквивалент квантора $\forall$.

Там было две переменных и только одно словосочетание "при всех".

migmit в сообщении #471461 писал(а):

А нормальный путь - добавить $X$ как аксиому и доказывать, фактически, его же, только для $m+1$.

В формуле $\forall m,n ~ [(\forall k ~ \varphi(m, k)) \to \varphi(m+1, n)]$ Ваше $X$, если я правильно понял, соответствует $\forall k ~ \varphi(m, k)$, что не является предложением исчисления предикатов, ибо содержит свободную переменную. А добавить как аксиому можно только предложение.

Выше я упоминал бескванторный вариант арифметики - примитивно-рекурсивную арифметику Сколема, в которой тоже есть математическая индукция: из $\varphi(0)$ и $\varphi(x) \to \varphi(x+1)$ выводится $\varphi(x)$. Предлагаю Вам в качестве упражнения попробовать реализовать двухступенчатую математическую индукцию в рамках этого - бескванторного - формализма. Допустим пары $(m,n)$ упорядочены лексикографически и Вы знаете, что если $\varphi$ верно для всех пар аргументов, меньших $(m,n)$, то оно верно и для $(m,n)$. Честно говоря, я даже не знаю, можно ли формализовать это условие в бескванторной теории... Ибо квантификация по бесконечной области определения - вещь совсем не тривиальная и не самоочевидная.

[migmit]

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

А добавить как аксиому можно только предложение.

Хорошо, уговорили: добавим в теорию сначала константу $m$, про которую не будет известно ничего, кроме того, что она означает натуральное число. А потом — предложение $X$.

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

Предлагаю Вам в качестве упражнения попробовать реализовать двухступенчатую математическую индукцию в рамках этого - бескванторного - формализма.

Не вижу особого смысла.

[epros]

migmit в сообщении #471612 писал(а):

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

А добавить как аксиому можно только предложение.

Хорошо, уговорили: добавим в теорию сначала константу $m$, про которую не будет известно ничего, кроме того, что она означает натуральное число. А потом — предложение $X$

С константой не получится, поскольку по этому аргументу далее предполагается квантификация. На словах всё легко, а Вы попробуйте формализовать.

[migmit]

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

С константой не получится, поскольку по этому аргументу далее предполагается квантификация. На словах всё легко, а Вы попробуйте формализовать.

А в чём проблема? Ещё один метаматематический факт: если, добавив в теорию константу $x$, мы можем доказать утверждение $\varphi$, то в исходной теории мы можем доказать утверждение $\forall x~\varphi$. Конечно, в теориях без кванторов это, по понятным причинам, не работает.

[epros]

migmit в сообщении #471664 писал(а):

... если, добавив в теорию константу $x$, мы можем доказать утверждение $\varphi$...

Наверное я туплю. Какое отношение добавленная константа имеет к утверждению $\varphi$? Может Вы хотели сказать:
"Если, добавив в теорию константу $c$, мы можем доказать $\varphi(c)$ (подстановка новой константы вместо свободной переменной формулы), то доказано $\forall x ~ \varphi(x)$"?

[migmit]

Вы пишете $\varphi(c)$, я пишу просто $\varphi$. $c$ может входить свободно в $\varphi$, а может и не входить, мне без разницы.

[epros]

migmit в сообщении #471930 писал(а):

Вы пишете $\varphi(c)$, я пишу просто $\varphi$. $c$ может входить свободно в $\varphi$, а может и не входить, мне без разницы.

Если я правильно понял, то речь шла о формуле $\forall k ~ \varphi(m,k)$, где $\varphi(m,k)$ означает: "функция Аккермана определена для аргументов $m$ и $k$". Вы, кажется хотели сказать, что можно подставить новую константу $c$ вместо $m$ и добавить получившееся утверждение $\forall k ~ \varphi(c,k)$ в аксиомы? Выведя отсюда $\forall n ~ \varphi(c+1,n)$, мы считаем доказанным $\forall n ~ [\forall k ~ \varphi(c,k) \to \varphi(c+1,n)]$. Правильно? Далее, поскольку $c$ - новая константа, мы можем считать доказанным $\forall m,n ~ [\forall k ~ \varphi(m,k) \to \varphi(m+1,n)]$, так?

Это всё понятно. Но интересная фишка в том, что в бескванторной теории эта схема где-то не срабатывает. Я даже догадываюсь где. Из $\varphi(c,k)$ можно вывести $\varphi(c+1,n)$ и можно считать отсюда доказанным $\varphi(c,k) \to \varphi(c+1,n)$, но это не то же самое, что $\forall n ~ [\forall k ~ \varphi(c,k) \to \varphi(c+1,n)]$. Кажется где-то так, если я нигде не ошибся.

-- Пт июл 29, 2011 10:17:47 --

А, нет, вот это как раз и неверно:

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

Из $\varphi(c,k)$ можно вывести $\varphi(c+1,n)$

[vek88]

Как обещал в post471396.html#p471396, начал в своей теме рассмотрение трансфинитного варианта определения истинности в К-системах. См. post472251.html#p472251.