Comment by bubblyworld 3 days ago
Thanks, I see, so you pick some Gödel numbering and then quantifying over propositions is actually just quantifying over elements of the domain (and using your encodings of Sub(...) and Proves(...) and such). I see why that might have a chance of working, because it's now much higher up the arithmetic hierarchy.
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.
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".)