On a~Diophantine representation of the predicate of provability

M. Carl ; B. Z. Moroz

Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part XII, Tome 407 (2012), pp. 77-104

Résumé

Let $\mathcal P$ be the first order predicate calculus with a single binary predicate letter. Making use of the techniques of Diophantine coding developed in the works on Hilbert tenth problem, we construct a polynomial $F(t;x_1,\ldots,x_n)$ with integral rational coefficients such that the Diophantine equation $$ F(t_0;x_1,\ldots,x_n)=0 $$ is soluble in integers if and only if the formula of $\mathcal P$, numbered $t_0$ in the chosen numbering of the formulae of $\mathcal P$, is provable in $\mathcal P$. As an application of that construction, we describe a class of Diophantine equations which can be proved insoluble only under some additional axioms of the axiomatic set theory, for instance, assuming existence of an inaccessible cardinal.