I would just like to clarify my ideas about a bunch of standard notations introduced in (elementary) mathematical logic.
1) $\quad a\to b\quad$ material/internal/syntactical implication; it's a mere symbol denoting the proposition $\lnot a \vee b$.
2) $\quad T \vdash a\quad$ "there's a proof of $a$ from the theory $T$".
2') $\quad a \vdash b$ (resp. $a \vdash_T b$)$\quad$ turnstile sign, "$b$ provably follows from $a$" i.e. there's a proof of $b$ from $a$ (resp. there's a proof of $b$ from the theory $T\!+\!a$).
2'') $\quad\vdash a\quad$ "$a$ is a tautology" i.e. $a$ follows from the empty set of axioms.
3) $\quad\mathfrak M \models a$ (resp. $\mathfrak M \models T$)$\quad$ "the structure $\mathfrak M$ is a model of/satisfies the sentence $a$" (resp., of the theory $T$)
3') $\quad\models a\quad$ "the sentence $a$ is semantically a tautology" i.e. $a$ is satisfied in every structure (of signature given by the language).
3'') $\quad\models_T a$ (or $T\models a$)$\quad$ "$a$ is a semantic consequence of the theory $T$", i.e. $a$ is satisfied in every model of $T$.
3''') $\quad a\models b\quad$ "$b$ is a semantic consequence of $a$"
3'''') $\quad a \models_T b\quad$ "$b$ is a semantic consequence of $a$ in every model of $T$" i.e.: in every model of $T$ in which $a$ holds, also $b$ holds.
4) $\quad a\equiv b\quad$ "$a$ and $b$ are logically equivalent", i.e. $a$ is true whenever $b$ is true and viceversa.
5) $\quad a \implies b\quad$ blackboard implication symbol.
Q.1 Are the above definitions correct? ( except for 5), which I haven't defined or described )
Q.2 Is $a\vdash b$ the same as $\vdash a\to b$? Is $a\models b$ the same as $\models a\to b$?
Q.3 Is the notation $a\equiv b$ of "logical equivalence" of sentences the same as something expressible by the above other standard notations? ( e.g. $\vdash\!(a\to b\; \wedge\; b\to a)$ ? )
Q.4 As for 5), this is a notation usually used on the blackboard in an informal manner, when you don't really want to distinguish between theory and metatheory, syntax and semantics, or when you're in a specific context left as understood (e.g. ZFC, or when the completeness theorem holds). If one really wanted to pin down a meaning for "$a\implies b$", how should this notation be understood in terms of the above other more formal notations?