$\to$ vs. $\vdash$ in logic

First, I'm surprised that nobody has pointed out that reading $\vdash$ as "infers" is simply wrong: implies versus infers.

You might read $\vdash$ as "proves" or "entails". On the other hand, "infers" is roughly the same as "deduces". Saying $A\vdash B$ means that one can deduce $B$ from $A$; if you read $\vdash$ as "infers" you're reading $A\vdash B$ as "$A$ deduces $B$", which, regardless of whether it makes any sense, certainly does not mean the same thing.

On the difference between $\to$ and $\vdash$: $A\to B$ is just a formula in ur formal system; it does not say anything (it's not an assertion). On the other hand, $A\vdash B$ is a statement about the formulas $A$ and $B$; it says that given $A$ there is a proof of $B$ in whatever formal proof system we're taking about.

If the proof system is sound and complete then $A\vdash B$ is equivalent to "$A\to B$ is a tautology". But jumping from there to the conclusion that $A\vdash B$ is equivalent to $A\to B$ is wrong; "$A\to B$ is a tautology" is a statement about $A$ and $B$, while $A\to B$ is simply not a statement at all.

An analogy from algebra: if $x$ and $y$ are numbers then $x>y$ is a statement about $x$ and $y$, while $x-y$ is not a statement at all, it's just a number. It is true that "$x>y$ is equivalent to $x-y>0$", but if you concluded that "$x>y$ is equivalent to $x-y$" that would be clearly nonsense. Going from the true fact "$A\vdash B$ is equivalent to the statement that $A\to B$ is a tautology" to "$A\vdash B$ is equivalent to $A\to B$" is making exactly the same error

We have in place a very sharp distinction between the object language connective $\to$ and the metalinguistic sign $\vdash$ for the derivability relation (and the metalinguistic sign $\vDash$ for the logical consequence (or entailment) relation).

$(P \land Q) \vdash Q$ expresses the existence in the propositional claculus of an argument.

The metalinguistic formula asserts that we have a derivation of $Q$ from hypothesis $P \land Q$.

A derivation in the calculus is the formal counterpart of the concept of inference: every step in the derivation is the application of a rule of inference (like e.g. modus ponens) and a rule of inference is the formalization of an "elementary step" in the inferential process.

The formula $(P \land Q) \to Q$ is a single formula in the language of propositional calculus.

If we assert it, we are assering that "either $(P \land Q)$ is false or $Q$ is true".

In ordwer to appreciate the difference, we have to consider that we can formalize the propositional calculus with only teo conenctives :

$\land$ and $\lnot$ (or $\lor$ and $\lnot$)

but the derivability relation does not change its definition.

Of course, there is a link between the two notions, and the link is formalized by the meta-logic property of the calculus expressed by the Deduction Theorem stating that :

if a formula $B$ is derivable from a set of assumptions $\Delta \cup \{A\}$, then the formula $A \to B$ is derivable from $\Delta$.

The deduction theorem is a formalization of the common proof technique in which an implication $A \to B$ is proved by assuming $A$ and then deriving $B$ from this assumption conjoined with known results.