Because the method of Gödel numbering was novel, and to avoid any ambiguity, Gödel presented a list of 45 explicit formal definitions of primitive recursive functions and relations used to manipulate and test Gödel numbers. He used these to give an explicit definition of a formula Bew("x") that is true if and only if "x" is the Gödel number of a sentence φ and there exists a natural number that is the Gödel number of a proof of φ. The name of this formula derives from "Beweis", the German word for proof.