How to show validity in classical logic?

Question

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?

Answer 1

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.

Answer 2

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$).