Возведение в степень в арифметике Пеано

[Padawan]

Можно ли в формальной арифметике Пеано (с сигнатурой $0, s, +, \cdot$) записать формулу $P(x,y,z)$, выражающую, что $x^y=z$ ?

[bot]

А формула в сигнатуре $(0,s, +)$, выражающая, что $x\cdot y=z $ есть? Или иначе, что такое формула?

[Padawan]

bot в сообщении #1196992 писал(а):

А формула в сигнатуре $(0,s, +)$, выражающая, что $x\cdot y=z $ есть?

Не знаю. Формула - правильно построенное выражение из символов данной формальной системы.

[Someone]

Padawan в сообщении #1196991 писал(а):

Можно ли в формальной арифметике Пеано (с сигнатурой $0, s, +, \cdot$) записать формулу $P(x,y,z)$, выражающую, что $x^y=z$ ?

Говорят, что можно. Но я эту формулу не видел.

bot в сообщении #1196992 писал(а):

А формула в сигнатуре $(0,s, +)$, выражающая, что $x\cdot y=z $ есть? Или иначе, что такое формула?

Говорят, что нет (арифметика Пресбургера).

[Sonic86]

А что такое формула?
Кванторы там допустимы или нет?
Если допустимы, то, если я правильно понял, это - результат Матиясевича (см. Десятая проблема Гильберта, 2-я глава про диофантовость множества $\{x,y,z:x^y=z\}$)
Если кванторы недопустимы, то мне кажется, что нет ($x^x$ слишком быстро растет)

[Padawan]

Sonic86 в сообщении #1197032 писал(а):

Кванторы там допустимы или нет?

Да, допустимы. По-моему понятие "формула" имеет четкое индуктивное определение, которое много где приводится.

[Xaositect]

Там все достаточно просто. Мы кодируем кортеж чисел одним числом (https://en.wikipedia.org/wiki/G%C3%B6de ... 2_function), и записываем формулой факт, что кортеж представляет собой некоторое вычисление (например, в случае $x^y$ - что каждый следующий элемент получается из предыдущего умножением на $x$).

[bot]

В таком случае, в чём отличие от умножения? Там каждый следующий элемент получается прибавлением икса. Именно потому я и спросил

bot в сообщении #1196992 писал(а):

А формула в сигнатуре $(0,s, +)$, выражающая, что $x\cdot y=z $ есть?

[Xaositect]

Там нет возможности закодировать кортеж одним числом.

[mihaild]

Sonic86 в сообщении #1197032 писал(а):

результат Матиясевича

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

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

[Padawan]

Xaositect
Не могу понять, как использовать кодирование $n$-ок, чтобы построить нужную мне формулу. Объясните поподробнее, пожалуйста.

[Xaositect]

Смотрите. Трюк Геделя с $\beta$-функцией говорит, что есть формула $Beta(x, y, z, v)$ такая, что для любого кортежа $a_1, \dots, a_p$ существуют числа $N, M$, для которых $Beta(N, M, i, a)$ истинна тогда и только тогда, когда $a = a_i$.
Дальше, можно легко записать $a_0 = 1, a_{i + 1} = a_i x$, а именно $Beta(N, M, 0, 1)$ и \forall i < y\, \exists a b: Beta(N, M, i, a) \wedge Beta(N, M, i + 1, b) \wedge b = a \cdot x$.
При таких условиях $\Beta(N, M, y, z)$ истинно тогда и только тогда, когда $z = x^y$.
Осталось только кванторы расставить.

[Sonic86]

(mihaild)

mihaild в сообщении #1197147 писал(а):

Sonic86 в сообщении #1197032 писал(а):

результат Матиясевича

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

Матиясевич Десятая проблема Гильберта писал(а):

Глава 2
Диофантовость возведения в степень
...
... цель настоящей главы - установление диофантовости функции $b^c$. В другой терминологии это звучит как установление диофантовости множества троек

$$\{\langle a,b,c\rangle : a=b^c\}$$

...

mihaild в сообщении #1197147 писал(а):

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

Ну ОК

[mihaild]

Sonic86, да, я проврался, конечно. Диофантовость указанного множества неочевидна даже по модулю $\beta$-функции, по модулю $\beta$-функции очевидна только его перечислимость.
Но она тут и не нужна - $\Sigma_1$-выразимость любого перечислимого множества гораздо проще его диофантовости.

[Padawan]

Xaositect
$\beta$-функция Гёделя - это гениально! $\beta(x_1,x_2,x_3)=\operatorname{rem}(x_1,1+(x_3+1)\cdot x_2)$
$\beta(a,b,i)=c$ можно записать как

$$B(a,b,i,c)=\exists u (c+u'=(i'\cdot b)') \wedge \exists t (a=t\cdot(i'\cdot b)'+c)$$

И далее, как Вы написали

$$\exists N\exists M \big(B(N,M,0,1)\wedge \forall i \big(\exists v (i+v'=y)\to\exists a \exists b (B(N,M,i,a)\wedge B(N,M,i',b) \wedge (b=x\cdot a))\big)\wedge B(N,M,y,z)\big)$$

($u'$ это то же самое, что $s(u)$)