On a Diophantine representation of the predicate of provability (Q2253864)

The authors of the paper under review construct a polynomial encoding provability in Gödel-Bernay axiomatic set theory. In other words, the authors explicitly construct a polynomial \(F(t,\bar x)\) with coefficients in \(\mathbb Z\) such that for \(a \in \mathbb N\) we have that \(F(a, \bar x)=0\) has solutions in \(\mathbb Z\) if and only if the formula with the sequence number \(a\) (under some enumeration of well-formed formulas) has a proof in Gödel-Bernay axiomatic set theory. The fact that such a polynomial can be constructed and a method for constructing it are derived from the proof by Yuri Matyasevich (building on results of Julia Robinson, Martin Davis and Hilary Putnam) of the fact that every r.e. set of integers is Diophantine (or existentially definable in the language of rings).