patternMinor
What is the purpose of interpreting elements in the proof of reduction of PCP to validity decidability problem of predicate logic?
Viewed 0 times
problemtheelementswhatinterpretinglogicpredicatevalidityreductiondecidability
Problem
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_
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_
Solution
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)$.
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)$.
Context
StackExchange Computer Science Q#66501, answer score: 7
Revisions (0)
No revisions yet.