[proofplan] We argue by contradiction. If the empty sequent had an LK-derivation, cut elimination would give a cut-free derivation of the same empty sequent. We then inspect the last rule of such a cut-free derivation and show that no possible axiom, logical rule, or structural rule can have the empty sequent as its conclusion. This contradiction proves that the empty sequent is not derivable. [/proofplan] [step:Reduce a derivation of the empty sequent to a cut-free derivation] Assume, for contradiction, that there exists an LK-derivation $\mathcal{D}$ whose end sequent is $\Rightarrow$. By the cut-elimination theorem for first-order LK (citing a result not yet in the wiki: Cut Elimination Theorem for First-Order LK), applied to the derivation $\mathcal{D}$, there exists a cut-free LK-derivation $\mathcal{D}_0$ whose end sequent is also $\Rightarrow$. [guided] Assume, for contradiction, that the empty sequent is derivable. That means there is a finite LK-derivation $\mathcal{D}$ with end sequent $\Rightarrow$, where $\Rightarrow$ abbreviates $\varnothing \Rightarrow \varnothing$. The theorem we use is cut elimination for first-order LK: if a sequent has an LK-derivation, then it has an LK-derivation with no application of the cut rule. Applying that result to $\mathcal{D}$ gives a cut-free derivation $\mathcal{D}_0$ with the same end sequent $\Rightarrow$. Thus it is enough to prove that no cut-free LK-derivation can end in the empty sequent. [/guided] [/step] [step:Rule out the possibility that the derivation ends with an initial sequent] The derivation $\mathcal{D}_0$ is finite, so its end sequent is either an initial sequent or is obtained by applying a final inference rule. It cannot be an initial sequent, because every initial sequent of LK has the form $A \Rightarrow A$ for some formula $A$, and therefore contains a formula on both sides. The empty sequent $\Rightarrow$ contains no formula on either side. [guided] Since $\mathcal{D}_0$ is a finite derivation tree, its root is either an initial sequent or the conclusion of some inference rule. We first exclude the initial-sequent case. In LK, an initial sequent has the form $A \Rightarrow A$, where $A$ is a first-order formula. Such a sequent has at least one formula on the left and at least one formula on the right. The empty sequent $\Rightarrow$ has left side $\varnothing$ and right side $\varnothing$. Therefore $\Rightarrow$ is not an initial sequent. [/guided] [/step] [step:Rule out every logical rule as the final inference] No logical rule of LK can have $\Rightarrow$ as its conclusion. Each logical left-introduction rule has a principal formula in the antecedent of its conclusion, and each logical right-introduction rule has a principal formula in the succedent of its conclusion. Hence the conclusion of any logical rule contains at least one formula. Since $\Rightarrow$ contains no formula, it cannot be the conclusion of a logical inference. [guided] Now suppose the last inference of $\mathcal{D}_0$ were a logical inference. Logical rules in LK introduce a principal formula in the conclusion. For example, a left-introduction rule concludes with a sequent whose left side contains the newly introduced formula, while a right-introduction rule concludes with a sequent whose right side contains the newly introduced formula. Thus the conclusion of any logical rule contains at least one formula: the principal formula introduced by that rule. But the empty sequent $\Rightarrow$ contains no formula on either side. Therefore the last inference of $\mathcal{D}_0$ cannot be a logical rule. [/guided] [/step] [step:Rule out every structural rule as the final inference] No structural rule of LK can have $\Rightarrow$ as its conclusion. Exchange only permutes formulas, so it cannot produce an empty conclusion unless its premise is already empty, and then the inference is vacuous and not an instance changing a sequent. Contraction replaces two occurrences of a formula by one occurrence, so its conclusion still contains that formula. Weakening adds a formula to the conclusion, so its conclusion contains the weakened formula. Therefore no structural rule has $\Rightarrow$ as its conclusion. [guided] It remains to check structural rules. Exchange merely changes the order of formulas in a sequent; for finite multisets this has no effect on the number of formula occurrences. Thus exchange cannot turn a nonempty sequent into the empty sequent. Contraction has the form of replacing two occurrences of a formula by one occurrence. Hence the conclusion of a contraction inference still contains that formula. Therefore contraction cannot conclude with $\Rightarrow$. Weakening adds a formula to one side of the sequent. Thus the conclusion of a weakening inference contains the added formula, either in the antecedent or in the succedent. Therefore weakening also cannot conclude with $\Rightarrow$. So none of the structural rules of LK can be the last inference of a cut-free derivation whose end sequent is empty. [/guided] [/step] [step:Conclude that no cut-free derivation of the empty sequent exists] The cut-free derivation $\mathcal{D}_0$ cannot end with an initial sequent, cannot end with a logical rule, and cannot end with a structural rule. Since $\mathcal{D}_0$ is cut-free, it also cannot end with the cut rule. These cases exhaust all possible last steps in an LK-derivation, contradicting the existence of $\mathcal{D}_0$. Hence no LK-derivation of $\Rightarrow$ exists. [/step]