Является ли функция примитивно рекурсивной?

[TypucT]

Профессор Снэйп писал(а):

TypucT писал(а):

Формула $P$ разрешима в теории $K$, если $\vdash_K P$ либо $\vdash_K \neg P$. Т.е. $P$ можно доказать либо опровергнуть в $K$.

Первый раз встречаю термин "разрешимость" в таком смысле. Обычно сами теории на предмет разрешимости изучают...

В Мендельсоне на с. 159 вводится этот термин. Я так понимаю, чтобы не писать постоянно "невыводима и неопровержима".
Разрешимость формулы, конечно же, имеет смысл только относительно конкретной теории.

[TypucT]

Читая Роджерса "Теория рекурсивных функций и эффективная вычислимость" наткнулся на разбор в точности приведенной задачи на с.26. Любопытствующие могут убедиться, что функция $h(x)$ "примитивнорекурсивна, хотя мы не знаем, как построить верную схему". В сноске сказано, что "мы допускаем неконструктивные методы; мы используем правила и соглашения классической двузначной логики (как это практикуется в других частях математики)".