Does disjunction elim require subproofs or can it use implications?

Question

I've seen two different versions of disjunction elimination:

$\{A \lor B, A \vdash C, B \vdash C\} \vdash C$

and

$\{A \lor B, A \to C, B \to C\} \vdash C$

Is there any reason to go with one versus the other?

Answer 1

$A\vdash C$ is not a formula so (at least for most proof systems), it doesn't make sense to have something like $(A\vdash C)\vdash C$. You could mean something like: $$\dfrac{\Gamma\vdash A\lor B\qquad\Gamma,A\vdash C\qquad \Gamma,B\vdash C}{\Gamma\vdash C}$$ The other rule could then be either: $$\dfrac{\Gamma\vdash A\lor B\qquad\Gamma\vdash A\to C\qquad \Gamma\vdash B\to C}{\Gamma\vdash C}$$ or something like: $$\dfrac{\Gamma\vdash A\lor B}{\Gamma, A\to C,B\to C\vdash C}$$

The last is a bit weird, but in the context of the usual rules for constructive (or classical) logic, these are all interderivable. In that sense, it doesn't matter which you choose.

That said, the first is the usual choice as it has some nice meta-theoretic properties. For example, it only involves $\lor$, so we don't need our logic to include $\to$ to have $\lor$ if we use this rule. That is, the rules are more modular this way, and this allows us to add and remove connectives a la carte. Properties like local soundness and completeness are also likely easiest with the first definition.

That said, as you are most likely working in a classical logic, a multi-succedent form of entailment fits more naturally. This leads to a rule like: $$\dfrac{\Gamma\vdash A\lor B,\Delta}{\Gamma\vdash A,B,\Delta}$$ This avoids having to introduce the motive ($C$) which otherwise comes out of nowhere. The real benefit is that there's no structurally clean way to incorporate the rules that give classical logic in single-succedent natural deduction. You can certainly add a rule like $\dfrac{}{\Gamma\vdash A\lor\neg A}$ but this has meta-theoretic issues which make it less than desirable, e.g. using both $\lor$ and $\neg$ together.

Answer 2

In addition to Derek Elkin's reasons, here's 2 more important reasons to use $$\dfrac{A \vdash X,~~ B \vdash X,~~ \vdash A \lor B}{\vdash X} \tag{OE1}$$ instead of $$\dfrac{A \to X, B \to X, A \lor B}{X} \tag{OE2}$$

Consider proving the following basic tautology in natural deduction:

$$(A \land B) \lor (C \land D) \vdash (A \lor C) \land (B \lor D) \tag{T}$$

with the following Fitch style normal proof:

$$\begin{array} {r|l} & A \land B \\ & \quad A \\ & \quad A \lor C \\ & \quad B \\ & \quad B \lor D \\ & \quad (A \lor C) \land (B \lor D) \\ \\ & C \land D \\ & \quad C \\ & \quad A \lor C \\ & \quad D \\ & \quad B \lor D \\ & \quad (A \lor C) \land (B \lor D) \\ \\ \text{By Assumption:} & (A \land B) \lor (C \land D) \\ \text{By Or Elim:} & (A \lor C) \land (B \lor D) \\ \end{array}$$

That proof has a very important property that every expression in it is a subexpression of (T). That was one of Gentzen's design principle of N.D.; he was using it to prove things about consistency. If the proof had used (OE2) then it would have $(A \land B) \to ((A \lor C) \land (B \lor D))$ as an expression, which is not a subexpression of (T). That would violate the principle for N.D. (besides also looking bad).

Further, since type theory, proofs for natural deduction aren't formally recorded using Fitch style, but rather as a single Lambda Calculus expression, along with types for variables. Since the proof for an expression like $M \vdash N$ is a lambda calculus expression of the form $\lambda x^M.E^N$ for some lambda expression $E$ (with type $N$), the proof of (T) is something like

$$\lambda x^{(A \land B) \lor (C \land D)}.E^{(A \lor C) \land (B \lor D)}$$

for some expression $E$. The type of $x$ is a union of either a pair with type A first and type B second, or of a pair with type C first and type D second. Overall the expression has to convert a union of pairs (x) into a pair of unions (E), which would be naturally done like:

$$\begin{array} {l} \lambda x.\text{match }(x) ~\{ \\ \quad \lambda z_1{}^{(A, B)}.\text{pair}(\text{union}(\text{first}(z_1)),~ \text{union}(\text{second}(z_1))) \\ \quad \lambda z_2{}^{(C, D)}.\text{pair}(\text{union}(\text{first}(z_2)),~ \text{union}(\text{second}(z_2))) \\ \} \end{array}$$

And there you can see each option of the match corresponding to each $\vdash$ in (OE1). If you tried to force it to use (OE2) you'd have to use functional application (applying an argument to a lambda expression) which is the correlating proof structure for $\to$ expressions, lambda calculus would have to be modified to look something like:

$$\begin{array} {l} \lambda x.\text{match }(x) ~\{ \\ \quad (\lambda z_1{}^{(A, B)}.\text{pair}(\text{union}(\text{first}(z_1)),~ \text{union}(\text{second}(z_1))) ~) x\\ \quad (\lambda z_2{}^{(C, D)}.\text{pair}(\text{union}(\text{first}(z_2)),~ \text{union}(\text{second}(z_2))) ~) x \\ \} \end{array}$$

which is just a bunch of extra ugly unnecessary junk. So that is why you should use (OE1).