@MoreAnonymous It is known that deciding truth of an arithmetical sentence is not a problem that can be solved recursively, but the goal of Goedel-encoding is to get encodings where operations on the strings are simple (often times e.g. primitive recursive).