Proving a formula is valid

Question

Let a formula $A$, and a term $t$ such that $x\in FV(t)$. Show that $\varphi = A\{t/x\}\to \exists x (x=t\to A)$ is valid.

So let's assume by contradiction that the formula isn't valid. Therefore there's a structure $M$ and an interpretation $\rho$ such that:

$$[|A\{t/x\}|]^M_\rho = T \text{ and } [|\exists x(x=t\to A)|]^M_\rho = F$$

So for every $a\in D^M$ (the domain of $M$):

$$[|(x=t)\to A|]^M_{\rho[a/x]} = F$$

So,by definition of $\to$:

$$[|x=t|]^M_{\rho[a/x]} = T \text{ and } [|A|]^M_{\rho[a/x]} = F$$

From the first one we get that: $[|t|]^M_\rho = a$ and therefore from the second one we get $[|A\{t/x\}|]^M_\rho = F$ - Contradiction!

The Question
I have a problem with this proof: at first we said for every $a\in D^M$ but then we discovered that $[|t|]^M_\rho = a$! (Must be a specific $a$) - So it must be that the domain has the size of exactly $1$? Isn't it?

Notations
$A\{t/x\}$ - means that we replace the term $t$ with $x$ for formula $A$.
$\rho[a/x]$ - means that we update the interpretation $\rho$ such that $\rho(x) = a$.

Answer 1

Long comment

You are right.

The proof aims to show that $\varphi := A[t/x] → ∃y \ (y=t → A[y/x])$ is valid, i.e. true in every structure [I've slightly modified the formula, in order to avoid problems with the quantifier acting on the $x \in FV(t)$].

The proof is by contradicition, i.e. it considers $\lnot \varphi$ and shows that it is not satisfiable [if a formula is not satisfiable, then its negation (in this case the original formula) is valid].

But $\lnot \varphi$ is:

$A[t/x] \land \lnot ∃y \ (y=t → A[y/x])$,

i.e.

$A[t/x] \land \forall y \ (y=t \land \lnot A[y/x])$,

and the argument shows that it is not satisfiable in a domain with one element ($a \in D^M$).

But the "condition" : $\forall y \ (y=t)$ "forces" all the elements of the domain to be identical, and thus, if the formula is not satisfiable in a $1$-element domain, it is not satisfiable at all.