Well, there's a tricky thing in mathematics called "the law of excluded middle". Using the law, you can e.g. prove that a implies b is logically equivalent to (not a) or b. It also lets you do existence proofs by proving it isn't possible for there to be no examples. So in classical logic every statement is confused with its double negation.

I generally try to use intuitionistic logic though, where a->b is not logically equivalent to anything else and double negations have to be written out. You do have , but that only goes one direction and results in a weaker statement. If you look at my other reply with an intuitionistic frame of mind, then you'll see that the "only" is an implication, with no negation in sight.

Not necessarily: see mathnerd314's comment below (or above). In fact, in “there is no other”, there is a double negation (the second being in “other”, which hides “not equal to”), which can be eliminated.

Indeed, but one of Eliezer's points was that mathematical objects, e.g. the set of prime numbers, don't need labels. I can write without giving it a name at all, or just call it P.