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
- Grigori Mints and Shane Steinert-Threlkeld ADC method of proof search for intuitionistic propositional natural deduction (2016): page 396.
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?
