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?
Because we know the exact sentence $\text{Con}(\text{PA})$, we know that if (a) was false then (b) would also be false. Any counterexample to (a), if written down, would immediately lead to a counterexample to (b), that is, it would show $\lnot \text{Con}(\text{PA})$.
The deeper issue in threads about "is PA consistent?" is whether that quoted question should be judged by the same standards as other mathematical knowledge, or whether there are somehow stronger standards that should be applied.
By normal mathematical standards of justification, the question "is PA consistent" is settled. But if we raise the burden of proof for that specific question high enough, we can make it impossible to settle.