Background/Motivation
A theory T over a signature(language) Σ is a set of formulae over Σ. These formulae are called the non-logical axioms of T.
To talk about what is provable in T we can agree on Hilbert calculus and first-order logic.
A theory $ T' $ over $ Σ' $ is said to be an extension of a theory $ T $ over $ Σ $ if
- every sort/relation symbol/function symbol in $ Σ $ is also a sort/relation symbol/function symbol in $ Σ' $
- Every non-logical axiom of $ T $ is a non-logical axiom of $ T' $.
An extension $ T' $ of $ T $ is said to be conservative (over $ T $) if every formula over $ T $ that is provable in $ T' $ is also provable in $ T $
$ T' := T_1 \cup T_2 $ is a theory with signature $Σ_1 \cup Σ_2 $ and $Σ_1 \cap Σ_2 = Σ$ and is exactly the disjoint union of the nonlogical axioms of $T_1$ and $T_2$. (By this I mean that the instances of the axioms are united, and axiom schemas are not automatically applied to each other's signatures but rather kept separate and treated as an infinite set of axioms. Every non-logical axiom in $T'$ is a nonlogical axiom in $T_1$ or $T_2$)
Question
If $T_1$ and $T_2$ are extensions of a theory $T$, then so is $T_1 \cup T_2$ . If $T_1$ and $T_2$ are conservative, and therefore add no new theorems to $ T $ , is the same true for $T'$ ?
Is $ T' := T_1 \cup T_2 $ a conservative extension of $ T $, if $T_1$ and $T_2$ are conservative extensions of $T$ ?
And if not, what would a simple counterexample be?
Attempts
So far I have
- considered the weaker question (due to conservative over T ⇒ consistent over T):
Is $ T' $ a consistent extension of $ T $, if $T_1$ and $T_2$ are conservative extensions of $T$ ?
- tried to find or construct counterexamples specifically for this purpose but failed
- tried to prove the statement by induction over a hilbert-style proof tree. The main problem were the logical axioms at the leaves, which being axiom schemes, allow for a "mixing" of the signatures, making it difficult to "split" the prooftree into separate branches for $T_1$ and $T_2$. I still find this attempt promising but haven't made much progress yet. I also took into account the conservativity of a language extension.
- found no sources on this, especially since taking the union of theories as I have seems uncommon, and because it seems most material on (conservative) extensions takes a model theoretic rather than proof-theoretic approach.
Best Answer
Yes, this is true (and somewhat nontrivial). That is, if $T$ is a theory in a language $\Sigma$, and $T_1$ and $T_2$ are conservative extensions of $T$ in languages $\Sigma_1$ and $\Sigma_2$ (respectively) such that $\Sigma_1\cap\Sigma_2=\Sigma$, then $T_1\cup T_2$ is a conservative extension of $T$. This is a form of Robinson’s joint consistency theorem.
To derive it from a more common formulation of the joint consistency theorem that requires $T$ to be complete, let $\phi$ be any $\Sigma$-sentence such that $T\nvdash\phi$; we will show $T_1\cup T_2\nvdash\phi$. Since $T\nvdash\phi$, there exists a complete consistent $\Sigma$-theory $T'\supseteq T\cup\{\neg\phi\}$. Since $T_1$ and $T_2$ are conservative over $T$, the theories $T_1\cup T'$ and $T_2\cup T'$ are consistent. But then $T_1\cup T_2\cup T'$ is also consistent by the joint consistency theorem, hence $T_1\cup T_2\nvdash\phi$.
The requirement $\Sigma_1\cap\Sigma_2=\Sigma$ is essential, otherwise there are very simple counterexamples: e.g., let $T$ be the empty theory in the empty language, $T_1$ the theory $\{\exists x\,R(x)\}$ in language $\{R(x)\}$, and $T_2=\{\neg\exists x\,R(x)\}$ in the same language.