Comment by ryujin on You only need faith in two things · 2013-03-12T23:50:39.865Z · LW · GW

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!

Comment by ryujin on You only need faith in two things · 2013-03-12T23:40:28.621Z · LW · GW

Given that we can't define that function in PA what do you mean by Goodstein(256)?