  Here Con(PA) is a statement of arithmetic that expresses the informal statement that PA is consistent.[1] Under slightly stronger assumptions (for example, that PA is Σ01-sound[2]) one can strengthen the conclusion by adding that PA does not prove ¬Con(PA); in other words, under this stronger assumption, Con(PA) is independent of PA.  Thus, we have here a case of a statement of arithmetic (and, in fact, a very simple one) that cannot be settled on the basis of the standard axioms.  Moreover, the theorem is completely general—it holds not just for PA but for any sufficiently strong formal system T.