Let $A$ be a formula without quantifiers, in a language with at least one constant. I need to prove/disprove the following:
If $\exists_xA$ is logically valid (meaning is is true for every structure), then for every Herbrand structure $H$ there exists a closed term $t$ such that $H \vdash A \{t/x \}$
I think that this is true. Because $\exists_xA$ is logically valid then it is also valid in $H$, so there is $v$ such that $H,v \vdash \exists_xA$. It means that there is a $x$-variant $v'$ such that $H,v' \vdash A$, but because all variables in $H$ are closed terms then $v'(x) = t$ where $t$ is a closed term. which means $$H,v'[x = t] \vdash A$$ and we can use the replacement theorem to get: $H,v \vdash A \{t/x \}$ (it is legal since there are no quantifiers in $A$ meaning $x$ is free)
Am I right here? Because I get really confused in those logic questions.
Help would be appreciated.