In this lengthy thread there's people bickering back and forth about the consistency of PA (Peano Arithmetic) and misunderstandings abound. In reading it I came to an understanding I found useful, though I am not certain of the correctness of. If we take a formalist perspective on the situation and understand mathematical propositions as statements about what happens when we manipulate strings given certain rules, there are two ways of interpreting "the consistency of PA". That is
(a) we can say "PA is consistent" means that any finite series of the applications of logical rules to the axioms of PA will not result in a contradiction, and
(b) the statement "PA is consistent" is rendered as "Con(PA)" appropriately formalized in some formal system (e.g. $\neg (0=1)$ in ZFC) and the question is about provability of "Con(PA)" in the given formal system.
It is my understanding (a) has not/cannot be demonstrated as any proofs done in any given formal system of the consistency of PA depend on the consistency of that formal system, which cannot be proved without resorting to a stronger system, and so on, but (b) has been demonstrated in various formal systems. It seems all disagreement as to whether "is PA consistent" is an open question is the result of one party referring to sense (a) and another referring to sense (b), where for sense (a) it is an open (and perhaps unanswerable) question while in sense (b), which is the usual meaning of an open question, it is definitively closed.
Does this analysis make sense? Am I missing anything important?