On a diophantine representation of the predicate of provability

Abstract

Let 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’s tenth problem, we construct a polynomial F(t; x1, . . . , xn) with integral rational coefficients such that the Diophantine equation<br />F(t₀;x₁,…, x_n)=0<br />is soluble in integers if and only if the formula of P numbered t0 in the chosen numbering of the formulas of P is provable in P. As an application of that construction, we describe a class of Diophantine equations that can be proved insoluble only under some additional axioms of the axiomatic set theory, for instance, assuming the existence of an inaccessible cardinal. Bibliography: 14 titles.