Earlier I discussed the question of whether the encodings of the theorems of a formal system are an arithmetic set. We don’t yet have a formal system for arithmetic. That will come soon, but for now we do have a language and an interpretation, so we can ask about the true sentences. By sentence I mean a statement which is unconditionally true or false, since it has no free variables or parameters which need values to be assigned to them. The answer turns out to be no. This is a theorem of Alfred Tarski.
Tarski’s theorem is not easy to prove, but the idea behind it is fairly simple. Suppose the set of true sentences is arithmetic, i.e. that we have an expression meaning “… is the encoding of a true statement”. We already have, or rather know that there is, an expression meaning “… is the encoding of …”. With a bit of cleverness we can combine these to to create a sentence which asserts that it is false.