With regards to the bracket notation, you're basically correct. It's easiest to state the idea as follows. Let's say, for concreteness, we're dealing with a sentence "A or not-B". This is logically equivalent to "not-(not-A and B)" and "if B, then A" (at least in classical logic). But all three of these are distinct sentences (one's a disjunction, another's a negation of a conjunction, another a conditional). The notation "[A]" or sometimes "[[A]]" can be thought of as conveniently denoting the "propositional content" of A (which can be made mathematically more precise). For instance, in our original example, [A or not-B] = [not-(not-A and B)] = [if B, then A]. (I don't think there's a significant difference between single brackets and double brackets; as far as I know, it's merely notational preference.)
For instance, in the context of modal logic, [A] can denote the set of states in some model at which A is true. In the context of lattices or algebraic logic, [A] can be thought of as a point on a lattice which A (and all its logical equivalents) denotes.
Corner quotes, on the other hand, are more syntactic in nature. They're most often seen in the context of nonstandard models of PA, set theory, or whenever you're dealing with systems which are powerful enough to code sentences of their language (as you sometimes see, for instance, in debates about the Liar's paradox). Corner quotes placed around a proposition form a term in the language you're dealing with, and hence can appear and be referred to in formulae directly. Usually, though, corner quotes around logically equivalent propositions will not denote the same terms.
They're also sometimes used in order to properly account for the use-mention distinction with complex formulae, though this is more of a philosophical device/concern than a mathematical one. (See John MacFarlane's handout on Substitutional Quantifiers for an explanation.)