Доказуема ли в PRA вычислимость функции Аккермана?

[epros]

Господа, как Вы думаете, можно ли в примитивно-рекурсивной арифметике (PRA) доказать вычислимость функции Аккермана?

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

Вспомнив, что доказательная сила PRA характеризуется ординалом $\omega^{\omega}$, что больше $\omega^2$, можно прийти к выводу, что PRA, вроде бы, должна доказывать вычислимость $A(m,n)$. Однако механизм не вполне понятен. В частности, для каждого заданного $m$ функция $f(n) = A(m,n)$ является примитивно-рекурсивной, т.е. для её определения в PRA есть соответствующие аксиомы и, стало быть, её вычислимость тоже доказуема. Но из вычислимости каждой такой $f(n)$ для любого $m$ вроде бы не выводится общего утверждения о вычислимости $A(m,n)$, ибо в языке PRA нет кванторов! Как же быть?

[Dandan]

Из вашей ссылки на википедию:
PRA replaces the axiom schema of induction for first-order arithmetic with the rule of (quantifier-free) induction:
* From $\phi(0)$ and $\phi(x)$ $\to$ $\phi(S(x))$, deduce $\phi(x)$, for any predicate $\phi$.

Для вычислимости функции Аккермана вам явно прийдется использовать какую-то индукцию.

[epros]

Dandan в сообщении #342509 писал(а):

Из вашей ссылки на википедию:
PRA replaces the axiom schema of induction for first-order arithmetic with the rule of (quantifier-free) induction:
* From $\phi(0)$ and $\phi(x)$ $\to$ $\phi(S(x))$, deduce $\phi(x)$, for any predicate $\phi$.

Для вычислимости функции Аккермана вам явно прийдется использовать какую-то индукцию.

Хм. Тогда, наверное, нужно будет сначала откуда-то взять: "$A(m,n)$ вычислима $\to$ $A(m+1,n)$ вычислима".

[Профессор Снэйп]

Что значит "доказать вычислимость"? Как Вы собираетесь формулировать утверждение о вычислимости функции Аккермана на языке примитивно рекурсивной арифметики?

[epros]

Профессор Снэйп в сообщении #342578 писал(а):

Что значит "доказать вычислимость"? Как Вы собираетесь формулировать утверждение о вычислимости функции Аккермана на языке примитивно рекурсивной арифметики?

Это тоже часть вопроса, на которую интересно было бы получить ответ. В принципе, что такое "вычислимость" вроде бы понятно. Например, в синтаксисе арифметики Пеано утверждение о вычислимости функции $f$ я бы записал примерно так:
$\forall x \exists y~ y=f(x)$
(если есть синтаксис для записи самой функции $f$).
Но как это делается без кванторов не представляю. Наверное, должны быть какие-то средства.

Можно понимать вычислимость и в другом смысле: как наличие в теории доказательства $b=f(a)$ для любой константы $a$, где $b$ - тоже некоторая константа. Но чтобы такая вычислимость была выразима в языке теории, необходимо в языке теории записать предикат доказуемости. В арифметике Пеано такое возможно, в PRA - не уверен.

[Профессор Снэйп]

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

Это тоже часть вопроса, на которую интересно было бы получить ответ. В принципе, что такое "вычислимость" вроде бы понятно. Например, в синтаксисе арифметики Пеано утверждение о вычислимости функции $f$ я бы записал примерно так:
$\forall x \exists y~ y=f(x)$
(если есть синтаксис для записи самой функции $f$).
Но как это делается без кванторов не представляю. Наверное, должны быть какие-то средства.

Можно понимать вычислимость и в другом смысле: как наличие в теории доказательства $b=f(a)$ для любой константы $a$, где $b$ - тоже некоторая константа. Но чтобы такая вычислимость была выразима в языке теории, необходимо в языке теории записать предикат доказуемости. В арифметике Пеано такое возможно, в PRA - не уверен.

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

[epros]

Профессор Снэйп в сообщении #342685 писал(а):

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

В смысле? Есть понятие "частично-рекурсивной функции", которое по-сути означает, что в нашем распоряжении есть алгоритм, определяющий способ вычисления значений функции. И всё, конечность этого алгоритма не гарантируется. То, что функция Аккермана частично-рекурсивная, доказательства не требует, это ясно из её определения. И есть понятие "общерекурсивной функции" , каковые суть подмножество частично-рекурсивных, но ОПРЕДЕЛЁННЫЕ для каждого аргумента. А вот это для функции Аккермана уже не очевидно.

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

[Профессор Снэйп]

Увы, действительно бред...

[epros]

Профессор Снэйп в сообщении #342724 писал(а):

Увы, действительно бред...

Поясните плизз.
Вот смотрим, хотя бы, здесь:

"A function which is defined for all possible arguments is called total. If a computable function is total, it is called a total computable function or total recursive function."

Что здесь не так?

[Dandan]

мне тоже не понятно, в чем бред, вполне резонный вопрос.

[Профессор Снэйп]

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

If a computable function is total, it is called a total computable function or total recursive function.

То есть "computable function" не обязана быть "total", не так ли?

-- Чт авг 05, 2010 23:21:30 --

Вы что хотите доказать: что функция total, или что она computable?

[epros]

Профессор Снэйп в сообщении #342788 писал(а):

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

If a computable function is total, it is called a total computable function or total recursive function.

То есть "computable function" не обязана быть "total", не так ли?

-- Чт авг 05, 2010 23:21:30 --

Вы что хотите доказать: что функция total, или что она computable?

Ну, я же сказал, что меня интересует total computable. При том, что computable она согласно определению, остаётся доказать что total.

