Implication arrows, turnstiles etc

Question

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?

Answer 1

1. Yes.
2. Yes. Note that if the completeness theorem holds (this is the case in propositional or first-order logic), then $\vdash$ and $\models$ are essentially interchangeable, except that $\mathfrak{M} \vdash a$ and $\mathfrak{M} \vdash T$ make no sense.
3. Yes, more precisely $a \equiv b$ usually means $\models (a \to b) \land (b \to a)$ (which is the same as $\vdash (a \to b) \land (b \to a)$ if the completeness theorem holds). Sometimes you can also find the notations $a \equiv_T b$ (which means $T \models (a \to b) \land (b \to a)$), and $a \dashv\vdash b$ (which means $\vdash (a \to b) \land (b \to a)$, and $a \dashv\vdash_T b$ (which means $T \vdash (a \to b) \land (b \to a)$).
4. Often $a \implies b$ stands for $T \vdash a \to b$ where the theory $T$ is clear from the context (and usually $T$ is a theory in a logic where the completeness theorem holds). But this notation is very informal (though useful and common), and it can have other meanings. So, be careful. For instance, sometimes it can mean that "Since $a$ holds (in a theory $T$) and $b$ follows from $a$, then $b$ holds" (i.e., also a modus ponens is left implicit); formally, in this case it stands for $T \vdash a \land (a \to b)$ (and hence $T \vdash b$).