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.

Pentashagon comments on How to cheat Löb's Theorem: my second try - Less Wrong Discussion

14 Post author: Benja 22 August 2012 06:21PM

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

Comments (25)

You are viewing a single comment's thread.

Comment author: Pentashagon 25 August 2012 11:16:14PM *  1 point [-]

First, assume the existence of up(n) that replaces K with K+1 in the godel number of a sentence.

Let C="#[up(&'If K>0, and PPT.2 |- #[&C], then #[down(C)]')]" so the axiom "If K>0, and PPT.2 |- #[&C], then #[down(C)]" implies #[down(#[up(&'If K>0, and PPT.2 |- #[&C], then #[down(C)]')])] and cancelling the ups and downs shows we've just proven our own consistency.

I probably butchered the syntax, but couldn't something similar to this be used put Löb's theory back in business?