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.
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?