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

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

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

Ещё с таким апломбом... Тут по мелочам не придирайтесь, здесь индукцию по ординалам не понимаю... А по мне, так тупое альтовство и ничего более: нагородили набор несвязанных друг с другом терминов, смысла которых в половине случаев не понимаете, и сидите дуете щёки.

Осенью вернусь из отпуска в институт --- покажу эту тему всему отделу математической логики. Если хоть один человек скажет мне, что афтар прав а я не прав со своими наездами, обязуюсь торжественно съесть какую-нибудь шляпу.

[Dandan]

У вас запущенное ЧСВ http://lurkmore.ru/%D0%A7%D0%A1%D0%92. И это не зависит от того, кто прав а кто нет.

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

Думаю, что всё же зависит...

Вы же, наверное, если заболеете, не пойдёте лечится к лётчикам в аэропорт. А если полетите в отпуск на самолёте, не станете требовать, чтоб за пилотское кресло посадили врача из поликлинники. Уверен, что предпочтёте обратное: болезни пусть лечит врач, а самолётом управляет пилот. Пусть каждый занимается тем, чему он научен и в чём разбирается.

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

[epros]

Ёлы-палы, Профессор Снэйп, я не претендую на то, что я знаток теории вычислимости или на то, что я в чём-то категорически прав. Я просто задал вопрос. И если я вдруг в своём вопросе что-то некорректно сформулировал, так мы вроде бы с этим уже разобрались.

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

[epros]

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

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 нет правил работы с кванторами.

Если я понял правильно, то в беспредикатной форме, т.е. в нормальной форме Сколема, формула $\forall x \forall y \exists z A(x,y,z)$ запишется просто как $A(x,y,f(x,y))$, где $f$ - это новый функциональный символ (собственно, он обозначает эту самую функцию Аккермана). После этого индукцией по переменной $y$ доказывается: $A(x,0,f(x,0)) \rightarrow A(x,y,f(x,y))$, затем доказываем переход через "предельный ординал": $A(x,y,f(x,y)) \rightarrow A(s(x),0,f(s(x),0))$ и, сопоставив последние две формулы, индукцией по переменной $x$ доказываем собственно $A(x,y,f(x,y))$. Насколько я понимаю, примерно такая схема доказательства как раз и является "реализацией в PRA трансфинитной индукции до $\omega^2$". Или я где-то ошибаюсь?

[Dandan]

Вообще говоря, такие специфические вопросы лучше задавать на mathoverflow, что я и сделал
http://mathoverflow.net/questions/35217 ... arithmetic

Говорят, что выразить тотальность функции Акермана можно, а вот вывести - нет.

[epros]

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

Вообще говоря, такие специфические вопросы лучше задавать на mathoverflow, что я и сделал
http://mathoverflow.net/questions/35217 ... arithmetic

Говорят, что выразить тотальность функции Акермана можно, а вот вывести - нет.

Ух, супер! Интересный нетривиальный вывод. К сожалению, моего уровня знаний не хватает для отчётливого понимания ответов
Я понял так, что если мы подставим Гёделевкий номер, присвоенный функции Аккермана, в Т-предикат Клини, то получим формулу в языке PRA, равносильную утверждению об общерукурсивности функции Аккермана. Правда я не до конца понял, что это за класс арифметической иерархии - $I - \Sigma_1^0$, который характеризует PRA и который свидетельствует о недоказуемости в ней указанной формулы.

Замечание касательно того, что доказуемость утверждения об общерекурсивности функции может зависеть от того, какой индекс (Гёделевкий номер?) для неё был выбран, также повергает меня в шок... Что бы всё это значило?

[epros]

Хочу добавить пояснения к ответу на вопрос, которые я добыл самостоятельно и которые, увы, в этой теме так и не прозвучали. Полагаю, что этого как раз не хватало для окончательного закрытия вопроса. Итак:

1) Специфическая особенность PRA, отличающая её, например, от арифметики Пеано первого порядка, заключается вовсе не в бескванторном синтаксисе языка. Существуют варианты формализации PRA в языке логики первого порядка, т.е. с кванторами. И формулы с кванторами без проблем переводятся в формулы без кванторов - путём сколемизации.

2) Особенность PRA заключается в ограничениях на применение математической индукции: PRA разрешает применять индукцию только к примитивно-рекурсивным формулам.

3) Именно по этой причине всюду определенность функции Аккермана недоказуема в PRA: Мы не можем применить правило индукции к соответствующей формуле.

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

Так что ларчик просто открывался...

[VPopov]

Профессор Снэйп писал:
Ой, ладно... Я этими темами полжизни занимаюсь, два диссера защитил. И вот смотрю и думаю, с какой стороны к этой галиматье подступаться... Пожалуй, что ни с какой не буду.

Как мне известно (я разрабатываю систему логики для теоретического естествознания, которую называю "реальной логикой") одним из достижений символической логики и, можно сказать, ее завершением выступила разработка понятия общерекурсивной функции (1934) и формулировка тезиса Чёрча (1936), утверждающего, что понятие рекурсивной функции является просто уточнением интуитивного представления об алгоритме. В общем, это идея "машины Тьюринга", которую Тьюринг и Пост завершили к концу 30-х. Т. о., мечта Лейбница ("давайте посчитаем и определим, кто из философов прав") сбылась. И если в математике обнаруживаются "неразрешимые алгоритмические проблемы", то, значит, это не математика,а открытая и динамическая семиотическая система. В научно-исследовательской программе "искусственный интеллект", поэтому, умными людьми ставится проблема не "существования искомого алгоритма", а поиска такого алгоритма, с помощью, кстати сказать, и нетрадиционных (немонотонных и нечетких) логик. А вообще, в математике как в языке для науки нужно срочно возвращаться к конструктивистским идеям Пуанкаре, Вейля и, конечно, Брауэра.

[Sonic86]

(Оффтоп)

VPopov в сообщении #566449 писал(а):

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

facepalm.jpg
Если прочесть определение термина "динамическая система", то сразу становится ясно, что то, что Вы пишите - ложь.
И вообще в целом опять фейлософия. Вот Вам проблема тогда:
http://ru.wikipedia.org/wiki/%D0%A1%D0% ... 1%82%D1%8C
Решите ее, что ли...