Robinson's joint consistency theorem

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

Boolos, George S.; Burgess, John P.; Jeffrey, Richard C. (2002). Computability and Logic. Cambridge University Press. p. 264. ISBN 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.

Mathematical logic

General

Axiom
- list
Cardinality
First-order logic
Formal proof
Formal semantics
Foundations of mathematics
Information theory
Lemma
Logical consequence
Model
Theorem
Theory
Type theory

Theorems (list)
and paradoxes

Gödel's completeness and incompleteness theorems
Tarski's undefinability
Banach–Tarski paradox
Cantor's theorem, paradox and diagonal argument
Compactness
Halting problem
Lindström's
Löwenheim–Skolem
Russell's paradox

Logics

Traditional	Classical logic Logical truth Tautology Proposition Inference Logical equivalence Consistency Equiconsistency Argument Soundness Validity Syllogism Square of opposition Venn diagram
Propositional	Boolean algebra Boolean functions Logical connectives Propositional calculus Propositional formula Truth tables Many-valued logic 3 finite ∞
Predicate	First-order list Second-order Monadic Higher-order Fixed-point Free Quantifiers Predicate Monadic predicate calculus

Set theory

Set hereditary Class (Ur-)Element Ordinal number Extensionality Forcing Relation equivalence partition Set operations: intersection union complement Cartesian product power set identities
Types of sets	Countable Uncountable Empty Inhabited Singleton Finite Infinite Transitive Ultrafilter Recursive Fuzzy Universal Universe constructible Grothendieck Von Neumann
Maps and cardinality	Function/Map domain codomain image In/Sur/Bi-jection Schröder–Bernstein theorem Isomorphism Gödel numbering Enumeration Large cardinal inaccessible Aleph number Operation binary
Set theories	Zermelo–Fraenkel axiom of choice continuum hypothesis General Kripke–Platek Morse–Kelley Naive New Foundations Tarski–Grothendieck Von Neumann–Bernays–Gödel Ackermann Constructive

Formal systems (list),
language and syntax

Alphabet Arity Automata Axiom schema Expression ground Extension by definition conservative Relation Formation rule Grammar Formula atomic closed ground open Free/bound variable Language Metalanguage Logical connective ¬ ∨ ∧ → ↔ = Predicate functional variable propositional variable Proof Quantifier ∃ ! ∀ rank Sentence atomic spectrum Signature String Substitution Symbol function logical/constant non-logical variable Term Theory list
Example axiomatic systems (list)	of arithmetic: Peano second-order elementary function primitive recursive Robinson Skolem of the real numbers Tarski's axiomatization of Boolean algebras canonical minimal axioms of geometry: Euclidean: Elements Hilbert's Tarski's non-Euclidean Principia Mathematica