Robinson's joint consistency theorem explained

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} \cap T _{2} is complete (in the common language of T _{1} and T _{2} ), then the union T _{1} \cup T _{2} is consistent. A theory T is called complete if it decides every formula, meaning that for every sentence \varphi, the theory contains the sentence or its negation but not both (that is, either T \vdash \varphi or T \vdash \neg \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 \varphi in the common language of T _{1} and T _{2} such that T _{1} \vdash \varphi and T _{2} \vdash \neg \varphi, then the union T _{1\cup} T _{2} is consistent.

References

• Book: Boolos, George S. . George Boolos. Burgess, John P. . John P. Burgess. Richard C. Jeffrey. Jeffrey, Richard C.. Computability and Logic. Cambridge University Press. 2002. 264. 0-521-00758-5.
• Robinson, Abraham, 'A result on consistency and its application to the theory of definition', Proc. Royal Academy of Sciences, Amsterdam, series A, vol 59, pp 47-58.