Qual é o objetivo de interpretar elementos na prova de redução do PCP ao problema de decidibilidade da validade da lógica de predicados?

Como minha pergunta se relaciona diretamente a uma parte do texto de um livro de 2004, Lógica em Ciência da Computação: Modelagem e Raciocínio sobre Sistemas (2ª Edição), de Michael Huth e Mark Ryan , para fornecer contexto para a discussão a seguir, citando parcialmente o livro literalmente:

O problema de decisão da validade na lógica de predicados é indecidível: não existe um programa que, dado qualquer , decida se .$\varphi$$\varphi$

PROVA: Como dissemos antes, pretendemos que a validade é decidível para a lógica de predicados e, assim, resolvemos o problema (insolúvel) de correspondência posterior. Dada uma instância de problema de correspondência : , precisamos ser capazes de construir, dentro de espaço e tempo finitos e uniformemente, para todas as instâncias, alguma fórmula de lógica predicada como mantém se a instância do problema de correspondência acima tiver uma solução.$C$

$$s_1 s_2 ... s_k$$ $$t_1 t_2 ... t_k$$ $\varphi$$\varphi$$C$

Como símbolos de função, escolhemos uma constante e dois símbolos de função e cada um dos quais requer um argumento. Pensamos em como a sequência vazia, ou palavra, e e representam simbolicamente a concatenação com 0, respectivamente 1. Portanto, se é uma sequência binária de bits, podemos codificá-la como o termo . Observe que essa codificação soletra essa palavra para trás. Para facilitar a leitura dessas fórmulas, abreviamos termos como por .$e$$f_0$$f_1$$e$$f_0$$f_1$$b_1 b_2 ... b_l$$f_{b_l}(f_{b_{l−1}}...(f_{b_2}(f_{b_1}(e)))...)$$f_{b_l}(f_{b_{l−1}}...(f_{b_2}(f_{b_1}(t)))...)$$f_{{b_1}{b_2}...{b_l}}(t)$

Também exigimos um símbolo predicado que espera dois argumentos. O significado pretendido de é que existe alguma sequência de índices tal que é o termo que representa e representa . Assim, constrói uma string usando a mesma sequência de índices que ; somente usa o enquanto usa o .$P$$P(s,t)$$(i_1,i_2,...,i_m)$$s$$s_{i_1} s_{i_2}...s_{i_m}$$t$$t_{i_1} t_{i_2}...t_{i_m}$$s$$t$$s$$s_i$$t$$t_i$

Nossa frase tem a estrutura grossa onde definimos$\varphi$$\varphi_1 \wedge \varphi_2 \implies \varphi_3$

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

Nossa afirmação é é válida se o problema de correspondência posterior tiver uma solução.$\varphi$$C$

Ao provar PCP ⟹ Validade:

Por outro lado, suponhamos que o problema de pós-correspondência C tenha alguma solução, [...] A maneira como procedemos aqui é interpretando seqüências finitas e binárias no domínio dos valores do modelo . Isso não é diferente da codificação de um intérprete para uma linguagem de programação em outra. A interpretação é feita por uma função interpretada que é definida indutivamente na estrutura de dados de seqüências finitas e binárias:$A′$$M′$

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

[...] Usando [ ] e o fato de que , concluímos que para . [...] desde , sabemos que para todos temos isso para . Usando esses dois fatos, começando com , usamos repetidamente a última observação para obter$\text{interpret}(b_1 b_2...b_l) = f_{b_l}^{M′}(f_{b_{l-1}}^{M′}(...(f_{b_1}^{M′}(e{M′})...)))$$M\models\varphi_1$$(\text{interpret}(s_i), \text{interpret}(t_i)) \in P^{M′}$$i = 1,2,...,k$$M′ \models \varphi_2$$(s,t) \in P^{M′}$$(\text{interpret}(ss_i),\text{interpret}(tt_i)) \in P^{M′}$$i=1,2,...,k$$(s, t) = (s_{i_1}, t_{i_1})$

(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′}$

[...] Portanto (2.9) verifica em e, portanto, .$\exists{z} P(z,z)$$M′$$M′ \models \varphi_3$

Ao provar que a validade da lógica de predicados é indecidível, de acordo com a abordagem que aprendi na escola, que se baseia na do livro de Huth & Ryan (2ª edição, página 135) , ao construir a redução do problema de PCP para validade, "cadeias binárias finitas" do universo são interpretadas com uma " função de interpretação ", que codifica cadeias binárias em compostos de funções do modelo.

Em seguida, mostra que, usando o fato de que o antecedente de deve ser considerado não trivial, ambas as subfórmulas do antecedente podem ser expressas com a referida " função de interpretação ". A partir daí, conclui-se que a consequência também se mantém, pois também pode ser expressa de uma maneira com a função interpretar que se segue das expressões anteriores com interpretar .$\varphi$

