= 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)
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?