A formula is satisfiable under $I \iff |I|=1$? 
Let $A(x_1, . . . , x_n)$ be a formula with no quantifiers and no function symbols.
Prove that $∀x_1 · · · ∀x_nA(x_1, . . . , x_n)$ is satisfiable if and only if it is satisfiable in an
interpretation whose domain has only one element.

Attempt:
$\leftarrow$ It follows by hypothesis.
$\to$ Suppose $∀x_1 · · · ∀x_nA(x_1, . . . , x_n)=S$ is satisfiable.
$\implies $ There exists an interpretation $I$ such that $S^I=true$
in other words there is a model for $S$
$\implies$ There exists a Herbrand model for $S$.
By hypothesis $A(x_1, . . . , x_n)$ is a formula with no quantifiers and no function symbols, hence the domain of $I$ must consist only of constants.

I am stuck here.
What can I do from here?
How to prove that the domain must consist of only one constant $c$?
Help me please

Edit Although this exercise is from Logic for computer science book by Mordechai it's expected to do the proof with 'similar' notation and conventions used in Introduction to mathematical logic by Mendelson, for instance an  interpretation I looks like: $I=\begin{cases} D=\mathbb N \\ a^I=2\\ f^I(x)=x^2\\ P^I(x)="x\ is\ even" \end{cases}$
as you can see there is no relations, just a domain,constants,functions and predicates.
 A: If there is more than one constant symbol in the language, then this is not true. For example if $c$ and $d$ are constant symbols, then $A$ could be the sentence (with no free variables) $\lnot (c = d)$, which is satisfiable, but only in a structure of size at least $2$.
Sometimes, constant symbols are viewed as special kinds of function symbols (of arity $0$), so the hypothesis "no function symbols" might include "no constant symbols". In this case (also assuming the usual convention that all structures are nonempty), the statement is true.
Indeed, suppose $\forall \overline{x}\, A(\overline{x})$ is satisfiable in a structure $M$. Since $M$ is nonempty, there is some $n\in M$. Let $N$ be the substructure of $M$ with domain $\{n\}$ (so if $R$ is a relation in the language, then $R(n,\dots,n)$ holds in $N$ if and only if $R(n,\dots,n)$ holds in $M$). Now $M\models \forall \overline{x},A(\overline{x})$, so in particular $M\models A(n,\dots,n)$, which implies that $N\models A(n,\dots,n)$ (since $A$ is quantifier-free), and hence $N\models \forall \overline{x}\, A(\overline{x})$ (since the universal quantifiers just range over the single element $n$ in the domain of $N$).
In the case that there is a single constant symbol $c$ in the language, we can use the same proof, but pick $n$ to be the interpretation of $c$ in $M$. This fails is there are more constant symbols (or if there are function symbols), since then the singleton $\{n\}$ might not be the domain of a substructure, since it might not contain the interpretations of all the constant symbols or be closed under the interpretations of all the function symbols.
Finally, I'll just note that the proof I gave above is a special case of the (also quite easy) proof that "universal sentences go down": If $\varphi$ is a universal sentence (of the form $\forall \overline{x}\,\psi(\overline{x})$ where $\psi$ is quantifier-free), and $N$ is a substructure of $M$, then $M\models \varphi\implies N\models \varphi$.

