#### 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.



Is the union of two conservative extensions of a theory conservative?
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](https://en.wikipedia.org/wiki/Robinson%27s_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.


