= 27d567bc2d48d9f40e9ccc20ea370b15)
MrMind comments on You only need faith in two things - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (86)
Would using the length of the demonstration of a contradiction work? Under the Curry-Howard correspondence, a lengthy proof should correspond to a lengthy program, which under Solomonoff induction should have less and less credit.
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)?
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!