Robinson's joint consistency theorem

From Wikipedia, the free encyclopedia

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 T1 and T2 be first-order theories. If T1 and T2 are consistent and the intersection T_1\cap T_2 is complete (in the common language of T1 and T2), then the union T_1\cup T_2 is consistent. Note that a theory is complete if it decides every formula, i.e. 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 T1 and T2 be first-order theories. If T1 and T2 are consistent and if there is no formula \varphi in the common language of T1 and T2 such that T_1 \vdash \varphi and T_2 \vdash \neg\varphi, then the union T_1\cup T_2 is consistent.

[edit] References