2
$\begingroup$

My question regards a proof search procedure, ADC, for a natural deduction in sequent style calculus:

According to

"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?

$\endgroup$
8
  • $\begingroup$ Basically, proof search in Sequent Calculus is bottom up; start from the goal and "unpack" it using rules. But in SC all rules are "introduction rules" (in the antecedent or in the consequent). $\endgroup$ Jun 15, 2017 at 15:56
  • $\begingroup$ Mints' proof system (see page 10) is the so-called "Natural Deduction in SC-style": the rules are expressed with sequents but there are intro- and elim-rules, all "acting" on the consequent. $\endgroup$ Jun 15, 2017 at 15:58
  • $\begingroup$ Thus, it seems that the procedure described by Mints is a proof search one "adapted" to the chosen style for the rules. $\endgroup$ Jun 15, 2017 at 15:59
  • $\begingroup$ I understand this proof system and have worked in it. I don't yet have a firm grip of ADC, partly because it is atrociously described by Mints (with misprints I believe). $\endgroup$
    – user65526
    Jun 15, 2017 at 16:00
  • $\begingroup$ It seems to me 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 (see page 397 of the paper). Thus, going bottom-up, we start from the goal and unpack it with elim rules: this may be the "analysis" part of the proof procedure. Why restricted only to $\to$-rules ? $\endgroup$ Jun 16, 2017 at 6:16

1 Answer 1

2
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ Thank you. :) I have again substantially revised and edited my question. I have added questions which relate to confusions on my part. $\endgroup$
    – user65526
    Jun 22, 2017 at 15:09

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .