In this paper, we establish an extended joint consistency theorem for an infinite family of free modal logics with equality. The extended joint consistency theorem incorporates the Craig and Lyndon interpolation lemmas and the Robinson joint consistency theorem. In part, the theorem states that two theories which are jointly unsatisfiable are separated by a sentence in the vocabulary common to both theories.

Our family of free modal logics includes the free versions of I, M, and S4 studied by Leblanc [5, Chapters 8 and 9], supplemented with equality as in [3]. In the relational semantics for these logics, there is no restriction on the accessibility relation in I, while in M(S4) the restriction is reflexivity (refiexivity and transitivity). We say that a restriction on the accessibility relation countenances backward-looping if it implies a sentence of the form ∀x1 …xn(x1Rx2 &…&xn ⊃ xkRxj) (1 ≤ j < k ≤ n ≥ 2), where the xi (1 ≤ i ≤ n) are distinct individual variables. Just as reflexivity and transitivity do not countenance backward-looping, neither do any of the restrictions in our family of free modal logics. (The above terminology is derived from the effect of such restrictions on Kripke tableaux constructions.) The Barcan formula, its converse, the Fitch formula, and the formula T ≠ T′ ⊃ □T ≠ T′ do not hold in our logics.