$Parightarrow exists y Qy vdash exists y (Parightarrow Qy)$ using natural deduction
$begingroup$
$Parightarrow exists y Qy vdash exists y (Parightarrow Qy)$
My friend asked me to prove this using natural deduction. He knows I studied logic but I know little about natural deduction since I studied logic only by hilbert style.
Using inference rules he presented I thought a lot, but couldn't find any proof easier than these two. First, introduce $Parightarrow exists y Qy$ as a premise.
1-1. Assume $negexists y(Parightarrow Qy)$ and derive $forall yneg(Parightarrow Qy)$
1-2. Derive $neg(Parightarrow Qb)$ and find subproof of $(Pawedge neg Qb)$
1-3. Derive $forall yneg Qy$ from $neg Qb$ and $exists y Qy$ from $Pa$
1-4. Derive $negexists yQy$ from $forall y neg Qy$ and conclude there's a contradiction
Here's another.
2-1. Drive $neg Pa veeexists yQy$
2-2. Derive $Parightarrow Qb$ each from $neg Pa$ and $exists y Qy$ and conclude $exists y(Parightarrow Qy)$
Since I haven't tried this in a full content, I don't know how long proof will be but I guess it will be.. I think there should be easier proof than these but I don't know how to find it.
logic predicate-logic natural-deduction
edited Dec 9 '18 at 11:31
Mauro ALLEGRANZA
65.9k449114
asked Dec 8 '18 at 16:29
fbgfbg
423211
$endgroup$
add a comment |
$begingroup$
$Parightarrow exists y Qy vdash exists y (Parightarrow Qy)$
My friend asked me to prove this using natural deduction. He knows I studied logic but I know little about natural deduction since I studied logic only by hilbert style.
Using inference rules he presented I thought a lot, but couldn't find any proof easier than these two. First, introduce $Parightarrow exists y Qy$ as a premise.
1-1. Assume $negexists y(Parightarrow Qy)$ and derive $forall yneg(Parightarrow Qy)$
1-2. Derive $neg(Parightarrow Qb)$ and find subproof of $(Pawedge neg Qb)$
1-3. Derive $forall yneg Qy$ from $neg Qb$ and $exists y Qy$ from $Pa$
1-4. Derive $negexists yQy$ from $forall y neg Qy$ and conclude there's a contradiction
Here's another.
2-1. Drive $neg Pa veeexists yQy$
2-2. Derive $Parightarrow Qb$ each from $neg Pa$ and $exists y Qy$ and conclude $exists y(Parightarrow Qy)$
Since I haven't tried this in a full content, I don't know how long proof will be but I guess it will be.. I think there should be easier proof than these but I don't know how to find it.
logic predicate-logic natural-deduction
edited Dec 9 '18 at 11:31
Mauro ALLEGRANZA
65.9k449114
asked Dec 8 '18 at 16:29
fbgfbg
423211
$endgroup$
2
$begingroup$
It might be worth noting that any proof will necessarily involve something like excluded middle or double negation elimination - the statement is not valid in intuitionistic first-order logic.
$endgroup$
– Daniel Schepler
Dec 9 '18 at 0:28
add a comment |
$begingroup$
$Parightarrow exists y Qy vdash exists y (Parightarrow Qy)$
My friend asked me to prove this using natural deduction. He knows I studied logic but I know little about natural deduction since I studied logic only by hilbert style.
Using inference rules he presented I thought a lot, but couldn't find any proof easier than these two. First, introduce $Parightarrow exists y Qy$ as a premise.
1-1. Assume $negexists y(Parightarrow Qy)$ and derive $forall yneg(Parightarrow Qy)$
1-2. Derive $neg(Parightarrow Qb)$ and find subproof of $(Pawedge neg Qb)$
1-3. Derive $forall yneg Qy$ from $neg Qb$ and $exists y Qy$ from $Pa$
1-4. Derive $negexists yQy$ from $forall y neg Qy$ and conclude there's a contradiction
Here's another.
2-1. Drive $neg Pa veeexists yQy$
2-2. Derive $Parightarrow Qb$ each from $neg Pa$ and $exists y Qy$ and conclude $exists y(Parightarrow Qy)$
Since I haven't tried this in a full content, I don't know how long proof will be but I guess it will be.. I think there should be easier proof than these but I don't know how to find it.
logic predicate-logic natural-deduction
edited Dec 9 '18 at 11:31
Mauro ALLEGRANZA
65.9k449114
asked Dec 8 '18 at 16:29
fbgfbg
423211
$endgroup$
$Parightarrow exists y Qy vdash exists y (Parightarrow Qy)$
My friend asked me to prove this using natural deduction. He knows I studied logic but I know little about natural deduction since I studied logic only by hilbert style.
Using inference rules he presented I thought a lot, but couldn't find any proof easier than these two. First, introduce $Parightarrow exists y Qy$ as a premise.
1-1. Assume $negexists y(Parightarrow Qy)$ and derive $forall yneg(Parightarrow Qy)$
1-2. Derive $neg(Parightarrow Qb)$ and find subproof of $(Pawedge neg Qb)$
1-3. Derive $forall yneg Qy$ from $neg Qb$ and $exists y Qy$ from $Pa$
1-4. Derive $negexists yQy$ from $forall y neg Qy$ and conclude there's a contradiction
Here's another.
2-1. Drive $neg Pa veeexists yQy$
2-2. Derive $Parightarrow Qb$ each from $neg Pa$ and $exists y Qy$ and conclude $exists y(Parightarrow Qy)$
Since I haven't tried this in a full content, I don't know how long proof will be but I guess it will be.. I think there should be easier proof than these but I don't know how to find it.
logic predicate-logic natural-deduction
logic predicate-logic natural-deduction
edited Dec 9 '18 at 11:31
Mauro ALLEGRANZA
65.9k449114
asked Dec 8 '18 at 16:29
fbgfbg
423211
edited Dec 9 '18 at 11:31
Mauro ALLEGRANZA
65.9k449114
asked Dec 8 '18 at 16:29
fbgfbg
423211
edited Dec 9 '18 at 11:31
Mauro ALLEGRANZA
65.9k449114
edited Dec 9 '18 at 11:31
Mauro ALLEGRANZA
65.9k449114
edited Dec 9 '18 at 11:31
Mauro ALLEGRANZA
65.9k449114
65.9k449114
asked Dec 8 '18 at 16:29
fbgfbg
423211
asked Dec 8 '18 at 16:29
fbgfbg
423211
asked Dec 8 '18 at 16:29
fbgfbg
423211
423211
2
$begingroup$
It might be worth noting that any proof will necessarily involve something like excluded middle or double negation elimination - the statement is not valid in intuitionistic first-order logic.
$endgroup$
– Daniel Schepler
Dec 9 '18 at 0:28
add a comment |
2
$begingroup$
It might be worth noting that any proof will necessarily involve something like excluded middle or double negation elimination - the statement is not valid in intuitionistic first-order logic.
$endgroup$
– Daniel Schepler
Dec 9 '18 at 0:28
2
2
$begingroup$
It might be worth noting that any proof will necessarily involve something like excluded middle or double negation elimination - the statement is not valid in intuitionistic first-order logic.
$endgroup$
– Daniel Schepler
Dec 9 '18 at 0:28
$begingroup$
It might be worth noting that any proof will necessarily involve something like excluded middle or double negation elimination - the statement is not valid in intuitionistic first-order logic.
$endgroup$
– Daniel Schepler
Dec 9 '18 at 0:28
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
The first proof works, also if you need a lot of sub-proof to "play with" the propositional and quantifiers equivalences.
A more straightforward proof will be :
1) $Pa → ∃yQy$ --- premise
2) $lnot Pa lor Pa$ --- Excluded Middle
3) $lnot Pa$ --- first sub-proof from 2) by $lor$-elim
4) $Pa$ --- assumed [a]
5) $bot$
6) $Qb$ --- from 5)
7) $Pa to Qb$ --- by $→$-intro, discharging [a]
8) $∃y(Pa to Qy)$ --- by $∃$-intro, closing 1st sub-proof
9) $Pa$ --- second sub-proof from 2) by $lor$-elim
10) $∃yQy$ --- from 1) and 9) by $→$-elim
11) $Qb$ --- assumed from 10) for $∃$-elim
12) $Pa$ --- reiteration of 9)
13) $Pa to Qb$ --- by $→$-intro, discharging 12)
14) $∃y(Pa to Qy)$ --- by $∃$-intro, closing the $∃$-elim sub-proof and closing 2nd sub-proof
15) $∃y(Pa → Qy)$ --- from 3)-8) and 9)-14) and 2) by $lor$-elim.
answered Dec 8 '18 at 16:42
Mauro ALLEGRANZAMauro ALLEGRANZA
65.9k449114
$endgroup$
1
$begingroup$
I also thought about this before. what I was worried about is second assumption [b] exists after assuming [a]. So I thought that [b] should handled first and then [a]. I couldn't find such a way so I give up this method before
$endgroup$
– fbg
Dec 8 '18 at 17:21
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%2f3031314%2fpa-rightarrow-exists-y-qy-vdash-exists-y-pa-rightarrow-qy-using-natural-d%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
The first proof works, also if you need a lot of sub-proof to "play with" the propositional and quantifiers equivalences.
A more straightforward proof will be :
1) $Pa → ∃yQy$ --- premise
2) $lnot Pa lor Pa$ --- Excluded Middle
3) $lnot Pa$ --- first sub-proof from 2) by $lor$-elim
4) $Pa$ --- assumed [a]
5) $bot$
6) $Qb$ --- from 5)
7) $Pa to Qb$ --- by $→$-intro, discharging [a]
8) $∃y(Pa to Qy)$ --- by $∃$-intro, closing 1st sub-proof
9) $Pa$ --- second sub-proof from 2) by $lor$-elim
10) $∃yQy$ --- from 1) and 9) by $→$-elim
11) $Qb$ --- assumed from 10) for $∃$-elim
12) $Pa$ --- reiteration of 9)
13) $Pa to Qb$ --- by $→$-intro, discharging 12)
14) $∃y(Pa to Qy)$ --- by $∃$-intro, closing the $∃$-elim sub-proof and closing 2nd sub-proof
15) $∃y(Pa → Qy)$ --- from 3)-8) and 9)-14) and 2) by $lor$-elim.
answered Dec 8 '18 at 16:42
Mauro ALLEGRANZAMauro ALLEGRANZA
65.9k449114
$endgroup$
1
$begingroup$
I also thought about this before. what I was worried about is second assumption [b] exists after assuming [a]. So I thought that [b] should handled first and then [a]. I couldn't find such a way so I give up this method before
$endgroup$
– fbg
Dec 8 '18 at 17:21
add a comment |
$begingroup$
The first proof works, also if you need a lot of sub-proof to "play with" the propositional and quantifiers equivalences.
A more straightforward proof will be :
1) $Pa → ∃yQy$ --- premise
2) $lnot Pa lor Pa$ --- Excluded Middle
3) $lnot Pa$ --- first sub-proof from 2) by $lor$-elim
4) $Pa$ --- assumed [a]
5) $bot$
6) $Qb$ --- from 5)
7) $Pa to Qb$ --- by $→$-intro, discharging [a]
8) $∃y(Pa to Qy)$ --- by $∃$-intro, closing 1st sub-proof
9) $Pa$ --- second sub-proof from 2) by $lor$-elim
10) $∃yQy$ --- from 1) and 9) by $→$-elim
11) $Qb$ --- assumed from 10) for $∃$-elim
12) $Pa$ --- reiteration of 9)
13) $Pa to Qb$ --- by $→$-intro, discharging 12)
14) $∃y(Pa to Qy)$ --- by $∃$-intro, closing the $∃$-elim sub-proof and closing 2nd sub-proof
15) $∃y(Pa → Qy)$ --- from 3)-8) and 9)-14) and 2) by $lor$-elim.
answered Dec 8 '18 at 16:42
Mauro ALLEGRANZAMauro ALLEGRANZA
65.9k449114
$endgroup$
1
$begingroup$
I also thought about this before. what I was worried about is second assumption [b] exists after assuming [a]. So I thought that [b] should handled first and then [a]. I couldn't find such a way so I give up this method before
$endgroup$
– fbg
Dec 8 '18 at 17:21
add a comment |
$begingroup$
The first proof works, also if you need a lot of sub-proof to "play with" the propositional and quantifiers equivalences.
A more straightforward proof will be :
1) $Pa → ∃yQy$ --- premise
2) $lnot Pa lor Pa$ --- Excluded Middle
3) $lnot Pa$ --- first sub-proof from 2) by $lor$-elim
4) $Pa$ --- assumed [a]
5) $bot$
6) $Qb$ --- from 5)
7) $Pa to Qb$ --- by $→$-intro, discharging [a]
8) $∃y(Pa to Qy)$ --- by $∃$-intro, closing 1st sub-proof
9) $Pa$ --- second sub-proof from 2) by $lor$-elim
10) $∃yQy$ --- from 1) and 9) by $→$-elim
11) $Qb$ --- assumed from 10) for $∃$-elim
12) $Pa$ --- reiteration of 9)
13) $Pa to Qb$ --- by $→$-intro, discharging 12)
14) $∃y(Pa to Qy)$ --- by $∃$-intro, closing the $∃$-elim sub-proof and closing 2nd sub-proof
15) $∃y(Pa → Qy)$ --- from 3)-8) and 9)-14) and 2) by $lor$-elim.
answered Dec 8 '18 at 16:42
Mauro ALLEGRANZAMauro ALLEGRANZA
65.9k449114
$endgroup$
The first proof works, also if you need a lot of sub-proof to "play with" the propositional and quantifiers equivalences.
A more straightforward proof will be :
1) $Pa → ∃yQy$ --- premise
2) $lnot Pa lor Pa$ --- Excluded Middle
3) $lnot Pa$ --- first sub-proof from 2) by $lor$-elim
4) $Pa$ --- assumed [a]
5) $bot$
6) $Qb$ --- from 5)
7) $Pa to Qb$ --- by $→$-intro, discharging [a]
8) $∃y(Pa to Qy)$ --- by $∃$-intro, closing 1st sub-proof
9) $Pa$ --- second sub-proof from 2) by $lor$-elim
10) $∃yQy$ --- from 1) and 9) by $→$-elim
11) $Qb$ --- assumed from 10) for $∃$-elim
12) $Pa$ --- reiteration of 9)
13) $Pa to Qb$ --- by $→$-intro, discharging 12)
14) $∃y(Pa to Qy)$ --- by $∃$-intro, closing the $∃$-elim sub-proof and closing 2nd sub-proof
15) $∃y(Pa → Qy)$ --- from 3)-8) and 9)-14) and 2) by $lor$-elim.
answered Dec 8 '18 at 16:42
Mauro ALLEGRANZAMauro ALLEGRANZA
65.9k449114
edited Dec 8 '18 at 19:14
answered Dec 8 '18 at 16:42
Mauro ALLEGRANZAMauro ALLEGRANZA
65.9k449114
answered Dec 8 '18 at 16:42
Mauro ALLEGRANZAMauro ALLEGRANZA
65.9k449114
answered Dec 8 '18 at 16:42
Mauro ALLEGRANZAMauro ALLEGRANZA
65.9k449114
65.9k449114
1
$begingroup$
I also thought about this before. what I was worried about is second assumption [b] exists after assuming [a]. So I thought that [b] should handled first and then [a]. I couldn't find such a way so I give up this method before
$endgroup$
– fbg
Dec 8 '18 at 17:21
add a comment |
1
$begingroup$
I also thought about this before. what I was worried about is second assumption [b] exists after assuming [a]. So I thought that [b] should handled first and then [a]. I couldn't find such a way so I give up this method before
$endgroup$
– fbg
Dec 8 '18 at 17:21
1
1
$begingroup$
I also thought about this before. what I was worried about is second assumption [b] exists after assuming [a]. So I thought that [b] should handled first and then [a]. I couldn't find such a way so I give up this method before
$endgroup$
– fbg
Dec 8 '18 at 17:21
$begingroup$
I also thought about this before. what I was worried about is second assumption [b] exists after assuming [a]. So I thought that [b] should handled first and then [a]. I couldn't find such a way so I give up this method before
$endgroup$
– fbg
Dec 8 '18 at 17:21
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%2f3031314%2fpa-rightarrow-exists-y-qy-vdash-exists-y-pa-rightarrow-qy-using-natural-d%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
2
$begingroup$
It might be worth noting that any proof will necessarily involve something like excluded middle or double negation elimination - the statement is not valid in intuitionistic first-order logic.
$endgroup$
– Daniel Schepler
Dec 9 '18 at 0:28