Meaning of free variables Consider the statement:
$$\forall x [x=x] \tag1$$
And the statement:
$$x=x \tag2$$
Statement $(1)$ is easily understood: for every $x$ in the universe, $x=x$ is true.
However, what does statement $(2)$ mean? What even is $x$? What is the statement claiming? How does one decide is truth? I have seen theorem-proving machines remove and adjoin $\forall x$ at will; how is this justified?
 A: 
what does the statement $x=x$ mean?

The details of the semantics of the language dictate "how to read" a formula with free variables.
Usually, we use a "context" [technically called: variable assignment function], i.e. a way to assign a "temporary meaning" to the free variables.
We can compare a free variable to a pronoun of natural language.
To assert "$x$ is red" is the same as "it is red": its meaning depends on what the context assigns to "it".
In the same way, we can read $x=x$ as follows: "it is equal to itself", that is true for whatever "object" we will assign to "it" as reference.

Proof systems for first-order logic have rules for adding and removing the quantifiers.
The first one:

$\forall x \varphi \vdash \varphi[x/a]$,

corresponds to the specialization principle : "what holds for all, holds for any".
And the same intuition supports the corresponding introduction rule (aka: generalization rule):

if $Γ ⊢ \varphi[x/a]$, then $Γ ⊢ ∀x \varphi$, provided that $x$ is not free in $\Gamma$;

"if something holds for an arbitrary object, then it holds for all objects".


But the example can be a little bit misleading: the fact that $x=x$ and $\forall x (x=x)$ are "equivalent", does not mean that this is so in general.
Compare $x=0$ and $\forall x (x=0)$ in $\mathbb N$. The first one is sometime true (if we assign to $x$ the "temporary meaning" $0$) and sometime false (for $x$ meaning $1$) while the second is plainly false.
A: In "Understanding Identity Statements" by Thomas Morris you will find a discussion of "$x = x$" in the context of the famous examples,

Hesperus is Phosphorus
Phosphorus is Phosphorus

Initially, the first example does not seem problematic since it seems to be conveying the information that two names denote a single object.  The truth of the statement seemingly resides with an answer to the question of whether or not it is indeed the case that the two names denote a single object.  But, the second example introduces a problem.
Presumably, one needs no account of truth beyond the form of the statement to claim that the statement is true.  This is referred to as an analytical conception of truth, and is said to be based upon the meaning of words.  Unfortunately, a semantic conception of truth is presumably based upon denotations given through a satisfaction mapping.  And, while one can no more demonstrate the existence of zero than one can demonstrate a completed infinity, the received view of semantics in mathematics is Tarski's semantic conception of truth.
This means that "$x = x$" actually presents a problem in the foundation of mathematics that is masked by the first-order schema asserting the truth of every instance through the reflexive axiom.  The truth being asserted here is through an analytical conception and not a semantic conception.
In Frege's original formulation of mathematical logic, any statement containing a non-denoting term was simply false.  Hence, "$t = t$" could be a false statement if the term $t$ does not denote.  The modern logic with this semantics is called negative free logic.  One of the characteristics of negative free logic is the "identity of non-existents".  If you read Frege's first paper on arithmetic, you will find that he invokes this property to define the number $0$.  Using "$\neg ( x = x )$" as a concept with a vacuous extension, he had an "extension of a concept" that could be proven to be unique.  From this as a base case, he developed his definition of cardinal numbers.
In free logic, one speaks of "existential import".  The axioms of first order logic impose existential import in the quantifier rules.  So, there is no explicit relationship between identity statements and the semantic interpretation of an existential quantifier (think about Henkin arguments and models built from constants).  However, this relationship is restored by an axiom used by Tarski in his algebraization of first-order logic via cylindric algebras.
The axiom
$$
\forall x \forall y( x = y \leftrightarrow \exists z ( x = z \wedge z = y ) )
$$
serves to ensure that the correlate to identity for the algebraic presentation is transitive.  As can be seen from the syntax, the truth of an identity statement is now bound to an existential quantifier.  But, since cylindric algebras are motivated by first-order logic, an axiom corresponding to $\forall x ( x = x )$ will also be present.
