Is $\exists x(x=a)$ a valid formula in first order logic with equality? Under Tarskian semantics, is $\exists x(x=a)$ true in every interpretation in first order logic (FOL) with equality? If so, could $\exists x(x=a)$ be considered a tautology?
This question was motivated by another which was closed for lacking clarity. Here I have attempted to add that clarity myself so that the same question can be useful to others who are wondering a similar thing.
This is a self answer question.
 A: A valid formula is true in every interpretation of FOL, and an invalid formula is false in at least one interpretation.
Assume that $\exists x(x=a)$ is invalid. Then $\forall x\lnot(x=a)$ must be true in some interpretation. Then if we instance $x$ to $a$ in the same interpretation ($a$ is already a name in the language), we get $a\neq a$ which is a contradiction. So it must be the case that $\exists x(x=a)$ is a valid formula.
$\exists x (x=a)$ is a valid statement because it is true in every interpretation. Some, but not all authors will refer to $\exists x (x=a)$ as a tautology as well, taking tautology to mean any true well formed formula. Others will use the word tautology in a more narrow sense, referring to statements which are true according to some truth-functional structure$^{[1]}$ (like a truth table).
A: Your question does not specify what $a$ is. The simpler case is if $a$ is a constant-symbol. Your posted answer is more or less correct for that case, but there are some issues. Firstly, it is not correct to write "$a≠a$" when referring to the element that $a$ is interpreted as in a structure $M$. Either write "$M ⊨ a≠a$" or "$a^M ≠ a^M$". Secondly, it is not a very good idea to prove that it is a tautology by proving that its negation is contradictory in every structure, because this relies on classical FOL semantics, which is unnecessary here. It is always better to rely on only the relevant aspects.
Here is a fully rigorous proof: Take any FOL structure $M$ over a language that has constant-symbol $a$. Then $M ⊨ a=a$, so $M[x:=a^M] ⊨ x=a$ and hence $M ⊨ ∃x ( x=a )$. Therefore, $∃x ( x=a )$ is an FOL tautology.
The other case is when $a$ is a variable. In this case, since $a$ is free in $∃x ( x=a )$, it is semantically interpreted as being universally quantified over the domain. That is, it is equivalent to $∀a ∃x ( x=a )$. That is how one should understand it, and indeed a deductive system for FOL that permits free variables in its theorems would allow you to prove the equivalence. But the completely semantic proof does not need to use that fact: Take any FOL structure $M$. For every element $c$ in $M$, we have $M[a:=c] ⊨ a=a$, so $M[a:=c][x:=c] ⊨ x=a$ and hence $M[a:=c] ⊨ ∃x ( x=a )$. Therefore, $∃x ( x=a )$ is an FOL tautology.
