Difference between "if $\vdash P$, then $\vdash Q$" and "$\vdash(P\Rightarrow Q)$"? I have agonized about the difference between


*

*If $\vdash P$, then $\vdash Q$,

*$\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.
 A: 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
A: About the Axiom of Quantifier Introduction, in your quotation you have forgot the proviso.
The complete formulation is:

$\vdash (\varphi → ∀x \varphi)$, if $x$ is not [free] in $\varphi$.

This formula is valid and the proviso does not licence the derivation of the invalid : $(Px \rightarrow \forall xPx)$.
The proviso is also the reason why this axiom and the Rule of Modus Ponens are not enough to derive the Rule of Generalization.
With them we can only derive a "restricted version" of it :

If $\vdash \varphi$ and $x$ is not free in $\varphi$, then $\vdash \forall x \varphi$.


This axiom can be used in connection with another quantifier axiom : the Axiom of Quantified Implication, to prove the :

GENERALIZATION (meta-)THEOREM : If $\Gamma \vdash \varphi$ and $x$ does not occur free in any formula in $\Gamma$, then $\Gamma \vdash \forall x \varphi$.

From it, with $\Gamma = \emptyset$ [there are no formulae in $\Gamma$: thus, the proviso is vacuously satisfied], we can derive the (unrestricted) Rule of Generalization :

If $\vdash \varphi$, then $\vdash \forall x \varphi$.



About :

if $\vdash P$, then $\vdash Q$

and :

$\vdash (P \rightarrow Q)$

there is a difference : the two are not equivalent.
Consider propositional logic; if we have derived : $P \rightarrow Q$ and $P$, it is enough to apply modus ponens to derive : $Q$.
But from the assumption : if $\vdash P$, then $\vdash Q$, does not follows that : $\vdash (P \rightarrow Q)$.
It is well known that, if $p_1$ is a sentential letter, we cannot have $\vdash p_1$ (no sentential letter is a tautology); of course, the same holds with $\vdash \lnot p_1$. Thus, both $\vdash p_1$ and $\vdash \lnot p_1$ are false (meta-)logical assertions.
Then, the conditional : "if $\vdash p_1$, then $\vdash \lnot p_1$" is true.
But of course, $\nvdash p_1 \rightarrow \lnot p_1$ ($p_1 \rightarrow \lnot p_1$ is not a tautology).
See Jan von Plato, Elements of Logical Reasoning (2013), page 47 :

The "argument" :

Assume that if $P$ is derivable, then $Q$ is. Then $P \rightarrow Q$ is derivable

is a logical fallacy.


These considerations apply also to Generalization : we have "if $\vdash \varphi$, then $\vdash \forall x \varphi$" (it is the Rule of Generalization.) but not (without proviso) $\vdash (\varphi \rightarrow \forall x \varphi)$.
A: A simple counter example.
Let $P(x)$ be "$x$ is prime", and $Q(x)$ be "$x$ is odd".
The statement $\vdash (P \implies Q)$ is false, because there is a prime number that is not odd.
However, since not all numbers are prime, we have $\vdash P$ is false.  Thus, $(\vdash P) \implies (\vdash Q)$ is true.
Translated into English:
$\vdash (P \implies Q)$ means "For all $x$, if $x$ is prime, then $x$ is odd."
$(\vdash P) \implies (\vdash Q)$ means " 'For all $x$, $x$ is prime' implies 'For all $x$, $x$ is odd'."
