Comment by LegionMammal978
Comment by LegionMammal978 3 days ago
As far as the arithmetic hierarchy goes, ω-consistency should just be a Π₂ sentence, with a universal quantifier over the encoded propositions, and an existential quantifier for the negated antecedent. All the implementation details of the encoding should be bounded. (Cf. ordinary consistency, which is the Π₁ sentence "there does not exist an encoded proof of a contradiction".)
Thanks, I'm on the same page. Where I'm still confused - so you add in an axiom representing w-consistency that says "for all P, if for all n there exists a proof of P(n) then there exists a proof of forall n . P(n)". But does this really mean the same thing as w-consistency? We still have no link between our provability predicate and truth. For instance there could be models where the witnessing proofs are non-standard.
So I'm not convinced this is enough to conclude "forall x . P(x)" within PA itself, which is what you need to prove Goodstein's. We can merely conclude that there exists a (possibly non-standard) n coding for that statement.