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

[epros]

Вопрос в заголовке темы тесно связан с вопросом о наличии у алгоритма точки останова, т.е. с вопросом о возможности конструктивного решения соответствующих проблем. Для начала поясню: алгоритм, заведомо имеющий точку останова, моделируется общерекурсивной функцией. Общерекурсивность некоторых рекурсивных функций невозможно доказать элементарными средствами (типа математической индукции). Простейший пример: функция Аккермана - т.к. она не является примитивно рекурсивной, то невозможно с помощью математической индукции доказать, что функция имеет значение для любой пары натуральных аргументов (т.е. что определяющая функцию рекурсия имеет точку останова). Однако это можно легко доказать с помощью трансфинитной индукции до ординала $\omega^2$.

На этом вступление закончилось, а вот и собственно вопрос: А на чём основана сама трансфинитная индукция? Т.е. с какой стати мы должны из предпосылки $\forall y<x ~ \varphi(y) \, \to \, \varphi(x)$ сделать вывод о верности $\varphi(x)$ для любого $x$?

Хотя бы на примере той же функции Аккермана: Здесь в качестве переменных индукции рассматриваются пары аргументов функции: $(m,n)$, упорядоченные лексикографически. Т.е. $(m_1,n_1) < (m_2,n_2)$ тогда и только тогда, когда $m_1 < m_2$ или $n_1 < n_2$ при $m_1 = m_2$. В качестве $\varphi(m,n)$ выступает утверждение о том, что функция Аккермана имеет значение для аргументов $m$ и $n$ (т.е. что рекурсия заканчивается). Так с какой стати мы должны из предпосылки $\forall (\tilde{m},\tilde{n})<(m,n) ~ \varphi(\tilde{m},\tilde{n}) \, \to \, \varphi(m,n)$ сделать вывод $\varphi(m,n)$ для любой пары чисел $(m,n)$? Есть ли какие-нибудь доводы в защиту этого кроме "математической интуиции"?

[migmit]

А при чём тут вообще интуиция? Принцип трансфинитной индукции тривиально доказывается. Не говоря уж о том, что индукция до $\omega^2$ - это ровно то же самое, что две обычных индукции.

Вот, смотрите: докажем, что функция Аккермана корректно определена для всех $m$ и $n$. Докажем это индукцией по $m$.

1) База индукции - $m=0$. Утверждение тривиально; в этом случае $A(m,n)=n+1$.

2) Переход, $m>0$. Индукционное предположение состоит в следующем: при всех $n$ значение $A(m-1,n)$ корректно определено. Обозначим это утверждение буквой $X$. Докажем, что при всех $n$ значение $A(m,n)$ также корректно определено. Воспользуемся индукцией по $n$.

2.1) База - $n=0$. Тогда $A(m, n)=A(m-1,1)$, что корректно определено по утверждению $X$.

2.2) Переход, $n>0$. Индукционное предположение состоит в том, что значение $A(m, n-1)$ корректно определено. Обозначим это утверждение буквой $Y$. Докажем, что значение $A(m, n)$ также корректно определено. Но оно равно $A(m-1, A(m, n-1))$; значение $A(m, n-1)$ корректно определено по утверждению $Y$, а всё в целом корректно определено по утверждению $X$.

Конечно, трансфинитная индукция до $\omega^2$ выглядит проще для тренированного глаза. Но если она вам не нравится - пожалуйста.

[epros]

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

2) Переход, $m>0$. Индукционное предположение состоит в следующем: при всех $n$ значение $A(m-1,n)$ корректно определено. Обозначим это утверждение буквой $X$. Докажем, что при всех $n$ значение $A(m,n)$ также корректно определено.

Ну, попробуйте доказать. В общем случае $A(m,n)$ определяется в том числе через $A(m,n-1)$, так что индукционное предположение $X$ Вам не поможет.

