@kolyanchi1

Доказать, что предикат ¬¬B⊃B является (или не является) (примитивно) рекурсивным:
«х есть геделев номер частного случая схемы логических аксиом (10)»
Не пойму с чего подходить к доказательству. Буду рад любой помощи!

0

@3D Homer

Во-первых, задание должно формулироваться так: "Доказать, что следующий предикат является (или не является) (примитивно) рекурсивным: «х есть геделев номер частного случая схемы логической аксиомы (10) ¬¬B⊃B»".

Что вы знаете про примитивную рекурсивность предикатов вида "x есть геделев номер..." и про примитивно рекурсивные функции вообще?

0

@kolyanchi1

3D Homer, Я пробовал читать мендельсона по этим темам, но не уверен, что все понял. Еще отсюда читал инфу http://it.kgsu.ru/TI_6/rec_011.html

0

@3D Homer

С примитивно рекурсивными функциями (ПРФ), как и с машинами Тьюринга, есть довольно длинная последовательность рассмотрения все более сложных функций. Ее цель состоит в том, чтобы убедить читателя, что все это можно выразить ПРФ. Так, сначала показывается, что все знакомы арифметические функции — ПРФ, затем описывается, как представлять числами последовательности, показывается, что основные функции на последовательностях — ПРФ, затем рассматривается арифметизация логического синтаксиса, то есть представление формул числами, и доказывается, что все основные функции для анализа формул — ПРФ. Это действительно должно описываться в Мендельсоне, а также в следующих книгах:

Верещагин Н. К., Шень А. Лекции по математической логике и теории алгоритмов. Часть 3. Вычислимые функции. 4-е изд. М.: МЦНМО, 2012.

Булос Дж., Джеффри Р. Вычислимость и логика. — М.: Мир, 1994. Особенно глава "Арифметизация синтаксиса" или что-то в этом роде.

Результат состоит в том, что почти все нормальные функции являются ПРФ. Всюду определенные не-ПРФ нужно специально строить. Правда, все ПРФ всюду определенные. Интуитивно, операция примитивной рекурсии соответствует циклу for, но не while. Все, что можно вычислить в современном языке программирования с помощью for, можно выразить и через ПРФ. В частности, распознавание того, формула имеет вид той или иной схемы.

1