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.
As per answer above, we have to assume that there are no constant symbols in the formula.
See Mordechai Ben-Ari, page 168 :
See page 177 : let assume that $S$ is the set of clauses corresponding to the formula $\mathcal A$ :
Due to the lack of function symbols, we have $H_S = \{ a \}$.
See page 178:
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:
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] :
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:
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.