> Even what tromp is saying is quite strange to me
Indeed I mis-spoke. While for all n, PA can prove P(n),
it cannot prove "for all n: P(n)".
I don't know if there is a name for this, but it's not an omega-inconsistency.
It would only be omega-inconsistent to have PA contradict "for all n: P(n)", i.e. to prove "there exists an n: not P(n)".
Indeed I mis-spoke. While for all n, PA can prove P(n), it cannot prove "for all n: P(n)". I don't know if there is a name for this, but it's not an omega-inconsistency. It would only be omega-inconsistent to have PA contradict "for all n: P(n)", i.e. to prove "there exists an n: not P(n)".