Results 1 to 11 of 11

Math Help - Formal Predicate Logic

  1. #1
    Member
    Joined
    Dec 2009
    Posts
    224

    Formal Predicate Logic

    I need help with part (b) of the following question:





    Attempt:

    To solve this I'm trying to follow a similar worked example here. And the definition of the formal system K_L is here.

    So, we know that ((p \to q) \to (\neg q \to \neg p)) is a tautology since:

    (p \to q) \iff (\neg p \vee q)
    \iff (q \vee \neg p)
    \iff (\neg \neg q \vee \neg p)
    \iff (\neg q \to \neg p)

    Now, I guess the first step is to show that \{ \forall x (A \to B), \neg(\forall x \neg B) \} \vdash_{K_L} \neg \forall x \neg A.

    1. \forall x (A \to B) .....(Hyp)
    2. (\forall x (A \to B)) \to (\forall x (\neg B \to \neg A)) .....(instance of tautology ((p \to q) \to (\neg q \to \neg p)))
    3. (\forall x (\neg B \to \neg A)) .....(1,2, Modus Ponen)
    4. ...

    I'm stuck at this point... How should I continue? Any help is appreciated.
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,513
    Thanks
    769

    Re: Formal Predicate Logic

    A quick question: are you allowed to use the deduction theorem?
    Follow Math Help Forum on Facebook and Google+

  3. #3
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,513
    Thanks
    769

    Re: Formal Predicate Logic

    I should have looked at the example. If you can use the deduction theorem and generalization, it's pretty easy. Let me post a derivation in natural deduction. It is straightforward to convert it to a derivation in K_L.

    Follow Math Help Forum on Facebook and Google+

  4. #4
    Super Member

    Joined
    May 2006
    From
    Lexington, MA (USA)
    Posts
    11,683
    Thanks
    615

    Re: Formal Predicate Logic

    Hello, demode!

    \text{Verify that }\,(p \to q) \to (\sim\!q\to\:\sim\!p)\,\text{ is a tautology.}

    \begin{array}{cccccccccc}1. & (p \to q) \to (\sim\!q \to\: \sim\!p) && 1. & \text{Given} \\ 2. & (\sim\!p \vee q) \to (q\: \vee \sim\! p) && 2. & \text{Def. impl'n} \\ 3. & \sim(\sim\!p \vee q) \vee (q\: \vee \sim\!p) && 3. & \text{Def. Impl'n} \\ 4. & (p \:\wedge \sim\!q) \vee (q\: \vee \sim\!p) && 4. & \text{DeMorgan} \\ 5. & [(p\: \wedge \sim\!q) \vee q]\: \vee \sim\!p && 5. & \text{Assoc.} \\ 6. & [(p \vee q) \wedge (\sim\!q \vee q)]\: \vee \sim\!p && 6. & \text{Distr.} \\ 7. & [(p\vee q) \wedge T]\: \vee \sim\!p && 7. & s\: \vee\! \sim\!s \:=\:T \\ 8. & (p \vee q)\: \vee \sim\!p && 8. & s \wedge T \:=\:s \\ 9. & (p\: \vee \sim\!p) \vee q && 9. & \text{Comm, Assoc.} \\ 10. & T \vee q && 10. & s\: \vee\!\sim\!s \:=\:T \\ 11. & T && 11. & T \vee s \:=\:T  \end{array}

    Follow Math Help Forum on Facebook and Google+

  5. #5
    Member
    Joined
    Dec 2009
    Posts
    224

    Re: Formal Predicate Logic

    Quote Originally Posted by emakarov View Post
    A quick question: are you allowed to use the deduction theorem?
    I think we are required to follow the given example very closely. But yes we can use the Deduction Theorem. The deduction theorem for K_L goes like this: for \Sigma \cup \{A\} \vdash_{K_L} B, the derivation of B from \Sigma \cup \{A\} does not use an application of generalization to a free variable of A. Then \Sigma \vdash_{K_L} (A \to B).
    Follow Math Help Forum on Facebook and Google+

  6. #6
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,513
    Thanks
    769

    Re: Formal Predicate Logic

    Well, as my derivation shows, \forall x\,(A\to B),\forall x\,\neg B\vdash\neg A(x). Then you use generalization on x. Note that x does not occur free in the assumptions, so you can apply the deduction theorem.
    Follow Math Help Forum on Facebook and Google+

  7. #7
    Member
    Joined
    Dec 2009
    Posts
    224

    Re: Formal Predicate Logic

    Quote Originally Posted by emakarov View Post
    Well, as my derivation shows, \forall x\,(A\to B),\forall x\,\neg B\vdash\neg A(x). Then you use generalization on x. Note that x does not occur free in the assumptions, so you can apply the deduction theorem.
    I really appreciate your response. But I'm having some trouble following your derivation in post #3, could you please show it in the simple format (like the one in my post)?
    Follow Math Help Forum on Facebook and Google+

  8. #8
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,513
    Thanks
    769

    Re: Formal Predicate Logic

    1. \forall x\,(A\to B) Hyp
    2. (\forall x\,(A\to B))\to(A\to B) K4
    3. A\to B 1, 2, MP
    4. (A\to B)\to(\neg B\to\neg A) instance of tautology
    5. \neg B\to\neg A 3, 4, MP
    6. \forall x\,\neg B Hyp
    7. (\forall x\,\neg B)\to\neg B K4
    8. \neg B 6, 7, MP
    9. \neg A 5, 8, MP
    10. \forall x\,\neg A 9, generalization applied to x
    11. (\forall x\,\neg B)\to\forall x\,\neg A 6, 10, deduction theorem
    12. (\forall x\,(A\to B))\to(\forall x\,\neg B)\to\forall x\,\neg A 1, 11, deduction theorem

    In step 10, similar to part (c) of the example, generalization is a rule that must have been derived using K5. It applies to x, which is not free in either of the assumptions, so one can use the deduction theorem in steps 11 and 12.
    Follow Math Help Forum on Facebook and Google+

  9. #9
    Member
    Joined
    Dec 2009
    Posts
    224

    Re: Formal Predicate Logic

    I'm also stuck on a very similar question where I'm required to deduce that \{\forall x \neg (A \to B) \} \vdash_{K_L} \neg (\forall x A \to B). And I have already shown that \{\forall x \neg (A \to B) \} \vdash_{K_L} \neg B and \{\forall x \neg (A \to B) \} \vdash_{K_L} \forall x A. [And I want to use an instance of the tautology (p \to (\neg q \to \neg (p \to q)))]. So we have

    1. \neg(A \to B) Hyp

    2. \neg B Hyp

    3. \forall x A Hyp

    4. A K4

    5. A \to (\neg B \to \neg (A \to B)) Taut

    Any ideas how to proceed? I even tried K5, but to no avail... I don't see a way to get the \forall x part inside the bracket with next to A in ~(A -> B)...
    Last edited by demode; October 13th 2011 at 04:35 AM.
    Follow Math Help Forum on Facebook and Google+

  10. #10
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,513
    Thanks
    769

    Re: Formal Predicate Logic

    Since (\forall x\,A)\to\neg B\to\neg((\forall x\,A)\to B) is an instance of the tautology and you have shown \{\forall x \neg (A \to B) \} \vdash_{K_L} \forall x A and \{\forall x \neg (A \to B) \} \vdash_{K_L} \neg B, then what's the problem? Just use MP twice. Or do you need to derive \forall x\,(A\to B)?
    Follow Math Help Forum on Facebook and Google+

  11. #11
    Member
    Joined
    Dec 2009
    Posts
    224

    Re: Formal Predicate Logic

    Quote Originally Posted by emakarov View Post
    Since (\forall x\,A)\to\neg B\to\neg((\forall x\,A)\to B) is an instance of the tautology and you have shown \{\forall x \neg (A \to B) \} \vdash_{K_L} \forall x A and \{\forall x \neg (A \to B) \} \vdash_{K_L} \neg B, then what's the problem? Just use MP twice. Or do you need to derive \forall x\,(A\to B)?
    Edit: I get it. Thank You!
    Last edited by demode; October 13th 2011 at 12:12 PM.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Predicate Logic
    Posted in the Discrete Math Forum
    Replies: 1
    Last Post: November 5th 2010, 07:53 AM
  2. Predicate Logic
    Posted in the Discrete Math Forum
    Replies: 5
    Last Post: April 29th 2010, 03:51 PM
  3. predicate logic
    Posted in the Discrete Math Forum
    Replies: 1
    Last Post: March 6th 2009, 01:06 AM
  4. More predicate logic
    Posted in the Discrete Math Forum
    Replies: 1
    Last Post: March 4th 2009, 06:45 PM
  5. Formal Logic
    Posted in the Discrete Math Forum
    Replies: 2
    Last Post: April 23rd 2008, 02:06 PM

/mathhelpforum @mathhelpforum