Возьмите в качестве примера какие-нибудь аргументы, для которых расчёт $A(m,n)$ заведомо превосходит наши вычислительные возможности. Скажем, как убедиться в том, что $A(9,1)$ вычислимо? По определению оно равно $A(8,A(9,0)) = A(8,A(8,1))$, но $A(9,0)$, оно же $A(8,1)$ - хрен знает как велико. И нам просто неоткуда взять утверждение $\forall n ~ \varphi(8,n)$, на которое мы могли бы опереться при доказательстве $\varphi(9,1)$.

[epros]

migmit, я хочу сказать, что идея Вашей "двуступенчатой" математической индукции в общем понятна, однако я не вижу способа её формализовать. Может подскажете?

Вот смотрите, что я пытаюсь проделать. Сначала перевожу определение функции Аккермана в аксиомы, записанные через предикат $\varphi(m,n)$ - который равносилен $\exists k ~ k=A(m,n)$:

a) $\forall n ~ \varphi(0,n)$
b) $\forall m ~ [\varphi(m,1) \to \varphi(m+1,0)]$
c) $\forall m,n ~ [\varphi(m+1,n) \land \forall k ~ \varphi(m,k) \to \varphi(m+1,n+1)]$

Потом я пытаюсь отсюда что-то вывести. Например:

1) $\forall m ~ [\varphi(m+1,0) \land \forall n ~ \varphi(m,n) \to \varphi(m+1,1)]$ (из c подстановкой $n=0$)
2) $\forall m ~ [\forall n ~ \varphi(m,n) \to \varphi(m+1,0)]$ (в предпосылку подставляем $n=1$, потом используем b)
3) $\forall n ~ [\varphi(1,n) \to \varphi(1,n+1)]$ (из c подстановкой $m=0$ и с учётом a)
4) $\varphi(1,0)$ (из b подстановкой $m=0$ и с учётом подстановки в a $n=1$)
5) $\forall n ~ \varphi(1,n)$ (математической индукцией из 3 и 4)
6) $\varphi(2,0)$ (из 2 подстановкой $m=1$ и с учётом 5)

и т.д. Но что-то мне никак не удаётся вывести что-нибудь вроде $\forall m,n ~ [\varphi(m,n) \to \varphi(m,n+1)]$, которое позволило бы применить математическую индукцию по $n$.

[migmit]

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

migmit,
Но что-то мне никак не удаётся вывести что-нибудь вроде $\forall m,n ~ [\varphi(m,n) \to \varphi(m,n+1)]$, которое позволило бы применить математическую индукцию по $n$.

Ну дык надо воспользоваться индуктивным предположением для $m$ тоже. Стандартный метаматематический факт: если мы можем доказать утверждение $B$, добавив в нашу теорию утверждение $A$ как аксиому — то мы можем в нашей исходной теории доказать утверждение $A\to B$.

Если вам этот факт не знаком — ну, попробуйте сделать закат солнца вручную: рассмотрите предикат $P(n)$, определённый как $\forall m ~ [(\forall k ~ \varphi(m, k)) \to \varphi(m+1, n)]$, и докажите его по индукции. Затем рассмотрите предикат $Q(m)$, определённый как $\forall n~\varphi(m,n)$, и докажите по индукции уже его (используя доказанный $P(n)$).

[epros]

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

Стандартный метаматематический факт: если мы можем доказать утверждение $B$, добавив в нашу теорию утверждение $A$ как аксиому — то мы можем в нашей исходной теории доказать утверждение $A\to B$.

Этот факт мне известен, но я не понял к чему Вы это.

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

Если вам этот факт не знаком — ну, попробуйте сделать закат солнца вручную: рассмотрите предикат $P(n)$, определённый как $\forall m ~ [(\forall k ~ \varphi(m, k)) \to \varphi(m+1, n)]$, и докажите его по индукции. Затем рассмотрите предикат $Q(m)$, определённый как $\forall n~\varphi(m,n)$, и докажите по индукции уже его (используя доказанный $P(n)$).

Ага, понятно. $\forall m,n ~ [(\forall k ~ \varphi(m, k)) \to \varphi(m+1, n)]$ доказывается индукцией по $n$, а потом $\forall m,n ~\varphi(m,n)$ отсюда доказывается индукцией по $m$. Интересно.

Выше Вы говорили, что "Принцип трансфинитной индукции тривиально доказывается". Это касается любого утверждения и индукции до любого ординала? В том числе до ординала $\varepsilon_0$? Просто я хочу понять, когда для доказательства конечности алгоритма нам может потребоваться более сильная аксиоматика, чем используемая в элементарной арифметике. С функцией Аккермана, как я понял, нам достаточно уметь ставить кванторы на натуральные числа...

[Someone]

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

Выше Вы говорили, что "Принцип трансфинитной индукции тривиально доказывается".

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

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

Это касается любого утверждения и индукции до любого ординала? В том числе до ординала $\varepsilon_0$?

В арифметике трансфинитной индукции как таковой нет вообще, но индукцию до любого ординала, меньшего $\varepsilon_0$, можно смоделировать многократной индукцией по натуральным числам. Технических деталей не знаю.

О трансфинитной индукции можно почитать в главе VII книги

К.Куратовский, А.Мостовский. Теория множеств. "Мир", Москва, 1970.

[epros]

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

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

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

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

но индукцию до любого ординала, меньшего $\varepsilon_0$, можно смоделировать многократной индукцией по натуральным числам

Я уже понял как смоделировать до любого ординала, меньшего $\omega^\omega$. Что касается $\varepsilon_0$, то я был бы сильно удивлён, если бы индукцию до него можно было смоделировать многократной индукцией по натуральным числам, ибо это означало бы возможность доказать непротиворечивость арифметики Пеано с помощью одной только математической индукции.

Последний вопрос также связан с вопросом конечности некоторых алгоритмов, в частности, с вопросом о том, является ли конечным алгоритм генерации последовательности Гудстейна. Любопытно, доказуемо ли это без использования достаточно сильной аксиоматики?

[migmit]

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

Этот факт мне известен, но я не понял к чему Вы это.

Дык к тому самому. Посмотрите на рассуждение в моём первом комменте. В пункте (2) имеется индукционное предположение $X$; добавьте его как аксиому к нашей теории; после этого переход доказывается индукцией (пункты 2.1 и 2.2).

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

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

Если обходится без аксиоматики - то, пардон, чем вообще пользоваться-то?

[epros]

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

Если обходится без аксиоматики - то, пардон, чем вообще пользоваться-то?

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

-- Пн июл 25, 2011 15:47:01 --

Кстати, касательно этого:

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

В пункте (2) имеется индукционное предположение $X$; добавьте его как аксиому к нашей теории; после этого переход доказывается индукцией (пункты 2.1 и 2.2).

Я Вас не понял тогда, поскольку Вы пренебрегли кванторами. Соответственно, я не понял, куда воткнуть это индукционное предположение $X$. Как выяснилось из рассмотрения утверждения $\forall m,n ~ [(\forall k ~ \varphi(m, k)) \to \varphi(m+1, n)]$, это самое индукционное предположение $X$ оказалось воткнутым в предпосылку импликации, которая, в свою очередь, закрыта ещё одним квантором. И если я правильно понимаю, то вытащить его оттуда никак нельзя. По крайней мере, в бескванторном варианте арифметики трюк с "двойной математической индукцией" оказывается нереализуемым.

[Someone]

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

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

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

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

Собственно говоря, вся "сильная аксиоматика" сводится к одной только аксиоме бесконечности. Если из ZFC исключить аксиому бесконечности и взамен добавить аксиомы индукции по натуральным числам (которые, естественно, надо определить), то получится аксиоматическая система, равносильная арифметике Пеано. Некоторые детали можно посмотреть, например, в §§ 6, 7 главы I книги

П.Дж.Коэн. Теория множеств и континуум-гипотеза. "Мир", Москва, 1969.

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

Что касается $\varepsilon_0$, то я был бы сильно удивлён, если бы индукцию до него можно было смоделировать многократной индукцией по натуральным числам

Я тоже был бы сильно удивлён, поскольку известно, что это невозможно.

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

Последний вопрос также связан с вопросом конечности некоторых алгоритмов, в частности, с вопросом о том, является ли конечным алгоритм генерации последовательности Гудстейна. Любопытно, доказуемо ли это без использования достаточно сильной аксиоматики?

