= 27d567bc2d48d9f40e9ccc20ea370b15)
Unless I've missed something, it is easy to exhibit small formal systems such that the minimum proof length of a contradiction is unreasonably large. E.g. Peano Arithmetic plus the axiom "Goodstein(Goodstein(256)) does not halt" can prove a contradiction but only after some very, very large number of proof steps. Thus failure to observe a contradiction after small huge numbers of proof steps doesn't provide very strong evidence.
Given that we can't define that function in PA what do you mean by Goodstein(256)?
= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
= f037147d6e6c911a85753b9abdedda8d){kind=logo}
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!