What is the purpose of interpreting elements in the proof of reduction of PCP to validity decidability problem of predicate logic?

Question

Since my question relates directly to a part of the text from a 2004 book, Logic in Computer Science: Modelling and Reasoning about Systems (2nd Edition) by Michael Huth and Mark Ryan, in order to provide context for the following discussion, I'm partially quoting the book verbatim:

The decision problem of validity in predicate logic is undecidable: no program exists which, given any $\varphi$, decides whether $\varphi$.

PROOF: As said before, we pretend that validity is decidable for predicate logic and thereby solve the (insoluble) Post correspondence problem. Given a correspondence problem instance $C$: $$s_1 s_2 ... s_k$$ $$t_1 t_2 ... t_k$$ we need to be able to construct, within finite space and time and uniformly so for all instances, some formula $\varphi$ of predicate logic such that $\varphi$ holds iff the correspondence problem instance $C$ above has a solution.

As function symbols, we choose a constant $e$ and two function symbols $f_0$ and $f_1$ each of which requires one argument. We think of $e$ as the empty string, or word, and $f_0$ and $f_1$ symbolically stand for concatenation with 0, respectively 1. So if $b_1 b_2 ... b_l$ is a binary string of bits, we can code that up as the term $f_{b_l}(f_{b_{l−1}}...(f_{b_2}(f_{b_1}(e)))...)$. Note that this coding spells that word backwards. To facilitate reading those formulas, we abbreviate terms like $f_{b_l}(f_{b_{l−1}}...(f_{b_2}(f_{b_1}(t)))...)$ by $f_{{b_1}{b_2}...{b_l}}(t)$.

We also require a predicate symbol $P$ which expects two arguments. The intended meaning of $P(s,t)$ is that there is some sequence of indices $(i_1,i_2,...,i_m)$ such that $s$ is the term representing $s_{i_1} s_{i_2}...s_{i_m}$ and $t$ represents $t_{i_1} t_{i_2}...t_{i_m}$. Thus, $s$ constructs a string using the same sequence of indices as does $t$; only $s$ uses the $s_i$ whereas $t$ uses the $t_i$.

Our sentence $\varphi$ has the coarse structure $\varphi_1 \wedge \varphi_2 \implies \varphi_3$ where we set

$$\varphi_1 \stackrel{def}{=} \bigwedge\limits_{i=1}^k P\left(f_{s_i}(e),f_{t_i}(e)\right)$$

$$\varphi_2 \stackrel{def}{=} \forall v,w \hspace{1mm} P(v,w)\rightarrow\bigwedge\limits_{i=1}^kP(f_{s_i}(v),f_{t_i}(w))$$

$$\varphi_3 \stackrel{def}{=} \exists z\hspace{1mm} P(z,z)$$.

Our claim is $\varphi$ holds iff the Post correspondence problem $C$ has a solution.

In proving PCP ⟹ Validity:

Conversely, let us assume that the Post correspondence problem C has some solution, [...] The way we proceed here is by interpreting finite, binary strings in the domain of values $A′$ of the model $M′$. This is not unlike the coding of an interpreter for one programming language in another. The interpretation is done by a function interpret which is defined inductively on the data structure of finite, binary strings:

$$\text{interpret}(\epsilon) \stackrel{def}{=} e^{M′}$$

$$\text{interpret}(s0) \stackrel{def}{=} {f_0}^{M′}(\text{interpret}(s))$$

$$\text{interpret}(s1) \stackrel{def}{=} {f_1}^{M′}(\text{interpret}(s))$$.

[...] Using [$\text{interpret}(b_1 b_2...b_l) = f_{b_l}^{M′}(f_{b_{l-1}}^{M′}(...(f_{b_1}^{M′}(e{M′})...)))$] and the fact that $M\models\varphi_1$, we conclude that $(\text{interpret}(s_i), \text{interpret}(t_i)) \in P^{M′}$ for $i = 1,2,...,k$. [...] since $M′ \models \varphi_2$, we know that for all $(s,t) \in P^{M′}$ we have that $(\text{interpret}(ss_i),\text{interpret}(tt_i)) \in P^{M′}$ for $i=1,2,...,k$. Using these two facts, starting with $(s, t) = (s_{i_1}, t_{i_1})$, we repeatedly use the latter observation to obtain

(2.9) $(\text{interpret}(s_{i_1}s_{i_2}...s_{i_n}),\text{interpret}(t_{i_1}t_{i_2}...t_{i_n})) \in P^{M′}$.

[...] Hence (2.9) verifies $\exists{z} P(z,z)$ in $M′$ and thus $M′ \models \varphi_3$.

In proving that the validity of predicate logic is undecidable, according to the approach I learned from school, which is based on that of the Huth & Ryan book (2nd edition, page 135), when constructing the reduction of PCP to Validity problem, the "finite binary strings" of the universe are interpreted with a "interpret function", which encodes binary strings into composites of functions of the model.

