Is the union of two conservative extensions of a theory conservative?

Question

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.

Answer 1

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.

Answer 2

As Emil pointed out, assuming $\Sigma=\Sigma_1\cap\Sigma_2$, the union of 2 such theories is always conservative extension, Emil had proven it using the standard formulation Robinson’s joint consistency theorem, some places first prove the conservative extension variation and then uses it to get to the standard formulation, so here is a proof of this variation without assuming the Robinson’s joint consistency theorem but instead assumes Craig's interpolation (note that Craig's interpolation is as hard to prove as proving the joint consistency theorem in a different way, so it is not really "easier"):

Let $\phi$ be a sentence in $\Sigma$ provable in $T'$ and not provable in $T$.

Because $T_1$ is conservative, $\phi$ is also not provable there, but because $T_2 \cup (T_1\cup \{\lnot\phi\})$ is inconsistent there must be some $\psi$ provable in $T_2$ such that $\lnot\psi$ is provable in $T_1\cup\{\lnot\phi\}$ (this is a surprisingly tricky lemma when $T_1,T_2$ are not with the same language, it follows from Craig's interpolation), in particular $\psi$ and $\lnot\psi$ are sentences in $\Sigma$. Furthermore we have that $\lnot\phi\implies\lnot\psi$ is provable in $T_1$ and in the language $\Sigma$.

But because $T_2$ is conservative it means that $\psi$ is provable in $T$, and because $T_1$ is conservative we have $\lnot\phi\implies\lnot\psi$ also provable in $T$, but from $\psi$ and $\lnot\phi\implies\lnot\psi$ follows $\phi$ in $T$.

Note that the standard variation of the joint consistency theorem follows immediately, as any (consistent) extension of a complete theory is conservative.

Answer 3

The answer is no. Let $\phi$ be a non-theorem in the language of $T$, and let $c,d$ be two fresh symbols for constants. Now we can take $T_1$ to add the axiom $(c = d) \Rightarrow \phi$, and $T_2$ to add the axiom $c = d$.