proof for relational predicate logic
Clash Royale CLAN TAG#URR8PPP
up vote
3
down vote
favorite
I have been working on this problem for over an hour and I think I have simply missed something. I need some help. The rules I am allowed to use are the Basic Inference rules (MP, MT, HS, Simp, Conj, DS, Add, CD), the Replacement Rules (DN, Comm, Assoc, Dup, DeM, BE, Contrap, CE, Exp, Dist.), CP, IP, and EI, UI, EG, UG.
The problem is:
- ¬(∃x)(Axa ∧ ~Bxb)
- ¬(∃x)(Cxc ∧ Cbx)
- (∀x)(Bex → Cxf)
/∴ ¬(Aea ∧ Cfc)
Any help would be appreciated. Thanks.
Edit: Fixed the format of the question. The system is quantificational predicate logic. I've never called it anything else.
logic symbolic-logic
edited Dec 4 at 1:31
Frank Hubeny
6,48751344
asked Dec 4 at 0:29
fantasticorangina
192
add a comment |
up vote
3
down vote
favorite
I have been working on this problem for over an hour and I think I have simply missed something. I need some help. The rules I am allowed to use are the Basic Inference rules (MP, MT, HS, Simp, Conj, DS, Add, CD), the Replacement Rules (DN, Comm, Assoc, Dup, DeM, BE, Contrap, CE, Exp, Dist.), CP, IP, and EI, UI, EG, UG.
The problem is:
- ¬(∃x)(Axa ∧ ~Bxb)
- ¬(∃x)(Cxc ∧ Cbx)
- (∀x)(Bex → Cxf)
/∴ ¬(Aea ∧ Cfc)
Any help would be appreciated. Thanks.
Edit: Fixed the format of the question. The system is quantificational predicate logic. I've never called it anything else.
logic symbolic-logic
edited Dec 4 at 1:31
Frank Hubeny
6,48751344
asked Dec 4 at 0:29
fantasticorangina
192
1
This formula is unreadable. Please reformat it with ∀, ∃ for quantifiers, ∨, ∧, →, ¬ for connectives (you can copy symbols from here), and predicates as P(x,y,z). What > and // are I can not even guess. "Basic Inference rules" and "Replacement Rules" are specific to your book and not standard terminology, so best provide a reference and what type of system it is using (natural deduction, sequent calculus, something else?).
– Conifold
Dec 4 at 0:46
1
I formatted the premises and conclusion to use Conifold's symbols. You may roll this back or continue editing if I got it wrong.
– Frank Hubeny
Dec 4 at 1:32
@fantasticorangina Have the answers been of any help ?
– Graham Kemp
Dec 5 at 0:45
@fantasticorangina Is that a no?
– Graham Kemp
Dec 6 at 23:22
add a comment |
up vote
3
down vote
favorite
up vote
3
down vote
favorite
I have been working on this problem for over an hour and I think I have simply missed something. I need some help. The rules I am allowed to use are the Basic Inference rules (MP, MT, HS, Simp, Conj, DS, Add, CD), the Replacement Rules (DN, Comm, Assoc, Dup, DeM, BE, Contrap, CE, Exp, Dist.), CP, IP, and EI, UI, EG, UG.
The problem is:
- ¬(∃x)(Axa ∧ ~Bxb)
- ¬(∃x)(Cxc ∧ Cbx)
- (∀x)(Bex → Cxf)
/∴ ¬(Aea ∧ Cfc)
Any help would be appreciated. Thanks.
Edit: Fixed the format of the question. The system is quantificational predicate logic. I've never called it anything else.
logic symbolic-logic
edited Dec 4 at 1:31
Frank Hubeny
6,48751344
asked Dec 4 at 0:29
fantasticorangina
192
I have been working on this problem for over an hour and I think I have simply missed something. I need some help. The rules I am allowed to use are the Basic Inference rules (MP, MT, HS, Simp, Conj, DS, Add, CD), the Replacement Rules (DN, Comm, Assoc, Dup, DeM, BE, Contrap, CE, Exp, Dist.), CP, IP, and EI, UI, EG, UG.
The problem is:
- ¬(∃x)(Axa ∧ ~Bxb)
- ¬(∃x)(Cxc ∧ Cbx)
- (∀x)(Bex → Cxf)
/∴ ¬(Aea ∧ Cfc)
Any help would be appreciated. Thanks.
Edit: Fixed the format of the question. The system is quantificational predicate logic. I've never called it anything else.
logic symbolic-logic
logic symbolic-logic
edited Dec 4 at 1:31
Frank Hubeny
6,48751344
asked Dec 4 at 0:29
fantasticorangina
192
edited Dec 4 at 1:31
Frank Hubeny
6,48751344
asked Dec 4 at 0:29
fantasticorangina
192
edited Dec 4 at 1:31
Frank Hubeny
6,48751344
edited Dec 4 at 1:31
Frank Hubeny
6,48751344
edited Dec 4 at 1:31
Frank Hubeny
6,48751344
6,48751344
asked Dec 4 at 0:29
fantasticorangina
192
asked Dec 4 at 0:29
fantasticorangina
192
asked Dec 4 at 0:29
fantasticorangina
192
192
1
This formula is unreadable. Please reformat it with ∀, ∃ for quantifiers, ∨, ∧, →, ¬ for connectives (you can copy symbols from here), and predicates as P(x,y,z). What > and // are I can not even guess. "Basic Inference rules" and "Replacement Rules" are specific to your book and not standard terminology, so best provide a reference and what type of system it is using (natural deduction, sequent calculus, something else?).
– Conifold
Dec 4 at 0:46
1
I formatted the premises and conclusion to use Conifold's symbols. You may roll this back or continue editing if I got it wrong.
– Frank Hubeny
Dec 4 at 1:32
@fantasticorangina Have the answers been of any help ?
– Graham Kemp
Dec 5 at 0:45
@fantasticorangina Is that a no?
– Graham Kemp
Dec 6 at 23:22
add a comment |
1
This formula is unreadable. Please reformat it with ∀, ∃ for quantifiers, ∨, ∧, →, ¬ for connectives (you can copy symbols from here), and predicates as P(x,y,z). What > and // are I can not even guess. "Basic Inference rules" and "Replacement Rules" are specific to your book and not standard terminology, so best provide a reference and what type of system it is using (natural deduction, sequent calculus, something else?).
– Conifold
Dec 4 at 0:46
1
I formatted the premises and conclusion to use Conifold's symbols. You may roll this back or continue editing if I got it wrong.
– Frank Hubeny
Dec 4 at 1:32
@fantasticorangina Have the answers been of any help ?
– Graham Kemp
Dec 5 at 0:45
@fantasticorangina Is that a no?
– Graham Kemp
Dec 6 at 23:22
1
1
This formula is unreadable. Please reformat it with ∀, ∃ for quantifiers, ∨, ∧, →, ¬ for connectives (you can copy symbols from here), and predicates as P(x,y,z). What > and // are I can not even guess. "Basic Inference rules" and "Replacement Rules" are specific to your book and not standard terminology, so best provide a reference and what type of system it is using (natural deduction, sequent calculus, something else?).
– Conifold
Dec 4 at 0:46
This formula is unreadable. Please reformat it with ∀, ∃ for quantifiers, ∨, ∧, →, ¬ for connectives (you can copy symbols from here), and predicates as P(x,y,z). What > and // are I can not even guess. "Basic Inference rules" and "Replacement Rules" are specific to your book and not standard terminology, so best provide a reference and what type of system it is using (natural deduction, sequent calculus, something else?).
– Conifold
Dec 4 at 0:46
1
1
I formatted the premises and conclusion to use Conifold's symbols. You may roll this back or continue editing if I got it wrong.
– Frank Hubeny
Dec 4 at 1:32
I formatted the premises and conclusion to use Conifold's symbols. You may roll this back or continue editing if I got it wrong.
– Frank Hubeny
Dec 4 at 1:32
@fantasticorangina Have the answers been of any help ?
– Graham Kemp
Dec 5 at 0:45
@fantasticorangina Have the answers been of any help ?
– Graham Kemp
Dec 5 at 0:45
@fantasticorangina Is that a no?
– Graham Kemp
Dec 6 at 23:22
@fantasticorangina Is that a no?
– Graham Kemp
Dec 6 at 23:22
add a comment |
2 Answers
2
active
oldest
votes
up vote
2
down vote
It is useful to have a proof checker to aid learning how to use natural deduction. I have linked to one below in the references.
Using that proof checker and the rules described in forallx I was able to prove the result in 22 lines which included 3 lines for the premises and 1 line for the goal.
Although I don't see it listed I assume you have the change of quantifier replacement rule. If not a derivation is in forallx on pages 260-1. Use that to change the first two premises from "~(∃x)" to "(∀x)~".
Next eliminate the universal quantifier by assigning a different name to the variable "x" in each premise. You should chose these names wisely. Look at the goal to try to pick names that will help you reach the goal.
Then use De Morgan rules to transform the lines with a negation in front of the conjunction to a disjunction of negations.
After that preparatory work, I derived something like the following line: "¬Aea ∨ ¬¬Beb". I used disjunction elimination by considering both cases. I wanted to reach the following: "¬Aea ∨ ¬Cfc". Now that is not quite the desired result but with a use of the De Morgan rules I could convert that into the final goal: "¬(Aea ∧ Cfc)".
References
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 Dec 4 at 1:32
Frank Hubeny
6,48751344
add a comment |
up vote
2
down vote
Use an Indirect Proof.
Begin by assuming (Aea ∧ Cfc), use the first premise to derive Beb, the third to derive Cbf, and the second to derive a contradiction.
Some of your subproofs will likewise be Indirect Proofs; using existential generalisation to derive their contradictions.
Assuming, that the thing you call IP operates as expected (derive a contradiction from an assumption, thereby deducing that the negation of the assumption holds).
answered Dec 4 at 3:12
Graham Kemp
85918
add a comment |
Your Answer
StackExchange.ready(function()
var channelOptions =
tags: "".split(" "),
id: "265"
;
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',
convertImagesToLinks: false,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: null,
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%2fphilosophy.stackexchange.com%2fquestions%2f57639%2fproof-for-relational-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
up vote
2
down vote
It is useful to have a proof checker to aid learning how to use natural deduction. I have linked to one below in the references.
Using that proof checker and the rules described in forallx I was able to prove the result in 22 lines which included 3 lines for the premises and 1 line for the goal.
Although I don't see it listed I assume you have the change of quantifier replacement rule. If not a derivation is in forallx on pages 260-1. Use that to change the first two premises from "~(∃x)" to "(∀x)~".
Next eliminate the universal quantifier by assigning a different name to the variable "x" in each premise. You should chose these names wisely. Look at the goal to try to pick names that will help you reach the goal.
Then use De Morgan rules to transform the lines with a negation in front of the conjunction to a disjunction of negations.
After that preparatory work, I derived something like the following line: "¬Aea ∨ ¬¬Beb". I used disjunction elimination by considering both cases. I wanted to reach the following: "¬Aea ∨ ¬Cfc". Now that is not quite the desired result but with a use of the De Morgan rules I could convert that into the final goal: "¬(Aea ∧ Cfc)".
References
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 Dec 4 at 1:32
Frank Hubeny
6,48751344
add a comment |
up vote
2
down vote
It is useful to have a proof checker to aid learning how to use natural deduction. I have linked to one below in the references.
Using that proof checker and the rules described in forallx I was able to prove the result in 22 lines which included 3 lines for the premises and 1 line for the goal.
Although I don't see it listed I assume you have the change of quantifier replacement rule. If not a derivation is in forallx on pages 260-1. Use that to change the first two premises from "~(∃x)" to "(∀x)~".
Next eliminate the universal quantifier by assigning a different name to the variable "x" in each premise. You should chose these names wisely. Look at the goal to try to pick names that will help you reach the goal.
Then use De Morgan rules to transform the lines with a negation in front of the conjunction to a disjunction of negations.
After that preparatory work, I derived something like the following line: "¬Aea ∨ ¬¬Beb". I used disjunction elimination by considering both cases. I wanted to reach the following: "¬Aea ∨ ¬Cfc". Now that is not quite the desired result but with a use of the De Morgan rules I could convert that into the final goal: "¬(Aea ∧ Cfc)".
References
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 Dec 4 at 1:32
Frank Hubeny
6,48751344
add a comment |
up vote
2
down vote
up vote
2
down vote
It is useful to have a proof checker to aid learning how to use natural deduction. I have linked to one below in the references.
Using that proof checker and the rules described in forallx I was able to prove the result in 22 lines which included 3 lines for the premises and 1 line for the goal.
Although I don't see it listed I assume you have the change of quantifier replacement rule. If not a derivation is in forallx on pages 260-1. Use that to change the first two premises from "~(∃x)" to "(∀x)~".
Next eliminate the universal quantifier by assigning a different name to the variable "x" in each premise. You should chose these names wisely. Look at the goal to try to pick names that will help you reach the goal.
Then use De Morgan rules to transform the lines with a negation in front of the conjunction to a disjunction of negations.
After that preparatory work, I derived something like the following line: "¬Aea ∨ ¬¬Beb". I used disjunction elimination by considering both cases. I wanted to reach the following: "¬Aea ∨ ¬Cfc". Now that is not quite the desired result but with a use of the De Morgan rules I could convert that into the final goal: "¬(Aea ∧ Cfc)".
References
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 Dec 4 at 1:32
Frank Hubeny
6,48751344
It is useful to have a proof checker to aid learning how to use natural deduction. I have linked to one below in the references.
Using that proof checker and the rules described in forallx I was able to prove the result in 22 lines which included 3 lines for the premises and 1 line for the goal.
Although I don't see it listed I assume you have the change of quantifier replacement rule. If not a derivation is in forallx on pages 260-1. Use that to change the first two premises from "~(∃x)" to "(∀x)~".
Next eliminate the universal quantifier by assigning a different name to the variable "x" in each premise. You should chose these names wisely. Look at the goal to try to pick names that will help you reach the goal.
Then use De Morgan rules to transform the lines with a negation in front of the conjunction to a disjunction of negations.
After that preparatory work, I derived something like the following line: "¬Aea ∨ ¬¬Beb". I used disjunction elimination by considering both cases. I wanted to reach the following: "¬Aea ∨ ¬Cfc". Now that is not quite the desired result but with a use of the De Morgan rules I could convert that into the final goal: "¬(Aea ∧ Cfc)".
References
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 Dec 4 at 1:32
Frank Hubeny
6,48751344
answered Dec 4 at 1:32
Frank Hubeny
6,48751344
answered Dec 4 at 1:32
Frank Hubeny
6,48751344
answered Dec 4 at 1:32
Frank Hubeny
6,48751344
6,48751344
add a comment |
add a comment |
up vote
2
down vote
Use an Indirect Proof.
Begin by assuming (Aea ∧ Cfc), use the first premise to derive Beb, the third to derive Cbf, and the second to derive a contradiction.
Some of your subproofs will likewise be Indirect Proofs; using existential generalisation to derive their contradictions.
Assuming, that the thing you call IP operates as expected (derive a contradiction from an assumption, thereby deducing that the negation of the assumption holds).
answered Dec 4 at 3:12
Graham Kemp
85918
add a comment |
up vote
2
down vote
Use an Indirect Proof.
Begin by assuming (Aea ∧ Cfc), use the first premise to derive Beb, the third to derive Cbf, and the second to derive a contradiction.
Some of your subproofs will likewise be Indirect Proofs; using existential generalisation to derive their contradictions.
Assuming, that the thing you call IP operates as expected (derive a contradiction from an assumption, thereby deducing that the negation of the assumption holds).
answered Dec 4 at 3:12
Graham Kemp
85918
add a comment |
up vote
2
down vote
up vote
2
down vote
Use an Indirect Proof.
Begin by assuming (Aea ∧ Cfc), use the first premise to derive Beb, the third to derive Cbf, and the second to derive a contradiction.
Some of your subproofs will likewise be Indirect Proofs; using existential generalisation to derive their contradictions.
Assuming, that the thing you call IP operates as expected (derive a contradiction from an assumption, thereby deducing that the negation of the assumption holds).
answered Dec 4 at 3:12
Graham Kemp
85918
Use an Indirect Proof.
Begin by assuming (Aea ∧ Cfc), use the first premise to derive Beb, the third to derive Cbf, and the second to derive a contradiction.
Some of your subproofs will likewise be Indirect Proofs; using existential generalisation to derive their contradictions.
Assuming, that the thing you call IP operates as expected (derive a contradiction from an assumption, thereby deducing that the negation of the assumption holds).
answered Dec 4 at 3:12
Graham Kemp
85918
edited Dec 4 at 3:17
answered Dec 4 at 3:12
Graham Kemp
85918
answered Dec 4 at 3:12
Graham Kemp
85918
answered Dec 4 at 3:12
Graham Kemp
85918
85918
add a comment |
add a comment |
Thanks for contributing an answer to Philosophy 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.
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%2fphilosophy.stackexchange.com%2fquestions%2f57639%2fproof-for-relational-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
1
This formula is unreadable. Please reformat it with ∀, ∃ for quantifiers, ∨, ∧, →, ¬ for connectives (you can copy symbols from here), and predicates as P(x,y,z). What > and // are I can not even guess. "Basic Inference rules" and "Replacement Rules" are specific to your book and not standard terminology, so best provide a reference and what type of system it is using (natural deduction, sequent calculus, something else?).
– Conifold
Dec 4 at 0:46
1
I formatted the premises and conclusion to use Conifold's symbols. You may roll this back or continue editing if I got it wrong.
– Frank Hubeny
Dec 4 at 1:32
@fantasticorangina Have the answers been of any help ?
– Graham Kemp
Dec 5 at 0:45
@fantasticorangina Is that a no?
– Graham Kemp
Dec 6 at 23:22