1
$\begingroup$

Let $\Sigma=\{c,f^1,R_1^2,...,R_k^2\}$ where $c$ is constant, $f$ is one argument function, and $R_i$ are binary relations. Let $\Sigma_2=\{c',g^2,R_1'^1,...,R_k'^1\}$ where $c'$ is constant, $g$ is two argument function, and $R_i'$ are unary relations.
Show an algorithm that given a formula $\varphi$ above $\Sigma$, returns a new formula $\varphi'$ above $\Sigma_2$ such that:
$\varphi$ is satisfiable above $\Sigma$$\iff$ $\varphi'$ is satisfiable above $\Sigma_2$

Well I have a partial solution, goes as follow:
Consider the next recursive definition:
$c\rightarrow c'$
$f(t)\rightarrow g(t',t')$
$R_i(t_1,t_2)\rightarrow R_i'(g(t_1',t_2'))$

The problem with the definition is that it not complete:
The function $g$ should have two roles:

  1. defining the values of $f(t)$
  2. Map elements of the form $(t_1,t_2)$ in a way that will allow $R_1'^1,...,R_k'^1$ to be consistent with $R_1^2,...,R_k^2$

I haven't found a way to define $g$, such that second requirement will be met.

Would appreciate help, hints will be helpful as well.

$\endgroup$
0
2
$\begingroup$

First of all in your above 3 "recursive definitions" linking $\Sigma$ with $\Sigma_2$, clearly the function $g$ in $\Sigma_2$ doesn't have any role in defining the values of $f(t)$ in $\Sigma$, the values of $f(t)$ should be already defined in language $\Sigma$.

To check your 3 "recursive definitions" more deeply, it seems here the map from constant $c$ to constant $c'$ is critical since it completely determines your replacement of the argument $t'$ in function $g$. For example, in $\Sigma$ we only have one dimensional information such as coordinate $x$ of the real line. When we try to translate to $\Sigma_2$ where we may have two dimensional information such as 2-tuple coordinate $(x, y)$ in a plane, then the map from $c$ to $c'$ can be expressed as $m(c)=c \rightarrow (c, 0)$ via an ordered pair in the simplest case. So you may need to further clarify the map from $c$ to $c'$ in order to really find correct arguments for your function $g$ during the translation...

$\endgroup$

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.