What is the reasoning behind making ForAll hold its arguments? I find this surprising and it causes behaviour that I found confusing. There are no other functions that I am aware of that deal with symbolic computation and hold their arguments.

The behaviour is documented:

The value of x in ForAll[x,expr] is taken to be localized, as in Block.

Here are some examples which I found confusing before realizing the HoldAll property:

In[94]:= Clear[x, z]

In[95]:= ForAll[x, x > -1, Abs[x] == x]
Out[95]= ForAll[x, x > -1, Abs[x] == x]

In[96]:= z = x
Out[96]= x

In[97]:= ForAll[z, x > -1, Abs[x] == x]
Out[97]= x > -1 \[Implies] Abs[x] == x

In[98]:= x = 1
Out[98]= 1

In[99]:= ForAll[x, x > -1, Abs[x] == x]
Out[99]= ForAll[x, x > -1, Abs[x] == x]

In[100]:= ForAll[z, x > -1, Abs[x] == x]
Out[100]= True

The two confusing points are that:

1. Even with z=x, ForAll[z, ...] behaved differently from ForAll[x, ...]. Of course this is because of the HoldAll. This bit me when I did something like ForAll[Variables[expr], expr > 0].

2. Now that we know that ForAll is HoldAll, we may assume that it is safe to use it with variables that have a value. Not so, because ForAll may evaluate to Implies, which is not HoldAll, like the majority of symbolic processing functions.

So is there anything special about ForAll (or Exists) that make it a good idea to have the HoldAll attribute, and wouldn't apply to functions such as Reduce, Solve, Integrate, etc.?