What are these symbols in logic called? Per Ebbinghaus' Mathematical Logic, or any other standard mathematical logic books:

*

*Is $\models$   called (logical) consequence relation between formulas?


*Is $\unicode{x27DA}$  called (logical) equivalence relation between formulas?


*Is $\vdash$  called derivable   relation between formulas?


*Is $\unicode{x27DB}$ (a symmetric relation between formulas, defined in terms of $\vdash$) called derivable equivalence? (Does Ebbinghaus' book ever use it?)


*Is $\to$  called (material) implication (a connective between formulas, to create a compound formula)? Is $⇒$ the same as $\to$?


*Is $\leftrightarrow$ (a connective between formulas, to create a compound formula, defined in terms of $\to$) called (material) equivalence?  Is $⇔$ the same as $\leftrightarrow$?


*What does $\equiv$ mean in logic? ($\unicode{x27DA}$, $\unicode{x27DB}$, $\leftrightarrow$, $=$, or something else?). ($\equiv$ is called "equality" symbol in II.3.1 in Ebbinghaus' book and used to create a formula from two terms. Does it have a different meaning $\unicode{x27DA}$ in this Wikipedia page ?)
Thanks.
 A: 

*

*Is $\models$   called (logical) consequence relation between formulas?


Yes. Or (logical) inference or (logical) entailment or semantic consequence/inference/entailment.


*

*Is $\unicode{x27DA}$  called (logical) equivalence relation between formulas?


Yes.


*

*Is $\vdash$  called derivable   relation between formulas?


It is called derivability.


*

*Is $\unicode{x27DB}$ (a symmetric relation between formulas, defined in terms of $\vdash$) called derivable equivalence? (Does Ebbinghaus' book ever use it?)


It is called interderivability. Don't know the entire Ebbinghaus book by heart, but you don't see it as often as logical equivalence or unidirectional derivability.


*

*Is $\to$  called (material) implication (a connective between formulas, to create a compound formula)?


Yes, or (material) conditional. Sometimes (esp. in older texts) you also see

⊃

being used for material implication.


*

*Is $⇒$ the same as $\to$?


Sometimes yes; sometimes $⇒$ means logical consequence; sometimes $⇒$ means a meta-linguistic (= mathematical English) "if ... then".


*

*Is $\leftrightarrow$ (a connective between formulas, to create a compound formula, defined in terms of $\to$) called (material) equivalence?


It is ususally called biimplication or biconditional, perhaps sometimes (material) equivalence.


*

*Is $⇔$ the same as $\leftrightarrow$?


Analogous to above: Sometimes yes; sometimes it means logical equivalence; sometimes sometimes a meta-linguistic "if and only if".


*

*What does $\equiv$ mean in logic? ($\unicode{x27DA}$, $\unicode{x27DB}$, $\leftrightarrow$, $=$, or something else?).


Usually it means logical equivalence, sometimes biimplication and sometimes syntactic identity (= literal sameness of formulas).

$=$

usually means term equality in FOL; sometimes it is used for logical equivalence and sometimes for syntactic identity.

$\bumpeq$

is sometimes seen for syntactic identity.
A: An example using all of the symbols:
The second symbol ($\unicode{x27DA}$) is stating that 2 formula are each a logical consequence of each other i.e.
$A \unicode{x27DA} B$ states that:
$A \vDash B $ and $ B \vDash A$
Therefore, $ A \equiv B $ ($\equiv$ meaning logical equivalence).
They are logically equivalent because $ A \leftrightarrow B $ is a Tautology.
$ (A \rightarrow B) \wedge (B \rightarrow A) $ would also be a Tautology.
$A \unicode{x27DA} B$ would also mean that $ A \unicode{x27DB} B $ (assuming a 'complete' inference system) i.e.
$ A \vdash B $ and $ B \vdash A $
Meaning that B can be derived from A and that A can be derived from B.
A: Original question: "What does $\leftrightarrow$ mean?"
It is called a bi-conditional relation. If given statements $P$ and $Q$, then $P\leftrightarrow Q$ means that $$(P\rightarrow Q )\wedge (Q\rightarrow P)$$