Без "достаточно сильной" (выходящей за пределы стандартной аксиоматики арифметики) - не доказуемо.

[epros]

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

Без "достаточно сильной" (выходящей за пределы стандартной аксиоматики арифметики) - не доказуемо.

Под достаточно сильной аксиоматикой Вы здесь имеете в виду аксиому регулярности? Я слышал, что в ZF она эквивалентна аксиоме индукции (т.е. одна с другой взаимозаменяемы), коя последняя, собственно, и есть готовая трансфинитная индукция.

Однако ж в контексте вопроса о конечности алгоритмов это всё уж слишком сильные предположения. Принимая их, мы фактически декларируем, что трансфинитная индукция уже в готовом виде заложена в интуицию математиков. Но алгоритм, генерирующий последовательности Гудстейна, можно написать и не имея никаких понятий о свойствах множеств. Когда же мы пытаемся доказать конечность этого алгоритма, то оказывается существенным то, что на его аргументах мы можем определить отношение полного порядка, в соответствии с которым потом и применяем трансфинитную индукцию. С определением линейного порядка я не вижу никаких проблем: соответствующие аксиомы порядка (антисимметричность, транзитивность, тотальность) оказываются выводимы. Самое сложное, как я понимаю, заключается в том чтобы доказать существование минимального аргумента. Честно говоря, я даже не представляю себе, как это можно сформулировать, оставаясь в рамках арифметики (т.е. не прибегая к понятиям о множествах).

-- Вт июл 26, 2011 15:08:23 --

Хотя, сформулировать-то, наверное, можно. Если заменить понятие "множества" формулой арифметики $\varphi$, то утверждение о существовании минимального аргумента $x$ запишется как $\exists x ~ \varphi(x) \land \forall y ~ [\varphi(y) \to x \le y]$. Т.е. нам нужна соответствующая схема аксиом для каждой формулы арифметики. Вопрос только в том, откуда она возьмётся и почему это даёт нам право применять трансфинитную индукцию....

[Someone]

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

Под достаточно сильной аксиоматикой Вы здесь имеете в виду аксиому регулярности?

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

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

Я слышал, что в ZF она эквивалентна аксиоме индукции (т.е. одна с другой взаимозаменяемы), коя последняя, собственно, и есть готовая трансфинитная индукция.

Нет. Там же написано: "is a special case".

К.Куратовский, А.Мостовский. Теория множеств. "Мир", Москва, 1970.

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

Я бы сказал, что аксиомы индукции являются следствием аксиомы бесконечности. Но я здесь не знаю деталей. Я давал Вам ссылку на Коэна. Он, описывая аксиоматическую систему $Z_2$, которая фактически есть ZF без аксиомы бесконечности, считает нужным сформулировать аксиомы индукции по натуральным числам, чтобы получилась теория, равносильная арифметике Пеано. А в других местах мне встречалось утверждение, что арифметика Пеано равносильна ZFC, в которой аксиома бесконечности заменена утверждением, что каждое множество конечно, то есть, равномощно натуральному числу. Но я не понимаю, откуда возьмутся здесь аксиомы индукции.

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

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

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

[epros]

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

Нет. Там же написано: "is a special case".

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

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

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

Я бы сказал, что аксиомы индукции являются следствием аксиомы бесконечности.

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

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

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

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

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

[vek88]

Не шалю, никого не трогаю, починяю примус в своей теме Основания математики - элементарное рассмотрение. И оттуда иногда совершаю набеги на другие темы. Вот и сейчас ... хочу задать вопрос, надеюсь, к месту в данной теме.

А всем ли ясно, что определение И-, Л-выводов в К-системе можно сформулировать как трансфинитное определение? См. post284468.html#p284468

Кстати, честно скажу, что именно трансфинитный эквивалент упомянутого определения раскрыл мне интуицию и смысл, стоящие за трансфинитной индукцией. До этого трансфинитную индукцию воспринимал как нечто абсолютно абстрактное.

С учетом развития данной темы через некоторое время предполагаю рассмотреть это в своей теме Основания ....