Я понял, что невольно сбил Вас с толку, заговорив "в прозе" о "вычислимости" - Вы решили, что (partial) computable function - это всё, что мне нужно. Нет, мне нужна вычислимость для КАЖДОГО аргумента. Меня как раз несколько сбивает с толку такое определение "вычислимости", которое предполагает возможность неразрешимости вычисляющего алгоритма.

[Профессор Снэйп]

Ох, ох, ох...

То есть, насколько я понял, Вы хотите примерно следующее:

1) К языку примитивно рекурсивной арифметики добавляем символ трёхместного предиката $A(x,y,z)$.

2) К аксиомам PRA добавляем определение функции Аккермана: $A(0,x,y) \leftrightarrow (y = s(x))$, $A(s(x),0,y) \leftrightarrow A(x, s(0), y)$ и $(A(s(x),y,t) \mathop{\&} A(x,t,z)) \rightarrow A(s(x), s(y), z)$. К схеме индукции добавляем формулы, построенные по той же схеме и содержащие $A$..

3) После этого (используя схему индукции) в PRA можно будет доказывать все равенства вида $A(\mathbf{n}, \mathbf{m}, \mathbf{k})$ для $n,m,k \in \mathbb{N}$, таких что $k = A(n,m)$. Формулу же $\forall x \forall y \exists ! z A(x,y,z)$ Вы, естественно, не докажете, просто потому, что в PRA нет правил работы с кванторами.

Вам этого достаточно или нет?

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

Вспомнив, что доказательная сила PRA характеризуется ординалом $\omega^\omega$, что больше $\omega^2$, можно прийти к выводу, что PRA, вроде бы, должна доказывать вычислимость $A(m,n)$.

Откуда Вы взяли этот термин --- "доказательная сила"?

В любом случае насчёт ординалов Вы поняли неправильно. Ординал $\omega^\omega$ --- это такой ординал, индукцией по которому можно доказать непротиворечивость PRA. В метаязыке, естественно, а не в языке самой PRA. А внутри PRA никаких трансфинитных индукций осуществлять нельзя!

P. S. Не понимаю, зачем Вам всё это.

P. P. S. Старайтесь всё же использовать термины грамотно. Вычислимость и всюду определённость --- совершенно разные вещи. Вычислимость означает наличие алгоритма вычисления (программы для машины Тьюринга, представления функции через элементарные путём суперпозиции, примитивной рекурсии и минимизации, etc...)

[Dandan]

ну чо, есть даже такой раздел логики http://en.wikipedia.org/wiki/Reverse_mathematics.
Правда тут без строгих определений далеко не зайдешь канешна.

[epros]

Профессор Снэйп в сообщении #343033 писал(а):

Вам этого достаточно или нет?

Нет, недостаточно. Этим Вы докажете, что для каждой пары аргументов в PRA есть средства для вычисления $A(m,n)$. Это и так очевидно, поскольку для любого $m$ функция $f(n) = A(m,n)$ является примитивно-рекурсивной, а значит в PRA есть средства для вычисления её значения для любого $n$. Но это не означает наличия в PRA доказательства общерекурсивности функции Аккермана.

Вы верно подметили, что доказательству общего утверждения мешает отсутствие кванторов. Но ведь должны же быть какие-то средства, их заменяющие? В частности, квантификация по всеобщности заменяется тем, что переменная оставляется свободной. С квантором существования непонятно. Как записать в PRA утверждение о существовании чего-либо, не зная явного вида этого чего-либо? Например, как записать утверждение о существовании нечётного совершенного числа? Или это невозможно?

Профессор Снэйп в сообщении #343033 писал(а):

В любом случае насчёт ординалов Вы поняли неправильно. Ординал $\omega^\omega$ --- это такой ординал, индукцией по которому можно доказать непротиворечивость PRA. В метаязыке, естественно, а не в языке самой PRA. А внутри PRA никаких трансфинитных индукций осуществлять нельзя!

Уточню: минимальный ординал, индукцией до которого доказывается непротиворечивость PRA. Это значит, что индукция до любого меньшего ординала не доказывает непротиворечивость PRA. А это в свою очередь означает, что реализуемость в PRA индукции до $\omega^2$ не приводит к противоречиям. Но если таковая индукция реализуема в PRA, то она докажет общерекурсивность функции Аккермана.

Профессор Снэйп в сообщении #343033 писал(а):

P. S. Не понимаю, зачем Вам всё это.

Вот Вы сходу заявили, что в PRA никаких трансфинитных индукций реализовать нельзя, а мне это не очевидно. У Вас есть доказательство? Мне это интересно, поскольку алгоритмическая разрешимость в некоторых случаях не очевидна, т.е. требует для своего доказательства достаточно сильной аксиоматики. Вот и хотелось бы понять НАСКОЛЬКО сильной аксиоматики. С примитивно-рекурсивными функциями всё ясно - их разрешимость доказывается обычной математической индукцией. Функция же Аккермана - один из простейших примеров общерекурсивной, но не примитивно-рекурсивной функции. С другой стороны, PRA - пример достаточно слабой теории, определяющей ВСЕ примитивно-рекурсивные функции. Поэтому вопрос о том, что она может сказать про алгоритмическую разрешимость не примитивно-рекурсивной функции, представляется мне естественным.

Профессор Снэйп в сообщении #343033 писал(а):

P. P. S. Старайтесь всё же использовать термины грамотно. Вычислимость и всюду определённость --- совершенно разные вещи. Вычислимость означает наличие алгоритма вычисления (программы для машины Тьюринга, представления функции через элементарные путём суперпозиции, примитивной рекурсии и минимизации, etc...)

Не придирайтесь по мелочам. Я использовал термин "вычислимость" в обычном (разговорном) смысле - как "возможность вычислить" (с помощью алгоритма), что означает нечто большее, чем просто НАЛИЧИЕ алгоритма. И я сразу же пояснил, что я имел в виду.