Results 1 to 6 of 6

Math Help - natural deduction

  1. #1
    Newbie
    Joined
    Oct 2009
    Posts
    15

    natural deduction

    Hey,

    I am having trouble proving...

     \sigma \rightarrow Y \vdash (\phi \lor \sigma ) \to (\phi \lor Y)

    I know that the beginning hypotheses are  \sigma \rightarrow Y and  (\phi \lor \sigma ), but I am not sure how to break down the "or" statement.

    Thanks!
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,513
    Thanks
    769
    You need the disjunction elimination rule (reasoning by cases). You have the assumption \phi\lor\sigma. If \phi is true, then \phi\lor Y is. If \sigma is true, then, using MP, again \phi\lor Y is true. In both cases the needed conclusion is true.
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Newbie
    Joined
    Oct 2009
    Posts
    15
    I understand that I need to use disjunctive elimination, but I need to solve using natural deduction. Don't I need to break down the first "or" statement? If so, how do I do that only using the hypotheses I have?
    Follow Math Help Forum on Facebook and Google+

  4. #4
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,513
    Thanks
    769
    Disjunction elimination is one of the inference rules of Natural Deduction. See lecture notes by Frank Pfenning (CMU), p. 8 and the famous book "Proofs and Types" by Girard, Lafont and Taylor, ch. 10, p. 72; these are available online. For an authoritative reference concerning the set of rules see the monograph by H. Schwichtenberg and A. Troelstra, "Basic Proof Theory".
    Follow Math Help Forum on Facebook and Google+

  5. #5
    Newbie
    Joined
    Oct 2009
    Posts
    15
    thank you so much for your help! do you know of any more good resources that explain  \forall and \exists introduction and elimination for natural deduction? All of the books and web sources I have looked at are difficult for me to understand. I don't know when I can introduce or eliminate those symbols because I don't understand the restrictions on free variables or the substitutions needed.
    Follow Math Help Forum on Facebook and Google+

  6. #6
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,513
    Thanks
    769
    I don't know what concrete source to recommend. Natural deduction is a very standard topic that is described in multiple textbooks. The original (and readable) book about ND is by the guy who popularized it: "Natural Deduction. A Proof-Theoretic Study" by Dag Prawitz (actually, this was his PhD dissertation). The book by Girard, Lafont & Taylor is highly praised but is written for smart readers. Frank Pfenning has taught many deep courses on constructive mathematics (which usually starts with ND), and he has good lecture notes.

    I would choose some source by a solid practicing mathematical logician, such as
    Frank Pfenning. I personally don't like texts by philosophers, and I don't like texts that start proof theory using either Hilbert-style axiomatic system or in general anything other than ND or Sequent Calculus.

    The brief idea concerning variables is to distinguish whether you are proving something or using an assumption, and between "for all" and "exists". To prove "for all", you fix some fresh x; you don't have control in choosing it. Similarly, when you use an existential fact, you say, "let's call the object that exists x". Again, there is no control over choosing it.

    On the other hand, when you need to prove existence, any existing object works: you can choose 0, 5, or anything that makes the statement true. Similarly, if you have a universal assumption that starts with "for all x", you can take its special case for any x you like.

    I could also add that natural deduction is close to such topics as lambda-calculus, type theory and constructive mathematics (though these are usually not considered elementary topics). Studying them, you can also understand natural deduction better.

    After re-reading this, I think these recommendations are too comprehensive, but feel free to ask concrete questions here.

    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. natural deduction
    Posted in the Discrete Math Forum
    Replies: 3
    Last Post: December 12th 2011, 08:31 AM
  2. Abstract reasoning/natural deduction with Fitch
    Posted in the Discrete Math Forum
    Replies: 10
    Last Post: October 19th 2011, 12:37 PM
  3. Natural Deduction
    Posted in the Discrete Math Forum
    Replies: 9
    Last Post: June 9th 2011, 03:15 AM
  4. Could use some help with a Natural Deduction proof
    Posted in the Discrete Math Forum
    Replies: 2
    Last Post: May 4th 2010, 05:58 AM
  5. Help with Logic (Natural Deduction)
    Posted in the Discrete Math Forum
    Replies: 7
    Last Post: January 12th 2010, 02:07 PM

Search Tags


/mathhelpforum @mathhelpforum