Thank you Ian for your workarround and particular for your distingtion according the understanding of "free". The behavior of your workarround seems to be very similar to "HoldForm[]":
In[163]:= SetAttributes[Formula, HoldAll];
foo[Formula[ForAll[a_, b_] && c_]] :=
Formula[ForAll[a, b && c]] /; FreeQ[Formula[c], a]
In[169]:= foo[Formula[ForAll[x, A] && B]]
Out[169]= Formula[ForAll[x, A && B]]
Now substituted "Formular" --> "HoldForm":
In[170]:= foo[HoldForm[ForAll[a_, b_] && c_]] :=
HoldForm[ForAll[a, b && c]] /; FreeQ[HoldForm[c], a]
In[171]:= foo[HoldForm[ForAll[x, A] && B]]
Out[171]= HoldForm[ForAll[x, A && B]]
where the expression can be released now for evaluation with "ReleaseHold[]"
The first two bulletins of your distingtion show how Mathematica is interpreting the word "free of", I guess due to the internal structure and philosophy of the WL. But the third interpretation is that, what is really needed in symbolic mathematics.
Because of that difference, it is difficult, to implement rules for quantifiers in predicate logic with Mathematica in an intuitive symbolic way.
But nevertheless, thank you for your help
Regards Uwe