1
$\begingroup$

There are several (equivalent) ways to formulate the eliminating rule of $\vee$ ("or")

Here are two of them:

  1. $\begin{array}{c} A\vee B \quad A\vdash C \quad B\vdash C\\ \hline C \end{array}$

  2. $\begin{array}{c} A\vee B \quad A\rightarrow C \quad B\rightarrow C\\ \hline C \end{array}$

My question is: Which variant is the most natural one (in your opinion)?

A disadvantage/detour of the 1. formulation is noticeable when proving the implications by contraposition.

$\endgroup$
1
  • 2
    $\begingroup$ The second one is kinda awkward, because it involves another conective. For instance, you won't be able to study disjunction in isolation from implication $\endgroup$ – Pedro Sánchez Terraf Jul 4 '15 at 15:09
3
$\begingroup$

Answer: neither of those is happy.

In a natural deduction framework -- and talk of introduction and elimination rules has its natural(!) home here -- the canonical formulation of $\lor$-elimination looks like this:

$${}\quad \quad \quad [A] \quad \quad \quad [B]\\ \quad \quad \quad \vdots \quad \quad \quad \;\;\vdots\\ (A \lor B)\quad \quad \quad C \quad \quad \quad \;\;C\quad\quad\quad\\ -------------\quad\quad\quad\\ C\quad\quad$$

That is to say, given $(A \lor B)$ and a subproof from the temporary assumption $A$ to $C$ and a subproof from the temporary assumption $B$ to $C$, we can discharge the two temporary assumptions (marking the discharge by square brackets) and infer $C$.

Your first formulation is unhappy as it seems aiming to be part of a sequent calculus formulation, but all the expressions in a sequent calculus argument have to be sequents, involving $\vdash$ (or whatever your sequent-constructor is). If on the other hand you intend $\vdash$ to be the usual metalinguistic expression for syntactic entailment, then what you have above the line is an unhappy mix of object and metalanguage statements.

Your second formulation is unhappy as we ideally want introduction and elimination for a connective not to involve other connectives (you might not have a conditional primitively available in the language, and if you have introduced $A \to B$ as short for $\neg A \lor B$, you are in trouble!).

$\endgroup$
4
  • $\begingroup$ $[A] \dots C$ is exactly the same I meant with $A\vdash C$. Assume, you have already proven that $A\vee B$ and $\neg C \rightarrow \neg A$ and $\neg C \rightarrow \neg B$. How would you prove that $C$ holds with your $\vee$-elimination rule? $\endgroup$ – asdfusername Jul 4 '15 at 15:24
  • $\begingroup$ (1) Then you misused the standard notation $A \vdash C$. (2) There is obviously a subproof from $A$ and the additional assumption $\neg C \to \neg A$ to $C$, and similarly a subproof from $B$ and the additional assumption $\neg C \to \neg B$ to $C$. $\endgroup$ – Peter Smith Jul 4 '15 at 15:29
  • $\begingroup$ (1) I just used the notation that is also used in the wikipedia article de.wikipedia.org/wiki/Systeme_nat%C3%BCrlichen_Schlie%C3%9Fens (2) Are you sure that this wouldn't be a bit artificial? For me, it appears to be a detour. $\endgroup$ – asdfusername Jul 4 '15 at 15:41
  • $\begingroup$ (2) Yes, it is very natural. $\endgroup$ – asdfusername Jul 4 '15 at 18:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.