A couple of recent threads have gone back and forth on the issue that there was no logical way to do something in Lojban or that the way to do it in Lojban wasn't very logical. Given relevant readings of "logical", these claims are true. But uninteresting. Lojban is not merely logical (in the relevant restricted senses), it is also a language and the things that are illogical to say in Lojban are things peculiar to language, without any logical significance (or significance that can be introduced into logic only with difficulty).
The matter of the comments inserted into quotations is purely a language matter, style,
in fact
(logic notoriously does not have style in the short run). Repeating "Alice said" or "said Alice" at the beginning or ending of every paragraph is monotonous. So you find other ways to do it without interfering with the structure and metastructural inserts do the job quite nicely. The quote is not "really" split, of course, because the {sei ...se'u} phrase is not really there (i.e. in the place it appears to be). Illogical because deceptive in appearance and unnecessary in the structure -- except for speaking and reading humans.
The "any" case is slightly more complex, because one can force some logical distinction into it sometimes. "Any" is broad scope universal quantifier which (quite logically) sometimes serves as a narrow scope particular in negative
contexts (and, perhaps, some other odd contexts as well -- dialects vary and donkey sentences make their own muck). That is the language situation. And the logic situation is not much different, but the use of an imperative form creates a problem, since it is not clear about the relative scopes of the quantifier and the speech-act indicator. Usually, the speech-act indicator has to come first, because, otherwise, we would have a sentence without performance instructions, but in complex situations this need not be a problem. But here we have a simple case: Give me an apple. That is, logicially, Imp(( Sx: apple x) you give x to me) (roughly speaking). A sentence which is "true" (fulfilled) if you give me something, anything, that is an apple. But, you say, suppose I want a particular apple -- or want to explicitly exclude that possibility. The exclusion is easy -- the given English (or {ko dando da poi plise/ su'o
plise}in Lojban) does the trick. I have explicitly NOT restricted the choice of apples. If I do want to restrict that choice, I have to take another step, either moving the quantifier (or marking it as moved), explicitly specifying some further restriction on the apple, or appealing implicitly to some aspect of the situation not in the present sentence: "There is an apple I want, give it to me", "Give me a certain apple", "Give me the golden apple", "Give me the apple". The first of these is, as noted, tricky to transcribe in strict logical form (though the dialogical form is probably straightforward). The second is equally difficult, since logic does not generally have expressions like "a certain" that have broad scope even in restricted contexts (that is language again, not logic). The third is obvious. The fourth uses some sort of descriptor, {le} or {lo} depending (more or less) on whether the implicit
context is internal or external. A case can be made that {lo} also functions as a long scope particular quantifier, running back at least to the introduction of its bound predicate, and so might also be used for the second case (again, this passes beyond logic somewhat to dialogical analysis, but that seems to be the wave of the future anyhow).
Oh yeah, the stuff about proofs goes into the one place where Logic does have style. We can, with a suitable proof system, either extend this complication or contract it. Generally, in logic, it is bad form to use the same notation for bound and free terms (and, indeed, the free terms are strictly only dummies, not really in the language at all). The descent to Bob and the like, rather than x4, say, is misleading in its specificity, as it were. The best solution (theoretically -- practically it is a nightmare) is to use the most likely F and the least likely F, which is
a modified version of Skolem's system: to prove {AxFx}, prove {F the least like x to be F}, to instantiate {Sx Fx} use {F the most likely x to be F}. For the rest, spelling out the steps carefully usually makes it clear -- eventually (or course, what constitutes a step is an extralogical issue: if you know how it goes, then you can skip it; if you don't, you have to have it in).