Consistency of PA from a Formalist Perspective

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?

• Note for (b), if ¬CON(A) then A⊦CON(PA), also if CON(A), then for A⊦CON(PA) to be true, A need to be the stronger system.
– ℋolo
Jan 23, 2019 at 10:01
• I have a related question at math.stackexchange.com/questions/3084683/… Jan 23, 2019 at 16:45
• Your analysis is OK, but I don't think it's a very fruitful topic for MSE for the same reasons as stated in David Roberts's comments on the MO question you link to. Jan 23, 2019 at 21:38

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})$$.
• While I agree that if (a) is false then (b) is false, but strangely enough even if (b) is true (by normal standards of truth, that Cons(PA) is provable in some System X), (a) could be false. That is because both systems could be inconsistent so, (a) could be false, that is there is some derivation of an inconsistency in PA, and Cons(PA) could be provable in System X, because if System X is inconsistent, then $\neg$Cons(PA) and Cons(PA) are both provable. That is why I'm not sure if the question "is there a finite set of applications of logical rules to the axioms of PA that lead to a..." cont. Jan 24, 2019 at 19:36