Difference between $\to$, $\models$ and $\implies$ I have a problem understanding the difference between $\to$, $\implies$ and $\models$. 
The way I understand it is as follows: 
$\to$ is used inside a formula between propositions. So saying $ A \to B $ is a formula. 
$ \models $ is a statement about formulas. So saying $ A \land B \models A \lor B $ is making a statement about those two formulas $ A \land B $ and $ A \lor B $  and their relationship to each other. 
And now comes my confusion: 
Where does $\implies$ come in all this? 
My textbook made the following distinction: 
"$ F \equiv \top $ is statement about formulas, so we can write (1) $F \equiv \top \implies G \equiv \top $. But this is not the same as (2) $F \models G$. "
But why not? Is it because $\models $ and $ \equiv$ are on the same level? And if yes, then on what level is $\implies$? Is it a statement about a statement about formulas? 
Thank you
 A: Your book uses $\to$ as a logical connective (the conditional), i.e. as a "syntactical object" of the Language of propositional calculus (see page 15).
The symbol : $\top$ denotes the logical constant $\text {TRUE}$ and $\bot$ denotes the $\text {FALSE}$; they are not part of the language (in other cases, they are, and thus $F \to \bot$ is a formula, that can be used as definition for $\lnot F$).
The symbol $\equiv$ is used by your book not as the bi-conditional connective ($\leftrightarrow$, see page 16) but as a meta-mathematical abbreviation for the rleation of (logical) equivalence (see page 17).
Thus

$F \equiv \top$

is not a formula of the language but reads "the formula $F$ is equivalent to the True", i.e. "$F$ is always true", i.e. $F$ is a tautology (see page 20), and thus it is a statement about the formula $F$.
As explicitly stated in the book (page 19), the symbol is a synonym of the usual way to denote the fact that a formula $F$ is a tautology : $\vDash F$.
The book uses $\Leftrightarrow$ as an abreviation for "iff" : this symbol is not part of the language but is part of the meta-language, i.e. it is not used to write formulas but to express relations between formulas. In the same way, the book uses $\Rightarrow$ in the meta-language, to abbreviate "if..., then...". 
Thus

$F≡ \top \Rightarrow G≡ \top$

is simply "if $F$ is a tautology, then $G$ is a tautology."
Also the symbol $\vDash$ is not part of the language of propositional calculus but is the meta-language symbol for logical consequence.
Thus

$F \vDash G$

reads : "there is no valuation $v$ such that $v(F)= \text T$ and $v(G)= \text F$," or (more plainly) :

"$G$ is TRUE in every interpretation where $F$ is TRUE."


The two relations are not the same : we have that "$F \vDash G$" is stronger than "if $F$ is a tautology, then $G$ is a tautology".
Consider the case with $P \lor Q$ as $F$ and $Q$ as $G$; clearly $P \lor Q \nvDash Q$, but $P \lor Q$ is not a tautology, and thus :

if $P \lor Q$ is a tautology, then $Q$ is a tautology,

holds.


Note : compare with van Daleen's textbook, where $\to$ and $\leftrightarrow$ are the conenctives while $\Rightarrow$ and $\Leftrightarrow$ are used as abbreviations in the meta-language