Minha pergunta é: qual é o objetivo dessa " função de interpretação "? Por que não podemos simplesmente usar o anteriormente concebido φ e obter o mesmo resultado? O que obtemos do uso de interpretar para expressar nossos elementos?

E também, e se o nosso universo contiver alguns elementos arbitrários; isto é, e se não forem cadeias binárias? Acabamos de construir algum mapeamento dos dois?

Vamos começar com o que exatamente você está tentando provar.

Você está lidando com uma assinatura que consiste em uma constante , dois símbolos de função e um predicado binário . Denotamos por o conjunto de todas as instâncias "yes" para o problema de pós-correspondência, ou seja, todas as seqüências de pares ordenados de cadeias binárias , de forma que exista índices para alguns que satisfazem ( significa concatenação).$\sigma$$e$$f_0,f_1$$P(s,t)$$\mathcal{C}$$(s_1,t_1),...,(s_k,t_k)$$i_1,...,i_n$$n\in\mathbb{N}$$s_{i_1}\cdot...\cdot s_{i_n}=t_{i_1}\cdot...\cdot t_{i_n}$$\cdot$

Você deseja mostrar que, dada uma instância para o problema de correspondência posterior,$c=(s_1,t_1),...,(s_k,t_k)$

$c\in\mathcal{C} \iff$ Se é algum modelo que interpreta , então$\mathcal{M}$$\sigma$$\mathcal{M\models\ \varphi(c)}$

Onde e$\varphi(c)=\varphi_1(c)\land\varphi_2(c)\rightarrow \varphi_3(c)$

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

No exemplo acima, dada uma sequência binária , indica a composição . Essa é a redução do PCP para a validade na lógica de predicados descrita em "lógica na ciência da computação" por Huth & Ryan.$s=s_1,...,s_l$$f_s$$f_{s_l}\circ f_{s_{l-1}}\circ ...\circ f_{s_1}$

Pensamos em como concatenação com correspondentemente e em como a string vazia. Nesse caso, podemos pensar em como uma representação da string no mundo de . Intuitivamente, força o predicado a reter quando (talvez em alguns outros casos também, mas não nos importamos) (o que significa que são as interpretações de algumas seqüências finitas no mundo de ) e existe uma sequência de índices modo que$f_0,f_1$$0,1$$e$$f_s(e)$$s$$\mathcal{M}$$\varphi_1,\varphi_2$$P(v,w)$$v=f_s(e), w=f_t(e)$$v,w$$s,t$$\mathcal{M}$$i_1...i_n$$s=s_{i_1}\cdot...\cdot s_{i_n}$ e . Se realmente tem esse significado (que é o que acontece se satisfizer ), então .$t=t_{i_1}\cdot...\cdot t_{i_n}$$P(v,w)$$\mathcal{M}$$\varphi_1\land\varphi_2$$c\in\mathcal{C}\iff \exists z P(z,z)$

Você pergunta sobre a direção da prova, portanto deve lidar com modelos arbitrários que interpretam , onde o mundo pode ter elementos que não têm nada a ver com strings (isso se refere à sua segunda pergunta). É aqui que entra a função de interpretação. Damos uma correspondência entre todas as seqüências finitas e um subconjunto do mundo de , o que é bastante natural, dada a natureza de nossa assinatura. Uma string é mapeada para o elemento , que pode ser uma string / número / tabela ou qualquer coisa que você desejar.$\Rightarrow$$\sigma$$\mathcal{M}$$s$$f_s(e)$

Agora, quando tivermos a capacidade de pensar em elementos do formato em (o mundo de ) como cadeias finitas, podemos continuar e provar a implicação . Se satisfaz , então, como mencionamos, é válido quando (agora podemos pensar em como cadeias ), e existe uma sequência de índices de tal modo que e . Portanto, se e$f_s(e)$$\mathcal{A}_{\mathcal{M}}$$\mathcal{M}$$\Rightarrow$$\mathcal{M}$$\varphi_1,\varphi_2$$P(v,w)$$v=f_s(e), w=f_t(e)$$v,w$$i_1...i_n$$s=s_{i_1}\cdot...\cdot s_{i_n}$$t=t_{i_1}\cdot...\cdot t_{i_n}$$c\in \mathcal{C}$$i_1...i_n$ é uma sequência de índices com , então é válido e temos , pois implica .$s=s_{i_1}...s_{i_n}=t_{i_1}...t_{i_n}=t$$P(f_s(e),f_t(e))$$\mathcal{M}\models \varphi_3$$s=t$$f_s(e)=f_t(e)$