Difference between bound and free variable What is the difference between 
$\forall x (P(x)\implies Q(x))$   and $P(x)\implies Q(x)$
I know in the first one the variable x is bound but in the second one the variable is free. What are the consequences of this when proving it(Is the proof of the first statement different from the second)?
Also $ x>2 \implies x>4$ and $\forall x (x>2 \implies x>4)$ What is the difference(When proving how are the proofs different) ?
Also, in limits $\forall \epsilon >0 \exists \delta >0 \forall x ( |x-a|<\delta \implies |f(x)-L|<\epsilon)$. Are $\epsilon, \delta,x$ bound and $a,f(x)$ free?
 A: In first-order logic typical rules governing the quantifiers are :

$${\Gamma \vdash \forall x \alpha \over \Gamma \vdash \alpha [x/t] }\, \, (\text{where} \, t \, \text{is substitutable for} \, x \text{in} \alpha)$$
$${\Gamma \vdash \alpha [x/y] \over \Gamma \vdash \forall x \alpha }\, \, (y \, \text{not free in} \, X \cup \alpha)$$

Thus, in your example, having proved :

$∀x[P(x) \rightarrow Q(x)]$

we can derive :

$P(t) \rightarrow Q(t)$

for every term $t$, included $x$ itself.
For the other "direction", if we have proved :

$\Gamma \vdash P(y) \rightarrow Q(y)$,

provided that $y$ is not free in any formula in $\Gamma$, we can conclude :

$\Gamma \vdash \forall x[P(x) \rightarrow Q(x)]$.

In the above proof $\Gamma$ is a set of formulae, and we can have $\Gamma = \emptyset$.
Thus, as a particular case of the above meta-theorem (usually called Generalization Theorem) we have :

if $\vdash \alpha[x/y]$, then $\vdash \forall x \alpha$.

The proviso is necessary in order to avoid fallacies.
If we assume $x = 0$, we can write the following derivation :
$x = 0 \vdash x = 0$;
from it, mis-applying the above rule [because $\Gamma = \{ x = 0 \}$ and $x$ is free in it]:
$x = 0 \vdash \forall x (x = 0)$.
By use of Deduction Theorem we can conclude :
$\vdash x = 0 \rightarrow \forall x (x = 0)$.
But this may not be because, by soundeness of first-order logic (i.e. : if $\vdash \alpha, then \vDash \alpha$) we expect that only valid formulae are provable, and the above formula is not valid.
Tho show that it is not, consider an interpretation with domain the set $\mathbb N$ of natural numbers and consider an assignement $s$ of value to the free variables [i.e. a function $s : Var \rightarrow \mathbb N$] such that $s(x)=0$.
Clearly :
$(x = 0 \rightarrow \forall x (x = 0))[s] = FALSE$
because $(x = 0)[s]$ is $0 = 0$, which is true, while $\forall x (x = 0)$ is false.
A: Pretty much nothing. Unless the quantifier is more specific like $\forall x \in (0, 1)$. Otherwise I would say there is absolutely no difference. $P(x) \implies Q(x)$ makes obvious the fact that the implication is true for each $x$. It means $Q(x)$ is true each time $P(x)$ is true. Makes no sense to put the quantifier at the beginning. Not a fan of doing it. 
As for the question on the definition of the limit:- Again the quantifier $\forall x$ seems superfluous. But the quantifiers on $\epsilon$ and $\delta$ are absolutely necessary. I would just read it out in English "For any given $\epsilon \gt 0$ there is a positive number $\delta \gt 0$ such that $ |f(x) - L| $ is less than $\epsilon \;$ whenever $|x - a|$" is less than $\delta$. The "for each $x$" seems redundant. Just trying to make a point here about redundant quantifiers. I am not familiar with the terminology involving bound and free vaiables. Apologies.. Hope I helped. 
A: From my answer to What are the truth-values of intuitionistic logic?

The truth values of classical propositional logic form a Boolean algebra. The only subdirectly irreducible Boolean algebra has cardinality 2 (True & False). Hence the equational theory of classical propositional logic is completely determined by the two element Boolean algebra.

Classical logic can be regarded as the logic of (arbitrary) subsets. Then the formula $P(x)\implies Q(x)$ represents the subset $S=\{x\in X:P(x)\implies Q(x)\}$ of the set $X$. If $S=X$ the proposition is true, if $S=\emptyset$ it is false. The formula $\forall x (P(x)\implies Q(x))$ represents the subset $T=\{y\in \{()\}:\forall x (P(x)\implies Q(x))\}$ of the set $\{()\}$. If $T=\{()\}$ the proposition is true, if $T=\emptyset$ it is false. (The notation "$()$" for the empty tuple is really used in some fields.)
It's easy to see that $S$ is true if and only if $T$ is true. If $\lnot S$ is true then $\lnot T$ is also true. However, if $\lnot T$ is true it is not necessary that $\lnot S$ is also true. This is no big magic, but just the fact that $\lnot(\forall x (P(x)\implies Q(x)))$ doesn't necessarily imply $\lnot(P(x)\implies Q(x))$.

An interesting point is that $P\implies Q$ could also be written as $P(x)\implies Q(x)$, if one wants to emphasise that even a classical proposition is not necessarily bivalued. However, this sort of question normally arises in the exactly opposite way. Somebody who assumes that classical logic is necessarily bivalued has problems making any sense of $P(x)\implies Q(x)$ at all, and hopes to fix this by defining it to mean $\forall x (P(x)\implies Q(x))$. The issue with the negation is slightly annoying, but it's not really a big problem (and it's easy to see what goes wrong). More problematic is that the functoriality of truth values of subformulas has been destroyed by this definition. However, as long as you stay with classical logic, these problems are sufficently small and don't cause too much pain. But if you want to treat intuitionistic logic as the logic of open subsets, it may help if you accept that free variables can be given a prefectly fine meaning. (You can assign them slightly different meanings in different contexts, as long as the functoriality of truth values holds.)
A: 
What is the difference between
$\forall x (P(x)\implies Q(x))$   and $P(x)\implies Q(x)$
I know in the first one the variable x is bound but in the second one the variable is free.

Correct.

What are the consequences of this when proving it? Is the proof of the first statement different from the second?

Under the right circumstances, $\forall x(P(x)\implies Q(x))$ can actually be derived from $P(x)\implies Q(x).$
If, for example, we started a proof with the assumption that $P(x)$ is true (i.e. for a particular $x$), and were able to prove that $Q(x)$ would also have to be true, then we could conclude that $P(x)\implies Q(x)$ (for that same, particular  $x$).
Since $x$ was introduced in the original premise at the beginning of the proof, we could then make a universal generalization about $x$, namely that $\forall x(P(x)\implies Q(x)).$ (Note that universal generalization can also be applied in other circumstances.)
We could not, however, generalize to obtain $\forall x(P(x)\implies Q(x))$  if we simply assumed from the start that $P(x)\implies Q(x).$ We cannot conclude that something is true for all $x$ by simply assuming it is true for a particular $x.$
A: you can use the completness theorem to show that from $P(x)\rightarrow Q(x)$ you can prove $\forall x (P(x)\rightarrow Q(x))$ (using GEN) and the same for the opposing direction (using IMPLIFICATION AX, and MP).
Which shows that they are logically equivalent.
