Hacker News new | past | comments | ask | show | jobs | submit login

You can exclude any particular Gödel statement (a specific string of symbols), and as you're suggesting you can even exclude an infinite sequence of derived statements too, found by systematically adding the previous ones as axioms and applying a "Gödelisation" procedure to make another.

But "this statement is not provable" isn't a statement in the logic. It's an English language description of a type of statement, one which has certain self-referential characteristics and shows us the incompleteness of the logic.

There are an infinite number of statements in the logic which fit that type by having the relevant characteristics, and they aren't all obvious. The self-referential recursion implied in Gödel's construction is designed to make it obvious, but it can be encoded in less and less obvious ways while still containing an encoded image of themselves.

You can even get to statements where the self-reference is encrypted (using an actual encryption algorithm)! Only a mathematician with the "secret key", or a clever super-mathematician with amazing brute-forcing skills, would be able to read the statement and confirm that it's true!

And so "perceivable truth" is a thing too. Some truths are too complex for an ordinary mind to verify, yet still true.

To exclude all self-referential statements in the logic of type "this statement is not provable", you would need a decision procedure to tell you which statements in the logic are those.

Unfortunately you can't make such a decision procedure. It's very similar to Turing's halting problem. Just as you can't make a program which will take any input X and tell you if the program encoded as X will eventually terminate, you can't make a procedure which will take any statement S and tell you if it contains a fancy encoding of itself.

There's just no way to do it. The fact it can be related to Turing's halting problem, which is about real machines and real algorithms running on them, may give you some idea that the core principle can be grounded in something quite down to earth which affects practical applications.




Join us for AI Startup School this June 16-17 in San Francisco!

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: