Grigori Mints' ADC method of proof search for a natural deduction in "sequent-style" calculus My question regards a proof search procedure, ADC, for a natural deduction in sequent style calculus:


*

*See Grigori Mints, A short introduction to Intuitionistic logic (2000): 2.6. Direct Chaining and Analysis into Subgoals, page 15-16.


According to 


*

*Grigori Mints and Shane Steinert-Threlkeld ADC method of proof search for
intuitionistic propositional natural deduction (2016). 


"the method proceeds first by $Analysing$ the sequent into sub-goals by applying all possible introduction rules, and then by checking whether each of these sub-goals can be established using only elimination rules ($Direct \hspace{0.1cm} Chaining$)."
The relevant elimination rules are
:
$$\frac{\Gamma \Rightarrow A \rightarrow B \qquad \Delta \Rightarrow A}{\Gamma, \Delta \Rightarrow B}\hspace{0.1cm} \rightarrow E \hspace{0.1cm}$$ 
$$\frac{\Gamma \Rightarrow A \land B}{\Gamma \Rightarrow A}\hspace{0.1cm}  \& E \hspace{0.1cm}$$ 
$$\frac{\Gamma \Rightarrow A \land B}{\Gamma \Rightarrow B}\hspace{0.1cm}  \& E \hspace{0.1cm}$$  

DEFINITION 2.2: $\textit{A deduction using only rules mentioned in} \hspace{0.1cm} \textbf{LEMMA 2.4.}, \textit{cut
and structural rules is called} \hspace{0.2cm} \text{direct chaining}.$
Note: A good heuristic for deducing $\Gamma \Rightarrow \alpha$ by direct chaining is to take $\Gamma$
  as the initial set of data and saturate it by adding conclusions of all the
  rules [$\textit{Mints means all elimination rules}$] except $\lor \Rightarrow$,
  $$\frac{\alpha, \Gamma \Rightarrow \phi\qquad \beta, \Gamma \Rightarrow \phi}{\alpha \lor \beta, \hspace{0.2cm} \Gamma \Rightarrow \phi}\hspace{0.5cm} \lor \Rightarrow \hspace{0.1cm}$$ 
  mentioned in $\textbf{LEMMA 2.4.}(see \hspace{0.1cm} below)$ plus cut (Example 2.5.), restricting
  applications of $\bot_i$ 
  $$\frac{\Gamma \Rightarrow \bot}{\Gamma \Rightarrow A}\hspace{0.5cm}  \bot_i \hspace{0.1cm}$$ 
  to subformulas of $\Gamma, \alpha$ producing say $\Gamma_1 \equiv \Gamma^+$. Stop if $\alpha$ is
  obtained, otherwise apply $\lor \Rightarrow$ bottom-up for each formula $\alpha \lor \beta \in \Gamma$, that is,
  form $(\hspace{0.03cm} \alpha, \Gamma_1 \hspace{0.03cm})^+$ and $(\hspace{0.03cm} \beta, \Gamma_1 \hspace{0.03cm})^+$ Now add all formulas $\gamma \in (\hspace{0.03cm} \alpha, \Gamma_1 \hspace{0.03cm})^+ \cup(\hspace{0.03cm} \beta, \Gamma_1 \hspace{0.03cm})^+$  to $\Gamma_1$
  forming $\Gamma_2$. Iterate the process till it stops.
LEMMA 2.4: $ \text{(bottom of p.16)}\hspace{0.7cm} \textit{The following rules are derivable in Njp}$: $\rightarrow E, \hspace{0.1cm} \& E, \hspace{0.1cm} \neg E,\hspace{0.1cm} \bot_i, \hspace{0.1cm} \lor \Rightarrow \thinspace\text{(see above for most of these)}$
  $$\frac{\Gamma \Rightarrow \alpha \longleftrightarrow \beta}{\alpha \lor \beta, \hspace{0.2cm} \Gamma \Rightarrow \alpha \longrightarrow \beta}\hspace{0.5cm} \longleftrightarrow E \hspace{0.1cm}$$ 
  $$\frac{\Gamma \Rightarrow \alpha \longleftrightarrow \beta}{\alpha \lor \beta, \hspace{0.2cm} \Gamma \Rightarrow \beta \longrightarrow \alpha}\hspace{0.5cm} \longleftrightarrow E \hspace{0.1cm}$$
  $$\frac{\Gamma \Rightarrow \neg \alpha\qquad \Delta \Rightarrow \alpha}{[\Gamma, \Delta] \hspace{0.2cm} \Rightarrow \beta}\hspace{0.5cm} \neg E \hspace{0.1cm}$$ 

