Grigori Mints' ADC method of proof search for a natural deduction in "sequent-style" calculus

Question

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?

Answer 1

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.