A polynomial encoding provability in pure mathematics (outline of an explicit construction) (Q351271)

The starting point of the paper under review is 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, i.e. given an r.e. set \(S\) there exists a polynomial \(P_S(t,\vec x)\) with coefficients in \(\mathbb Z\) such that \(t \in S\) if and only if \(P_S(t,\vec x)=0\) has solutions \(\vec x\) in \(\mathbb Z\). The authors observe that the set of propositions provable in Zermelo-Fraenkel set theory is a recursively enumerable set. Thus under a suitable encoding, one can produce a polynomial equation which has a solution in \(\mathbb Z\) if and only if a parameter corresponds to a theorem in Zermelo-Fraenkel set theory, i.e. a polynomial equation as complicated as ``the whole of Mathematics''. The paper gives details of such an encoding.