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 ∩ T 2 is complete (in the common language of T 1 and T 2 ), then the union T 1 ∪ T 2 is consistent. Note that a theory is complete if it decides every formula, i.e. either T ⊢ φ or T ⊢ ¬ φ .
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 φ in the common language of T 1 and T 2 such that T 1 ⊢ φ and T 2 ⊢ ¬ φ , then the union T 1 ∪ T 2 is consistent.
