Extension of a theory vs conservative extension

820 Views Asked by At

I'm not sure whether I get the difference between extension $T'$ of some theory $T$ and conservative extension $T''$ of this theory.

Extension $T'$ of $T$:

Language $L\{P\}$ and it's theory $T$

Language $L'\{P,*\}$ and it's theory $T'$

So the theory $T'$ is an extension of theory $T$ if the language $L'$ contains language $L$ AND all formulas from $T$ can be proved using $T'$.

And theory $T''$ is a conservative extension of $T$ if $T''$ is an extension of $T$ AND all formulas from language $L$ which can be proved in $T''$ can be proved in $T$.

Is this True?

Here are my examples of a) extension and b) conservative extension:

$L=\{P\}\ where\ P\ is\ a\ binary\ predicate $

$T\ of\ L\:\ T=\{ \phi== \exists x \exists y(P(x,y))\}$

a) $L'\ = \{P,*\}\ where\ P\ is\ a\ binary\ predicate\ and\ *\ is\ a\ binary\ function $ $T'\ = \{ \phi == \exists x \exists y(P(x,y)), \psi == anything\} $

b) $L'' = \{P,*\}\ where\ P\ is\ a\ bin.\ predicate\ and\ *\ is\ a\ bin.\ function $ $T'' = \{ \phi == \exists x \exists y(P(x,y), \psi == \forall x \forall y(P(x,y)\} $

I know that the b is incorrect. Maybe a) too. Could you give me advice or some hints to get it?

1

There are 1 best solutions below

0
On

a) is fine.

b) is incorrect because $T''$ does prove new theorems: you can't prove $\psi$ in $T$, and $\psi$ is in the language of $T$.

A common case is extension by definitions: a conservative extension $T''$ of $T$ introduces new symbols, and the theory $T''$ only adds definitions of those symbols in terms of the symbols of the language of $T$. Let's say the language of $T$ is $L$, and the expanded language of $T''$ is $L''$.. Because $T''$ proves no new theorems using only symbols of $L$, we know that we can, in principle, use the definitions of the new symbols to eliminate them from any theorem of $T''$. By doing so, we obtain an $L$-sentence that's equivalent in $T''$, hence a theorem of $T''$; because $T''$ is conservative, this equivalent $L$-sentence is a theorem of $T$ as well.

Sidebar: In the scenario just described, $T''$ is intended from the start to be a conservative extension, but that's not always the case. It can happen that a extension $T''$ of a theory $T$ is seen to be conservative only after someone proves it. Two worthwhile wikipedia articles: for general culture, see Conservative extensions; for proofs of why defined symbols can be eliminated, see Extension by definitions.

A simple example of a conservative extension $T''$ is to use the $T$ and $\phi$ that you have, and take $\psi$ to not use $P$ at all: $$ \psi := \forall u,v\, (u*v=u). $$ $\psi$ says that $*$ is just the first-projection function.

If the language of $T$ had a ternary predicate, or any non-unary function symbols, it would be easy to come up with a $T$ and a $T''$ that's an extension of $T$ by definitions. But it doesn't, so here's a slightly strained example: $$\begin{align} &\phi := \forall x\exists y\,(P(x,y) \land \forall z\,(P(x,z)\to y=z) \\ &\psi := \forall u,v,w\, [u*v = w \leftrightarrow ((u=v\land P(u,w)) \lor (u\ne v\land w = v) )]. \end{align}$$ Take $T = \{\phi\}, T'' = \{\phi, \psi\}$.

$\phi$ says that $P$ is the graph of a unary total function - it's single-valued with respect to its first argument. $\psi$ says: when the arguments $u,v$ of $*$ are equal, then the value of $u*v$ is just the value of the function that $P$ describes; otherwise, the value is $v$.

$T''$ is a conservative extension of $T$ because $$ T\vdash \forall u,v \exists! w\,((u=v\land P(u,w)) \lor (u\ne v\land w = v) ), $$ so a theorem proved in the second wikipedia article cited above guarantees that the definition of the function symbol $*$ can be "translated away". Here $\exists! w$ means "there is a unique w (such that)", a standard abbreviation. Using $\exists!$, $\phi$ can be written as $\forall x\exists!y\,P(x,y)$.