The most fundamental results of monadic second-order decidability, beyond the decidability of just pure monadic second-order logic, deal with the decidability of the monadic second-order theories of one and two successors and the decidability of the second-order theory of linear order (Buchi, Rabin). Having moved from sets to multisets, we refine the underlying logic as linear logic. In contrast to the classical results, we prove the undecidability of just pure monadic linear logic, even if we use nothing but Horn formulas built up from unary predicates, in which no function symbols are present.

As for affine logic (linear logic plus weakening), we prove the undecidability of the Horn fragment of affine logic, which involves only one binary predicate ("linear order") and a fixed finite number of unary predicates, and which contains no function symbols at all. We also show the undecidability of the Horn fragment of monadic affine logic of one constant symbol ("zero") and one unary function symbol ("successor"), and a fixed finite number of unary predicates.

Along these lines, we obtain the undecidability of the optimistic protocol completion even for the class of communication protocols with two participants such that either of them is a finite automaton provided with one register capable of storing one atomic message, all the predicates used are at most unary, and no compound messages are used.