Results 1 to 11 of 11

Math Help - Natural Deduction: Predicate Logic. Need help!

  1. #1
    Newbie
    Joined
    Aug 2012
    From
    United Kingdom
    Posts
    6

    Natural Deduction: Predicate Logic. Need help!

    I have a question about Natural Deduction for Predicate Logic.

    |-- Ǝx. ~P(x) ---> ~∀x. P(x) [ ~ = not ]

    How about do you solve this, as I'm really getting a headache in figuring it out. The reason is that it contains no premises and just the conclusion, but my lecturer said it is solvable.

    Does Ƚ can be assumed as ~∀x. P(x) (from ȽE)?
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,528
    Thanks
    773

    Re: Natural Deduction: Predicate Logic. Need help!

    Quote Originally Posted by nash160 View Post
    |-- Ǝx. ~P(x) ---> ~∀x. P(x)
    Do you mean "(Ǝx. ~P(x)) ---> ~∀x. P(x)" or "Ǝx. (~P(x) ---> ~∀x. P(x))"? I personally like the convention where the scope of ∀ is as small as possible, so that "Ǝx ~P(x) ---> ~∀x P(x)" means "(Ǝx ~P(x)) ---> ~∀x P(x)," but when a quantifier is followed by a dot, then its scope extends as far as possible, so that "Ǝx. ~P(x) ---> ~∀x. P(x)" means "Ǝx (~P(x) ---> ~∀x P(x))."

    Assuming you need (Ǝx ~P(x)) ---> ~∀x P(x), an informal proof is as follows. Assume Ǝx ~P(x) and break into into some x and a proof of ~P(x) using existential elimination. To prove ~∀x P(x), assume ∀x P(x). Instantiate it with x to get P(x). It gives a contradiction with ~P(x). Closing the assumption ∀x P(x), we get ~∀x P(x).

    Do you need a Fitch-style or tree-like derivation?

    Quote Originally Posted by nash160 View Post
    Does Ƚ can be assumed as ~∀x. P(x) (from ȽE)?
    What do you mean by Ƚ and ȽE?
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Newbie
    Joined
    Aug 2012
    From
    United Kingdom
    Posts
    6

    Post Re: Natural Deduction: Predicate Logic. Need help!

    I meant it as " (Ǝx ~P(x)) ---> ~∀x P(x) ".

    Does a tree-like derivation look something like,

    Solve,

    Code:
    ∀x.P(x), ∀x.Q(x) |-  ∀x.(P(x) ^ Q(x))
    Code:
    | ∀x P(x)                1.
    | ∀x Q(x)                  2.
    |--------
    |     | [c]                3.
    |     |----
    |     | P(c)              4. ∀E: 1
    |     | Q(c)                5.  ∀E:2
    |     | P(c) ^ Q(c)        6. ^I: 4,5
    |  ∀x(P(x) ^ Q(x))        7. ∀I: 3-6

    By "Ƚ", I meant one of the negation rule "ȽE" where "Ƚ" can be used for assumption.
    Last edited by nash160; August 16th 2012 at 08:17 AM.
    Follow Math Help Forum on Facebook and Google+

  4. #4
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,528
    Thanks
    773

    Re: Natural Deduction: Predicate Logic. Need help!

    Quote Originally Posted by nash160 View Post
    Does a tree-like derivation look something like,

    ∀x.P(x), ∀x.Q(x) |- ∀x.(P(x) ^ Q(x))

    | ∀x P(x) 1.
    | ∀x Q(x) 2.
    |--------
    | | [c] 3.
    | |----
    | | P(c) 4. ∀E: 1
    | | Q(c) 5. ∀E:2
    | | P(c) ^ Q(c) 6. ^I: 4,5
    | ∀x(P(x) ^ Q(x)) 7. ∀I: 3-6
    This is a Fitch-style derivation. Tree-like derivations look like the one in this post.

    Quote Originally Posted by nash160 View Post
    By "Ƚ", I meant one of the negation rule "ȽE" where "Ƚ" can be used for assumption.
    I am still not sure what the crossed L has to do with natural deduction rules. To prove ~∀x. P(x), indeed, you assume ∀x. P(x) and arrive at contradiction. This is probably called negation introduction rule.
    Follow Math Help Forum on Facebook and Google+

  5. #5
    Newbie
    Joined
    Aug 2012
    From
    United Kingdom
    Posts
    6

    Re: Natural Deduction: Predicate Logic. Need help!

    I just used that symbol because I can't find the symbol that fits it. Sorry for the confusion. The symbol I was looking for is an upside down T That's what I meant.
    Follow Math Help Forum on Facebook and Google+

  6. #6
    MHF Contributor

    Joined
    Aug 2006
    Posts
    18,616
    Thanks
    1578
    Awards
    1

    Re: Natural Deduction: Predicate Logic. Need help!

    Quote Originally Posted by nash160 View Post
    I just used that symbol because I can't find the symbol that fits it. Sorry for the confusion. The symbol I was looking for is an upside down T That's what I meant.
    [tex] \bot [/tex] gives  \bot .
    Follow Math Help Forum on Facebook and Google+

  7. #7
    Newbie
    Joined
    Aug 2012
    From
    United Kingdom
    Posts
    6

    Re: Natural Deduction: Predicate Logic. Need help!

    Quote Originally Posted by Plato View Post
    [tex] \bot [/tex] gives  \bot .
    Thanks, will keep that in mind!
    Follow Math Help Forum on Facebook and Google+

  8. #8
    Newbie
    Joined
    Aug 2012
    From
    United Kingdom
    Posts
    6

    Re: Natural Deduction: Predicate Logic. Need help!

    This was how I solved it, and I'm not sure if it's correct...

    Code:
    1.   | 
    2.   |--------
    3.   |     | Ǝx.~P(x)
    4.   |     |----
    5.   |     |  |  [c]
    6.   |     |  |  ~P(c)
    7.   |     |  |------
    8.   |     |  |  |  ∀x.P(x)
    9.   |     |  |  |------
    10.  |     |  |  |  P(c)                       ∀E: 9
    11.  |     |  |  |  _L                         _LI: 6,10
    12.  |     |  |  ~∀x.P(x)                   ~I: 8-11
    13.  |     |  ~∀x.P(x)                      ƎE: 3,5-12
    14.  |   (Ǝx.~P(x)) ---> ~∀x.P(x)     -->I:3-13
    btw, _L is \bot. It appears as an image, so it messed up the indent..
    Follow Math Help Forum on Facebook and Google+

  9. #9
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,528
    Thanks
    773

    Re: Natural Deduction: Predicate Logic. Need help!

    Seems OK. This is not a remark about this derivation, but the rule deriving ⊥ from A and ~A should be called ~E. In some precise sense it is dual to ~I. In fact, if ~A is considered an abbreviation for A -> ⊥, then ~I becomes ->I and ~E becomes ->E. As for ⊥, it has an elimination rule but no introduction rule.
    Follow Math Help Forum on Facebook and Google+

  10. #10
    Newbie
    Joined
    Aug 2012
    From
    United Kingdom
    Posts
    6

    Re: Natural Deduction: Predicate Logic. Need help!

    Cheers, so does it mean that my working is acceptable?

    Oh btw, I was following the rules that my lecturer provided for us. Here's the screenshot
    Natural Deduction: Predicate Logic. Need help!-nd-rule.png

    As an alternative to my answer above (I will post it soon) from using ⊥E, can it be safe to assume ⊥ = "~∀x.P(x)" ?
    Follow Math Help Forum on Facebook and Google+

  11. #11
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,528
    Thanks
    773

    Re: Natural Deduction: Predicate Logic. Need help!

    Quote Originally Posted by nash160 View Post
    Cheers, so does it mean that my working is acceptable?
    I think it's fine. One thing is that I am not sure it is necessary to number lines that don't have formulas.

    Quote Originally Posted by nash160 View Post
    Oh btw, I was following the rules that my lecturer provided for us.
    Rule names is not a big deal.

    Quote Originally Posted by nash160 View Post
    As an alternative to my answer above (I will post it soon) from using ⊥E, can it be safe to assume ⊥ = "~∀x.P(x)" ?
    I am nor sure I understand "As an alternative to my answer... from using ⊥E." Did you use ⊥E? And of course ⊥ and ~∀x.P(x) are completely different formulas.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Natural Deduction in propositional logic
    Posted in the Discrete Math Forum
    Replies: 4
    Last Post: August 7th 2012, 07:05 AM
  2. Like below: Natural Deduction for Predicate Calculus
    Posted in the Discrete Math Forum
    Replies: 3
    Last Post: August 7th 2012, 06:44 AM
  3. natural deduction
    Posted in the Discrete Math Forum
    Replies: 3
    Last Post: December 12th 2011, 08:31 AM
  4. Help with Logic (Natural Deduction)
    Posted in the Discrete Math Forum
    Replies: 7
    Last Post: January 12th 2010, 02:07 PM
  5. classical logic - proofs via natural deduction
    Posted in the Discrete Math Forum
    Replies: 1
    Last Post: April 25th 2009, 10:27 AM

Search Tags


/mathhelpforum @mathhelpforum