Robinson's joint consistency theorem

{{Short description|Theorem of mathematical logic}}

Robinson's joint consistency theorem is an important theorem of mathematical logic. It is related to Craig interpolation and Beth definability.

The classical formulation of Robinson's joint consistency theorem is as follows:

Let $T\_1$ and $T\_2$ be first-order theories. If $T\_1$ and $T\_2$ are consistent and the intersection $T\_1\; \backslash cap\; T\_2$ is complete (in the common language of $T\_1$ and $T\_2$), then the union $T\_1\; \backslash cup\; T\_2$ is consistent. A theory $T$ is called complete if it decides every formula, meaning that for every sentence $\backslash varphi,$ the theory contains the sentence or its negation but not both (that is, either $T\; \backslash vdash\; \backslash varphi$ or $T\; \backslash vdash\; \backslash neg\; \backslash varphi$).

Since the completeness assumption is quite hard to fulfill, there is a variant of the theorem:

Let $T\_1$ and $T\_2$ be first-order theories. If $T\_1$ and $T\_2$ are consistent and if there is no formula $\backslash varphi$ in the common language of $T\_1$ and $T\_2$ such that $T\_1\; \backslash vdash\; \backslash varphi$ and $T\_2\; \backslash vdash\; \backslash neg\; \backslash varphi,$ then the union $T\_1\backslash cup\; T\_2$ is consistent.