Логика предикатов

[cyb12]

Можно ли формулой логики предикатов первого порядка выразить предикат

$$P(x)= \text{

в сигнатуре $\langle \mathbb{N}; <, =; +,-,\cdot,/\rangle$?

Или подобные рекурсии невозможно задать в логике первого порядка и нужно переходить во второй, взяв $\forall f$? Если да, то как (где?) это доказыватся?

[_hum_]

$\exists\, n\in \mathbb{N}\, (x = n!)$
Нет?

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

cyb12 в сообщении #550340 писал(а):

Можно ли...

Можно!!!

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

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

-- Вт мар 20, 2012 21:23:16 --

_hum_ в сообщении #550362 писал(а):

$\exists\, n\in \mathbb{N}\, (x = n!)$
Нет?

Нет. По условию операции взятия факториала нет в сигнатуре, так что и использовать в записи этот самый восклицательный знак нельзя.

Кстати, замечу, что условие на сигнатуру у топикстартера несколько избыточно. Факториал можно выразить уже в модели $\langle \mathbb{N}; +, \cdot \rangle$. Естественно, если рассматривать исчисление с равенством. Если нет, то надо ещё равенство в сигнатуру добавить.

-- Вт мар 20, 2012 21:29:52 --

Кстати, если добавить в сигнатуру ещё константу $1$, то утверждение $x = y!$ можно записать в экзистенциальном виде, то есть обойтись одними кванторами существования (и не использовать отрицаний). Это следует из решения десятой проблемы Гильберта и того факта, что предикат $x = y!$ рекурсивен.

[_hum_]

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

_hum_ в сообщении #550362 писал(а):

$\exists\, n\in \mathbb{N}\, (x = n!)$
Нет?

Нет. По условию операции взятия факториала нет в сигнатуре, так что и использовать в записи этот самый восклицательный знак нельзя.

Это понятно. Просто хотел подчеркнуть, что проблема вроде как сводится к проблеме выражения факториала.

[_hum_]

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

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

_hum_ в сообщении #550762 писал(а):

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

Да, достаточно.

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

Если интересует наиболее простое доказательство "с нуля"... Я вот сегодня немножко нетрезв, а завтра буду в другом состоянии и это самое доказательство в схематичном виде здесь изложу Если поступит заявка на такое изложение.

[_hum_]

Заинтересовался, кое-чего полистал. И вроде как идея проясняется, вот только для нее нужен ограниченный квантор общности ($\forall\, x \leq n $). В Боссе написано, что он выразим в исходной сигнатуре, но каким образом не пояснено. А в других источниках не нашел :(

[Joker_vD]

$$\forall x\leqslant n\; P(x) \equiv \forall x ((x<n) \vee (x=n) \to P(x))$$

[_hum_]

Joker_vD в сообщении #551076 писал(а):

$$\forall x\leqslant n\; P(x) \equiv \forall x ((x<n) \vee (x=n) \to P(x))$$

Неее... Нужно же ж через набор $\{+,\cdot, =, \exists\}$, в котором изначально присутствует только квантор существования.

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

_hum_ в сообщении #551088 писал(а):

Неее... Нужно же ж через набор $\{+,\cdot, =, \exists\}$, в котором изначально присутствует только квантор существования.

Да вроде нигде не сказано, что квантор всеобщности употреблять запрещается. По крайней мере, топикстартер такого запрета не провозглашал.

Если квантор всеобщности вдруг с какого-то перепуга запретить, то тогда я вижу путь только через теорему о диофантовом представлении...

[_hum_]

Профессор Снэйп
У Босса в Лекциях по математике (том 6, "От Тьюринга до Диафанта") говорится об арифметическом языке как языке $L_0 = \{+,\cdot,=,\exists\}$. И далее утверждается, что в нем выражаются $\{\wedge, \vee,\neq, \geqslant, >, |\}$ и даже (!) $\forall_{\leqslant }$. Насчет того, как выразить $\wedge$ и оcтальные пояснение есть, а вот насчет $\forall_{\leqslant }$ только "оказывается". Интуитивно кажется, что вероятно для этого берется какой-то арифметический факт, из выполнения которого для какого-нибудь одного $x$, $x > n$ вытекает невыполнение его для всех $x \leqslant n$.
Не могли бы Вы прояснить ситуацию?

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

_hum_ в сообщении #552067 писал(а):

У Босса в Лекциях по математике...

Я Босса, Шефа, Президента и других Главных Начальников не читал

На ум пока что приходит только теорема о диофантовом представлении. Но даже и тут есть одна загвоздка...

Нам надо выразить равенство $p = q$, где $p$ и $q$ --- многочлены с натуральными коэффициентами. Я не знаю, как именно выглядит многочлен $p - q$; вроде, кто-то где-то его выписывал в явном виде, но я явного вида в глаза не видел, знаю лишь о существовании многочленов. И вот тут если у многочлена $p-q$ свободный член равен нулю, то равенство $p = q$ легко выражается в $L_0$ и никаких проблем нет, а если свободный член $\neq 0$, то...

По идее, надо выразить в $L_0$ число $1$. Если начинать натуральный ряд с $0$, то этого сделать просто невозможно. А если с $1$, то не знаю...

[_hum_]

Да, скорее всего предполагается, что $\mathbb{N}$ начинается с единицы. Тогда все сходится - сама единица в $L_0 $ вместе с любой наперед заданной константой выражаются, и нет проблем с диофантовым представлением.
Но как все-таки в этом случае ограниченный квантор общности выражать, чтобы решить задачу с факториалом без задействования диофантова представления?

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

_hum_ в сообщении #552305 писал(а):

Тогда все сходится - сама единица в $L_0 $ вместе с любой наперед заданной константой выражаются...

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

[_hum_]

Единица выражается как решение (единственное в $\mathbb{N}$) уравнения $x^2 = x$. Нет?