 Notice that it is always possible to choose substitution instances of a pair of formulas so that the sets of their propositional variables are disjoint, because formulas are finite objects. The most general common instance of two formulas \(A\) and \(B\) (that do not share a propositional variable) is \(C\), where \(C\) is a substitution instance of both \(A\) and \(B\), and  propositional variables are identified by the substitutions only if the identification is necessary to obtain a formula that is a substitution instance of both \(A\) and \(B\). The unification theorem (specialized to simple types) implies that if two formulas \(A\) and \(B\) have a common instance then there is a formula \(C\) such that all the common instances of \(A\) and \(B\) are substitution instances of \(C\). Obviously, a pair of formulas either has no common instance at all, or it has \(\aleph_0\) many most general common instances.