How about: The set of arithmetic theorems of any formal system is recursively enumerable, while the set of arithmetic truths is not. So any sound formal system must fail to prove some arithmetic truth. Martin