Results 1 to 6 of 6

Math Help - Prenex Normal Forms

  1. #1
    Member
    Joined
    Dec 2009
    Posts
    224

    Prenex Normal Forms

    Find a predicate form in prenex normal form which is logically equivalent to using the equivalences:

    (a) ((Agxy \vee Bz) \to \exists y (By \to Bgy))

    (b) (\forall x (Cxyz \to Bx) \wedge \neg \exists z \forall x (Dzy \to Dxy))

    Attempt:

    (a) ((Agxy \vee Bz) \to \exists y (By \to Bgy))

    Here we only have one quantifier to be shifted to the front, so we can use equivalence number 12 to get

    \exists y ((Agxy \vee Bz) \to (By \to Bgy))

    Is this right? Because we are only justified in using this equivalence if the variable y doesn not occur free in (Agxy \vee Bz), but we don't know that since y doesn't not appear in the scope of any quantifiers in it...

    (b) (\forall x(Cxyz \to Bx) \wedge \neg \exists z \forall x (Dzy \to Dxy))

    \forall x ((Cxyz \to Bx) \wedge \neg \exists z \forall x (Dzy \to Dxy))

    In our case the variables are not distinct so we can't apply the equivalcences straight away, so we have to change bound variables first so that we can move quantifiers past the free variables:

    \forall x ((Cxyz \to Bx) \wedge \neg \exists z \forall w (Dzy \to Dwy))

    Now, I'm a bit confused about the negation, but I applied equivalence number 4

    \forall x \neg \exists z ((Cxyz \to Bx) \wedge \forall w (Dzy \to Dwy))

    Now we apply equivalence number 3

    \forall x \neg \exists z \forall w((Cxyz \to Bx) \wedge (Dzy \to Dwy))

    I would appreciate it if anyone could correct me.
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,536
    Thanks
    778

    Re: Prenex Normal Forms

    Quote Originally Posted by demode View Post
    (a) ((Agxy \vee Bz) \to \exists y (By \to Bgy))

    Here we only have one quantifier to be shifted to the front, so we can use equivalence number 12 to get

    \exists y ((Agxy \vee Bz) \to (By \to Bgy))
    You captured y in Agxy. The quantified y in the conclusion has to be renamed first.

    Quote Originally Posted by demode View Post
    (b) (\forall x(Cxyz \to Bx) \wedge \neg \exists z \forall x (Dzy \to Dxy))

    \forall x ((Cxyz \to Bx) \wedge \neg \exists z \forall x (Dzy \to Dxy))

    In our case the variables are not distinct so we can't apply the equivalcences straight away, so we have to change bound variables first so that we can move quantifiers past the free variables:

    \forall x ((Cxyz \to Bx) \wedge \neg \exists z \forall w (Dzy \to Dwy))
    But z also occurs free in the first part, so it has to be renamed as well.

    Quote Originally Posted by demode View Post
    Now, I'm a bit confused about the negation, but I applied equivalence number 4

    \forall x \neg \exists z ((Cxyz \to Bx) \wedge \forall w (Dzy \to Dwy))
    You need the equivalences \neg\exists x\,A\Leftrightarrow\forall x\,\neg A and \neg\forall x\,A\Leftrightarrow \exists x\,\neg A.
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Member
    Joined
    Dec 2009
    Posts
    224

    Re: Prenex Normal Forms

    Quote Originally Posted by emakarov View Post
    But z also occurs free in the first part, so it has to be renamed as well.

    You need the equivalences \neg\exists x\,A\Leftrightarrow\forall x\,\neg A and \neg\forall x\,A\Leftrightarrow \exists x\,\neg A.
    Is the following correct? I used the equivalence you mentioned:

    \forall x (( Cxyz \to Bx) \wedge \neg \exists z \forall w (Dzy \to Dwy))

    \forall x (( Cxyz \to Bx) \wedge \neg \exists u \forall w (Duy \to Dwy))

    \forall x (( Cxyz \to Bx) \wedge \forall u \forall w \neg(Duy \to Dwy))

    \forall x \forall u \forall w(( Cxyz \to Bx) \wedge \neg(Duy \to Dwy))


    You captured y in Agxy. The quantified y in the conclusion has to be renamed first.
    ((Agxy \vee Bz) \to \exists y (By \to Bgy))

    ((Agxy \vee Bz) \to \exists w (Bw \to Bgw))

    \exists w ((Agxy \vee Bz) \to (Bw \to Bgw))

    Did I derive it correctly correct? It looks like it's in the prenex normal form since it's in the form Q_1x_1Q_2x_2...Q_nx_n B (B being a predicate form with no quantifiers and Q_n is any quantifier).
    Follow Math Help Forum on Facebook and Google+

  4. #4
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,536
    Thanks
    778

    Re: Prenex Normal Forms

    Quote Originally Posted by demode View Post
    Is the following correct? I used the equivalence you mentioned:

    \forall x (( Cxyz \to Bx) \wedge \neg \exists z \forall w (Dzy \to Dwy))

    \forall x (( Cxyz \to Bx) \wedge \neg \exists u \forall w (Duy \to Dwy))

    \forall x (( Cxyz \to Bx) \wedge \forall u \forall w \neg(Duy \to Dwy))

    \forall x \forall u \forall w(( Cxyz \to Bx) \wedge \neg(Duy \to Dwy))
    The quantifier of w should change from ∀ to ∃ when you carry negation over it. Otherwise, it seems correct.

    Quote Originally Posted by demode View Post
    ((Agxy \vee Bz) \to \exists y (By \to Bgy))

    ((Agxy \vee Bz) \to \exists w (Bw \to Bgw))

    \exists w ((Agxy \vee Bz) \to (Bw \to Bgw))

    Did I derive it correctly correct?
    Yes.
    Follow Math Help Forum on Facebook and Google+

  5. #5
    Member
    Joined
    Dec 2009
    Posts
    224

    Re: Prenex Normal Forms

    Quote Originally Posted by emakarov View Post
    The quantifier of w should change from ∀ to ∃ when you carry negation over it. Otherwise, it seems correct.

    Yes.
    You mean every time I shift the negation to the right of the ∀ it changes to ∃ like this:

    \forall x (( Cxyz \to Bx) \wedge \neg \exists u \forall w (Duy \to Dwy))

    \forall x (( Cxyz \to Bx) \wedge \forall u \exists w \neg(Duy \to Dwy))

    \forall x \forall u \exists w(( Cxyz \to Bx) \wedge \neg(Duy \to Dwy))

    Is this okay now?
    Follow Math Help Forum on Facebook and Google+

  6. #6
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,536
    Thanks
    778

    Re: Prenex Normal Forms

    Quote Originally Posted by demode View Post
    Is this okay now?
    Yes.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Replies: 1
    Last Post: January 16th 2012, 07:21 PM
  2. Help with prenex normal form
    Posted in the Discrete Math Forum
    Replies: 13
    Last Post: July 13th 2011, 06:31 AM
  3. Jordan Normal Forms
    Posted in the Advanced Algebra Forum
    Replies: 1
    Last Post: March 27th 2010, 03:01 PM
  4. Prenex normal form: moving quantifiers
    Posted in the Discrete Math Forum
    Replies: 2
    Last Post: February 23rd 2010, 08:01 AM
  5. 2-forms
    Posted in the Calculus Forum
    Replies: 4
    Last Post: November 10th 2007, 01:52 PM

/mathhelpforum @mathhelpforum