Completeness of the Gentzen Sequent Calculus Let $A_1, \dots, A_n ,B_1, \dots, B_m \in  \mathcal{F}_{¬,\lor}$ with $\models \lnot A_1 \lor \ldots \lor \lnot A_n \lor B_1 \lor \ldots \lor B_m$ ($\mathcal{F}_{¬,\lor}$ is the set of formulas built up from propositional variables and the connectives $\lnot$ and $\lor$). Show that this implies that the sequent  $A_1, \ldots, A_n \vdash_G B_1, \ldots, B_m$ is derivable in the Gentzen sequent calculus.
Use induction over the overall number of operators ($\lor$ and $\lnot$) in $A_1, \dots, A_n, B_1, \dots, B_m$.
Note: As a special case of the statement above we get: if $\models B_1$ then $\vdash_G B_1$ is derivable (for $B_1 \in \mathcal{F}_{\lnot,\lor}$).
I understand Gentzen sequence calculus. But I am unable to prove this using induction. 
 A: The proof of your statement is by induction on the number $k \in \mathbb{N}$ of occurrences of $\lor$ and $\lnot$ in the finite sequence of formulas $A_1, \dots, A_n, B_1, \dots, B_m$ (I refer to the inference rules for Gentzen sequent calculus listed here).
If $k = 0$ then all $A_i$'s and $B_j$'s are propositional variables. 
Since $\models \lnot A_1 \lor \dots \lor \lnot A_n \lor B_1 \lor \dots \lor B_m$, there exist $1 \leq i \leq n$ and $1 \leq j \leq m$ such that $A_i = B_j$ (otherwise $ \lnot A_1 \lor \dots \lor \lnot A_n \lor B_1 \lor \dots \lor B_m$ is falsified by the valuation assigning true to all $A_i$'s and false to all $B_j$'s). Therefore, $A_1, \dots, A_n \vdash B_1, \dots, B_m$ is derivable, for instance by  the following derivation
\begin{equation}
\dfrac{\dfrac{\dfrac{}{A_i \vdash B_j}\text{ax}}{A_i \vdash B_1, \dots, B_m}\text{w}_R \text{ ($m-1$ times)}}{A_1, \dots, A_n \vdash B_1, \dots, B_m}\text{w}_L \text{ ($n-1$ times)}.
\end{equation}
If $k > 0$ then there are four cases:


*

*There exists $1 \leq i \leq n$ such that $A_i = \lnot A$.
As $\models \lnot A_1 \lor \dots \lor \lnot \lnot A \lor \dots \lor \lnot A_n \lor B_1 \lor \dots \lor B_m$ by hypothesis, then $\models \lnot A_1 \lor \dots \lor \lnot A_{i-1} \lor \lnot A_{i+1} \lor \dots \lor \lnot A_n \lor A \lor B_1 \lor \dots \lor B_m$.
By induction hypothesis, $A_1, \dots, A_{i-1}, A_{i+1}, \dots A_n \vdash A, B_1, \dots, B_m$ is derivable; therefore, $A_1, \dots, A_n \vdash B_1, \dots, B_m$ is derivable, for instance by the following derivation
\begin{equation}
\dfrac{\overset{\vdots}{A_1, \dots, A_{i-1}, A_{i+1}, \dots A_n \vdash A, B_1, \dots, B_m}}{A_1, \dots,  \lnot A, \dots A_n \vdash B_1, \dots, B_m}\lnot_L.
\end{equation}

*There exists $1 \leq i \leq n$ such that $A_i = A \lor A'$. 
As $\models \lnot A_1 \lor \dots \lor \lnot (A \lor A') \lor \dots \lor \lnot A_n \lor B_1 \lor \dots \lor B_m$ by hypothesis, then $\models \lnot A_1 \lor \dots \lor \lnot A \lor \dots \lor \lnot A_n \lor B_1 \lor \dots \lor B_m$ and $\models \lnot A_1 \lor \dots \lor \lnot A' \lor \dots \lor \lnot A_n \lor B_1 \lor \dots \lor B_m$.
By induction hypothesis, $A_1, \dots, A, \dots, A_n \vdash B_1, \dots, B_m$ and $A_1, \dots, A', \dots, A_n \vdash B_1, \dots, B_m$ are derivable;
therefore, $A_1, \dots, A_n \vdash B_1, \dots, B_m$ is derivable, for instance by the following derivation
\begin{equation}
\dfrac{\overset{\vdots}{A_1, \dots, A, \dots A_n \vdash B_1, \dots, B_m} \qquad \overset{\vdots}{A_1, \dots, A', \dots A_n \vdash B_1, \dots, B_m}}{A_1, \dots, A \lor A', \dots A_n \vdash B_1, \dots, B_m}\lor_L.
\end{equation}

*There exists $1 \leq j \leq m$ such that $B_j = \lnot B$.
As $\models \lnot A_1 \lor \dots \lor \lnot A_n \lor B_1 \lor \dots \lor \lnot B \lor \dots \lor B_m$ by hypothesis, then $\models \lnot A_1 \lor \dots \lor \lnot A_n \lor \lnot B \lor B_1 \lor \dots \lor B_m$.
By induction hypothesis, $A_1, \dots, A_n, B \vdash B_1, \dots, B_m$ is derivable; therefore, $A_1, \dots, A_n \vdash B_1, \dots, B_m$ is derivable, for instance by the following derivation
\begin{equation}
\dfrac{\overset{\vdots}{A_1, \dots, A_n, B \vdash B_1, \dots, B_m}}{A_1, \dots, A_n \vdash B_1, \dots, \lnot B, \dots, B_m}\lnot_R.
\end{equation}

*There exists $1 \leq j \leq m$ such that $B_j = B \lor B'$.
As $\models \lnot A_1 \lor \dots \lor \lnot A_n \lor B_1 \lor \dots \lor (B \lor B') \lor \dots \lor B_m$ by hypothesis, then $\models \lnot A_1 \lor \dots \lor \lnot A_n \lor B \lor B' \lor B_1 \lor \dots \lor B_m$.
By induction hypothesis, $A_1, \dots, A_n \vdash B_1, \dots, B, B', \dots, B_m$ is derivable; therefore, $A_1, \dots, A_n \vdash B_1, \dots, B_m$ is derivable, for instance by the following derivation
\begin{equation}
\dfrac{\overset{\vdots}{A_1, \dots, A_n \vdash B_1, \dots, B, B', \dots, B_m}}{A_1, \dots, A_n \vdash B_1, \dots, B \lor B', \dots, B_m}\lor_R.
\end{equation}
