On a Diophantine representation of the predicate of provability

Обозначим через $\mathcal P$ исчисление предикатов первого порядка с фиксированным бинарным предикатом. Пользуясь развитой в работах по десятой проблеме Гильберта техникой диофантова кодирования, мы строим полином $F(t;x_1,\ldots,x_n)$ с целыми рациональными коэффициентами такой, что при подходящей нумерации формул теории $\mathcal P$, формула под номером $t_0$ доказуема в $\mathcal P$ тогда и только тогда, когда уравнение
$$F(t_0;x_1,\ldots,x_n)=0$$
разрешимо в целых числах. В качестве одного из приложений этой конструкции описывается класс диофантовых уравнений, для доказательства неразрешимости которых в целых числах необходимо привлечь дополнительную аксиому теории иножеств, например, аксиому о существовании недостижимых кардиналов. Библ. – 14 назв.