How to prove this logical equivalence in predicate logic?
$begingroup$
Prove that:
$ ( forall x)(forall y)(exists z)((P(x)Rightarrow Q(y)) wedge neg Q(z))$
is equivalent with
$ neg((exists xP(x) lor forall zQ(z))$
How should I attempt such problems?
I tried a lot like changing the implication in a disjunction. I applied Morgan rules here and there...
It looks like I should use the transitivity rule to get rid of the Y but I didn't find how
EDIT: Corrected question, thanks to Mauro
logic predicate-logic
$endgroup$
add a comment |
$begingroup$
Prove that:
$ ( forall x)(forall y)(exists z)((P(x)Rightarrow Q(y)) wedge neg Q(z))$
is equivalent with
$ neg((exists xP(x) lor forall zQ(z))$
How should I attempt such problems?
I tried a lot like changing the implication in a disjunction. I applied Morgan rules here and there...
It looks like I should use the transitivity rule to get rid of the Y but I didn't find how
EDIT: Corrected question, thanks to Mauro
logic predicate-logic
$endgroup$
$begingroup$
Is there an $y$ missing in the first formula ?
$endgroup$
– Mauro ALLEGRANZA
Jan 30 at 13:51
$begingroup$
Indeed, thanks!
$endgroup$
– Ayoub Rossi
Jan 30 at 13:54
$begingroup$
Well in the case that $Q(y)$ for all $y$, then it is true for any specific choice of $y$, namely $z$. Hence we can replace $forall y(P(x) rightarrow Q(y))$ with $ (P(x) rightarrow Q(z)) $
$endgroup$
– NazimJ
Jan 30 at 14:37
add a comment |
$begingroup$
Prove that:
$ ( forall x)(forall y)(exists z)((P(x)Rightarrow Q(y)) wedge neg Q(z))$
is equivalent with
$ neg((exists xP(x) lor forall zQ(z))$
How should I attempt such problems?
I tried a lot like changing the implication in a disjunction. I applied Morgan rules here and there...
It looks like I should use the transitivity rule to get rid of the Y but I didn't find how
EDIT: Corrected question, thanks to Mauro
logic predicate-logic
$endgroup$
Prove that:
$ ( forall x)(forall y)(exists z)((P(x)Rightarrow Q(y)) wedge neg Q(z))$
is equivalent with
$ neg((exists xP(x) lor forall zQ(z))$
How should I attempt such problems?
I tried a lot like changing the implication in a disjunction. I applied Morgan rules here and there...
It looks like I should use the transitivity rule to get rid of the Y but I didn't find how
EDIT: Corrected question, thanks to Mauro
logic predicate-logic
logic predicate-logic
edited Jan 30 at 16:34
Mauro ALLEGRANZA
67.7k449117
67.7k449117
asked Jan 30 at 13:42
Ayoub RossiAyoub Rossi
11110
11110
$begingroup$
Is there an $y$ missing in the first formula ?
$endgroup$
– Mauro ALLEGRANZA
Jan 30 at 13:51
$begingroup$
Indeed, thanks!
$endgroup$
– Ayoub Rossi
Jan 30 at 13:54
$begingroup$
Well in the case that $Q(y)$ for all $y$, then it is true for any specific choice of $y$, namely $z$. Hence we can replace $forall y(P(x) rightarrow Q(y))$ with $ (P(x) rightarrow Q(z)) $
$endgroup$
– NazimJ
Jan 30 at 14:37
add a comment |
$begingroup$
Is there an $y$ missing in the first formula ?
$endgroup$
– Mauro ALLEGRANZA
Jan 30 at 13:51
$begingroup$
Indeed, thanks!
$endgroup$
– Ayoub Rossi
Jan 30 at 13:54
$begingroup$
Well in the case that $Q(y)$ for all $y$, then it is true for any specific choice of $y$, namely $z$. Hence we can replace $forall y(P(x) rightarrow Q(y))$ with $ (P(x) rightarrow Q(z)) $
$endgroup$
– NazimJ
Jan 30 at 14:37
$begingroup$
Is there an $y$ missing in the first formula ?
$endgroup$
– Mauro ALLEGRANZA
Jan 30 at 13:51
$begingroup$
Is there an $y$ missing in the first formula ?
$endgroup$
– Mauro ALLEGRANZA
Jan 30 at 13:51
$begingroup$
Indeed, thanks!
$endgroup$
– Ayoub Rossi
Jan 30 at 13:54
$begingroup$
Indeed, thanks!
$endgroup$
– Ayoub Rossi
Jan 30 at 13:54
$begingroup$
Well in the case that $Q(y)$ for all $y$, then it is true for any specific choice of $y$, namely $z$. Hence we can replace $forall y(P(x) rightarrow Q(y))$ with $ (P(x) rightarrow Q(z)) $
$endgroup$
– NazimJ
Jan 30 at 14:37
$begingroup$
Well in the case that $Q(y)$ for all $y$, then it is true for any specific choice of $y$, namely $z$. Hence we can replace $forall y(P(x) rightarrow Q(y))$ with $ (P(x) rightarrow Q(z)) $
$endgroup$
– NazimJ
Jan 30 at 14:37
add a comment |
2 Answers
2
active
oldest
votes
$begingroup$
Hint
We have to work with Prenex normal form equivalences.
The first formula is equivalent to :
$((∃x)P(x) to (∀y)Q(y)) ∧ (∃z)¬Q(z)$.
By De Morgan, the second formula is :
$¬(∃x) P(x) ∧ ¬(∀z)Q(z)$, i.e. $¬(∃x) P(x) ∧ (∃z)¬Q(z)$.
The first one implies the second : if we have that $(∃z)¬Q(z)$ holds, then it is false that $(∀y)Q(y)$ and thus also $(∃x)P(x)$ is false.
Thus : $¬(∃x) P(x)$ holds.
The second one implies the first : if $¬(∃x) P(x)$ holds, then $(∃x)P(x) to R$ holds, for $R$ whatever.
Thus : $(∃x)P(x) to (∀y)Q(y)$ holds.
$endgroup$
$begingroup$
One question: You say we have to work with prenex normal form but your first step switches to a non-prenex normal form if I'm not wrong?
$endgroup$
– Ayoub Rossi
Jan 30 at 17:04
$begingroup$
Second question: If I recognize a prenex normal form, should I always switch to an equivalent in non-prenex form
$endgroup$
– Ayoub Rossi
Jan 30 at 17:06
add a comment |
$begingroup$
$ forall x forall y exists z((P(x)rightarrow Q(y)) land neg Q(z)) overset{Prenex}{Leftrightarrow}$
$ forall x forall y ((P(x)rightarrow Q(y)) land exists z neg Q(z)) overset{Implication}{Leftrightarrow}$
$ forall x forall y ((neg P(x) lor Q(y)) land exists z neg Q(z))) overset{Distribution}{Leftrightarrow}$
$ forall x forall y ((neg P(x) land exists z neg Q(z)) lor ((Q(y) land exists z neg Q(z)) overset{Prenex x 2}{Leftrightarrow}$
$ forall x (neg P(x) land exists z neg Q(z)) lor forall y (Q(y) land exists z neg Q(z)) overset{Prenex x 2}{Leftrightarrow}$
$ ( forall x neg P(x) land exists z neg Q(z)) lor (forall y Q(y) land exists z neg Q(z)) overset{Quantifier Negation}{Leftrightarrow}$
$ (neg exists x P(x) land neg forall z Q(z)) lor (forall y Q(y) land neg forall z Q(z)) overset{Replacing Variables}{Leftrightarrow}$
$ (neg exists x P(x) land neg forall z Q(z)) lor (forall y Q(y) land neg forall y Q(y)) overset{Complement}{Leftrightarrow}$
$ (neg exists x P(x) land neg forall z Q(z)) lor bot overset{Identity}{Leftrightarrow}$
$ neg exists x P(x) land neg forall z Q(z)overset{DeMorgan}{Leftrightarrow}$
$ neg( exists x P(x) lor neg forall z Q(z))$
$endgroup$
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%2f3093536%2fhow-to-prove-this-logical-equivalence-in-predicate-logic%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
$begingroup$
Hint
We have to work with Prenex normal form equivalences.
The first formula is equivalent to :
$((∃x)P(x) to (∀y)Q(y)) ∧ (∃z)¬Q(z)$.
By De Morgan, the second formula is :
$¬(∃x) P(x) ∧ ¬(∀z)Q(z)$, i.e. $¬(∃x) P(x) ∧ (∃z)¬Q(z)$.
The first one implies the second : if we have that $(∃z)¬Q(z)$ holds, then it is false that $(∀y)Q(y)$ and thus also $(∃x)P(x)$ is false.
Thus : $¬(∃x) P(x)$ holds.
The second one implies the first : if $¬(∃x) P(x)$ holds, then $(∃x)P(x) to R$ holds, for $R$ whatever.
Thus : $(∃x)P(x) to (∀y)Q(y)$ holds.
$endgroup$
$begingroup$
One question: You say we have to work with prenex normal form but your first step switches to a non-prenex normal form if I'm not wrong?
$endgroup$
– Ayoub Rossi
Jan 30 at 17:04
$begingroup$
Second question: If I recognize a prenex normal form, should I always switch to an equivalent in non-prenex form
$endgroup$
– Ayoub Rossi
Jan 30 at 17:06
add a comment |
$begingroup$
Hint
We have to work with Prenex normal form equivalences.
The first formula is equivalent to :
$((∃x)P(x) to (∀y)Q(y)) ∧ (∃z)¬Q(z)$.
By De Morgan, the second formula is :
$¬(∃x) P(x) ∧ ¬(∀z)Q(z)$, i.e. $¬(∃x) P(x) ∧ (∃z)¬Q(z)$.
The first one implies the second : if we have that $(∃z)¬Q(z)$ holds, then it is false that $(∀y)Q(y)$ and thus also $(∃x)P(x)$ is false.
Thus : $¬(∃x) P(x)$ holds.
The second one implies the first : if $¬(∃x) P(x)$ holds, then $(∃x)P(x) to R$ holds, for $R$ whatever.
Thus : $(∃x)P(x) to (∀y)Q(y)$ holds.
$endgroup$
$begingroup$
One question: You say we have to work with prenex normal form but your first step switches to a non-prenex normal form if I'm not wrong?
$endgroup$
– Ayoub Rossi
Jan 30 at 17:04
$begingroup$
Second question: If I recognize a prenex normal form, should I always switch to an equivalent in non-prenex form
$endgroup$
– Ayoub Rossi
Jan 30 at 17:06
add a comment |
$begingroup$
Hint
We have to work with Prenex normal form equivalences.
The first formula is equivalent to :
$((∃x)P(x) to (∀y)Q(y)) ∧ (∃z)¬Q(z)$.
By De Morgan, the second formula is :
$¬(∃x) P(x) ∧ ¬(∀z)Q(z)$, i.e. $¬(∃x) P(x) ∧ (∃z)¬Q(z)$.
The first one implies the second : if we have that $(∃z)¬Q(z)$ holds, then it is false that $(∀y)Q(y)$ and thus also $(∃x)P(x)$ is false.
Thus : $¬(∃x) P(x)$ holds.
The second one implies the first : if $¬(∃x) P(x)$ holds, then $(∃x)P(x) to R$ holds, for $R$ whatever.
Thus : $(∃x)P(x) to (∀y)Q(y)$ holds.
$endgroup$
Hint
We have to work with Prenex normal form equivalences.
The first formula is equivalent to :
$((∃x)P(x) to (∀y)Q(y)) ∧ (∃z)¬Q(z)$.
By De Morgan, the second formula is :
$¬(∃x) P(x) ∧ ¬(∀z)Q(z)$, i.e. $¬(∃x) P(x) ∧ (∃z)¬Q(z)$.
The first one implies the second : if we have that $(∃z)¬Q(z)$ holds, then it is false that $(∀y)Q(y)$ and thus also $(∃x)P(x)$ is false.
Thus : $¬(∃x) P(x)$ holds.
The second one implies the first : if $¬(∃x) P(x)$ holds, then $(∃x)P(x) to R$ holds, for $R$ whatever.
Thus : $(∃x)P(x) to (∀y)Q(y)$ holds.
answered Jan 30 at 16:34
Mauro ALLEGRANZAMauro ALLEGRANZA
67.7k449117
67.7k449117
$begingroup$
One question: You say we have to work with prenex normal form but your first step switches to a non-prenex normal form if I'm not wrong?
$endgroup$
– Ayoub Rossi
Jan 30 at 17:04
$begingroup$
Second question: If I recognize a prenex normal form, should I always switch to an equivalent in non-prenex form
$endgroup$
– Ayoub Rossi
Jan 30 at 17:06
add a comment |
$begingroup$
One question: You say we have to work with prenex normal form but your first step switches to a non-prenex normal form if I'm not wrong?
$endgroup$
– Ayoub Rossi
Jan 30 at 17:04
$begingroup$
Second question: If I recognize a prenex normal form, should I always switch to an equivalent in non-prenex form
$endgroup$
– Ayoub Rossi
Jan 30 at 17:06
$begingroup$
One question: You say we have to work with prenex normal form but your first step switches to a non-prenex normal form if I'm not wrong?
$endgroup$
– Ayoub Rossi
Jan 30 at 17:04
$begingroup$
One question: You say we have to work with prenex normal form but your first step switches to a non-prenex normal form if I'm not wrong?
$endgroup$
– Ayoub Rossi
Jan 30 at 17:04
$begingroup$
Second question: If I recognize a prenex normal form, should I always switch to an equivalent in non-prenex form
$endgroup$
– Ayoub Rossi
Jan 30 at 17:06
$begingroup$
Second question: If I recognize a prenex normal form, should I always switch to an equivalent in non-prenex form
$endgroup$
– Ayoub Rossi
Jan 30 at 17:06
add a comment |
$begingroup$
$ forall x forall y exists z((P(x)rightarrow Q(y)) land neg Q(z)) overset{Prenex}{Leftrightarrow}$
$ forall x forall y ((P(x)rightarrow Q(y)) land exists z neg Q(z)) overset{Implication}{Leftrightarrow}$
$ forall x forall y ((neg P(x) lor Q(y)) land exists z neg Q(z))) overset{Distribution}{Leftrightarrow}$
$ forall x forall y ((neg P(x) land exists z neg Q(z)) lor ((Q(y) land exists z neg Q(z)) overset{Prenex x 2}{Leftrightarrow}$
$ forall x (neg P(x) land exists z neg Q(z)) lor forall y (Q(y) land exists z neg Q(z)) overset{Prenex x 2}{Leftrightarrow}$
$ ( forall x neg P(x) land exists z neg Q(z)) lor (forall y Q(y) land exists z neg Q(z)) overset{Quantifier Negation}{Leftrightarrow}$
$ (neg exists x P(x) land neg forall z Q(z)) lor (forall y Q(y) land neg forall z Q(z)) overset{Replacing Variables}{Leftrightarrow}$
$ (neg exists x P(x) land neg forall z Q(z)) lor (forall y Q(y) land neg forall y Q(y)) overset{Complement}{Leftrightarrow}$
$ (neg exists x P(x) land neg forall z Q(z)) lor bot overset{Identity}{Leftrightarrow}$
$ neg exists x P(x) land neg forall z Q(z)overset{DeMorgan}{Leftrightarrow}$
$ neg( exists x P(x) lor neg forall z Q(z))$
$endgroup$
add a comment |
$begingroup$
$ forall x forall y exists z((P(x)rightarrow Q(y)) land neg Q(z)) overset{Prenex}{Leftrightarrow}$
$ forall x forall y ((P(x)rightarrow Q(y)) land exists z neg Q(z)) overset{Implication}{Leftrightarrow}$
$ forall x forall y ((neg P(x) lor Q(y)) land exists z neg Q(z))) overset{Distribution}{Leftrightarrow}$
$ forall x forall y ((neg P(x) land exists z neg Q(z)) lor ((Q(y) land exists z neg Q(z)) overset{Prenex x 2}{Leftrightarrow}$
$ forall x (neg P(x) land exists z neg Q(z)) lor forall y (Q(y) land exists z neg Q(z)) overset{Prenex x 2}{Leftrightarrow}$
$ ( forall x neg P(x) land exists z neg Q(z)) lor (forall y Q(y) land exists z neg Q(z)) overset{Quantifier Negation}{Leftrightarrow}$
$ (neg exists x P(x) land neg forall z Q(z)) lor (forall y Q(y) land neg forall z Q(z)) overset{Replacing Variables}{Leftrightarrow}$
$ (neg exists x P(x) land neg forall z Q(z)) lor (forall y Q(y) land neg forall y Q(y)) overset{Complement}{Leftrightarrow}$
$ (neg exists x P(x) land neg forall z Q(z)) lor bot overset{Identity}{Leftrightarrow}$
$ neg exists x P(x) land neg forall z Q(z)overset{DeMorgan}{Leftrightarrow}$
$ neg( exists x P(x) lor neg forall z Q(z))$
$endgroup$
add a comment |
$begingroup$
$ forall x forall y exists z((P(x)rightarrow Q(y)) land neg Q(z)) overset{Prenex}{Leftrightarrow}$
$ forall x forall y ((P(x)rightarrow Q(y)) land exists z neg Q(z)) overset{Implication}{Leftrightarrow}$
$ forall x forall y ((neg P(x) lor Q(y)) land exists z neg Q(z))) overset{Distribution}{Leftrightarrow}$
$ forall x forall y ((neg P(x) land exists z neg Q(z)) lor ((Q(y) land exists z neg Q(z)) overset{Prenex x 2}{Leftrightarrow}$
$ forall x (neg P(x) land exists z neg Q(z)) lor forall y (Q(y) land exists z neg Q(z)) overset{Prenex x 2}{Leftrightarrow}$
$ ( forall x neg P(x) land exists z neg Q(z)) lor (forall y Q(y) land exists z neg Q(z)) overset{Quantifier Negation}{Leftrightarrow}$
$ (neg exists x P(x) land neg forall z Q(z)) lor (forall y Q(y) land neg forall z Q(z)) overset{Replacing Variables}{Leftrightarrow}$
$ (neg exists x P(x) land neg forall z Q(z)) lor (forall y Q(y) land neg forall y Q(y)) overset{Complement}{Leftrightarrow}$
$ (neg exists x P(x) land neg forall z Q(z)) lor bot overset{Identity}{Leftrightarrow}$
$ neg exists x P(x) land neg forall z Q(z)overset{DeMorgan}{Leftrightarrow}$
$ neg( exists x P(x) lor neg forall z Q(z))$
$endgroup$
$ forall x forall y exists z((P(x)rightarrow Q(y)) land neg Q(z)) overset{Prenex}{Leftrightarrow}$
$ forall x forall y ((P(x)rightarrow Q(y)) land exists z neg Q(z)) overset{Implication}{Leftrightarrow}$
$ forall x forall y ((neg P(x) lor Q(y)) land exists z neg Q(z))) overset{Distribution}{Leftrightarrow}$
$ forall x forall y ((neg P(x) land exists z neg Q(z)) lor ((Q(y) land exists z neg Q(z)) overset{Prenex x 2}{Leftrightarrow}$
$ forall x (neg P(x) land exists z neg Q(z)) lor forall y (Q(y) land exists z neg Q(z)) overset{Prenex x 2}{Leftrightarrow}$
$ ( forall x neg P(x) land exists z neg Q(z)) lor (forall y Q(y) land exists z neg Q(z)) overset{Quantifier Negation}{Leftrightarrow}$
$ (neg exists x P(x) land neg forall z Q(z)) lor (forall y Q(y) land neg forall z Q(z)) overset{Replacing Variables}{Leftrightarrow}$
$ (neg exists x P(x) land neg forall z Q(z)) lor (forall y Q(y) land neg forall y Q(y)) overset{Complement}{Leftrightarrow}$
$ (neg exists x P(x) land neg forall z Q(z)) lor bot overset{Identity}{Leftrightarrow}$
$ neg exists x P(x) land neg forall z Q(z)overset{DeMorgan}{Leftrightarrow}$
$ neg( exists x P(x) lor neg forall z Q(z))$
edited Jan 31 at 0:37
answered Jan 30 at 22:39
Bram28Bram28
64.2k44793
64.2k44793
add a comment |
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.
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%2f3093536%2fhow-to-prove-this-logical-equivalence-in-predicate-logic%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
$begingroup$
Is there an $y$ missing in the first formula ?
$endgroup$
– Mauro ALLEGRANZA
Jan 30 at 13:51
$begingroup$
Indeed, thanks!
$endgroup$
– Ayoub Rossi
Jan 30 at 13:54
$begingroup$
Well in the case that $Q(y)$ for all $y$, then it is true for any specific choice of $y$, namely $z$. Hence we can replace $forall y(P(x) rightarrow Q(y))$ with $ (P(x) rightarrow Q(z)) $
$endgroup$
– NazimJ
Jan 30 at 14:37