Why is it specified in the 2nd incompleteness theorem that a system of arithmetic cannot prove its own consistency? I have seen in places I have read about Godel's incompleteness theorem that the second incompleteness theorem can be summarized as saying:
No axiomatic system with sufficiently strong arithmetic can prove its own consistency.
Can someone explain what that means? I would think it is trivially the case that no system could prove its own consistency, since consistency and completeness are "meta" notions, and aren't formalized in the object language.
 A: As lemontree says in the comments, the axiomatic systems to which the incompleteness theorem applies are capable of discussing their own consistency, that's the whole reason this theorem is possible. This is done using the "sufficiently strong arithmetic."
The upshot of "sufficiently strong arithmetic," say first-order Peano arithmetic ("PA") to be specific, is that it lets you discuss the behavior of arbitrary Turing machines, including the Turing machine which prints out a list of all the theorems of PA. So you can discuss the statement "the Turing machine which prints out a list of all the theorems of PA never prints 'false,'" which is equivalent to the consistency of PA. The claim then is that PA can't prove this, although it can state it.
Note that in order to do this the axiomatic system must be computable in a suitable sense, so that one can actually write down this Turing machine. This is a crucial part of both the statement and proof of the incompleteness theorem and people always omit it when they state the theorem informally; without this condition the theorem is false. The incompleteness theorem does not apply to non-computable axiomatic systems, such as true arithmetic, the system whose axioms consist of all true statements about the natural numbers. True arithmetic can't discuss itself in the same way that Peano arithmetic can because it doesn't know what its own axioms are (and neither do we!) - this is Tarski's undefinability theorem.