Edit: Let me try to rewrite the argument in a way that matches your terminology. We have a formula $A(x_1,\dots,x_n)$ with no quantifiers and no function or constant symbols. Let's say it contains the predicate symbols $\{p_1,\dots,p_m\}$, where $p_i$ has arity $n_i$. If the closed formula $B: \forall x_1\cdots\forall x_n A(x_1,\dots,x_n)$ is satisfiable, then there is an interpretation $\mathscr{I} = (D,\{R_1,\dots,R_m\})$ such that $v_{\mathscr{I}}(B) = T$. 
Pick any element $a\in D$. We'll define a new interpretation $\mathscr{I}' = (\{a\},\{R_1',\dots,R_m'\})$ whose domain has only the single element $a$. To do this, we have to specify the $n_i$-ary relation $R_i'$ on $\{a\}$ for all $i$. Now an $n_i$-ary relation on $\{a\}$ is a subset of $\{a\}^{n_i} = \{(a,\dots,a)\}$, so it is either $\{(a,\dots,a)\}$ or $\emptyset$. We define $R_i'$ to be $\{(a,\dots,a)\}$ if $(a,\dots,a)\in R_i$ and $\emptyset$ if $(a,\dots,a)\notin R_i$.
Now since $v_{\mathscr{I}}(B) = T$, we have that for all $a_1,\dots,a_n\in D$, letting $\sigma\colon \mathcal{V}\to \mathscr{I}$ be the assignment $x_i\mapsto a_i$, $v_\sigma(A) = T$. In particular, taking $a_i = a$ for all $i$, we have $v_\sigma(A) = T$. 
Now you need to check by induction on the structure of $A$, starting from the atomic formulas, that letting $\sigma'\colon \mathcal{V}\to \mathscr{I}'$ be the assignment $x_i\mapsto a$ for all $i$, we also have $v_{\sigma'}(A) = T$.
Finally, we find that $v_{\mathscr{I}'}(B) = T$, since the only possible assignment for the universal quantifiers appearing in $B$ is $\sigma'$.
A: As per answer above, we have to assume that there are no constant symbols in the formula.
See Mordechai Ben-Ari, page 168 :

Constant symbols are no longer needed since they are the same as $0$-ary functions.

See page 177 : let assume that $S$ is the set of clauses corresponding to the formula $\mathcal A$ :

let $H_S$, the Herbrand universe of $S$ [...] If there are no constant symbols or $0$-ary function symbols in $S$, initialize the inductive definition of $H_S$ with an arbitrary constant symbol $a$.
The Herbrand universe is just the set of ground terms that can be formed from
symbols in $S$.

Due to the lack of function symbols, we have $H_S = \{ a \}$.
See page 178:

Let $H_S$ be the Herbrand universe for $S$. $B_S$, the Herbrand base for
$S$, is the set of ground atomic formulas that can be formed from predicate symbols in $S$ and terms in $H_S$.

But $a$ is the only term in $H_S$; thus, if e.g. $p_1(x_1,\ldots,x_n),\ldots, p_m(x_1,\ldots,x_n)$ are the predicate symbols occurring in $\mathcal A$, the Herbrand base will be:

$B_S = \{ p_1(a,\ldots,a),\ldots, p_m(a,\ldots, a) \}$.

An Herbrand interpretation for $S$ can be defined by giving the subset of the Herbrand base where the relations $R_1,\ldots, R_m$, i.e. the interpretations of the corresponding predicates, hold.
Now we can apply [page 179] :

Theorem 9.24 A set of clauses $S$ has a model iff it has an Herbrand model.

We know that $S$ [the set of clauses corresponding to the formula $\forall x_i \ \mathcal A$] is satisfiable; thus, it has a model and so also an Herbrand model, i.e. an interpretation $\mathcal H$ with domain the Herbrand universe $H_S = \{ a \}$, such that:


$\mathcal H \vDash S$.



We can follow the "instructions" of Alex's answer to manufacture the Herbrand interpretation based on the above Herbrand base.
Basically, we may describe Alex's inductive construction of the interpretation this way: $A(x_1,\ldots, x_n)$ may be expressed equivalently a a set of clauses, i.e. as disjunctions of predicates $p_i$ and their negation.
Consider the simple example $p_1(x_1,\ldots,x_n) \lor \lnot p_m(x_1,\ldots, x_m)$. We know that it is satisfiable: thus either $p_1(a,\ldots,a)$ holds or $\lnot p_m(a,\ldots, a)$ holds.
In the first case, we have to assume that the interpretation of $p_1$ is satisfied by $(a,\ldots,a)$, i.e. $(a,\ldots,a) \in R_1$, while in the second case we have to assume that $(a,\ldots,a) \notin R_m$.
And so on. The satisfiability of the original formula guarantee that this procedure will succeed.
