An extension by definition is the formal way of introducing new symbols in a mathematical theory.
Theories can be extended into new ones by adding new symbols and new axioms to it. We're interested in a special kind of extension, called \textit{conservative extension}.
\begin{defin}[Conservative Extension]
A theory $\mathcal{T}_2$ is a conservative extension over a theory $\mathcal{T}_1$ if:
A theory $\mathcal{T}_2$ is a conservative extension of a theory $\mathcal{T}_1$ if:
\begin{itemize}
\item$\mathcal{T}_1\subset\mathcal{T}_2$
\item For any formula $\phi$ in the language of $\mathcal{T}_1$, if $\mathcal{T}_2\vdash\phi$ then $\mathcal{T}_1\vdash\phi$
...
...
@@ -29,7 +29,7 @@ Moreover, in that case we require that
$$
\exists! y. \phi_{y, x_1,...,x_k}
$$
is a theorem of $\mathcal{T}_1$
is a theorem of $\mathcal{T}_1$.
\end{itemize}
\end{itemize}
\end{defin}
...
...
@@ -38,7 +38,7 @@ We also say that a theory $\mathcal{T}_k$ is an extension by definition of a the
For function definition, it is common in logic textbooks to only require the existence of $y$ and not its uniqueness. The axiom one would then obtain would only be $\phi[f(x_1,...,x_n)/y]$ This also leads to conservative extension, but it turns out not to be enough in the presence of axiom schemas (axioms containing schematic symbols).
\begin{lemma}
In ZF, an extension by definition without uniqueness doesn't necessarily yields a conservative extension if the use of the new symbol is allowed in axiom schemas.
In ZF, an extension by definition without uniqueness doesn't necessarily yield a conservative extension if the use of the new symbol is allowed in axiom schemas.
\end{lemma}
\begin{proof}
In ZF, consider the formula $\phi_c :=\forall x. \exists y. (x \neq\emptyset)\implies y \in x$ expressing that nonempty sets contain an element, which is provable in ZFC.
...
...
@@ -54,8 +54,8 @@ For the definition with uniqueness, there is a stronger result than only conserv
\begin{defin}
A theory $\mathcal{T}_2$ is a fully conservative extension over a theory $\mathcal{T}_1$ if:
\begin{itemize}
\itemIt is conservative
\itemFor any formula $\phi_2$ with free variables $x_1, ..., x_k$ in the language of $\mathcal{T}_2$, there exists a formula $\phi_1$ in the language of $\mathcal{T}_1$ with free variables among $x_1, ..., x_k$ such that
\itemit is conservative, and
\itemfor any formula $\phi_2$ with free variables $x_1, ..., x_k$ in the language of $\mathcal{T}_2$, there exists a formula $\phi_1$ in the language of $\mathcal{T}_1$ with free variables among $x_1, ..., x_k$ such that
@@ -64,7 +64,7 @@ An extension by definition with uniqueness is fully conservative.
\end{thm}
The proof is done by induction on the height of the formula and isn't difficult, but fairly tedious.
\begin{thm}
If an extension $\mathcal{T}_2$ of a theory $\mathcal{T}_1$ with axiom schemas is fully conservative, then for any instance of the axiom schemas of an axiom schemas $\alpha$containing a new symbol, $\Gamma\vdash\alpha$ where $\Gamma$ contains no axiom schema instantiated with new symbols.
If an extension $\mathcal{T}_2$ of a theory $\mathcal{T}_1$ with axiom schemas is fully conservative, then for any instance of the axiom schemas containing a new symbol$\alpha$, $\Gamma\vdash\alpha$ where $\Gamma$ contains no axiom schema instantiated with new symbols.