ADC method of establishing deducibility:  $\text{(top of p.16)}\hspace{0.7cm}$
  One of the most straightforward methods of establishing deducibility of a
  sequent $\Gamma \Rightarrow \alpha$ consists in its analysis into subgoals $\Gamma_1 \Rightarrow \alpha_1, ..., \Gamma_n \Rightarrow \alpha_n$ using
  $\textbf{LEMMA 2.6.}$ ($\textbf{LEMMA 2.6.}$ is the deduction theorem: $\Gamma, \alpha \Rightarrow \beta$ iff $\Gamma \Rightarrow \alpha \rightarrow \beta$), and establishing each subgoal by direct chaining. We say that a
  sequent $\Delta \Rightarrow \alpha \lor \beta$ is established when one of $\hspace{0.2cm}\Delta \Rightarrow \alpha, \thinspace \Delta \Rightarrow \beta \hspace{0.2cm}$ is established.
  The combination of Analysis and Direct Chaining described above will be called
  ADC-$\textit{method}$ or simply ADC.


-Mints and Steinert-Threlkeld furthermore claim ADC is 

"incomplete. For example, the sequent
  p∨q⇒q∨p
  obviously cannot be derived so that ∨+ is the last rule in the derivation"
  $$\frac{\Gamma \Rightarrow A}{\Gamma \Rightarrow A \lor B}\hspace{0.1cm}  \lor + \hspace{0.1cm}$$
  $$\frac{\Gamma \Rightarrow B}{\Gamma \Rightarrow A \lor B}\hspace{0.1cm}  \lor + \hspace{0.1cm}$$ 



*

*Question 1: Could anyone give a simple example illustrating the ADC proof procedure? In particular I do not understand the procedure described in the sentence starting "Stop if $\alpha$ is obtained", and the two sentences following it.

*Question 2: Clearly, p∨q⇒q∨p cannot be derived so that ∨+ is the last rule in the derivation. However, if we introduce the axiom p∨q⇒q∨p, then vacuously we have applied all introduction rules and elimination rules, and so, why shouldn't this qualify as a derivation by ADC? In any case, instances of axioms are obviously not excluded from proofs by ADC.

*Question 3: How can we determine, in general, which sorts of sequents are capable of a proof by ADC, and which are not? Could you give another example (or examples), $\textit{other than the examples they give}$ of a sequent which is not derivable via ADC? It would be useful to have at my fingertips some guidance as to when a proof via ADC is worth pursuing or not!

*Question 4: in an comment below it is pointed out that "the proof procedure is related to the well-know Prawitz's result about normalization: every deduction tree in ND can be written as a part with only elim rules followed by a part with only intro rules". What exactly is the relationship between ADC and normalisation. Do they differ in any significant way?
 A: Consider Example 2.7, page 12. We want to prove:

$\Rightarrow (p \to r) \to [(q \to r) \to ((p \lor q) \to r)]$.

The first step in showing derivability is to apply Lemma 2.6 "bottom-up" to analyze the goal.
Applying it three times, we get:

$p \to r, q \to r, p \lor q \Rightarrow r$.

Now we need $\lor \Rightarrow$ to generate the two paths:

$p \to r, q \to r, p \Rightarrow r \ \ $ and $ \ \ p \to r, q \to r, q \Rightarrow r$.

It is enough to prove one of the paths; consider the first one (the second is the same) and apply "Direct Chaining".
In order to show the derivability of $p \to r, q \to r, p \Rightarrow r$ we have to apply the elimination rules to the premises (the "saturation" step).
It is enough to consider a single application of $\to$-E:
$$\frac{p \to r \Rightarrow p \to r \qquad p \Rightarrow p}{p \to r, p \Rightarrow r}$$
followed by weakening to conclude the search procedure.

Now we can re-build the "normal" derivation (first all elimination rules, followed by introduction rules only):
1) $\dfrac{p \to r \Rightarrow p \to r \qquad p \Rightarrow p}{p \to r, p \Rightarrow r}$ --- $\to$E
2) $\dfrac{p \to r, p \Rightarrow r}{p \to r, q \to r, p \Rightarrow r}$ --- weakening
3) $\dfrac{q \to r \Rightarrow q \to r \qquad q \Rightarrow q}{q \to r, q \Rightarrow r}$ --- $\to$E
4) $\dfrac{q \to r, q \Rightarrow r}{p \to r, q \to r, q \Rightarrow r}$ --- weakening
5) $\dfrac{p \to r, q \to r, p \Rightarrow r \qquad p \to r, q \to r, q \Rightarrow r}{p \to r, q \to r, p \lor q \Rightarrow r}$ --- from 2) and 4) by $\lor \Rightarrow$
6) $\dfrac{p \to r, q \to r, p \lor q \Rightarrow r}{p \to r, q \to r \Rightarrow (p \lor q) \to r}$ --- $\to$I
7) $\dfrac{p \to r, q \to r \Rightarrow (p \lor q) \to r}{p \to r \Rightarrow (q \to r) \to ((p \lor q) \to r)}$ --- $\to$I

8) $\dfrac{p \to r \Rightarrow (q \to r) \to ((p \lor q) \to r)}{ \Rightarrow (p \to r) \to [(q \to r) \to ((p \lor q) \to r)]}$ --- $\to$I.

