Inference rules and tautologies relationship I'm new to logic and I read different books on the same topics to get different insights. The book I'm reading now is "A First Course in Mathematical Logic and Set Theory by Michael L. O'Leary" and in the book he gives a list of inference rules, for example:
Modus Ponens: $p→q, p ⇒ q$
Modus Tolens: $p→q, ¬q ⇒ ¬p$
Hypothetical Syllogism: $p→q, q→r ⇒ p→r$
etc.
He makes a distinction between "$→$" and "$⇒$", he introduces the symbol $⇒$ saying:
The propositional forms $p_0, p_1, …, p_{n-1}$
infer $q$ if $q$ can be written whenever $p_0, p_1, …, p_{n-1}$ are written. Denote this by $p_0, p_1, …, p_{n-1}⇒q$
so that just means that its a deductively valid argument.
in the other books i read, they don't do this, they give a list of tautologies, also called "laws of logic", and I "discovered" that all of these inference rules (valid arguments) are tautologies and can be written in 2 more ways:
Modus Ponens:
$$p→q, p ⇒ q$$ $$(p→q)→(p→q)$$
$$((p→q)∧p)→q$$
Modus Tolens:
$$p→q, ¬q ⇒ ¬p$$
$$(p→q)→(¬q→¬p)$$
$$((p→q)∧¬q)→(¬p)$$
Hypothetical Syllogism: $$p→q, q→r ⇒ p→r$$ $$(p→q)→((q→r)→(p→r))$$
$$((p→q)∧(q→r))→(p→r)$$
etc.
So I guess i'm missing something, in a book they explained this while talking about truth trees, but that's not really the explanation i'm looking for, I would like to know the reason why this happens, i would like to know the "rule" i'm missing, can you guys help me please?
 A: The author uses $⇒$ to mean (see page 21): 

"it is the conclusion of a rule of inference".

Most textbooks use the "bi-dimensional" pattern in page 21 to represent rules, like e.g.

$\dfrac {p \ \ p \to q} {q}$

and the standard $\vdash$ symbol for "it is derivable" (page 26) and $\vDash$ for "it is a (semantical) consequence" or "logical consequence" of "logically implies" (page 21).
Thus, IMO, there is no need of a specific symbol for "infer", because a derivation may have a single step, and thus an application of MP can be written simply as:

$p, p \to q \vdash q$.

See also the post: Meaning of symbols $⊢$ and $⊨$, as well as the post: Difference between $→$, $⊨$ and $⟹$.

The link between inference and tautologies in propositional logic is quite simple (see Deduction Theorem and Soundness and Completeness of the calculus):

$\varphi \vdash \psi \text { iff } \vdash \varphi \to \psi$ (and the same for $\vDash$).

Thus, for a typical two-premises rules of inference: $\dfrac {\varphi_1 \ \ \varphi_2}{\psi}$ we have:


$\vDash \varphi_1 \to (\varphi_2 \to \psi)$,


which is equivalent (by Exportation) to: $\vDash (\varphi_1 \land \varphi_2) \to \psi$.
