Don't Ask Alice - Part the Sixth

This is the sixth installment on Dodgson's unsolved sorites - for the previous five go here:
Don't ask Alice, I don't think she'll know [from Dodgson's Symbolic Logic, p. 186]
Don't ask Alice - Part the Second [from Dodgson's Symbolic Logic, p. 187]
Don't ask Alice - Part the Third [from Dodgson's Symbolic Logic, p. 188]
Don't ask Alice - Part the Fourth [from Dodgson's Symbolic Logic, p. 190]
Don't ask Alice - Part the Fifth [from Dodgson's Symbolic Logic, p. 191]
Without further ado, here is the sixth of Dodgson's [hitherto] unsolved sorites:

After the six friends, named in Problem 5, had returned from their tour, three of them, Barry, Cole, and Dix, agreed with two other friends of theirs, Lang and Mill, that the five should meet, every day, at a certain table d'hôte. Remembering how much amusement they had derived from their code of rules for walking-parties, they devised the following rules to be observed whenever beef appeared on the table:---
(1) If Barry takes salt, then either Cole or Lang takes one only of the two condiments, salt and mustard: if he takes condiment, or Mill takes both.
(2) If Cole takes salt, then either Barry takes only one condiment, or Mill takes neither: if he takes mustard, then either Dix or Lang takes both.
(3) If Dix takes salt, then either Barry takes neither condiment or Cole take both: if he takes mustard, then either Lang or Mill takes neither.
(4) If Lang takes salt, then Barry or Dix takes only one condiment: if he take mustard, the either Cole or Mill takes neither.
(5) If Mill takes salt, then either Barry or Lang takes both condiments: if he takes mustard, then either Cole or Dix takes only one.
The Problem is to discover whether these rules are compatible; and, if so, what arrangements are possible.
[N.B. In this Problem, it is assumed that the phrase "if Barry takes salt" allows of two possible cases, viz. (1) "he takes salt only"; (2) "he takes both condiments". And so with all similar phrases.
It is also assumed that the phrase "either Cole or Lang takes one only of the two condiments" allows three possible cases, viz. (1) "Cole takes one only, Lang takes both or neither"; (2) "cole takes both or neither, Lang takes one only"; (3) "Cole take one only, Lang takes one only". And so with all similar phrases.
It is also assumed that every rule is to be understood as implying the words "and vice versâ." Thus the first rule would imply the addition "and, if either Cole or Lang takes only one condiment, then Barry takes salt."]

This problem is a completely different type from the previous ones, as will be seen. As in the previous problem (Problem 5), introduce the propositional characteristic functions s_J = {U,U^~} and m_J = {U,U^~} representing the condition (true or false, respectively) that the individual "J" uses salt or mustard, respectively. The universe of individuals is {B, C, D, L, M} representing Barry, Cole, Dix, Lang, and Mill, so there are 10 unknowns in all. From Dodgson's comments following the premises, each premise is not simply an implication but a material equivalence, since implications are assumed in both directions. So the premises can be transcribed as:
1a) s_b = (s_c^ m_c)(s_l^ m_l)
1b) m_b = (s_d^~ · m_d^~)(s_m · m_m)
2a) s_c = (s_b^ m_b)(s_m^~ · m_m^~)
2b) m_c = (s_d · m_d)(s_l · m_l)
3a) s_d = (s_b^~ · m_b^~)(s_c · m_c)
3b) m_d = (s_l^~ · m_l^~)(s_m^~ · m_m^~)
4a) s_l = (s_b^ m_b)(s_d^ m_d)
4b) m_l = (s_c^~ · m_c^~)(s_m^~ · m_m^~)
5a) s_m = (s_b · m_b)(s_l · m_l)
5b) m_m = (s_c^ m_c)(s_d^ m_d)
where, following the boolean conventions employed in this series, concatenation represents disjunction (or), "^~" represents complementation (negation), "·" represents conjunction (and), and "^" represents the exclusive-or operation.

Now, there are no terms appearing complemented and uncomplemented, and therefore the general method used in the previous problems is not applicable. The arithmetic approach of traditional propositional logic would enumerate all combinations of the 10 variables, resulting in 2¹⁰ = 1,024 combinations, and then proceed to determine which, if any, satisfied the 10 relations (1a)-(5b). This is so unwieldy that no one would even attempt it. The obvious algebraic approach is substitution to successively eliminate unknowns. Substituting (1a) and (1b) into (2a):
(2a.1) s_c = (s_b^ m_b)(s_m^~ · m_m^~) = {[(s_c^ m_c)(s_l^ m_l)]^~(s_d^~· m_d^~)(s_m · m_m)}^~ {(s_c^ m_c)(s_l^ m_l)[(s_d^~· m_d^~)(s_m · m_m)]^~}^~ (s_m^~· m_m^~)
This is an equation in which the variable s_c appears on both sides of the equality. Simplifying and collecting terms in s_c and s_c^~ on the right side:
(2a.2) s_c = (s_m^~· m_m^~) [(s_d^~· m_d^~)(s_l^ m_l)^~(s_m· m_m)]^~ [(s_d^ m_d)^~(s_l· m_l)(s_m· m_m)s_c^~]^~ [{[(s_d· m_d)^~(s_m· m_m)]^~ [(s_d^~· m_d^~)(s_l^ m_l)]^~ [(s_d^ m_d)^~(s_l^~· m_l^~)^~]^~ [(s_l^ m_l)(s_m· m_m)^~]^~ [(s_d^~· m_d^~)(s_l· m_l)^~(s_m· m_m)]^~ [(s_d· m_d)(s_l^~· m_l^~)^~(s_m· m_m)^~]^~}^~s_c]^~
We seem to have reached an impasse – this type of equation is outside the realm of traditional logic. Fortunately, there is a simple method available in this case. Since the variables are assumed propositional, we can assume the two possible values for s_c and investigate the consequences of each assumption.

