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