 The penultimate definition in Gödel’s list is the relation \(\mathsf{Proof}_{\mathsf{P}}(x,y)\) which holds between the Gödel number of a \(\mathsf{P}\)-formula \(\varphi\) and the Gödel number of a finite sequence of \(\mathsf{P}\)-formulas \(\psi_1,\ldots, \psi_n\) just in case the latter is a correctly formed derivation of the former from the axioms of \(\mathsf{P}\)—i.e.,