 Herbrand (1932) gave a semantic characterization of what it means for a number theoretic function \(f\) to be defined by a system of equations \(\mathcal{E}(\psi_1,\ldots,\psi_n,\vec{x})\) by requiring both that there is a solution to the system and that \(f\) coincides with the function determined as \(\psi_1\) for every solution. He also suggested that this fact should be proved intuitionistically, which might in turn be thought to yield an effective procedure for computing the values of  \(f\).[13]  He did not, however, specify a formal system in which such a proof should be carried out. And thus Gödel suggested (essentially) the following syntactic replacement for Herbrand’s definition: