formal proof of $(p → q) → (¬q → ¬p)$
$begingroup$
I'm asked to give a formal proof of $(p → q) → (¬q → ¬p)$ using natural deduction. Is that like saying prove $⊢ (p → q) → (¬q → ¬p$), where it should be proved from nothing?
natural-deduction
edited Dec 29 '18 at 14:05
Key Flex
8,56171233
asked Dec 29 '18 at 13:12
Richard CameronRichard Cameron
121
$endgroup$
add a comment |
$begingroup$
I'm asked to give a formal proof of $(p → q) → (¬q → ¬p)$ using natural deduction. Is that like saying prove $⊢ (p → q) → (¬q → ¬p$), where it should be proved from nothing?
natural-deduction
edited Dec 29 '18 at 14:05
Key Flex
8,56171233
asked Dec 29 '18 at 13:12
Richard CameronRichard Cameron
121
$endgroup$
1
$begingroup$
Exactly; you have to start assuming one or more premises that you will discharge later.
$endgroup$
– Mauro ALLEGRANZA
Dec 29 '18 at 13:13
1
$begingroup$
Please use MathJax in future.
$endgroup$
– Shaun
Dec 29 '18 at 13:18
$begingroup$
Assume $q$ follows from $p$. Further assume not $q$. What can you say about $p$? By the way, this is called the contrapositive.
$endgroup$
– David Diaz
Dec 29 '18 at 14:11
$begingroup$
Not a duplicate, but the only answer to this question solves 95% of this problem.
$endgroup$
– Git Gud
Dec 29 '18 at 14:23
$begingroup$
What rules do you have to work with? There are many different systems of 'natural deduction', each with their own set of rules.
$endgroup$
– Bram28
Dec 29 '18 at 18:13
add a comment |
$begingroup$
I'm asked to give a formal proof of $(p → q) → (¬q → ¬p)$ using natural deduction. Is that like saying prove $⊢ (p → q) → (¬q → ¬p$), where it should be proved from nothing?
natural-deduction
edited Dec 29 '18 at 14:05
Key Flex
8,56171233
asked Dec 29 '18 at 13:12
Richard CameronRichard Cameron
121
$endgroup$
I'm asked to give a formal proof of $(p → q) → (¬q → ¬p)$ using natural deduction. Is that like saying prove $⊢ (p → q) → (¬q → ¬p$), where it should be proved from nothing?
natural-deduction
natural-deduction
edited Dec 29 '18 at 14:05
Key Flex
8,56171233
asked Dec 29 '18 at 13:12
Richard CameronRichard Cameron
121
edited Dec 29 '18 at 14:05
Key Flex
8,56171233
asked Dec 29 '18 at 13:12
Richard CameronRichard Cameron
121
edited Dec 29 '18 at 14:05
Key Flex
8,56171233
edited Dec 29 '18 at 14:05
Key Flex
8,56171233
edited Dec 29 '18 at 14:05
Key Flex
8,56171233
8,56171233
asked Dec 29 '18 at 13:12
Richard CameronRichard Cameron
121
asked Dec 29 '18 at 13:12
Richard CameronRichard Cameron
121
asked Dec 29 '18 at 13:12
Richard CameronRichard Cameron
121
121
1
$begingroup$
Exactly; you have to start assuming one or more premises that you will discharge later.
$endgroup$
– Mauro ALLEGRANZA
Dec 29 '18 at 13:13
1
$begingroup$
Please use MathJax in future.
$endgroup$
– Shaun
Dec 29 '18 at 13:18
$begingroup$
Assume $q$ follows from $p$. Further assume not $q$. What can you say about $p$? By the way, this is called the contrapositive.
$endgroup$
– David Diaz
Dec 29 '18 at 14:11
$begingroup$
Not a duplicate, but the only answer to this question solves 95% of this problem.
$endgroup$
– Git Gud
Dec 29 '18 at 14:23
$begingroup$
What rules do you have to work with? There are many different systems of 'natural deduction', each with their own set of rules.
$endgroup$
– Bram28
Dec 29 '18 at 18:13
add a comment |
1
$begingroup$
Exactly; you have to start assuming one or more premises that you will discharge later.
$endgroup$
– Mauro ALLEGRANZA
Dec 29 '18 at 13:13
1
$begingroup$
Please use MathJax in future.
$endgroup$
– Shaun
Dec 29 '18 at 13:18
$begingroup$
Assume $q$ follows from $p$. Further assume not $q$. What can you say about $p$? By the way, this is called the contrapositive.
$endgroup$
– David Diaz
Dec 29 '18 at 14:11
$begingroup$
Not a duplicate, but the only answer to this question solves 95% of this problem.
$endgroup$
– Git Gud
Dec 29 '18 at 14:23
$begingroup$
What rules do you have to work with? There are many different systems of 'natural deduction', each with their own set of rules.
$endgroup$
– Bram28
Dec 29 '18 at 18:13
1
1
$begingroup$
Exactly; you have to start assuming one or more premises that you will discharge later.
$endgroup$
– Mauro ALLEGRANZA
Dec 29 '18 at 13:13
$begingroup$
Exactly; you have to start assuming one or more premises that you will discharge later.
$endgroup$
– Mauro ALLEGRANZA
Dec 29 '18 at 13:13
1
1
$begingroup$
Please use MathJax in future.
$endgroup$
– Shaun
Dec 29 '18 at 13:18
$begingroup$
Please use MathJax in future.
$endgroup$
– Shaun
Dec 29 '18 at 13:18
$begingroup$
Assume $q$ follows from $p$. Further assume not $q$. What can you say about $p$? By the way, this is called the contrapositive.
$endgroup$
– David Diaz
Dec 29 '18 at 14:11
$begingroup$
Assume $q$ follows from $p$. Further assume not $q$. What can you say about $p$? By the way, this is called the contrapositive.
$endgroup$
– David Diaz
Dec 29 '18 at 14:11
$begingroup$
Not a duplicate, but the only answer to this question solves 95% of this problem.
$endgroup$
– Git Gud
Dec 29 '18 at 14:23
$begingroup$
Not a duplicate, but the only answer to this question solves 95% of this problem.
$endgroup$
– Git Gud
Dec 29 '18 at 14:23
$begingroup$
What rules do you have to work with? There are many different systems of 'natural deduction', each with their own set of rules.
$endgroup$
– Bram28
Dec 29 '18 at 18:13
$begingroup$
What rules do you have to work with? There are many different systems of 'natural deduction', each with their own set of rules.
$endgroup$
– Bram28
Dec 29 '18 at 18:13
add a comment |
2 Answers
2
active
oldest
votes
$begingroup$
Hint: the following statements are all equivalent:
- $pto q$
- $neg plor q$
- $negneg qlorneg p$
- $neg qtoneg p$
answered Dec 29 '18 at 13:33
J.G.J.G.
33.5k23252
$endgroup$
1
$begingroup$
The formal proof that comes naturally to me uses none of this. How is this helpful?
$endgroup$
– Git Gud
Dec 29 '18 at 14:20
$begingroup$
@GitGud If you have a different route, well done. But to any future reader considering this problem who doesn't, the use comes in providing a sequence of statements worth proving equivalent. How you stitch them together into a proof depends on your preferred notation.
$endgroup$
– J.G.
Dec 29 '18 at 15:59
$begingroup$
I didn't say what I should have said. How do you go from this to a formal proof? As I see it, you need to go to the moon and back, I don't see how this can be helpful.
$endgroup$
– Git Gud
Dec 29 '18 at 16:09
add a comment |
$begingroup$
The following proof uses modus tollens (MT):
However, one can derive the modus tollens rule in the following way. This uses the proof provided on page 138 of forallx linked to below along with a link to the proof checker used here:
Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/
answered Jan 21 at 0:43
Frank HubenyFrank Hubeny
5312519
$endgroup$
add a comment |
Your Answer
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%2f3055835%2fformal-proof-of-p-%25e2%2586%2592-q-%25e2%2586%2592-%25c2%25acq-%25e2%2586%2592-%25c2%25acp%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: the following statements are all equivalent:
- $pto q$
- $neg plor q$
- $negneg qlorneg p$
- $neg qtoneg p$
answered Dec 29 '18 at 13:33
J.G.J.G.
33.5k23252
$endgroup$
1
$begingroup$
The formal proof that comes naturally to me uses none of this. How is this helpful?
$endgroup$
– Git Gud
Dec 29 '18 at 14:20
$begingroup$
@GitGud If you have a different route, well done. But to any future reader considering this problem who doesn't, the use comes in providing a sequence of statements worth proving equivalent. How you stitch them together into a proof depends on your preferred notation.
$endgroup$
– J.G.
Dec 29 '18 at 15:59
$begingroup$
I didn't say what I should have said. How do you go from this to a formal proof? As I see it, you need to go to the moon and back, I don't see how this can be helpful.
$endgroup$
– Git Gud
Dec 29 '18 at 16:09
add a comment |
$begingroup$
Hint: the following statements are all equivalent:
- $pto q$
- $neg plor q$
- $negneg qlorneg p$
- $neg qtoneg p$
answered Dec 29 '18 at 13:33
J.G.J.G.
33.5k23252
$endgroup$
1
$begingroup$
The formal proof that comes naturally to me uses none of this. How is this helpful?
$endgroup$
– Git Gud
Dec 29 '18 at 14:20
$begingroup$
@GitGud If you have a different route, well done. But to any future reader considering this problem who doesn't, the use comes in providing a sequence of statements worth proving equivalent. How you stitch them together into a proof depends on your preferred notation.
$endgroup$
– J.G.
Dec 29 '18 at 15:59
$begingroup$
I didn't say what I should have said. How do you go from this to a formal proof? As I see it, you need to go to the moon and back, I don't see how this can be helpful.
$endgroup$
– Git Gud
Dec 29 '18 at 16:09
add a comment |
$begingroup$
Hint: the following statements are all equivalent:
- $pto q$
- $neg plor q$
- $negneg qlorneg p$
- $neg qtoneg p$
answered Dec 29 '18 at 13:33
J.G.J.G.
33.5k23252
$endgroup$
Hint: the following statements are all equivalent:
- $pto q$
- $neg plor q$
- $negneg qlorneg p$
- $neg qtoneg p$
answered Dec 29 '18 at 13:33
J.G.J.G.
33.5k23252
answered Dec 29 '18 at 13:33
J.G.J.G.
33.5k23252
answered Dec 29 '18 at 13:33
J.G.J.G.
33.5k23252
answered Dec 29 '18 at 13:33
J.G.J.G.
33.5k23252
33.5k23252
1
$begingroup$
The formal proof that comes naturally to me uses none of this. How is this helpful?
$endgroup$
– Git Gud
Dec 29 '18 at 14:20
$begingroup$
@GitGud If you have a different route, well done. But to any future reader considering this problem who doesn't, the use comes in providing a sequence of statements worth proving equivalent. How you stitch them together into a proof depends on your preferred notation.
$endgroup$
– J.G.
Dec 29 '18 at 15:59
$begingroup$
I didn't say what I should have said. How do you go from this to a formal proof? As I see it, you need to go to the moon and back, I don't see how this can be helpful.
$endgroup$
– Git Gud
Dec 29 '18 at 16:09
add a comment |
1
$begingroup$
The formal proof that comes naturally to me uses none of this. How is this helpful?
$endgroup$
– Git Gud
Dec 29 '18 at 14:20
$begingroup$
@GitGud If you have a different route, well done. But to any future reader considering this problem who doesn't, the use comes in providing a sequence of statements worth proving equivalent. How you stitch them together into a proof depends on your preferred notation.
$endgroup$
– J.G.
Dec 29 '18 at 15:59
$begingroup$
I didn't say what I should have said. How do you go from this to a formal proof? As I see it, you need to go to the moon and back, I don't see how this can be helpful.
$endgroup$
– Git Gud
Dec 29 '18 at 16:09
1
1
$begingroup$
The formal proof that comes naturally to me uses none of this. How is this helpful?
$endgroup$
– Git Gud
Dec 29 '18 at 14:20
$begingroup$
The formal proof that comes naturally to me uses none of this. How is this helpful?
$endgroup$
– Git Gud
Dec 29 '18 at 14:20
$begingroup$
@GitGud If you have a different route, well done. But to any future reader considering this problem who doesn't, the use comes in providing a sequence of statements worth proving equivalent. How you stitch them together into a proof depends on your preferred notation.
$endgroup$
– J.G.
Dec 29 '18 at 15:59
$begingroup$
@GitGud If you have a different route, well done. But to any future reader considering this problem who doesn't, the use comes in providing a sequence of statements worth proving equivalent. How you stitch them together into a proof depends on your preferred notation.
$endgroup$
– J.G.
Dec 29 '18 at 15:59
$begingroup$
I didn't say what I should have said. How do you go from this to a formal proof? As I see it, you need to go to the moon and back, I don't see how this can be helpful.
$endgroup$
– Git Gud
Dec 29 '18 at 16:09
$begingroup$
I didn't say what I should have said. How do you go from this to a formal proof? As I see it, you need to go to the moon and back, I don't see how this can be helpful.
$endgroup$
– Git Gud
Dec 29 '18 at 16:09
add a comment |
$begingroup$
The following proof uses modus tollens (MT):
However, one can derive the modus tollens rule in the following way. This uses the proof provided on page 138 of forallx linked to below along with a link to the proof checker used here:
Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/
answered Jan 21 at 0:43
Frank HubenyFrank Hubeny
5312519
$endgroup$
add a comment |
$begingroup$
The following proof uses modus tollens (MT):
However, one can derive the modus tollens rule in the following way. This uses the proof provided on page 138 of forallx linked to below along with a link to the proof checker used here:
Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/
answered Jan 21 at 0:43
Frank HubenyFrank Hubeny
5312519
$endgroup$
add a comment |
$begingroup$
The following proof uses modus tollens (MT):
However, one can derive the modus tollens rule in the following way. This uses the proof provided on page 138 of forallx linked to below along with a link to the proof checker used here:
Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/
answered Jan 21 at 0:43
Frank HubenyFrank Hubeny
5312519
$endgroup$
The following proof uses modus tollens (MT):
However, one can derive the modus tollens rule in the following way. This uses the proof provided on page 138 of forallx linked to below along with a link to the proof checker used here:
Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/
answered Jan 21 at 0:43
Frank HubenyFrank Hubeny
5312519
answered Jan 21 at 0:43
Frank HubenyFrank Hubeny
5312519
answered Jan 21 at 0:43
Frank HubenyFrank Hubeny
5312519
answered Jan 21 at 0:43
Frank HubenyFrank Hubeny
5312519
5312519
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%2f3055835%2fformal-proof-of-p-%25e2%2586%2592-q-%25e2%2586%2592-%25c2%25acq-%25e2%2586%2592-%25c2%25acp%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
1
$begingroup$
Exactly; you have to start assuming one or more premises that you will discharge later.
$endgroup$
– Mauro ALLEGRANZA
Dec 29 '18 at 13:13
1
$begingroup$
Please use MathJax in future.
$endgroup$
– Shaun
Dec 29 '18 at 13:18
$begingroup$
Assume $q$ follows from $p$. Further assume not $q$. What can you say about $p$? By the way, this is called the contrapositive.
$endgroup$
– David Diaz
Dec 29 '18 at 14:11
$begingroup$
Not a duplicate, but the only answer to this question solves 95% of this problem.
$endgroup$
– Git Gud
Dec 29 '18 at 14:23
$begingroup$
What rules do you have to work with? There are many different systems of 'natural deduction', each with their own set of rules.
$endgroup$
– Bram28
Dec 29 '18 at 18:13