Question: Given the following signatures: $S_1=\{c,f^1,,=^2\}$, $S_2=\{P^1, R^2,=^2\}$, prove/disprove that there exists and algorithm that for a formula $\phi$ in $S_1$, builds a formula $\phi'$ that is satisfiable iff $\phi$ is satisfiable.

My proof: I believe this is true so I defined the algorithm :

  1. Convert any instance of $c$ to and instance of $P(x)$ ($x$ is always a new variable) and to always define $P=\{v(c)\}$ (a singleton relation).
  2. Convert any instance of $f(x)$ to $R(x,f(x))$, and to define $R$ as the sources and images of the function $f$.

I was wondering if this proof is true, or am I missing anything. (Seems good to me, but in logic you can never know some counterexample might pop up)...

  • $\begingroup$ Please look at my edits to the question. One shouldn't keep alternating in and out of MathJax in the course of a single expression in mathematical notation; rather one should put the whole thing within MathJax. $\qquad$ $\endgroup$ – Michael Hardy Feb 18 '16 at 16:49
  • $\begingroup$ Not sure how detailed you need to be in describing the algorithm, but I think you're currently missing some steps about how to actually transform formulas. For example, if $\phi(x) : x = c$, simply turning $c$ into $P(y)$ gives you $\phi(x,y): x = P(y)$ which is not valid syntax. $\endgroup$ – Dan Simon Feb 18 '16 at 18:24

Your idea is mostly correct, but you need to be careful that the syntax works. I'm going to assume these signatures are on the same universe, say $A$. (I'm going to ignore the $=$ since it can be interpreted the same in either).

1) Then with $S_1$ we have some interpretation of $c$ in $A$ (say $c_1\in{}A$). We want to define the relation $P$ to be $P=\{{}c_1\}{}$. Then for any formula $\phi$ in signature $S_1$ we can keep all logical symbols the same, but we must change instances of $c$. Let's say $\psi(c)$ is a subformula of $\phi$ that contains $c$, then we replace it with $P(x)\wedge\psi(x)$, which checks that $x=c$ and then replaces all instances of $c$ with $x$.

2) Now we deal with instances of $f$. First we define $R=\{{}(x,f(x))\}{}$, for all $x$ in the domain of $f$. Next, whenever we have a formula $\phi$ in signature $S_1$ with subformula $\psi(f(x))$ that contains $f(x)$, we replace it with $R(x,y)\wedge{}\psi(y)$. If different terms $f(x_1),f(x_2),\dots{},f(x_n)$ appear, then we'll need to replace those accordingly.

Under these changes, if we have a formula $\phi$ in $S_1$, we see that we now get a formula $\phi'$ in $S_2$. Now all that remains is to show $\phi$ is satisfiable iff $\phi'$ is satisfiable. And that will be fairly straightforward given how we defined $P$ and $R$.


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.