What's the difference between "$\to$" (implication) and "$\vdash$" (therefore)? In Wikipedia, here in the last axiom of the Natural deduction system, it says "From [accepting $p$ allows a proof of $q$], infer $(p \to q)$." Isn't that a tautology? In the big table "Basic and Derived Argument Forms" that follows, I see it using a new symbol "$\vdash$" to express "therefore". Isn't that something can be done by the symbol "$\to$"? For example, what's the difference between "$(p \land q) \vdash p$" and "$(p \land q) \to p$"?
An interesting symbolic representation of the last axiom of NDS is that $(p \vdash q) \vdash (\vdash p \to q)$. Which I don't understand why is made so complicated.

What also puzzles me is in the "example of a proof" that follows. Since you list "$A$" as a promise, which is basically saying "assuming $A=\text{True}$", then why you have to go around such a big circle, using disjunction, conjunction, and conjunction elimination to prove back that "$A$" is true? If it is me, I would say "assuming $A=\text{True}$, we will know that $A=\text{true}$. Bang! Now we get $A \vdash A$, so we have $\vdash A \to A$." What's wrong in this deduction?
 A: $(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.
A: 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).
A: Talk of the 'metalanguage' can be a little confusing in my opinion, so maybe an order-theoretic perspective would be clearer? In particular, let $P$ denote a Heyting algebra. Consider $p,q \in P$. Then:


*

*$p \wedge q \leq p$ is simply true.

*$(p \wedge q) \rightarrow p$ is an element of $P$.

*That element happens to equal $1$.


Furthermore, $\vdash$ is a bit like $\leq$, except you can have multiple inputs on the left. For example, we could define:

Definition. A multiposet is a thin multicategory.
We write $x_0,\ldots, x_{n-1} \vdash y$ to mean that there exists a multiarrow $x_0,\ldots,x_{n-1} \rightarrow y$.

A: In addition to what got pointed out in the other comments, (p∧q)→p, once we write exactly what the author means, that is ((p∧q)→p), we have a well-formed formula (or formula or statement form).  On the other hand, ((p∧q)⊢p) is not a well-formed formula, as it doesn't follow the formation rules of some language, or at least needs a set of formation rules distinct from that of ((p∧q)→p) as it exists in the metalanguage, not the object language.
