On a Diophantine representation of the predicate of provability

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.