Многочлен, для которого сущ. корней недоказуемо и неопроверж

[AGu]

Помнится, где-то прошмыгивал конкретный пример многочлена с целочисленными коэффициентами, для которого существование целочисленных корней недоказуемо и неопровержимо в PA. Не поделитесь ссылочкой?

P.S. Честно пытался сам найти — не смог. Ни на dxdy, ни ваще в сетке. Видать, не по тем ключевым словам ищу. Вроде знаю, что тут диофантовый Матиясевич должен пересекаться с неполным Гёделем, но где?

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

Ну... Существует многочлен с целочисленными коэффициентами $p(x,y,z,x_1, \ldots, x_k)$, такой что

$$ \varphi_y(x) = z \Leftrightarrow \exists x_1 \ldots \exists x_k p(x,y,z,x_1, \ldots, x_k), $$

где $\varphi_y(x)$ --- частичная функция от одной переменной $x$, вычислимая на машине Тьюринга по программе с номером $y$. Этот многочлен Матиясевич как раз и придумал. (Вроде можно показать, что $k=27$, хотя точно не уверен).

Теперь пусть $y_0$ таково, что $\varphi_{y_0}(0), \varphi_{y_0}(1), \ldots$ --- гёделевские номера утверждений, доказуемых в ZFC, а $z_0$ --- гёделевский номер утверждения о непротиворечивости ZFC. Тогда многочлен $p(x,y_0,z_0,x_1,\ldots,x_k)$ --- то, что Вас интересует

-- Ср дек 09, 2009 19:10:12 --

Или Вас совсем конкретный пример интересует, с конкретными числами-коэффициентами? Тогда не знаю

[AGu]

Ура, теперь я отчетливо вижу искомое пересечение. Спасибо, Профессор!
Теоретически я удовлетворен. Осталось удовлетвориться практически.
Хотелось бы увидеть такой многочлен чиста конкретно (и чиста для фана, разумеется).
Вроде бы, он где-то был явно выписан, и эта запись, вроде бы, помещалась на страницу...
Не обязательно тот самый многочлен $p(x,y_0,z_0,x_1,\dots,x_k)$,
можно и любой другой, но с таким же логическим свойством...

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

Или Вас совсем конкретный пример интересует, с конкретными числами-коэффициентами?

Да-да, именно этого и хочется.

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

AGu в сообщении #269457 писал(а):

Хотелось бы увидеть такой многочлен чиста конкретно (и чиста для фана, разумеется).

Эх... Сколько людей при мне чисто для фана начинали писать программу для универсальной машины Тьюринга (то есть программу, вычисляющую $\varphi_y(x)$ как функцию от двух переменных). До конца не дошёл ни один

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