validity of a formula with one existential quantifier and one variable Let $\sigma$ a dictionary without equlity symbol that contains at least one constant symbol. 
Let $\varphi$ a formula over $\sigma$ without quantifiers such that $FV(\varphi)=\{x\}$. 
Prove that: $\exists x\varphi$ is valid $\iff$ 
There exist $s_1,\dots,s_n$ ground terms over $\sigma$,  such that $\varphi[s_1/x]\lor\dots\lor\varphi[s_n/x]$ is valid.
My approach:
Suppose that there exist $s_1,\dots,s_n$ ground terms over $\sigma$,  such that $\varphi[s_1/x]\lor\dots\lor\varphi[s_n/x]$ is valid.
Let $\mathcal{M}$ a model and $v$ an interpretation in it.
Then $\mathcal{M},v\vDash\varphi[s_1/x],\dots,\varphi[s_n/x]$, so $\mathcal{M},v\vDash\varphi[s_i/x]$ for some $i$ $\implies \mathcal{M},v[\bar{v}(s_i)/x]\vDash\varphi$.
So there exists some $d\in D^\mathcal{M}$ such that $\mathcal{M},v[d/x]\vDash\varphi\implies\mathcal{M},v\vDash\exists x\varphi$.
For the other direction I only managed to observe that:
since $\varphi$ has no quantifiers and $FV(\varphi)=\{x\}$ we have that $x$ is the only variable that appers in $\varphi$.

I assume that in your notation, the statement "$\psi_1,\dots,\psi_k$ is valid" is equivalent to "$\bigvee_{i=1}^k \psi_i$ is valid". Is that right?
For the converse, suppose $\exists x\,\varphi(x)$ is valid. Consider the set of sentences $T = \{\lnot \varphi(t)\mid t\text{ is a ground term}\}$. Suppose for contradiction that $T$ is consistent. Then there is a model $\mathcal{M}\models T$. Let $\mathcal{N}$ be the substructure of $\mathcal{M}$ generated by the constants (with domain $\{t^{\mathcal{M}}\mid t\text{ is a ground term}\}$). For every ground term $t$, since $\varphi(t)$ is quantifier-free and $\mathcal{N}$ is a substructure of $\mathcal{M}$, $\mathcal{M}\models \lnot \varphi(t)$ implies $\mathcal{N}\models \lnot \varphi(t)$, so $\mathcal{N}\models \lnot \exists x\, \varphi(x)$, contradiction.
So we conclude that $T$ is inconsistent. By the compactness theorem, a finite subset $T'\subseteq T$ is inconsistent, say $T' = \{\lnot \varphi(s_1),\dots,\lnot \varphi(s_n)\}$, where $s_1,\dots,s_n$ are ground terms. To say that $T'$ is inconsistent is to say that every $\sigma$-structure satisfies $\varphi(s_i)$ for some $1\leq i\leq n$, which is what we wanted to prove.
