Completeness of the Gentzen Sequent Calculus

197 Views Asked by At

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.