Adele_L comments on Intuitive cooperation - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (14)
[I tell you] X is analogous to "box X". Formally, the box is how we represent the statement (PA concludes X) inside the formal system S (which could also be PA). The brackets were meant to show which part corresponded with the box itself - the proper parentheses placement would be as you describe.
The turnstile means that S (or whatever system) concludes X. In other words, that X is provable in S. The box represents that (PA concludes X). So one difference is that it is for PA specifically. But more importantly, the box is a representation of that statement inside the system S. So the statement X must be encoded as a number - called the Godel nubmer of X. This is similar to how an image is encoded as a binary number on your computer. Then there is a function Bew - which is a 'compiler' for a number X. This is just a property of a natural number, carefully designed to represent the property that if n = encoding(X), then Bew(n) is true if PA proves the statement X. So "box X" means "Bew(encoding(X))".
It's like the difference between knowing you will do a certain thing - and you actually doing that thing. The box is what S thinks PA will do, and the turnstile is what it actually does.