DR(B) = C is easily seen to be false, since DR always defects (by definition), and in general, ~X is logically equivalent to X → False. So we take X to be the statement from the line above, and place DR(B) = C for False.
Oh, so it’s equivalent to “S⊢¬□(DR(B=C))”. Everything makes sense now. At first I thought you were saying it was equivalent to the claim “to say B(DR=D), we would need S⊢¬□(DR(B=C))”, and I was confused.
DR(B) = C is easily seen to be false, since DR always defects (by definition), and in general, ~X is logically equivalent to X → False. So we take X to be the statement from the line above, and place DR(B) = C for False.
Sorry that wasn’t more clear.
Oh, so it’s equivalent to “S⊢¬□(DR(B =C))”. Everything makes sense now. At first I thought you were saying it was equivalent to the claim “to say B(DR =D), we would need S⊢¬□(DR(B =C))”, and I was confused.