What's the difference between "$\to$" (implication) and "$\vdash$" (therefore)?
Solution 1:
$(p \land q) \to p$ is a sentence in propositional calculus. When $p$ and $q$ are assigned truth values, that sentence always gets the value true, that is, is a tautology.
$(p \land q) \vdash p$ is a statement in a metalanguage about propositional calculus. It says that $p$ can be deduced from $p \land q$ according to whatever deduction rules are valid.
Solution 2:
The connection between the material conditional and provability is an important one, and very intuitive once the basic definitions are understood. In a formal proof we assume a set of premises and derive a particular conclusion. Let's call the set of premises $\Gamma$ and the conclusion $\psi$. Now suppose we want to prove $\varphi$, but our premises are too weak to prove it by themselves. So we additionally assume $\theta$, and manage to derive $\varphi$. We represent this symbolically by saying that $\Gamma \cup \left\{\theta\right\} \vdash \varphi$.
Contrast this with a conditional statement, like the following: if $x + y < z$, then $x < z \wedge y < z$ (for $x,y,z \in \mathbb{N}$). We can formalise this in the predicate calculus using the material conditional: $\forall{x}\forall{y}\forall{z} (x + y < z \rightarrow x < z \wedge y < z)$.
The deduction theorem states that given $\Gamma \cup \left\{\theta\right\} \vdash \varphi$, we can assert that our initial set of premises $\Gamma$ proves the conditional statement $\theta \rightarrow \varphi$. Formally, $(\Gamma \cup \left\{\theta\right\} \vdash \varphi) \vdash (\Gamma \vdash \theta \rightarrow \varphi)$, which is just a slightly more general version of the conditional proof rule $(p \vdash q) \vdash (\vdash p \rightarrow q)$.
It's important to bear in mind the distinction here between the object language, which is the language in which the premises, conclusion and all steps of the proof are stated, and the metalanguage which lets us make assertions about what can be proved from what. $\rightarrow$ is a symbol of the object language, which informally corresponds to the if...then locution in English. $\vdash$ is a symbol of the metalanguage, and corresponds to provability: from these premises, this conclusion can be derived. The importance of the deduction theorem is that it shows a way for us to move from statements of the metalanguage to statements of the object language.
Here's an updated answer to your second question, having looked at the link page for more than a second. The example proof is complicated just so they can show a chain of reasoning with steps between the initial assumption and the derivation of $A \vdash A$.
- $A$ (Assumption)
- $A$ (From 1)
- $A \vdash A$ (From 1 and 2)
- $\vdash A \rightarrow A$ (From 3 by CP)
So far, so obvious. And of course by simply inspecting the truth table for $A \rightarrow A$ we can see that it's a tautology; this is the semantic approach, while the derivation shown on the Wikipedia page is a syntactic approach.
The problem with the truth table approach is that it doesn't scale to first-order logic: what's the truth table for $\forall{x} \; P(x)$? Assuming we assigned constants to every element of the domain, we could posit some kind of analogue for a truth table, but if the domain were infinite then the truth table would be infinitely wide! This is why semantics for first-order logic are given by model theory, not truth tables. However, the deduction theorem still holds in first-order logic (for closed formulae).