Argument pattern behavior for built-in symbol

Question

I'm having troubles with this:

test1[forAll[t,x_]]:=x
test2[ForAll[t,x_]]:=x

While syntactically exact, test1 works and test2 does not:

?test1
(* test1[forAll[t,x_]]:=x *)

?test2
(* test2[x_]:=x *)

Why doesn't ?test2 output test2[ForAll[t,x_]]:=x?

Edit 2

For anyone interested - for yet unknown reasons - this and only this works as expected:

test3[ForAll[t,t_]]:=t

Edit 3

The legit working solution to non-standard evaluation traps like this is to use unambiguous pattern matching syntax that does not provide any hints to the system that this can be evaluated:

test2[(f:ForAll)[t,x_]]:=x

Answer 1

First of all, though SetDelayed (:=) has HoldAll attribute, it still evaluates its 1st argument in this case, this behavior has been discussed in this post. To be specific, when test2 is defined, the argument ForAll[t, x_] will be evaluated.

Now the question becomes

Why ForAll[t, x_] evaluates to x_?

and this has been explained in the Scope of the document of ForAll:

If the expression does not explicitly contain a variable, ForAll simplifies automatically:

ForAll[x, y == 0] 
(* y == 0 *)

In your case, x_ doesn't explicitly contain t, and it's automatically simplified, while t_ explicitly contain t so it's not. (Notice the FullForm of t_ is Pattern[t, Blank[]] i.e. a function with 2 arguments whose 1st agrument is an explicit t. )

To get the desired function definition, you can make use of Unevaluated:

ClearAll@test2    
test2[Unevaluated@ForAll[t, x_]] := x
DownValues@test2
(* {HoldPattern[test2[ForAll[t, x_]]] :> x} *)

test2[ForAll[t, t + t^2]]
(* t + t^2 *)

But notice this function still won't work as expected if the ForAll[…] evaluates to something else, for example:

test2[ForAll[t, x]]
(* test2[x] *)

If you want it to evaluate to x, then Unevaluated again or as mentioned in the comment above, use HoldFirst:

test2[Unevaluated@ForAll[t, x]]
(* x *)
SetAttributes[test2, HoldFirst]
test2[ForAll[t, x]]
(* x *)