Difference between "if $\vdash P$, then $\vdash Q$" and "$\vdash(P\Rightarrow Q)$"?

Question

I have agonized about the difference between

1. If $\vdash P$, then $\vdash Q$,
2. $\vdash(P\Rightarrow Q)$.

For example, in the axiom set of predicate logic, there are two similar axioms, called and which are,

= Rule of Generalization =
Hypothesis    $\vdash\varphi$
Assertion    $\vdash\forall x\varphi$

= Axiom of Quantifier Introduction =
Hypothesis    None
Assertion    $\vdash(\varphi\rightarrow\forall x\varphi)$.

(Referred to http://us.metamath.org/mpegif/mmset.html#pcaxioms)

I do not know why there are two various version of same(I think) or similar(Maybe) axioms in the theory.

Is there anyone can tell me the right usage of hypothesis, assertion, and implying? If there is a recommended book, it is also welcome.

Answer 1

The headline version:

(1) says: if $P$ is a theorem [of whatever proof-system is in play], the $Q$ is a theorem.

(2) says: $(P \to Q)$ is a theorem.

These are quite different claims. Here's a simple example where they peel apart. In any standard modal logic we have

(1a) if $\varphi$ is a modal logical theorem, then so is $\Box\varphi$

Because if you can logically prove $\varphi$, then it is necessarily true (and that's a bit of logic!), so $\Box\varphi$. But

(2a) it is not a modal logical theorem that $\varphi \to \Box\varphi$.

It is not logically true that if some something is true it is necessarily true.

In many systems of first order logic, we similarly have

(1b) if $Px$ is a theorem, so is $\forall x Px$

[That's because wffs with free variables are in effect treated as implicitly universally quantified: but some systems don't like this!] But

(2b) it is not a theorem that $(Px \to \forall xPx)$.

For suppose otherwise. Then by (1b) we'd have the theorem $\forall x(Px \to\forall xPx)$, so instantiating with a name, we'd have the theorem $(Ps \to \forall xPx)$, and we'd have "proved", e.g. that if Socrates is a philosopher, everyone is a philosopher!!!

Any good textbook on first-order logic should make this sort of thing clear: for reading suggestions you can look here: http://www.logicmatters.net/resources/pdfs/TeachYourselfLogic9-2.pdf