FOL Equivalence and Theorems

So, this is sort of a 2-in-1 question.

There is no sentence W of FOL such that: ∀yB(y)⟛¬W True or False?

Now, my interpretation is: There is no sentence W in FOL where for all y in the extension of B, they are all not equivalent to A. I think this is False because of course, since we are talking about all the vast possibilities both W and A can be, there has to be at least one sentence that disproves this. Right?

Then, for the formula D, ∃z(G(x)->G(z)) Both ∃xD and ∀xD are theorems.

∃xD is a theorem, but ∀xD is not.

∀xD is a theorem, but ∃xD is not.

Neither are theorems

Now, my interpretation is that there exists a z such that if x is in the extension of G, then z is in the extension of G.

From my understanding, a theorem is something that can be logically derived from the axioms of FOL. By that definition, I think none of them are theorems since in logic, the consequent can not prove anything about the antecedent. But tbh, I am not quite sure how theorems work in FOL(all textbooks I can find focus on TFL but I read somewhere that the laws of TFL also apply to FOL since FOL is "an extension of TFL" which is why I think this answer is correct.)

For your first sentence: ∀yB(y) - its negation is simply ¬∀yB(y) so substituting that for W satisfies your logical equivalence relation.

∀yB(y) ⟛ ¬¬∀yB(y)

Classical logic is bivalent (at least in its standard form) so for any given pair of sentences A, ¬A the truth of one entails the falsehood of the other and vice versa. This seems rather too simple: are you sure you have the question right?