How to show validity in classical logic? Firstly, I would like to know what does it mean to be a valid expression in classical logic.
Secondly, How do we show validity of a formula (in sequent calculus) such as:
(∀x A → ∃xB) → ∃x(A → B)
As the above expression is not a sequent, how can we convert it to sequent form to show its validity using sequent calculus in classical logic?
 A: The sequent $\phi_1, \ldots, \phi_m, \vdash \psi_1, \ldots, \psi_n$ means that if all the antecedents $\phi_i$ hold, then at least one of the succedents $\psi_j$ holds. In some presentations, you must have exactly one formula on the right, so $n = 1$. However, whether or not you are requiring $n = 1$, to prove that a formula $\psi$ is valid using the sequent calculus, you convert it to the sequent $\vdash \psi$ (with $m = 0$ and $n = 1$).
A: Here is a proof is sequent calculus :

1) $B(a) \vdash B(a)$ --- axiom

2) $A(a), B(a) \vdash B(a)$ --- by Weakening
3) $B(a) \vdash A(a) \rightarrow B(a)$ --- by $\rightarrow$-right  
4) $B(a) \vdash \exists x(A \rightarrow B)$ --- by $\exists$-right
5) $\exists xB \vdash \exists x(A \rightarrow B)$ --- by $\exists$-left

6) $A(a) \vdash A(a)$ --- axiom

7) $A(a) \vdash A(a), B(a)$ --- by Weakening
8) $\vdash A(a) \rightarrow B(a), A(a)$ --- by $\rightarrow$-right
9) $\vdash \exists x(A \rightarrow B), A(a)$ --- by by $\exists$-right
10) $\vdash \exists x(A \rightarrow B), \forall xA$ --- by $\forall$-right
Now we "join" the branches 1)-5) and 6)-10) into :

11)$$\frac{\vdash \exists x(A \rightarrow B), \forall xA \, \, \, \, \, \, \, \, \, \, \exists xB \vdash \exists x(A \rightarrow B)}{∀xA \rightarrow ∃xB \vdash \exists x(A \rightarrow B)}$$ 

by $\rightarrow$-left


12) $\vdash (∀x A → ∃xB) → ∃x(A → B)$ --- by $\rightarrow$-right.