Then it goes on to show that, using the fact that the antecedent of $\varphi$ must hold for it to be non-trivial, both sub-formulae of the antecedent can be expressed with the said "interpret function". From there, it follows that the consequence holds, too, since it can also be expressed in a way with the interpret function that follows from the previous expressions with interpret.

My question is: what is the purpose of this "interpret function"? Why can't we just use the previously devised φ and get the same result? What do we get out of using interpret to express our elements?

And also, what if our universe contains some arbitrary elements; that is, what if they are not binary strings? Do we just construct some mapping of the two?

Answer 1

Lets start with what exactly you are trying to prove.

You're dealing with a signature $\sigma$ which consists of one constant $e$, two function symbols $f_0,f_1$, and one binary predicate $P(s,t)$. We denote by $\mathcal{C}$ the set of all "yes" instances to the post correspondence problem, i.e. all sequences of ordered pairs of binary strings $(s_1,t_1),...,(s_k,t_k)$ such that there exists indices $i_1,...,i_n$ for some $n\in\mathbb{N}$ which satisfy $s_{i_1}\cdot...\cdot s_{i_n}=t_{i_1}\cdot...\cdot t_{i_n}$ ($\cdot$ stands for concatenation).

You want to show that given an instance $c=(s_1,t_1),...,(s_k,t_k)$ to the post correspondence problem, then

$c\in\mathcal{C} \iff$ If $\mathcal{M}$ is any model interpreting $\sigma$, then $\mathcal{M\models\ \varphi(c)}$

Where $\varphi(c)=\varphi_1(c)\land\varphi_2(c)\rightarrow \varphi_3(c)$, and

$\varphi_1(c)=\bigwedge\limits_{i=1}^k P\left(f_{s_i}(e),f_{t_i}(e)\right)$,

$\varphi_2(c)=\forall v,w \hspace{1mm} P(v,w)\rightarrow\bigwedge\limits_{i=1}^kP(f_{s_i}(v),f_{t_i}(w))$,

$\varphi_3(c)=\exists z\hspace{1mm} P(z,z)$.

In the above, given a binary string $s=s_1,...,s_l$, $f_s$ denotes the composition $f_{s_l}\circ f_{s_{l-1}}\circ ...\circ f_{s_1}$. This is the reduction from PCP to validity in predicate logic described in "logic in computer science" by Huth & Ryan.

We think of $f_0,f_1$ as concatenation with $0,1$ correspondingly, and of $e$ as the empty string. In that case, we can think of $f_s(e)$ as a representation of the string $s$ in the world of $\mathcal{M}$. Intuitively, $\varphi_1,\varphi_2$ force the predicate $P(v,w)$ to hold when (perhaps in some other cases as well, but we wont care) $v=f_s(e), w=f_t(e)$ (meaning that $v,w$ are the interpretations of some finite strings $s,t$ in the world of $\mathcal{M}$) and there exists a sequence of indices $i_1...i_n$ such that $s=s_{i_1}\cdot...\cdot s_{i_n}$ and $t=t_{i_1}\cdot...\cdot t_{i_n}$. If $P(v,w)$ indeed has that meaning (which is what happens if $\mathcal{M}$ satisfies $\varphi_1\land\varphi_2$), then $c\in\mathcal{C}\iff \exists z P(z,z)$.

You ask about the $\Rightarrow$ direction of the proof, so you must handle arbitrary models which interpret $\sigma$, where the world can have elements which have nothing to do with strings (this relates to your second question). This is where the interpretation function comes in. We give a correspondence between all finite strings and a subset of the world of $\mathcal{M}$, which is rather natural given the nature of our signature. A string $s$ is mapped to the element $f_s(e)$, which can be a string/number/table or anything you like.

Now, when we have the ability to think of elements of the form $f_s(e)$ in $\mathcal{A}_{\mathcal{M}}$ (the world of $\mathcal{M}$) as finite strings, we can go on and prove the $\Rightarrow$ implication. If $\mathcal{M}$ satisfies $\varphi_1,\varphi_2$, then as we mentioned, $P(v,w)$ holds when $v=f_s(e), w=f_t(e)$ (now we can think of $v,w$ as strings), and there exists a sequence of indices $i_1...i_n$ such that $s=s_{i_1}\cdot...\cdot s_{i_n}$ and $t=t_{i_1}\cdot...\cdot t_{i_n}$. Thus, if $c\in \mathcal{C}$, and $i_1...i_n$ is a sequence of indices with $s=s_{i_1}...s_{i_n}=t_{i_1}...t_{i_n}=t$, then $P(f_s(e),f_t(e))$ holds, and we have $\mathcal{M}\models \varphi_3$, since $s=t$ implies $f_s(e)=f_t(e)$.