= 27d567bc2d48d9f40e9ccc20ea370b15)
orthonormal comments on Decision Theories, Part 3.75: Hang On, I Think This Works After All - 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 (45)
Proof that a Löbian cycle works out (hat tip, Eliezer and co.):
|- □A -> B
|- □B -> A
then
|- □(□A->B)
|- □□A->□B
|- □□A->A
|- □(□□A->A)
|- □□□A->□A
|- □A->□□A
|- □□□A->□□A
(apply Löb)
|- □□A
|- A
How about just,
(simple facts about PA:)
|- □(A ∧ B) -> (□A ∧ □B)
(apply the assumptions:)
|- □(A ∧ B) -> (B ∧ A)
|- □(A ∧ B) -> (A ∧ B)
(apply Löb:)
|- A ∧ B
Heh. Nice!
Am I supposed to be seeing lots of boxes here?
For once in Unicode's sad history, yes.
Yeah, it's the syntax "□A" for "there is a Gödel-numbered proof of A", and "|-" for "the following is provable".
Or is your browser showing a lot of junk instead of things that cash out to "it is provable that (a Gödel-numbered proof of A) implies B"?
Assuming the only operators you used were <box>, "|-" and "->" it all came through.
Note the key step,
|- □A->□□A
and why it's true even though
|- A->□A
is false: the formal system can see how to take a Gödel-numbered proof and replace all of the tokens with more complicated ones to get a Gödel-numbered proof of a Gödel-numbered proof, but it has nothing to work with if it starts by assuming just an object-level result.
What is special about A being provable that makes |- □A -> B provable, given only that it is true? For example, assume some A and B such that:
|- □A
|- B
|- □A -> B is trivial, as is |- □B -> A. (it follows from |-□A->A)
but |- □B is false.
Edit: changed some variables to be more clear.
Uh, I don't understand you. |- □A->□□A is a very special case.
That statement isn't true for general A!
□A->A, (true statement, assuming a sound system)
but not
|- (□A->A)
□(□A->A) (confirm these are false statements)
but
|- □□A->A
and
|- □A-> □□A (these are statements you have made)
|- □□A->A follows from the assumptions |- □A -> B and |- □B -> A; it's not a theorem in general.
Does it apply to (All A for which exist a B such that |- □A -> B and |- □B -> A)?
Is it possible to construct a B in general that meets those descriptions for an arbitrary statement? For example, B=" (a proof that a numbered proof of A implies B) and (a proof of a numbered proof of B implies A)" (B="( |- □A -> B) and ( |- □B -> A) ), or is a self-referential statement prohibited in sound systems?
Does B even have to be true, much less provable?
To the first question, yes. That's what the top comment in this sequence proved (and Benja's reply proved much more elegantly).
To the second question, self-referential statements can't be ruled out in sufficiently powerful formal systems- that's what Gödel's Incompleteness Theorem uses!
To the third, again, if any formal system proves □A -> B and □B -> A, then it proves A and B.
Consider the statement A "□A -> B and □B -> A" and the statement B "□A -> B and □B -> A and false"
Why are those two statements not provable in every system in which they can be written?