First, assume s_c = U^~. Substituting this value in (2a.2):
(I.2a.3)   U^~ = (s_m^~· m_m^~) [(s_d^~· m_d^~)(s_l^ m_l)^~(s_m· m_m)]^~ [(s_d· m_d)^~(s_m· m_m)]^~ [(s_d^~· m_d^~)(s_l^ m_l)]^~ [(s_d^ m_d)^~(s_l^~· m_l^~)^~]^~ [(s_l^ m_l)(s_m· m_m)^~]^~ [(s_d^~· m_d^~)(s_l· m_l)^~(s_m· m_m)]^~ [(s_d· m_d)(s_l^~· m_l^~)^~(s_m· m_m)^~]^~
from which we can conclude, using using an inference theorem and complementing if necessary:
(I.6a)   (s_m^~· m_m^~) = U^~
(I.6b)   (s_d^~· m_d^~)(s_l^ m_l)^~(s_m· m_m) = U
(I.6c)   (s_d· m_d)^~(s_m· m_m) = U
(I.6d)   (s_d^~· m_d^~)(s_l^ m_l) = U
(I.6e)   (s_d^ m_d)^~(s_l^~· m_l^~)^~ = U
(I.6f)   (s_l^ m_l)(s_m· m_m)^~ = U
(I.6g)   (s_d^~· m_d^~)(s_l· m_l)^~(s_m· m_m) = U
(I.6h)   (s_d· m_d)(s_l^~· m_l^~)^~(s_m· m_m)^~ = U
Applying the theorem to (I.6b) and (I.6d), (s_d^~· m_d^~)(s_m· m_m) = U, whence m_b = U. We can now start substituting and reducing the other relations:
(I.3a.1)   s_d = (s_b^~· m_b^~)(s_c· m_c) = (s_b(U^~)^~)^~((U^~)^~m_c^~)^~ = U^~
(I.2b.1)   m_c = (s_d· m_d)(s_l· m_l) = (U^~· m_d)(s_l· m_l) = (s_l· m_l)
(I.1a.1)   s_b = (s_c^ m_c)(s_l^ m_l) = (U^~^ m_c)(s_l^ m_l) = m_c(s_l^ m_l)= (s_l^ m_l)(s_l· m_l) = (s_l^~m_l)^~(s_lm_l^~)^~(s_l^~m_l^~)^~ = s_lm_l
(I.3b.1)   m_d = (s_l^~· m_l^~)(s_m^~· m_m^~) = (s_l^~· m_l^~)U^~ = (s_l^~· m_l^~)
(I.4a.1)   s_l = (s_b^ m_b)(s_d^ m_d) = (s_b^ U)(U^~^ m_d) = s_b^~m_d = (s_lm_l)^~
The only consistent combination satisfying this equation is s_l = U^~ and m_l = U. Finishing the substitutions:
(I.2b.2)   m_c = (s_l· m_l) = ((U^~)^~U^~)^~ = U^~
(I.1a.2)   s_b = s_lm_l = U^~U = U
(I.3b.2)   m_d = (s_l^~· m_l^~) = (((U^~)^~)^~(U^~)^~)^~ = U^~
(I.5a.1)   s_m = (s_b· m_b)(s_l· m_l) = (U^~U^~)^~((U^~)^~U^~)^~ = UU^~ = U
(I.5b.1)   m_m = (s_c^ m_c)(s_d^ m_d) = ((U^~)^~U^~)^~(U^~(U^~)^~)^~((U^~)^~U^~)^~(U^~(U^~)^~)^~ = U^~
Substitution of these values show that (1a)-(5b) are all satisified. Hence, all variables are completely determined and there is only one possible set of values for this assumption.

If we instead assume s_c = U, then we eventually encounter a contradiction, so the detailed calculations will not be presented. We can now definitively and conclusively answer Dodgson's questions, towit: The rules are compatible, and there is only one possible arrangement:

Barry and Mill take salt, and Barry and Lang take mustard.

This is not unreasonable; for a system of 10 independent, consistent equations in 10 unknowns, only one solution would be expected.

The other question, for which there is no answer, is: what was Dodgson's solution for this problem? The solution given here has used algebraic methods which were unavailable to Dodgson and are unususal even in modern symbolic logic. I have been unable to obtain any solution using the methods in Dodgson's book, and therefore am unable to envision Dodgson's method. The fact that he used the plural 'arrangements' might indicate he thought there was more than one solution, but this is mere speculation.