Variables and quantification
First-order predicate calculus allows variable arguments. These are quantified in two ways, existentially and universally.
The universal one is
"x [Expression] - means (forall (x) Expression).
For example,
"x [elephant(x) => has-tusks(x)].
The expression in [] is the scope of the x.
Existential quantification appears like
$x [elephant(x)] - means (exists (x) elephant(x))
There is at least one x that make elephant(x) true.