Let $\Sigma = \left\{ c,g(,),R_1(),\ldots,R_k() \right\}$. Given a sentence (a formula with no free variables) $\varphi$ above $\Sigma$, is there an algorithm to check if $\varphi$ is satisfiable?
I've understood one approach could be showing a contradiction to the general satisfiability problem. Meaning, assuming by a contradiction that there's such an algorithm and utilizing for the general problem (Which we know isn't decidable)
I'd be glad if you could help me with that.
Thanks!
If I understand your notation correctly, you have a binary function $g$ and several unary predicates $R_i$. With this vocabulary, you can write a first-order sentence saying that $g$ is a pairing function, i.e., every element is of the form $g(x,y)$ for a unique $x$ and $y$. Using a pairing function, you can encode binary (or higher-arity) relations as unary ones; just represent a binary $P$ by the unary $R$ such that $R(g(x,y))\iff P(x,y)$. With arbitrary-arity relations available, you can use the usual proof of undecidability for unrestricted vocabularies.