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$).

Answer 2

I would like to supplement the above answer with a couple of comments and note that Q2 needs more discussion.

1. Yes, this is a good list of "standard" notations, but because of equivalence theorems (especially the soundness and completeness theorems) some textbooks will deviate from these definitions. For example Boolos and Jeffrey use $\vdash$ when introducing "semantic inference" and after the completeness theorem re-use it to mean deductibility also. Also "semantic inference" is sometimes called "logical inference". These issues become important as one moves on from elementary logic, to the endless variety of other logics: modal logic, 3-valued logic, etc, in which the completeness theorem might not hold.

2. The statement that $a \vdash b$ implies $\vdash a \rightarrow b$ is actually the deduction theorem. Again primarily a propositional and first order logic (meta-)theorem, but it can be proven for other logics too, but again the given logic will need to establish this result. I see that a form of Quantum Logic is given as an example in which this meta-theorem fails.

3. As other answer.

4. In a formal logic textbook $\implies$ will probably be introduced early on, probably in the propositional logic chapter. However in a Mathematical lecture or notes $\implies$ is used to represent the steps in the mathematical proof being presented. E.g. in an Algebra class we might have some steps like : $x > 1 \implies x^2 > 1$ with the range of the variables implicit, but defined by the algebra, and so the full logical formulation of the algebraic proofs (in terms of models, languages, inference rules, etc) left implicit.