Why does "ForAll[a,b]" evaluate to b ?

Questions
1

I do not understand the very early evaluation of ForAll[a,b] to “b”. This should only be evaluated in this way, if it is sure, that “b” is free of “a” (FreeQ[b,a]==True).

ForAll[a, b]   
b

Due to the Attribute “HoldAll” of the symbol “ForAll”, it cannot be known, if “b” is finally free of “a”.

Attributes[ForAll]
{HoldAll, Protected, ReadProtected}

With the following input

b := x^2 + a^2
ForAll[a, b]

and the output:

ForAll[a, a^2 + x^2]

two questions are arising:

  • Why is “b” evaluated here, despite the Attribute “HoldAll”
  • After “b” is evaluated here, Mathematica recoginizes “b” as not free of “a”. Why is “b” assumed to be free of “a” in the first example ?

Thank you for any support.

Regards Uwe

2

Question two:
If b has no definition than the ‘value’ of ‘b’ is just symbolic ‘b’. And since ‘b’ does not contain ‘a’, so ‘b’ is independent of ‘a’, so it evaluates to ‘b’.

3

That is, what Mathematica is simply doing. But how can Mathematica know so early, that “b” is free of “a”, if “b” should not be evaluated due to the “HoldAll” Attribute ? The expression of “b” perhaps with an included “a” could be assigned later. That is, why the “HoldAll” -Attribute should work properly at this early moment to prevent Mathematica from early simplifications, which are not finally valid with a later assignment to “b”.
I hope, that the whole problem is clear, despite my poor german English.
Thank you for your answer.

4

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…

5

Even better example:

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

You want to evaluate ‘f’ for plotting, but using the local ‘x’, rather than the external 'x’… Hope you get the point… You need to evaluate the first argument, other you would not be able to any variable…

6

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

7

You need ‘f’ to evaluate of course… otherwise you would not be able to use variables! It is how you evaluate it that HoldAll changes…

8

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!

9

Thank you, I have to study your both examples, to really understand the difference between “substituted” and “evaluated” and to get a deeper understanding of the HoldAll attribute.

Best Regards Uwe

10

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

11

If you want to prevent any kind of evaluation in the input or output, you could use some kind of wrapper to do that for you:

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

Then define your function to act on expressions with head Formula:

In[2]:= foo[Formula[ForAll[a_, b_] && c_]] := 
 Formula[ForAll[a, b && c]] /; FreeQ[Formula[c], a]

The explanation for the behavior you saw in your test is two-fold. First, b_ is not “anything” assigned the name “b”, it is literally the expression Pattern[b, Blank[]]. It will match anything and assign it the name “b” when used in functions like MatchQ, Cases, ReplaceAll or in definitions, but it itself is just a Pattern expression with first argument b and second argument Blank[]. The reason ForAll[a_, b_] simplifies to b_ is because Pattern[a, Blank[]] does not literally appear in the expression Pattern[b, Blank[]]. Put another way, FreeQ[b_, sub_ /; sub === a_] gives True.

In summary, I think there are several definitions of “free” floating around here that need to be distinguished:

  • A Wolfram Language expression that is free of a pattern: FreeQ[expr, pattern]

  • A WL expression that is free of a literal subexpression: FreeQ[expr, sub_ /; sub === foo]

  • A formula in first-order logic that is free of certain variables

Hope this helps

12

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