Provability of sequents in LK In his answer to my question Andreas Blass writes: "$A\lor(B\land C)$ doesn't classically imply $(A\lor B)\land C$". I read this as: The sequent $A\lor(B\land C) \vdash (A\lor B)\land C$ is not derivable in Gentzen's sequent calculus LK. What are ways to prove the last statement?
I would appreciate a variety of ways of tackling that problem.
I apologize in advance for my lack of knowledge of proof theory and sequent calculus. However, I have so little understanding that I think I would profit from seeing a few strategies of proving non-derivability of a sequent.
 A: According to the soundness theorem for LK with respect to classical propositional logic, if a sequent $A_1, \dots, A_n \vdash B_1, \dots, B_m$ (with $n,m \geq 0$) is provable in LK then every valuation that makes all the formulas $A_1, \dots, A_n$ true makes also true at least one  among the formulas $B_1, \dots, B_m$.
Therefore, to prove that a sequent $A_1, \dots, A_n \vdash B_1, \dots, B_m$ is not provable in LK it suffices to show a valuation that makes all formulas $A_1, \dots, A_n$ true and all formulas $B_1, \dots, B_m$ false.
Let us apply this semantic method to your example. To prove that the sequent $A \lor (B \land C) \vdash (A \lor B) \land C$ is not provable in LK it is enough to show that the valuation $v$ such that
\begin{align}
v(A) &= \text{true} 
&
v(B) &= v(C) = \text{false}
\end{align}
makes the antecedent formula $A \lor (B \land C)$ true and the consequent formula $(A \lor B) \land C$ false.

There are also proof-theoretical methods to prove that a sequent is not provable in LK for propositional logic. For instance, consider the variant of LK made up of the inference rules below ($\Gamma$ and $\Delta$ are multisets of formulas):
\begin{align}
\dfrac{}{\Gamma, A \vdash A, \Delta}\text{ax} 
&&
\dfrac{\Gamma \vdash A , \Delta \qquad \Gamma \vdash B, \Delta}{\Gamma \vdash A \land B, \Delta}\land_R
&&
\dfrac{\Gamma, A, B \vdash \Delta}{\Gamma, A \land B \vdash \Delta}\land_L
&&
\dfrac{\Gamma, A \vdash \Delta}{\Gamma\vdash \lnot A,\Delta}\lnot_R
\\[0.5em]
&&
\dfrac{\Gamma, A \vdash \Delta \qquad \Gamma, B \vdash\Delta}{\Gamma, A \lor B \vdash \Delta}\lor_L
&&
\dfrac{\Gamma \vdash A, B , \Delta}{\Gamma \vdash A \lor B, \Delta}\lor_R
&&
\dfrac{\Gamma \vdash A, \Delta}{\Gamma, \lnot A \vdash \Delta}\lnot_L
\end{align}
Starting with any sequent $\Gamma \vdash \Delta$ in propositional logic, building a derivation tree bottom up by a series of steps, the right side of the turnstile can be processed until it includes only atomic symbols. Then, the same is done for the left side. Since every connective appears in one of the rules above, and is removed by the rule, the process terminates when no connectives remain: The start sequent $\Gamma \vdash \Delta$ has been decomposed.
Thus, the sequents in the leaves of the trees include only atomic symbols, which are either provable by the rule $\textit{ax}$ or not, according to whether one of the symbols on the right also appears on the left. The sequent $\Gamma \vdash \Delta$ (which is as the bottom--the root--of the tree) is provable in LK if and only if all the leaves of the tree are instances of the rule $\textit{ax}$. (It is easy to check the inference rules above are equivalent to the standard LK for propositional logic)
We can apply this method to your example. We obtain (some subtrees are omitted and denoted by vertical dots):
\begin{align}
\dfrac{\dfrac{\vdots}{A \lor (B \land C) \vdash A\lor B} \qquad \dfrac{A \vdash C \qquad \dfrac{\vdots}{B \land C \vdash C}}{A \lor (B \land C) \vdash C}\lor_L}{A \lor (B \land C) \vdash (A\lor B) \land C}\land_R
\end{align}
where there is a leave that is not an instance of the rule $\textit{ax}$ (as $A \neq C$), hence the sequent $A \lor (B \land C) \vdash (A \lor B) \land C$ is not provable in LK.
