How to prove $D \in S^* \implies S \vdash^r D $

Question

Let S be a set of disjuncts. D is a disjunct. I want to prove

$D \in S^* \implies S \vdash^r D$

Where $ S\vdash^r D$ means there's a sequence of disjuncts where every member is either a member of S, or it's a resolvent of two previous members of the sequence and D is the last disjunct in the sequence. $$ S_0 \equiv S \\ S_{n+1} \equiv Sn\cup\{D|D=R_L(D_1, D_2), D_1, D_2 \in S_n, L-literal\} \\ S^*= \bigcup\limits_{n=0}^{\infty} S_{n} $$

My try is with induction to prove that

$\forall n \ ( D \in S_n \implies S \vdash^r D)$

• $n=0, D \in S_0 = S$
• Let for some n the statement is true, i.e. if $ D' \in S_n$, then $S \vdash^r D'$.
• Lets consider $D' \in S_{n+1}$
  1. case I - $D' \in S_n$, and from the inductive hypothesis: $S \vdash^r D'$
  2. case II - D' is resolvent of $D_1, D_2, D=R_L(D_1, D_2), D1,D2 \in S_n\\$

And here I'm having hard time proving the second case for the disjunct D'. How can I prove that the statement is true for that case too?

Thanks in advance!

Answer 1

You should first make clear exactly what claim you are trying to prove using induction. I assume you are trying to prove the claim that:

$\forall n \ ( D \in S_n \implies S \vdash^r D)$

Also: your definition of $S \vdash^r D$ makes no reference to $D$. I assume you need to add that $D$ is the last entry of the sequence.

Base: $n=0$

Take any $D \in S_0$. Since $S_0=S$, that means $D \in S$. Hence the sequence of disjuncts consisting of just $D$ is such that every member of the sequence is a member of $S$, and the last entry is $D$, hence $S \vdash^r D$

OK, for the step you're doing the two cases, so that's good. And for case 2:

If $D = R_L(D_1,D_2)$ where $L$ is the literal that $D_1$ and $D_2$ get resolved on, and $D_1 \in S_n$ and $D_2 \in S_n$, then do the following:

Since $D_1 \in S_n$ and $D_2 \in S_n$, we know by the inductive hypothesis that there is some sequence of disjuncts

$$S_{D_1} = D_{1,1}, D_{1,2}, ..., D_{1,m_1}(=D_1)$$

of disjuncts where every entry $D_{1,k}$ of the sequence is a member of $S$ or is the result of resolving two earlier disjuncts $D_{1,i}$ and $D_{1,j}$ (so $i<k$ and $j<k$) in the sequence, and that there is also some sequence of disjuncts

$$S_{D_2} = D_{2,1}, D_{2,2}, ..., D_{2,m_2}(=D_2)$$

of disjuncts where every entry of the sequence is a member of $S$ or is the result of resolving two earlier disjuncts in the sequence.

So then simply append these two sequences , and add $D$ to the end of that. So the resulting sequence $S_D$ looks like:

$$S_D = D_{1,1}, D_{1,2}, ..., D_{1,m_1}=D_1, D_{2,1}, D_{2,2}, ..., D_{2,m_2}=D_2, D$$

And now you see that every entry in this sequence is either a member of $S$, or is the result of resolving two earlier disjuncts in the sequence. Hence, $S \vdash^r D$

In other words: you can see the sequences as derivations (or proofs), and you can combine two derivations simply by putting all lines in the derivations after each other.