# A method for proving sequents in natural deduction sequent style using solely elimination rules and structural rules

In a previous question, Proving a sequent in natural deduction sequent style with elimination rules only, $${p \hspace{0.1cm} \& \hspace{0.1cm} q, \hspace{0.2cm} p \hspace{0.01cm} \rightarrow \hspace{0.01cm} \neg \thinspace q \hspace{0.2cm} \vdash \hspace{0.2cm}\bot}$$

was shown using only elimination rules of a natural deduction sequent style calculus (the relevant elimination rules being in Proving a sequent in natural deduction sequent style with elimination rules only).

In

using $${p \hspace{0.1cm} \& \hspace{0.1cm} q, \hspace{0.2cm} p \hspace{0.01cm} \rightarrow \hspace{0.01cm} \neg \thinspace q \hspace{0.2cm} \vdash \hspace{0.2cm}\bot}$$ as an example (and defining $\neg p$ as $p \rightarrow \bot$), they propose a method for obtaining sequents derivable by direct chaining (that is derivable by elimination rules, cut and structural rules only):

"To see whether this sequent is derivable by direct chaining, we $\textit{saturate}$ $\Gamma=\{\hspace{0.09cm} p \hspace{0.2cm} \& \hspace{0.2cm} q, \hspace{0.2cm} p \rightarrow \neg q \hspace{0.09cm} \}$ with the conclusions of all applicable elimination rules (i.e. elimination rules where the consequents of the premises are in $\Gamma$ ). This saturation procedure generates, in order, the following sets:

$\Gamma_1 =\{\hspace{0.09cm} p \hspace{0.2cm} \& \hspace{0.2cm} q, \hspace{0.2cm} p \rightarrow \neg q,\hspace{0.2cm} p,\hspace{0.2cm} q \hspace{0.09cm} \}$

$\Gamma_2=\{\hspace{0.09cm} p \hspace{0.2cm} \& \hspace{0.2cm} q, \hspace{0.2cm} p \rightarrow \neg q, \hspace{0.2cm} p, \hspace{0.2cm}q, \hspace{0.2cm} q \rightarrow \bot \hspace{0.09cm} \}$

$\Gamma_3=\{\hspace{0.09cm} p \hspace{0.2cm} \& \hspace{0.2cm} q, \hspace{0.2cm} p \rightarrow \neg q ,\hspace{0.2cm}p, \hspace{0.2cm}q,\hspace{0.2cm} q \rightarrow \bot, \hspace{0.2cm} \bot \hspace{0.09cm} \}$

They claim that, because $\bot∈\Gamma_3$, we can derive $${p \hspace{0.1cm} \& \hspace{0.1cm} q, \hspace{0.2cm} p \hspace{0.01cm} \rightarrow \hspace{0.01cm} \neg \thinspace q \hspace{0.2cm} \vdash \hspace{0.2cm}\bot}$$

by elimination rules only.

• Why does it follow from the fact that because $\bot∈\Gamma_3$ that we can derive the sequent by elimination rules only? Could you give another example of this method of proving sequents via elimination rules only?
• They speak of 'the conclusions of all applicable elimination rules (i.e. elimination rules where the consequents of the premises are in $\Gamma$)'. But what is the reason for excluding repetitions in this method, and thereby generating?

$\Gamma_{1A}=\{\hspace{0.09cm} p \hspace{0.2cm} \& \hspace{0.2cm} q, \hspace{0.2cm} p \rightarrow \neg q ,\hspace{0.2cm} p, \hspace{0.2cm}q \hspace{0.2cm},\hspace{0.2cm} \textbf{p} \hspace{0.2cm} \textbf{&} \hspace{0.2cm} \textbf{q},\hspace{0.2cm}\textbf{p} \rightarrow \textbf{$\neg$q} \}$

$\Gamma_{2A}=\{\hspace{0.09cm} p \hspace{0.2cm} \& \hspace{0.2cm} q, \hspace{0.2cm} p \rightarrow \neg q ,\hspace{0.2cm} p \hspace{0.2cm},q \hspace{0.2cm}, q \rightarrow \bot, \hspace{0.2cm} \textbf{p} \hspace{0.2cm} \textbf{&} \hspace{0.2cm} \textbf{q},\hspace{0.2cm}\textbf{p} \rightarrow \textbf{$\neg$q} \}$

$\Gamma_{3A}=\{\hspace{0.09cm} p \hspace{0.2cm} \& \hspace{0.2cm} q, \hspace{0.2cm} p \rightarrow \neg q ,\hspace{0.2cm} p \hspace{0.2cm},q \hspace{0.2cm}, q \rightarrow \bot, \hspace{0.2cm} \bot, \hspace{0.2cm} \textbf{p} \hspace{0.2cm} \textbf{&} \hspace{0.2cm} \textbf{q},\hspace{0.2cm}\textbf{p} \rightarrow \textbf{$\neg$q} \}$

Is it just the fact that we are using sets $\Gamma_1,...$? But then why not use multisets, in which case repetition would be important? What forces the appeal to sets in the procedure?

• If you read the answer to your previous post you can easily check that the six formulas in $\Gamma_3$ are exactly the conclusion of the seven step in my proof ("modulo" the rewriting of $\lnot q$ as $q \to \bot$). – Mauro ALLEGRANZA Jun 16 '17 at 16:23