You're looking at Less Wrong's discussion board. This includes all posts, including those that haven't been promoted to the front page yet. For more information, see About Less Wrong.

MrMind comments on You only need faith in two things - Less Wrong Discussion

22 Post author: Eliezer_Yudkowsky 10 March 2013 11:45PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Article Navigation

Comments (86)
Tags: faith

Comments (86)

You are viewing a single comment's thread.

Comment author: MrMind 11 March 2013 09:24:09AM 0 points [-]

Work is ongoing on eliminating the requirement for faith in these two remaining propositions. For example, we might be able to describe our increasing confidence in ZFC in terms of logical uncertainty and an inductive prior which is updated as ZFC passes various tests that it would have a substantial subjective probability of failing, even given all other tests it has passed so far, if ZFC were inconsistent.

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.

Comment author: Eliezer_Yudkowsky 11 March 2013 06:04:53PM 2 points [-]

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.

Comment author: ryujin 12 March 2013 11:40:28PM 0 points [-]

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

Comment author: Eliezer_Yudkowsky 12 March 2013 11:42:27PM 2 points [-]

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).

Comment author: ryujin 12 March 2013 11:50:39PM 1 point [-]

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!

Powered by Reddit Powered by Reddit