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?