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?
Best Answer
$(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.