You need HoldAll just to have local variables basically. Like plot:

x = 3
Plot[x^2, {x, 0, 1}]

Just to make sure the x in the first argument is interpreted as the variable x in the second argument (and not being replaced by 3). It works the same for ForAll…

Thank you particular for the second example. It shows, that "f" will be evaluated and "x" is not evaluated with external settings. But why this difference, I do not really understand. If I look to the description of the attribute: "HoldAll is an attribute that specifies that all arguments to a function are to be maintained in an unevaluated form" the different evaluation rules are not really emphasized.

But nevertheless I found, that I can use HoldForm[ForAll[a,b]] alternatively for my intention to analyze "a" and "b" before evaluation by Mathematica.

Thank you for your support. Regards Uwe

Perhaps the usage message should be clearer, but a symbol having the attribute HoldAll does not necessarily imply that the arguments will never be evaluated, it means that the unevaluated form of the arguments will be substituted as-is in its definitions rather than evaluated first, then substituted. For example,

In[1]:= SetAttributes[f, HoldAll];

In[2]:= f[x_Plus, y_] := f[Evaluate[Echo[x]], y]

In[3]:= f[2 + 2, 3 + 3]

4

Out[3]= f[4, 3 + 3]

Without the HoldAll attribute, the standard evaluation sequence would evaluate f to f, evaluate 2 + 2 to 4, and evaluate 3 + 3 to 6 to get f[4, 6] and then it would look for definitions that match f[4, 6], of which there are none:

In[4]:= Attributes[f] = {}

Out[4]= {}

In[5]:= f[2 + 2, 3 + 3]

Out[5]= f[4, 6]

So in general you should not expect symbols with the HoldAll attribute to have no evaluation, just non-standard evaluation. Hope this helps!

The same problem, as I described above in the main entry, but now from another viewpoint: I want to implement the general wellknown rule for quantifiers:

And[ForAll[a_, b_], c_] -> ForAll[a, And[b, c]] /; FreeQ[c, a]

In this context, I tested the following expression:

expr := HoldForm[ForAll[a_, b_]]
ReleaseHold[expr]
b_

In this example the meaning of the pattern "b_" should be: "Anything" assigned the name "b".

How can Mathematica assume, that the pattern for "Anything" called "b" is free of "a_ ", so that the simplification to "b_" is valid ? Due to this short example, I guess that something goes wrong with the evaluation of "ForAll[]"

Regards Uwe

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