7
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ Welcome to the site! Please try to make your question more self contained. We cannot know what do you mean by antecedent of $\varphi$ if we don't know who $\varphi$ is, so you should probably add some description of the reduction. You should also specify your sources exactly (what book) so noone has to guess. I covered this in the first part of my answer, but i think it should also appear in the question. $\endgroup$ – Ariel Nov 26 '16 at 16:06
7
$\begingroup$

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)$.

$\endgroup$
  • $\begingroup$ Hello, Ariel! Thanks for answering! Sorry not getting back sooner. I wasn't expecting to be answered so promptly with such a nice answer! I'll revise my question to include more context (maybe by quoting the book)! Thanks! $\endgroup$ – RexYuan Nov 27 '16 at 17:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.