Results 1 to 10 of 10

Math Help - Proof Tree induction - proving conjunction

  1. #1
    Junior Member
    Joined
    Oct 2011
    Posts
    27

    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
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,561
    Thanks
    785

    Re: Proof Tree induction - proving conjunction

    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).

    Quote Originally Posted by ssharish View Post
    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)
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Junior Member
    Joined
    Oct 2011
    Posts
    27

    Re: Proof Tree induction - proving conjunction

    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
    Follow Math Help Forum on Facebook and Google+

  4. #4
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,561
    Thanks
    785

    Re: Proof Tree induction - proving conjunction

    Quote Originally Posted by ssharish View Post
    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.

    Quote Originally Posted by ssharish View Post
    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).

    Quote Originally Posted by ssharish View Post
    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).

    Quote Originally Posted by ssharish View Post
    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.
    Follow Math Help Forum on Facebook and Google+

  5. #5
    Junior Member
    Joined
    Oct 2011
    Posts
    27

    Re: Proof Tree induction - proving conjunction

    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
    Follow Math Help Forum on Facebook and Google+

  6. #6
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,561
    Thanks
    785

    Re: Proof Tree induction - proving conjunction

    You are welcome.

    Quote Originally Posted by ssharish View Post
    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.
    Follow Math Help Forum on Facebook and Google+

  7. #7
    Junior Member
    Joined
    Oct 2011
    Posts
    27

    Re: Proof Tree induction - proving conjunction

    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).
    Attached Thumbnails Attached Thumbnails Proof Tree induction - proving conjunction-tree.png  
    Follow Math Help Forum on Facebook and Google+

  8. #8
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,561
    Thanks
    785

    Re: Proof Tree induction - proving conjunction

    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,

    \frac{p\land (q\lor r)}{p}

    is an instance of conjunction elimination

    \frac{A\land B}{A}

    where A = p and B = q\lor r.

    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 p\land (q\lor r) that q\lor r holds. Case 1: q holds. Then from p\land (q\lor r) we get p and thus p\land q. Therefore, (p\land q)\lor (p\land r). Similarly for case 2, when r holds.

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

    Quote Originally Posted by emakarov View Post
    Are you proving q \/ r -> (p /\ q) \/ (p /\ r)?
    Of course it should be p /\ (q \/ r) -> (p /\ q) \/ (p /\ r).
    Follow Math Help Forum on Facebook and Google+

  9. #9
    Junior Member
    Joined
    Oct 2011
    Posts
    27

    Re: Proof Tree induction - proving conjunction

    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
    Follow Math Help Forum on Facebook and Google+

  10. #10
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,561
    Thanks
    785

    Re: Proof Tree induction - proving conjunction

    Quote Originally Posted by ssharish View Post
    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.

    Quote Originally Posted by ssharish View Post
    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.

    Quote Originally Posted by ssharish View Post
    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.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. binary tree math proof
    Posted in the Discrete Math Forum
    Replies: 0
    Last Post: January 14th 2012, 04:24 AM
  2. Tree Proof
    Posted in the Discrete Math Forum
    Replies: 1
    Last Post: September 22nd 2010, 08:36 PM
  3. Induction for binary tree.
    Posted in the Discrete Math Forum
    Replies: 3
    Last Post: March 30th 2010, 12:17 PM
  4. Tree with MOD proof
    Posted in the Discrete Math Forum
    Replies: 1
    Last Post: April 12th 2009, 01:50 PM
  5. Conjunction, Disjunction
    Posted in the Math Topics Forum
    Replies: 1
    Last Post: September 27th 2007, 10:18 AM

Search Tags


/mathhelpforum @mathhelpforum