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