Comment by LegionMammal978

> On the first question, how do you encode omega-consistency as a formula of PA? Just curious, it's not at all obvious to me.

I was also wondering about that, but going by the Wikipedia definition, it doesn't seem too complicated: you say, "For all encoded propositions P(x): If for every x there exists an encoded proof of P(x), then there does not exist an encoded proof of 'there exists an x such that ¬P(x)'." That is, if you can prove a proposition for each integer in the metatheory, then quantifiers within the target theory must respect that.

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.

Reply View 2 replies

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".)

Reply View | 1 reply
- bubblyworld 2 days ago
  
  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.
  
  Reply View | 0 replies