Thread: Proof Tree induction - proving conjunction

Hi all,

I a bit confused how the following got derived? The following is snap shot taken from the lecture notes. But the while tree itself is pretty big. Didn't want to put them all here. But the following i'n not sure how the [V-elmi] would yield to (q v r) from (p ^ q) v (p v r).

(q v r) (p ^ q) v (p ^ q) (p ^ q) v (p ^ q)
------------------------------------------------------------------------- [v-elmi]
(p ^ q) v (p ^ q)

I still cant understand how the (q v r) got in there, in the place of p v q from looking into rule of or-elimination. And also how did the Q is in assumption. I know I’m missing something really fundamental.

Sorry about not using Tex tag. I couldn't figure out how to draw tree well aligned using LaTex.

Thanks

ssharish

Are you talking about natural deduction and specifically about the following rule (taken from the book "Proofs and Types," p. 72)?



Do I understand right that there are three formulas above the line: (q v r), and two (p ^ q) v (p ^ q)? Then you get it from the rule above by having A = q, B = r and C = (p ^ q) v (p ^ q).

Originally Posted by ssharish

But the following i'n not sure how the [V-elmi] would yield to (q v r) from (p ^ q) v (p v r).

I don't see p v r. Also, why do you say "yield to (q v r) from ..."? The formula q v r is above the line, so one uses it as an assumption to yield the conclusion below the line.

Hint: To write things that require alignment, you can use the [code]...[/code] tags, which don't turn a sequence of spaces into a single space. Write what you want in a text editor using a fixed-width font like Courier New or Consolas and then paste it into the browser's text edit box. For example, you can have

Code:

 (q v r)    (p ^ q) v (p ^ q)    (p ^ q) v (p ^ q)
--------------------------------------------------- [v-elmi]
                (p ^ q) v (p ^ q)

That’s right; thats the deduction i was talking about. Or-Elimination what i still don’t understand is the (q v r). If I understand you well, you can put in anything above the line to derive the conclusion? Is that right? and also how could (q v r) yield to (p ^ q) v (p ^ r)? In this case.

Given just to prove the theorem (p ^ q) v (p ^ r)? How could I conclude that I should be using or-elmi rather than or-intro rule and substitute a v b with the q and r respectively. For me q v r has come from nowherein my previous post. Please help me to understand.

Many thanks

ssharish

Originally Posted by ssharish

If I understand you well, you can put in anything above the line to derive the conclusion?

Nobody said you can put anything above the line. You can take the inference rule in the first formula in post #2 and replace A with an arbitrary formula, B with another formula and C with a third formula.

Originally Posted by ssharish

and also how could (q v r) yield to (p ^ q) v (p ^ r)?

Disjunction elimination is reasoning by cases. Suppose you know that A \/ B and you need to show C. There are two cases: either A, or B. If you can show that C holds both assuming A and assuming B, then C holds in every case.

Here A = q and B = r. Apparently, from the assumption q you can prove C = (p ^ q) v (p ^ q), and from the assumption r you can prove (p ^ q) v (p ^ q). These two subderivations are located above the second and third premise of the rule. So, you can conclude (p ^ q) v (p ^ q).

Originally Posted by ssharish

Given just to prove the theorem (p ^ q) v (p ^ r)?

I am not sure I understood the question. Are you proving q \/ r -> (p /\ q) \/ (p /\ r)? Then the conclusion of the \/-elimination is probably (p /\ q) \/ (p /\ r), not (p /\ q) \/ (p /\ q).

Originally Posted by ssharish

How could I conclude that I should be using or-elmi rather than or-intro rule and substitute a v b with the q and r respectively. For me q v r has come from nowherein my previous post.

You use whatever rules are suitable to derive the necessary theorem. If you are indeed proving q \/ r -> (p /\ q) \/ (p /\ r), then q \/ r did not come from nowhere; it's the premise of the implication.

Hey thanks Emakarov that’s really helps me to understand. One clarification
>Apparently, from the assumption q you can prove C = (p ^ q) v (p ^ q), and from the assumption r you can prove (p ^ r) v (p ^ r)
I quite understand that you can say this from your experience. But I would like to know how. What inference rule do you use to conclude they are true from the assumption Q & R.

thanks Emakarov

ssharish

You are welcome.

Originally Posted by ssharish

One clarification
>Apparently, from the assumption q you can prove C = (p ^ q) v (p ^ q), and from the assumption r you can prove (p ^ r) v (p ^ r)
I quite understand that you can say this from your experience. But I would like to know how. What inference rule do you use to conclude they are true from the assumption Q & R.

This depends on what you are proving. What is the final theorem? Also, please be careful with formulas: I used (p ^ q) v (p ^ q) two times in post #4, while you used (p ^ r) v (p ^ r) the second time.

This is the whole tree. As you see i'm trying to understand the at second brach or how they use (q v r) r r to conclude (p ^ q) v (p ^ r).

Well, a proof tree is pretty self-explanatory. The only thing to check is that every horizontal line corresponds to an instance of an actual inference rule. For example,



is an instance of conjunction elimination



where and .

The subderivation above the first vertical line uses the assumption q, which is closed when \/-elim is applied. In words, we know from the assumption that holds. Case 1: q holds. Then from we get p and thus . Therefore, . Similarly for case 2, when r holds.

If you have questions about any specific rule, feel free to ask.

Originally Posted by emakarov

Are you proving q \/ r -> (p /\ q) \/ (p /\ r)?

Of course it should be p /\ (q \/ r) -> (p /\ q) \/ (p /\ r).

Thanks again Emakarov, i know this is a very simple question, from your previous post I do see that you use from jargon which i rather need to understand. In the lecture the proof does use them a lot. Like when you say P hold. Does that mean the "when the term or expression P is true?"

And also when we assume something like in the above theorem we assumed Q and R. Does the assumption mean that they are always true? And also is there scope for the assumption in the proof tree? As in the above image in see that R was assumed in one branch but used to conclude in a different branch and the assumption can be used any number of times to derive the conclusion?

Thanks

ssharish

Originally Posted by ssharish

Thanks again Emakarov, i know this is a very simple question, from your previous post I do see that you use from jargon which i rather need to understand. In the lecture the proof does use them a lot. Like when you say P hold. Does that mean the "when the term or expression P is true?"

I used "q holds" in the informal sense, when I described the derivation with words. This is what one says when reasoning by cases. Formally, a derivation is nothing but a tree of instances of inference rules where variables A, B, C, etc. are replaced by concrete formulas.

Originally Posted by ssharish

And also when we assume something like in the above theorem we assumed Q and R. Does the assumption mean that they are always true?

Derivations are purely syntactic; one does not talk about what's true or false. That would be semantics. Assuming q and r just means that they can be used as if they were axioms in the two subderivations of \/-elim.

Originally Posted by ssharish

And also is there scope for the assumption in the proof tree? As in the above image in see that R was assumed in one branch but used to conclude in a different branch and the assumption can be used any number of times to derive the conclusion?

Good questions. Yes, assumptions always have scopes. In the rule



the assumption A can only be used in the first subderivation, which is above the first C, and B can be used only in the second subderivation, above the second C. The rule \/-elim closes both A and B in their respective subderivations and they are not available below it. So, in the derivation in post #7, r can only be used in the second, i.e., last, subderivation of \/-elim. An assumption can be used any number of times. The rules that close assumptions, like =>-elim and \/-elim, can close any number of the corresponding open assumptions, i.e., they don't have to close all of them, though this depends on the flavor of natural deduction. Usually you want to close all relevant assumptions because the goal is to prove some conclusion without hanging assumptions.