Comment by dooglius 3 days ago
The interesting part to me (I have a background in both math+programming) isn't so much the encoding of computation but that one can work around the independence of goodstein's theorem in this self-referential way. I think this implies that PA+"PA is omega-consistent" can prove goodstein's theorem, and perhaps can more generally do transfinite induction up to epsilon_0? EDIT: I think just PA+"PA is consistent" is enough?
Unfortunately not, and apparently no other purely universally quantified formulas will do either (so this is a more general thing, not specific to Con(PA)): https://math.stackexchange.com/questions/5003237/can-goodste...
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.
> 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.
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.
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.
I also like the recursion. In essence, you're making a meta-proof about what PA proves, and given that you trust PA, you also trust this meta-proof.
> I think just PA+"PA is consistent" is enough?
It's not clear to me how. I believe PA+"PA is consistent" would allow a model where Goodstein's theorem is true for the standard natural numbers, but that also contains some nonstandard integer N for which Goodstein's theorem is false. I think that's exactly the case that's ruled out by the stronger statement of ω-consistency.
I think so, the math exchange post mentions that the PA + transfinite induction works on epsilon_0 proves PA. It seems likely to me that PA + PA is consistent would be able to prove transfinite induction on epsilon_0.
Asker of the SO question here: I edited the question to link to a few other answers on this kind of thing. Essentially, "PA is consistent" is not enough, but a "uniform reflection principle" that says "if PA proves something, it's true" is enough. I'm not 100% certain that this principle is equivalent to omega-consistency, but if I'm reading this correctly, it should be:
https://en.wikipedia.org/wiki/%CE%A9-consistent_theory#Relat...
The Wikipedia article says T is omega-consistent if "T + RFN_T + the set of all true sentences is consistent", which should mean the same thing as "T + RFN_T is true".