CNF quantifier elimination
Hello I have the following formula that I need to transform to a normal form required for the resolution rule. I understand that this from is a sum of OR's as in:
$(V1 lor V2 ) land ( V3 lor V4 ) )$
The formula:
$forall x forall y bigl[P(x,y) Rightarrow exists z [Q(y,z] land lnot R(x,z)]bigl] lor forall z Q(x,y,z)$
so, I use Skolem to substitute $exists z$ with a constant A, then removed the universal quantifiers and following the general logic rules I came up with this:
$bigl( lnot P(x,y) lor Q(y,A) lor Q(x,y,z) bigl) land bigl( lnot P(x,y) lor R(x,A) lor Q(x,y,z) bigl)$
Or should I first move the right most $forall z$ to the left and then through skolem substitute the $exists z$ with a function f(z) ?
$bigl( lnot P(x,y) lor Q(y,f(z)) lor Q(x,y,f(z)) bigl) land bigl( lnot P(x,y) lor R(x,f(z)) lor Q(x,y,f(z)) bigl)$
Which solution is correct?
logic quantifiers
asked Nov 29 '18 at 14:29
Jan JankowskiJan Jankowski
112
add a comment |
Hello I have the following formula that I need to transform to a normal form required for the resolution rule. I understand that this from is a sum of OR's as in:
$(V1 lor V2 ) land ( V3 lor V4 ) )$
The formula:
$forall x forall y bigl[P(x,y) Rightarrow exists z [Q(y,z] land lnot R(x,z)]bigl] lor forall z Q(x,y,z)$
so, I use Skolem to substitute $exists z$ with a constant A, then removed the universal quantifiers and following the general logic rules I came up with this:
$bigl( lnot P(x,y) lor Q(y,A) lor Q(x,y,z) bigl) land bigl( lnot P(x,y) lor R(x,A) lor Q(x,y,z) bigl)$
Or should I first move the right most $forall z$ to the left and then through skolem substitute the $exists z$ with a function f(z) ?
$bigl( lnot P(x,y) lor Q(y,f(z)) lor Q(x,y,f(z)) bigl) land bigl( lnot P(x,y) lor R(x,f(z)) lor Q(x,y,f(z)) bigl)$
Which solution is correct?
logic quantifiers
asked Nov 29 '18 at 14:29
Jan JankowskiJan Jankowski
112
The safe way to proceed is to rename one of the $z$'s. Next notice that the choice of $z$ in the existential quantifier depends on $x$ and $y$. Hence you need a Skolem function of both $x$ and $y$.
– Fabio Somenzi
Nov 29 '18 at 15:58
1
so if we rename the right most z to v we get: $forall x forall y bigl [P(x,y)⇒exists z [q(y,z) land lnot R(x,z)] bigl ] lor forall v Q(x,y,v) $ and later substitute $exists z$ with f(x,y) the CNF that we get is: $[lnot P(x,y) lor Q(y,f(x,y)) lor q(x,y,v)] land [lnot P(x,y) lor R(x,f(x,y) lor Q(x,y,v) ]$
– Jan Jankowski
Nov 29 '18 at 16:20
You have Q overloaded: is it bivariate or trivariate?
– Graham Kemp
Nov 29 '18 at 22:44
In your formula the $x$ and $y$ in the $Q(x,y,z)$ are outside the scope of the $forall x$ and $forall y$ quantifiers ... in fact, they are free variables. Is that what you want?
– Bram28
Nov 30 '18 at 3:55
add a comment |
Hello I have the following formula that I need to transform to a normal form required for the resolution rule. I understand that this from is a sum of OR's as in:
$(V1 lor V2 ) land ( V3 lor V4 ) )$
The formula:
$forall x forall y bigl[P(x,y) Rightarrow exists z [Q(y,z] land lnot R(x,z)]bigl] lor forall z Q(x,y,z)$
so, I use Skolem to substitute $exists z$ with a constant A, then removed the universal quantifiers and following the general logic rules I came up with this:
$bigl( lnot P(x,y) lor Q(y,A) lor Q(x,y,z) bigl) land bigl( lnot P(x,y) lor R(x,A) lor Q(x,y,z) bigl)$
Or should I first move the right most $forall z$ to the left and then through skolem substitute the $exists z$ with a function f(z) ?
$bigl( lnot P(x,y) lor Q(y,f(z)) lor Q(x,y,f(z)) bigl) land bigl( lnot P(x,y) lor R(x,f(z)) lor Q(x,y,f(z)) bigl)$
Which solution is correct?
logic quantifiers
asked Nov 29 '18 at 14:29
Jan JankowskiJan Jankowski
112
Hello I have the following formula that I need to transform to a normal form required for the resolution rule. I understand that this from is a sum of OR's as in:
$(V1 lor V2 ) land ( V3 lor V4 ) )$
The formula:
$forall x forall y bigl[P(x,y) Rightarrow exists z [Q(y,z] land lnot R(x,z)]bigl] lor forall z Q(x,y,z)$
so, I use Skolem to substitute $exists z$ with a constant A, then removed the universal quantifiers and following the general logic rules I came up with this:
$bigl( lnot P(x,y) lor Q(y,A) lor Q(x,y,z) bigl) land bigl( lnot P(x,y) lor R(x,A) lor Q(x,y,z) bigl)$
Or should I first move the right most $forall z$ to the left and then through skolem substitute the $exists z$ with a function f(z) ?
$bigl( lnot P(x,y) lor Q(y,f(z)) lor Q(x,y,f(z)) bigl) land bigl( lnot P(x,y) lor R(x,f(z)) lor Q(x,y,f(z)) bigl)$
Which solution is correct?
logic quantifiers
logic quantifiers
asked Nov 29 '18 at 14:29
Jan JankowskiJan Jankowski
112
asked Nov 29 '18 at 14:29
Jan JankowskiJan Jankowski
112
edited Nov 29 '18 at 14:35
Jan Jankowski
asked Nov 29 '18 at 14:29
Jan JankowskiJan Jankowski
112
asked Nov 29 '18 at 14:29
Jan JankowskiJan Jankowski
112
asked Nov 29 '18 at 14:29
Jan JankowskiJan Jankowski
112
112
The safe way to proceed is to rename one of the $z$'s. Next notice that the choice of $z$ in the existential quantifier depends on $x$ and $y$. Hence you need a Skolem function of both $x$ and $y$.
– Fabio Somenzi
Nov 29 '18 at 15:58
1
so if we rename the right most z to v we get: $forall x forall y bigl [P(x,y)⇒exists z [q(y,z) land lnot R(x,z)] bigl ] lor forall v Q(x,y,v) $ and later substitute $exists z$ with f(x,y) the CNF that we get is: $[lnot P(x,y) lor Q(y,f(x,y)) lor q(x,y,v)] land [lnot P(x,y) lor R(x,f(x,y) lor Q(x,y,v) ]$
– Jan Jankowski
Nov 29 '18 at 16:20
You have Q overloaded: is it bivariate or trivariate?
– Graham Kemp
Nov 29 '18 at 22:44
In your formula the $x$ and $y$ in the $Q(x,y,z)$ are outside the scope of the $forall x$ and $forall y$ quantifiers ... in fact, they are free variables. Is that what you want?
– Bram28
Nov 30 '18 at 3:55
add a comment |
The safe way to proceed is to rename one of the $z$'s. Next notice that the choice of $z$ in the existential quantifier depends on $x$ and $y$. Hence you need a Skolem function of both $x$ and $y$.
– Fabio Somenzi
Nov 29 '18 at 15:58
1
so if we rename the right most z to v we get: $forall x forall y bigl [P(x,y)⇒exists z [q(y,z) land lnot R(x,z)] bigl ] lor forall v Q(x,y,v) $ and later substitute $exists z$ with f(x,y) the CNF that we get is: $[lnot P(x,y) lor Q(y,f(x,y)) lor q(x,y,v)] land [lnot P(x,y) lor R(x,f(x,y) lor Q(x,y,v) ]$
– Jan Jankowski
Nov 29 '18 at 16:20
You have Q overloaded: is it bivariate or trivariate?
– Graham Kemp
Nov 29 '18 at 22:44
In your formula the $x$ and $y$ in the $Q(x,y,z)$ are outside the scope of the $forall x$ and $forall y$ quantifiers ... in fact, they are free variables. Is that what you want?
– Bram28
Nov 30 '18 at 3:55
The safe way to proceed is to rename one of the $z$'s. Next notice that the choice of $z$ in the existential quantifier depends on $x$ and $y$. Hence you need a Skolem function of both $x$ and $y$.
– Fabio Somenzi
Nov 29 '18 at 15:58
The safe way to proceed is to rename one of the $z$'s. Next notice that the choice of $z$ in the existential quantifier depends on $x$ and $y$. Hence you need a Skolem function of both $x$ and $y$.
– Fabio Somenzi
Nov 29 '18 at 15:58
1
1
so if we rename the right most z to v we get: $forall x forall y bigl [P(x,y)⇒exists z [q(y,z) land lnot R(x,z)] bigl ] lor forall v Q(x,y,v) $ and later substitute $exists z$ with f(x,y) the CNF that we get is: $[lnot P(x,y) lor Q(y,f(x,y)) lor q(x,y,v)] land [lnot P(x,y) lor R(x,f(x,y) lor Q(x,y,v) ]$
– Jan Jankowski
Nov 29 '18 at 16:20
so if we rename the right most z to v we get: $forall x forall y bigl [P(x,y)⇒exists z [q(y,z) land lnot R(x,z)] bigl ] lor forall v Q(x,y,v) $ and later substitute $exists z$ with f(x,y) the CNF that we get is: $[lnot P(x,y) lor Q(y,f(x,y)) lor q(x,y,v)] land [lnot P(x,y) lor R(x,f(x,y) lor Q(x,y,v) ]$
– Jan Jankowski
Nov 29 '18 at 16:20
You have Q overloaded: is it bivariate or trivariate?
– Graham Kemp
Nov 29 '18 at 22:44
You have Q overloaded: is it bivariate or trivariate?
– Graham Kemp
Nov 29 '18 at 22:44
In your formula the $x$ and $y$ in the $Q(x,y,z)$ are outside the scope of the $forall x$ and $forall y$ quantifiers ... in fact, they are free variables. Is that what you want?
– Bram28
Nov 30 '18 at 3:55
In your formula the $x$ and $y$ in the $Q(x,y,z)$ are outside the scope of the $forall x$ and $forall y$ quantifiers ... in fact, they are free variables. Is that what you want?
– Bram28
Nov 30 '18 at 3:55
add a comment |
2 Answers
2
active
oldest
votes
The safe way to proceed is to rename one of the z's. Next notice that the choice of z in the existential quantifier depends on x and y. Hence you need a Skolem function of both x and y.
so if we rename the right most z to v we get:
∀x∀y[P(x,y)⇒∃z[q(y,z)∧¬R(x,z)] ]∨∀vQ(x,y,v)
and later substitute ∃z with f(x,y) the CNF that we get is
[¬P(x,y)∨Q(y,f(x,y))∨q(x,y,v)]∧[¬P(x,y)∨R(x,f(x,y)∨Q(x,y,v)]
answered Nov 29 '18 at 16:36
Jan JankowskiJan Jankowski
112
add a comment |
Neither is correct.
First, I would recommend to always move the quantifiers to the top of the statement. That way, you know whether to skolemize or not, and if so, on what variables it depends.
Indeed, I am a little suspicious that you skolemized the exisntential simply because it was an existential. But you need to be super careful with that. For example, if you have
$neg exists P(x)$
you really don't want to skolemize the existential, but rather you should bring the quantifier out, and if you do, you get
$forall x neg P(x)$
and so you see that you shouldn't skolemize at all.
Now, in this particular case, you do end up with an existential if you bring the quantifier for the $z$ out, for you get (by the way, I am adding a set of parentheses to get the $Q(x,y,z)$ term inside the scope of the the $forall x forall y$ which I believe is meant):
$forall x forall y ((P(x,y) rightarrow exists z (Q(y,z) land neg P(x,z))) lor forall z Q(x,y,z)) Leftrightarrow$
$forall x forall y ((neg P(x,y) lor exists z (Q(y,z) land neg P(x,z))) lor forall z Q(x,y,z)) Leftrightarrow $
$forall x forall y (exists z (neg P(x,y) lor (Q(y,z) land neg P(x,z))) lor forall z Q(x,y,z)) Leftrightarrow$
$forall x forall y exists z ((neg P(x,y) lor (Q(y,z) land neg P(x,z))) lor forall z Q(x,y,z)) Leftrightarrow$
$forall x forall y exists z ((neg P(x,y) lor (Q(y,z) land neg P(x,z))) lor forall w Q(x,y,w)) Leftrightarrow$
$forall x forall y exists z forall w ((neg P(x,y) lor (Q(y,z) land neg P(x,z))) lor Q(x,y,w)) Leftrightarrow$
$forall x forall y exists z forall w (((neg P(x,y) lor Q(y,z)) land (neg P(x,y) lor neg P(x,z)) lor Q(x,y,w)) Leftrightarrow$
$forall x forall y exists z forall w ((neg P(x,y) lor Q(y,z) lor Q(x,y,w)) land (neg P(x,y) lor neg P(x,z) lor Q(x,y,w))$
So, we now see the first $z$ does indeed need to be quantofied existentially, and the second $z$ universally, but in order to bring out that second $z$ it had to be renamed to a different variable $w$.
OK, so we can now drop the universals and, m or importantly, we see the dependency of the $z$ on the $x$ and $y$, so we need to use a skolem function that takes in both $x$ and $y$:
$(neg P(x,y) lor Q(y,f(x,y)) lor Q(x,y,w)) land (neg P(x,y) lor neg P(x,f(x,y)) lor Q(x,y,w))$
answered Nov 30 '18 at 4:29
Bram28Bram28
60.4k44590
(by the way, I am adding a set of parentheses to get the Q(x,y,z)what is the rule that allows to do that? Can I assume that sinsce in $forall z Q(x,y,z)$ I had no universal quantifiers for x and y, that means that I can put this expression "under" the universal quantifiers from the left part of the formula?
– Jan Jankowski
Nov 30 '18 at 11:48
@JanJankowski No, there is no rule for that: By adding those paentheses I changed the meaning of the original formula ... but I figured that you or whoever gave you this problem made a typo and forgot those parentheses, because with parentheses, it no longer has free variables, and would also make it a more interesting problem.
– Bram28
Nov 30 '18 at 20:41
add a comment |
Your Answer
StackExchange.ifUsing("editor", function () {
return StackExchange.using("mathjaxEditing", function () {
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
});
});
}, "mathjax-editing");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "69"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3018693%2fcnf-quantifier-elimination%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
2 Answers
2
active
oldest
votes
2 Answers
2
active
oldest
votes
active
oldest
votes
active
oldest
votes
The safe way to proceed is to rename one of the z's. Next notice that the choice of z in the existential quantifier depends on x and y. Hence you need a Skolem function of both x and y.
so if we rename the right most z to v we get:
∀x∀y[P(x,y)⇒∃z[q(y,z)∧¬R(x,z)] ]∨∀vQ(x,y,v)
and later substitute ∃z with f(x,y) the CNF that we get is
[¬P(x,y)∨Q(y,f(x,y))∨q(x,y,v)]∧[¬P(x,y)∨R(x,f(x,y)∨Q(x,y,v)]
answered Nov 29 '18 at 16:36
Jan JankowskiJan Jankowski
112
add a comment |
The safe way to proceed is to rename one of the z's. Next notice that the choice of z in the existential quantifier depends on x and y. Hence you need a Skolem function of both x and y.
so if we rename the right most z to v we get:
∀x∀y[P(x,y)⇒∃z[q(y,z)∧¬R(x,z)] ]∨∀vQ(x,y,v)
and later substitute ∃z with f(x,y) the CNF that we get is
[¬P(x,y)∨Q(y,f(x,y))∨q(x,y,v)]∧[¬P(x,y)∨R(x,f(x,y)∨Q(x,y,v)]
answered Nov 29 '18 at 16:36
Jan JankowskiJan Jankowski
112
add a comment |
The safe way to proceed is to rename one of the z's. Next notice that the choice of z in the existential quantifier depends on x and y. Hence you need a Skolem function of both x and y.
so if we rename the right most z to v we get:
∀x∀y[P(x,y)⇒∃z[q(y,z)∧¬R(x,z)] ]∨∀vQ(x,y,v)
and later substitute ∃z with f(x,y) the CNF that we get is
[¬P(x,y)∨Q(y,f(x,y))∨q(x,y,v)]∧[¬P(x,y)∨R(x,f(x,y)∨Q(x,y,v)]
answered Nov 29 '18 at 16:36
Jan JankowskiJan Jankowski
112
The safe way to proceed is to rename one of the z's. Next notice that the choice of z in the existential quantifier depends on x and y. Hence you need a Skolem function of both x and y.
so if we rename the right most z to v we get:
∀x∀y[P(x,y)⇒∃z[q(y,z)∧¬R(x,z)] ]∨∀vQ(x,y,v)
and later substitute ∃z with f(x,y) the CNF that we get is
[¬P(x,y)∨Q(y,f(x,y))∨q(x,y,v)]∧[¬P(x,y)∨R(x,f(x,y)∨Q(x,y,v)]
answered Nov 29 '18 at 16:36
Jan JankowskiJan Jankowski
112
answered Nov 29 '18 at 16:36
Jan JankowskiJan Jankowski
112
answered Nov 29 '18 at 16:36
Jan JankowskiJan Jankowski
112
answered Nov 29 '18 at 16:36
Jan JankowskiJan Jankowski
112
112
add a comment |
add a comment |
Neither is correct.
First, I would recommend to always move the quantifiers to the top of the statement. That way, you know whether to skolemize or not, and if so, on what variables it depends.
Indeed, I am a little suspicious that you skolemized the exisntential simply because it was an existential. But you need to be super careful with that. For example, if you have
$neg exists P(x)$
you really don't want to skolemize the existential, but rather you should bring the quantifier out, and if you do, you get
$forall x neg P(x)$
and so you see that you shouldn't skolemize at all.
Now, in this particular case, you do end up with an existential if you bring the quantifier for the $z$ out, for you get (by the way, I am adding a set of parentheses to get the $Q(x,y,z)$ term inside the scope of the the $forall x forall y$ which I believe is meant):
$forall x forall y ((P(x,y) rightarrow exists z (Q(y,z) land neg P(x,z))) lor forall z Q(x,y,z)) Leftrightarrow$
$forall x forall y ((neg P(x,y) lor exists z (Q(y,z) land neg P(x,z))) lor forall z Q(x,y,z)) Leftrightarrow $
$forall x forall y (exists z (neg P(x,y) lor (Q(y,z) land neg P(x,z))) lor forall z Q(x,y,z)) Leftrightarrow$
$forall x forall y exists z ((neg P(x,y) lor (Q(y,z) land neg P(x,z))) lor forall z Q(x,y,z)) Leftrightarrow$
$forall x forall y exists z ((neg P(x,y) lor (Q(y,z) land neg P(x,z))) lor forall w Q(x,y,w)) Leftrightarrow$
$forall x forall y exists z forall w ((neg P(x,y) lor (Q(y,z) land neg P(x,z))) lor Q(x,y,w)) Leftrightarrow$
$forall x forall y exists z forall w (((neg P(x,y) lor Q(y,z)) land (neg P(x,y) lor neg P(x,z)) lor Q(x,y,w)) Leftrightarrow$
$forall x forall y exists z forall w ((neg P(x,y) lor Q(y,z) lor Q(x,y,w)) land (neg P(x,y) lor neg P(x,z) lor Q(x,y,w))$
So, we now see the first $z$ does indeed need to be quantofied existentially, and the second $z$ universally, but in order to bring out that second $z$ it had to be renamed to a different variable $w$.
OK, so we can now drop the universals and, m or importantly, we see the dependency of the $z$ on the $x$ and $y$, so we need to use a skolem function that takes in both $x$ and $y$:
$(neg P(x,y) lor Q(y,f(x,y)) lor Q(x,y,w)) land (neg P(x,y) lor neg P(x,f(x,y)) lor Q(x,y,w))$
answered Nov 30 '18 at 4:29
Bram28Bram28
60.4k44590
(by the way, I am adding a set of parentheses to get the Q(x,y,z)what is the rule that allows to do that? Can I assume that sinsce in $forall z Q(x,y,z)$ I had no universal quantifiers for x and y, that means that I can put this expression "under" the universal quantifiers from the left part of the formula?
– Jan Jankowski
Nov 30 '18 at 11:48
@JanJankowski No, there is no rule for that: By adding those paentheses I changed the meaning of the original formula ... but I figured that you or whoever gave you this problem made a typo and forgot those parentheses, because with parentheses, it no longer has free variables, and would also make it a more interesting problem.
– Bram28
Nov 30 '18 at 20:41
add a comment |
Neither is correct.
First, I would recommend to always move the quantifiers to the top of the statement. That way, you know whether to skolemize or not, and if so, on what variables it depends.
Indeed, I am a little suspicious that you skolemized the exisntential simply because it was an existential. But you need to be super careful with that. For example, if you have
$neg exists P(x)$
you really don't want to skolemize the existential, but rather you should bring the quantifier out, and if you do, you get
$forall x neg P(x)$
and so you see that you shouldn't skolemize at all.
Now, in this particular case, you do end up with an existential if you bring the quantifier for the $z$ out, for you get (by the way, I am adding a set of parentheses to get the $Q(x,y,z)$ term inside the scope of the the $forall x forall y$ which I believe is meant):
$forall x forall y ((P(x,y) rightarrow exists z (Q(y,z) land neg P(x,z))) lor forall z Q(x,y,z)) Leftrightarrow$
$forall x forall y ((neg P(x,y) lor exists z (Q(y,z) land neg P(x,z))) lor forall z Q(x,y,z)) Leftrightarrow $
$forall x forall y (exists z (neg P(x,y) lor (Q(y,z) land neg P(x,z))) lor forall z Q(x,y,z)) Leftrightarrow$
$forall x forall y exists z ((neg P(x,y) lor (Q(y,z) land neg P(x,z))) lor forall z Q(x,y,z)) Leftrightarrow$
$forall x forall y exists z ((neg P(x,y) lor (Q(y,z) land neg P(x,z))) lor forall w Q(x,y,w)) Leftrightarrow$
$forall x forall y exists z forall w ((neg P(x,y) lor (Q(y,z) land neg P(x,z))) lor Q(x,y,w)) Leftrightarrow$
$forall x forall y exists z forall w (((neg P(x,y) lor Q(y,z)) land (neg P(x,y) lor neg P(x,z)) lor Q(x,y,w)) Leftrightarrow$
$forall x forall y exists z forall w ((neg P(x,y) lor Q(y,z) lor Q(x,y,w)) land (neg P(x,y) lor neg P(x,z) lor Q(x,y,w))$
So, we now see the first $z$ does indeed need to be quantofied existentially, and the second $z$ universally, but in order to bring out that second $z$ it had to be renamed to a different variable $w$.
OK, so we can now drop the universals and, m or importantly, we see the dependency of the $z$ on the $x$ and $y$, so we need to use a skolem function that takes in both $x$ and $y$:
$(neg P(x,y) lor Q(y,f(x,y)) lor Q(x,y,w)) land (neg P(x,y) lor neg P(x,f(x,y)) lor Q(x,y,w))$
answered Nov 30 '18 at 4:29
Bram28Bram28
60.4k44590
(by the way, I am adding a set of parentheses to get the Q(x,y,z)what is the rule that allows to do that? Can I assume that sinsce in $forall z Q(x,y,z)$ I had no universal quantifiers for x and y, that means that I can put this expression "under" the universal quantifiers from the left part of the formula?
– Jan Jankowski
Nov 30 '18 at 11:48
@JanJankowski No, there is no rule for that: By adding those paentheses I changed the meaning of the original formula ... but I figured that you or whoever gave you this problem made a typo and forgot those parentheses, because with parentheses, it no longer has free variables, and would also make it a more interesting problem.
– Bram28
Nov 30 '18 at 20:41
add a comment |
Neither is correct.
First, I would recommend to always move the quantifiers to the top of the statement. That way, you know whether to skolemize or not, and if so, on what variables it depends.
Indeed, I am a little suspicious that you skolemized the exisntential simply because it was an existential. But you need to be super careful with that. For example, if you have
$neg exists P(x)$
you really don't want to skolemize the existential, but rather you should bring the quantifier out, and if you do, you get
$forall x neg P(x)$
and so you see that you shouldn't skolemize at all.
Now, in this particular case, you do end up with an existential if you bring the quantifier for the $z$ out, for you get (by the way, I am adding a set of parentheses to get the $Q(x,y,z)$ term inside the scope of the the $forall x forall y$ which I believe is meant):
$forall x forall y ((P(x,y) rightarrow exists z (Q(y,z) land neg P(x,z))) lor forall z Q(x,y,z)) Leftrightarrow$
$forall x forall y ((neg P(x,y) lor exists z (Q(y,z) land neg P(x,z))) lor forall z Q(x,y,z)) Leftrightarrow $
$forall x forall y (exists z (neg P(x,y) lor (Q(y,z) land neg P(x,z))) lor forall z Q(x,y,z)) Leftrightarrow$
$forall x forall y exists z ((neg P(x,y) lor (Q(y,z) land neg P(x,z))) lor forall z Q(x,y,z)) Leftrightarrow$
$forall x forall y exists z ((neg P(x,y) lor (Q(y,z) land neg P(x,z))) lor forall w Q(x,y,w)) Leftrightarrow$
$forall x forall y exists z forall w ((neg P(x,y) lor (Q(y,z) land neg P(x,z))) lor Q(x,y,w)) Leftrightarrow$
$forall x forall y exists z forall w (((neg P(x,y) lor Q(y,z)) land (neg P(x,y) lor neg P(x,z)) lor Q(x,y,w)) Leftrightarrow$
$forall x forall y exists z forall w ((neg P(x,y) lor Q(y,z) lor Q(x,y,w)) land (neg P(x,y) lor neg P(x,z) lor Q(x,y,w))$
So, we now see the first $z$ does indeed need to be quantofied existentially, and the second $z$ universally, but in order to bring out that second $z$ it had to be renamed to a different variable $w$.
OK, so we can now drop the universals and, m or importantly, we see the dependency of the $z$ on the $x$ and $y$, so we need to use a skolem function that takes in both $x$ and $y$:
$(neg P(x,y) lor Q(y,f(x,y)) lor Q(x,y,w)) land (neg P(x,y) lor neg P(x,f(x,y)) lor Q(x,y,w))$
answered Nov 30 '18 at 4:29
Bram28Bram28
60.4k44590
Neither is correct.
First, I would recommend to always move the quantifiers to the top of the statement. That way, you know whether to skolemize or not, and if so, on what variables it depends.
Indeed, I am a little suspicious that you skolemized the exisntential simply because it was an existential. But you need to be super careful with that. For example, if you have
$neg exists P(x)$
you really don't want to skolemize the existential, but rather you should bring the quantifier out, and if you do, you get
$forall x neg P(x)$
and so you see that you shouldn't skolemize at all.
Now, in this particular case, you do end up with an existential if you bring the quantifier for the $z$ out, for you get (by the way, I am adding a set of parentheses to get the $Q(x,y,z)$ term inside the scope of the the $forall x forall y$ which I believe is meant):
$forall x forall y ((P(x,y) rightarrow exists z (Q(y,z) land neg P(x,z))) lor forall z Q(x,y,z)) Leftrightarrow$
$forall x forall y ((neg P(x,y) lor exists z (Q(y,z) land neg P(x,z))) lor forall z Q(x,y,z)) Leftrightarrow $
$forall x forall y (exists z (neg P(x,y) lor (Q(y,z) land neg P(x,z))) lor forall z Q(x,y,z)) Leftrightarrow$
$forall x forall y exists z ((neg P(x,y) lor (Q(y,z) land neg P(x,z))) lor forall z Q(x,y,z)) Leftrightarrow$
$forall x forall y exists z ((neg P(x,y) lor (Q(y,z) land neg P(x,z))) lor forall w Q(x,y,w)) Leftrightarrow$
$forall x forall y exists z forall w ((neg P(x,y) lor (Q(y,z) land neg P(x,z))) lor Q(x,y,w)) Leftrightarrow$
$forall x forall y exists z forall w (((neg P(x,y) lor Q(y,z)) land (neg P(x,y) lor neg P(x,z)) lor Q(x,y,w)) Leftrightarrow$
$forall x forall y exists z forall w ((neg P(x,y) lor Q(y,z) lor Q(x,y,w)) land (neg P(x,y) lor neg P(x,z) lor Q(x,y,w))$
So, we now see the first $z$ does indeed need to be quantofied existentially, and the second $z$ universally, but in order to bring out that second $z$ it had to be renamed to a different variable $w$.
OK, so we can now drop the universals and, m or importantly, we see the dependency of the $z$ on the $x$ and $y$, so we need to use a skolem function that takes in both $x$ and $y$:
$(neg P(x,y) lor Q(y,f(x,y)) lor Q(x,y,w)) land (neg P(x,y) lor neg P(x,f(x,y)) lor Q(x,y,w))$
answered Nov 30 '18 at 4:29
Bram28Bram28
60.4k44590
answered Nov 30 '18 at 4:29
Bram28Bram28
60.4k44590
answered Nov 30 '18 at 4:29
Bram28Bram28
60.4k44590
answered Nov 30 '18 at 4:29
Bram28Bram28
60.4k44590
60.4k44590
(by the way, I am adding a set of parentheses to get the Q(x,y,z)what is the rule that allows to do that? Can I assume that sinsce in $forall z Q(x,y,z)$ I had no universal quantifiers for x and y, that means that I can put this expression "under" the universal quantifiers from the left part of the formula?
– Jan Jankowski
Nov 30 '18 at 11:48
@JanJankowski No, there is no rule for that: By adding those paentheses I changed the meaning of the original formula ... but I figured that you or whoever gave you this problem made a typo and forgot those parentheses, because with parentheses, it no longer has free variables, and would also make it a more interesting problem.
– Bram28
Nov 30 '18 at 20:41
add a comment |
(by the way, I am adding a set of parentheses to get the Q(x,y,z)what is the rule that allows to do that? Can I assume that sinsce in $forall z Q(x,y,z)$ I had no universal quantifiers for x and y, that means that I can put this expression "under" the universal quantifiers from the left part of the formula?
– Jan Jankowski
Nov 30 '18 at 11:48
@JanJankowski No, there is no rule for that: By adding those paentheses I changed the meaning of the original formula ... but I figured that you or whoever gave you this problem made a typo and forgot those parentheses, because with parentheses, it no longer has free variables, and would also make it a more interesting problem.
– Bram28
Nov 30 '18 at 20:41
(by the way, I am adding a set of parentheses to get the Q(x,y,z) what is the rule that allows to do that? Can I assume that sinsce in $forall z Q(x,y,z)$ I had no universal quantifiers for x and y, that means that I can put this expression "under" the universal quantifiers from the left part of the formula?– Jan Jankowski
Nov 30 '18 at 11:48
(by the way, I am adding a set of parentheses to get the Q(x,y,z) what is the rule that allows to do that? Can I assume that sinsce in $forall z Q(x,y,z)$ I had no universal quantifiers for x and y, that means that I can put this expression "under" the universal quantifiers from the left part of the formula?– Jan Jankowski
Nov 30 '18 at 11:48
@JanJankowski No, there is no rule for that: By adding those paentheses I changed the meaning of the original formula ... but I figured that you or whoever gave you this problem made a typo and forgot those parentheses, because with parentheses, it no longer has free variables, and would also make it a more interesting problem.
– Bram28
Nov 30 '18 at 20:41
@JanJankowski No, there is no rule for that: By adding those paentheses I changed the meaning of the original formula ... but I figured that you or whoever gave you this problem made a typo and forgot those parentheses, because with parentheses, it no longer has free variables, and would also make it a more interesting problem.
– Bram28
Nov 30 '18 at 20:41
add a comment |
Thanks for contributing an answer to Mathematics Stack Exchange!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
Some of your past answers have not been well-received, and you're in danger of being blocked from answering.
Please pay close attention to the following guidance:
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3018693%2fcnf-quantifier-elimination%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
The safe way to proceed is to rename one of the $z$'s. Next notice that the choice of $z$ in the existential quantifier depends on $x$ and $y$. Hence you need a Skolem function of both $x$ and $y$.
– Fabio Somenzi
Nov 29 '18 at 15:58
1
so if we rename the right most z to v we get: $forall x forall y bigl [P(x,y)⇒exists z [q(y,z) land lnot R(x,z)] bigl ] lor forall v Q(x,y,v) $ and later substitute $exists z$ with f(x,y) the CNF that we get is: $[lnot P(x,y) lor Q(y,f(x,y)) lor q(x,y,v)] land [lnot P(x,y) lor R(x,f(x,y) lor Q(x,y,v) ]$
– Jan Jankowski
Nov 29 '18 at 16:20
You have Q overloaded: is it bivariate or trivariate?
– Graham Kemp
Nov 29 '18 at 22:44
In your formula the $x$ and $y$ in the $Q(x,y,z)$ are outside the scope of the $forall x$ and $forall y$ quantifiers ... in fact, they are free variables. Is that what you want?
– Bram28
Nov 30 '18 at 3:55