3
$\begingroup$

Here is a basic technique in logic which seems well-known in folklore, but which I haven’t managed to find written down anywhere. $\newcommand{\T}{\mathbf{T}}$

Fact. Let $\Sigma$ be a signature (in the sense of predicate logic; i.e. sets of “function symbols” and “predicate symbols”, equipped with natural-number arities). Then there is a purely relational signature $\bar{\Sigma}$ and a theory $\T_\Sigma$ over $\bar{\Sigma}$, together with a translation from $L_\Sigma$ to $L_{\bar{\Sigma}}$ which is conservative modulo $\T_\Sigma$, i.e. $\varphi \vdash \psi$ over $\Sigma$ if and only if $\bar{\varphi} \vdash_{\T_\Sigma} \bar{\psi}$ over $\bar{\Sigma}$.

The idea is to replace each $n$-ary function of $\Sigma$ by an $(n+1)$-ary predicate in $\bar{\Sigma}$, and axioms in $\T_\Sigma$ stating that this predicate is functional.

Does anyone know a good citable source for some version of this technique?

(This is closely related to taking extensions by definitions, which is well-treated in the literature. It is straightforward to deduce this from the standard conservativity results for extensions by definitions, but it’s not quite a one-liner.)

$\endgroup$
0

1 Answer 1

4
$\begingroup$

The techique is in Bell & Machover: A course in mathematical logic, ch 2 §10 as theorem 10.5.

It states…

Select an $n$-ary function symbol $\mathbf f$ of $\mathcal L$, and let $\mathcal L'$ be obtained from $\mathcal L$ by excluding $\mathbf f$ and introducing a new $(n+1)$-ary predicate symbol $P$. We prove:

Theorem. For any $\mathcal L$-formula $\mathbf \alpha$ we can find an $\mathcal L'$-formula which is co-satisfiable with $\mathbf \alpha$ and an $\mathcal L'$ formula which is co-valid with $\mathbf \alpha$.

Google books link.

$\endgroup$
1
  • 2
    $\begingroup$ The technique is there, yes, but this result understates the result in OP's question, since co-validity is not the same thing as being a conservative extension. And on its face this theorem finds for each formula $\alpha$ two different formulas: one co-satisfiable with $\alpha$ and one co-valid, while OP cites a uniform translation from sentences using the function to sentences not, with an axiom making the two provably equivalent. Probably Bell and Machover somewhere state OP's result as OP states it but this theorem is not it. $\endgroup$ Jan 27, 2016 at 15:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.