Goodstein is definable, it just can’t be proven total. If I’m not mistaken, all Turing machines are definable in PA (albeit they may run at nonstandard times).
So I gather we define a Goodstein relation G such that [xGy] in PA if [y = Goodstein(x)] in ZFC, then you’re saying PA plus the axiom [not(exists y, (256Gy and exists z, (yGz)))] is inconsistent but the proof of that is huge because it the proof basically has to write an execution trace of Goodstein(Goodstein(256)). That’s interesting!
Given that we can’t define that function in PA what do you mean by Goodstein(256)?
Goodstein is definable, it just can’t be proven total. If I’m not mistaken, all Turing machines are definable in PA (albeit they may run at nonstandard times).
So I gather we define a Goodstein relation G such that [xGy] in PA if [y = Goodstein(x)] in ZFC, then you’re saying PA plus the axiom [not(exists y, (256Gy and exists z, (yGz)))] is inconsistent but the proof of that is huge because it the proof basically has to write an execution trace of Goodstein(Goodstein(256)). That’s interesting!