Is extension by compound definitions still conservative?

146 Views Asked by At

In first order logic extension by definition provides a way to conservatively extend a theory.

To define a $n$-ary function symbol $f$ we have to prove that $\forall x_1,\ldots, x_n:\exists y: \psi(y,x_1,\ldots, x_n)$ and then can add the axiom $\forall x_1, \ldots , x_n: \psi(f(x_1,\ldots, x_n), x_1,\ldots, x_n)$.

What if I want to decompose the new function symbol into multiple new symbols. So instead of defining $f$, I add two new symbols $a,b$ and the axiom

$\forall x_1, x_2,x_3: \psi(a(b(x_1,x_2),x_3), x_1,x_2,x_3)$

then later when I define a new compound function symbol I can reuse $a,b$ iff the defined compound terms do not overlap (overlap as in a term rewriting system sense).

So for example add the new axiom (after the appropriate existence theorem has been proven)

$\forall x_1, x_2,x_3: \psi(a(a(x_1,x_2),x_3), x_1,x_2,x_3)$

Question: Is this still conservative extension?

My greatest concern is with a statement like

$a(x,y) \implies \top$

which is provable but has no counterpart in the original language (but that seems to not be a requirement for conservative extension)

1

There are 1 best solutions below

9
On BEST ANSWER

I think part of the question is whether, after proving the existence condition for $f(x_1,x_2,x_3)$, one can conservatively add $\psi(a(b(x_1,x_2),x_3),x_1,x_2,x_3)$ instead of the usual $\psi(f(x_1,x_2,x_3),x_1,x_2,x_3)$. The answer is no. The point is that, in a finite structure whose universe $A$ consists of $n\geq2$ elements, $\psi$ might describe a ternary operation $J$ such that all $n^2$ of the functions $x_3\mapsto J(p,q,x_3)$ (for $p,q\in A$) are different. But $x_3\mapsto a(b(p,q),x_3)$ can describe only $n$ functions, because there are only $n$ values for $b(p,q)$. So your proposed $\psi(a(b(x_1,x_2),x_3),x_1,x_2,x_3)$ might be inconsistent even when $\psi(f(x_1,x_2,x_3),x_1,x_2,x_3)$ is consistent.

I'm not sure I understand the later part of your question, but it seems to be adding the additional information that $a$ can serve in place of $b$. That won't be conservative in general, even over the previously extended theory, but maybe the non-conservativity of the previously extended theory makes the later question moot.