Mixing
Fitch Logic Proof
Clash Royale CLAN TAG#URR8PPP
up vote
2
down vote
favorite
I am stumped on this proof. I have attached a link with my proof so far.
I'm not sure how to derive a contradiction from WeakPref(a,b) on line 12.
logic philosophy
edited Jul 24 at 4:54
Graham Kemp
80.1k43275
asked Jul 24 at 4:28
Laur
162
 |Â
show 1 more comment
up vote
2
down vote
favorite
I am stumped on this proof. I have attached a link with my proof so far.
I'm not sure how to derive a contradiction from WeakPref(a,b) on line 12.
logic philosophy
edited Jul 24 at 4:54
Graham Kemp
80.1k43275
asked Jul 24 at 4:28
Laur
162
Use negation introduction there.
– Graham Kemp
Jul 24 at 5:31
Did the advice help?
– Graham Kemp
Jul 24 at 13:41
@GrahamKemp Thank you for your help! However, I'm still stuck deriving a contradiction. I'm thinking of obtaining ~StrongPref(b,a) from StrongPref(a,b) ⟷ ~WeakPref(b,a) and WeakPref(a,b), but I'm not sure how to start.
– Laur
Jul 24 at 15:55
@GrahamKemp Is StrongPref(a,b) ↔ StrongPref(b,a) an assumption?
– Laur
Jul 24 at 22:42
Use Universal Elimination on premise 3: $forall x~forall y~(textsfStrongPref(x,y)leftrightarrowlnottextsfWeakPref(y,x))$ to obtain a useful biconditional to use with the assumptions of $textsfStrongPref(b,a)$ and $textsfWeakPref(a,b)$ .
– Graham Kemp
Jul 24 at 23:18
 |Â
show 1 more comment
up vote
2
down vote
favorite
up vote
2
down vote
favorite
I am stumped on this proof. I have attached a link with my proof so far.
I'm not sure how to derive a contradiction from WeakPref(a,b) on line 12.
logic philosophy
edited Jul 24 at 4:54
Graham Kemp
80.1k43275
asked Jul 24 at 4:28
Laur
162
I am stumped on this proof. I have attached a link with my proof so far.
I'm not sure how to derive a contradiction from WeakPref(a,b) on line 12.
logic philosophy
edited Jul 24 at 4:54
Graham Kemp
80.1k43275
asked Jul 24 at 4:28
Laur
162
edited Jul 24 at 4:54
Graham Kemp
80.1k43275
edited Jul 24 at 4:54
Graham Kemp
80.1k43275
edited Jul 24 at 4:54
Graham Kemp
80.1k43275
80.1k43275
asked Jul 24 at 4:28
Laur
162
asked Jul 24 at 4:28
Laur
162
asked Jul 24 at 4:28
Laur
162
162
Use negation introduction there.
– Graham Kemp
Jul 24 at 5:31
Did the advice help?
– Graham Kemp
Jul 24 at 13:41
@GrahamKemp Thank you for your help! However, I'm still stuck deriving a contradiction. I'm thinking of obtaining ~StrongPref(b,a) from StrongPref(a,b) ⟷ ~WeakPref(b,a) and WeakPref(a,b), but I'm not sure how to start.
– Laur
Jul 24 at 15:55
@GrahamKemp Is StrongPref(a,b) ↔ StrongPref(b,a) an assumption?
– Laur
Jul 24 at 22:42
Use Universal Elimination on premise 3: $forall x~forall y~(textsfStrongPref(x,y)leftrightarrowlnottextsfWeakPref(y,x))$ to obtain a useful biconditional to use with the assumptions of $textsfStrongPref(b,a)$ and $textsfWeakPref(a,b)$ .
– Graham Kemp
Jul 24 at 23:18
 |Â
show 1 more comment
Use negation introduction there.
– Graham Kemp
Jul 24 at 5:31
Did the advice help?
– Graham Kemp
Jul 24 at 13:41
@GrahamKemp Thank you for your help! However, I'm still stuck deriving a contradiction. I'm thinking of obtaining ~StrongPref(b,a) from StrongPref(a,b) ⟷ ~WeakPref(b,a) and WeakPref(a,b), but I'm not sure how to start.
– Laur
Jul 24 at 15:55
@GrahamKemp Is StrongPref(a,b) ↔ StrongPref(b,a) an assumption?
– Laur
Jul 24 at 22:42
Use Universal Elimination on premise 3: $forall x~forall y~(textsfStrongPref(x,y)leftrightarrowlnottextsfWeakPref(y,x))$ to obtain a useful biconditional to use with the assumptions of $textsfStrongPref(b,a)$ and $textsfWeakPref(a,b)$ .
– Graham Kemp
Jul 24 at 23:18
Use negation introduction there.
– Graham Kemp
Jul 24 at 5:31
Use negation introduction there.
– Graham Kemp
Jul 24 at 5:31
Did the advice help?
– Graham Kemp
Jul 24 at 13:41
Did the advice help?
– Graham Kemp
Jul 24 at 13:41
@GrahamKemp Thank you for your help! However, I'm still stuck deriving a contradiction. I'm thinking of obtaining ~StrongPref(b,a) from StrongPref(a,b) ⟷ ~WeakPref(b,a) and WeakPref(a,b), but I'm not sure how to start.
– Laur
Jul 24 at 15:55
@GrahamKemp Thank you for your help! However, I'm still stuck deriving a contradiction. I'm thinking of obtaining ~StrongPref(b,a) from StrongPref(a,b) ⟷ ~WeakPref(b,a) and WeakPref(a,b), but I'm not sure how to start.
– Laur
Jul 24 at 15:55
@GrahamKemp Is StrongPref(a,b) ↔ StrongPref(b,a) an assumption?
– Laur
Jul 24 at 22:42
@GrahamKemp Is StrongPref(a,b) ↔ StrongPref(b,a) an assumption?
– Laur
Jul 24 at 22:42
Use Universal Elimination on premise 3: $forall x~forall y~(textsfStrongPref(x,y)leftrightarrowlnottextsfWeakPref(y,x))$ to obtain a useful biconditional to use with the assumptions of $textsfStrongPref(b,a)$ and $textsfWeakPref(a,b)$ .
– Graham Kemp
Jul 24 at 23:18
Use Universal Elimination on premise 3: $forall x~forall y~(textsfStrongPref(x,y)leftrightarrowlnottextsfWeakPref(y,x))$ to obtain a useful biconditional to use with the assumptions of $textsfStrongPref(b,a)$ and $textsfWeakPref(a,b)$ .
– Graham Kemp
Jul 24 at 23:18
 |Â
show 1 more comment
1 Answer
1
active
oldest
votes
up vote
2
down vote
Yes, that's the way to go! Â You are almost spot on the ball. Â What you need to do at line 12 is assume $defSmathsfStrongPrefdefWmathsfWeakPrefW(a,b)$, assume $S(b,a)$, derive a contradiction, therefore introducing a negation so you may thereby use it in the disjunction elimination.
$$deffitch#1#2~~beginarrayl #1\hline #2endarraydefSmathsfStrongPrefdefWmathsfWeakPrefdeftooleftrightarrow
fitch~5.~S(a,b)~6.~S (a,b)tooneg W(b,a)\~7.~negW(b,a)\~8.~W(a,b)vee W(b,a)\fitch~9.~W(b,a)10.~bot\11.~neg S(b,a)\colorredfitch12.~W(a,b)fitch13.~S(b,a)~~vdots\~~vdots\16.~bot\17.~lnotS(b,a)\18.~neg S(b,a)$$
answered Jul 24 at 5:19
Graham Kemp
80.1k43275
add a comment |Â
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
2
down vote
Yes, that's the way to go! Â You are almost spot on the ball. Â What you need to do at line 12 is assume $defSmathsfStrongPrefdefWmathsfWeakPrefW(a,b)$, assume $S(b,a)$, derive a contradiction, therefore introducing a negation so you may thereby use it in the disjunction elimination.
$$deffitch#1#2~~beginarrayl #1\hline #2endarraydefSmathsfStrongPrefdefWmathsfWeakPrefdeftooleftrightarrow
fitch~5.~S(a,b)~6.~S (a,b)tooneg W(b,a)\~7.~negW(b,a)\~8.~W(a,b)vee W(b,a)\fitch~9.~W(b,a)10.~bot\11.~neg S(b,a)\colorredfitch12.~W(a,b)fitch13.~S(b,a)~~vdots\~~vdots\16.~bot\17.~lnotS(b,a)\18.~neg S(b,a)$$
answered Jul 24 at 5:19
Graham Kemp
80.1k43275
add a comment |Â
up vote
2
down vote
Yes, that's the way to go! Â You are almost spot on the ball. Â What you need to do at line 12 is assume $defSmathsfStrongPrefdefWmathsfWeakPrefW(a,b)$, assume $S(b,a)$, derive a contradiction, therefore introducing a negation so you may thereby use it in the disjunction elimination.
$$deffitch#1#2~~beginarrayl #1\hline #2endarraydefSmathsfStrongPrefdefWmathsfWeakPrefdeftooleftrightarrow
fitch~5.~S(a,b)~6.~S (a,b)tooneg W(b,a)\~7.~negW(b,a)\~8.~W(a,b)vee W(b,a)\fitch~9.~W(b,a)10.~bot\11.~neg S(b,a)\colorredfitch12.~W(a,b)fitch13.~S(b,a)~~vdots\~~vdots\16.~bot\17.~lnotS(b,a)\18.~neg S(b,a)$$
answered Jul 24 at 5:19
Graham Kemp
80.1k43275
add a comment |Â
up vote
2
down vote
up vote
2
down vote
Yes, that's the way to go! Â You are almost spot on the ball. Â What you need to do at line 12 is assume $defSmathsfStrongPrefdefWmathsfWeakPrefW(a,b)$, assume $S(b,a)$, derive a contradiction, therefore introducing a negation so you may thereby use it in the disjunction elimination.
$$deffitch#1#2~~beginarrayl #1\hline #2endarraydefSmathsfStrongPrefdefWmathsfWeakPrefdeftooleftrightarrow
fitch~5.~S(a,b)~6.~S (a,b)tooneg W(b,a)\~7.~negW(b,a)\~8.~W(a,b)vee W(b,a)\fitch~9.~W(b,a)10.~bot\11.~neg S(b,a)\colorredfitch12.~W(a,b)fitch13.~S(b,a)~~vdots\~~vdots\16.~bot\17.~lnotS(b,a)\18.~neg S(b,a)$$
answered Jul 24 at 5:19
Graham Kemp
80.1k43275
Yes, that's the way to go! Â You are almost spot on the ball. Â What you need to do at line 12 is assume $defSmathsfStrongPrefdefWmathsfWeakPrefW(a,b)$, assume $S(b,a)$, derive a contradiction, therefore introducing a negation so you may thereby use it in the disjunction elimination.
$$deffitch#1#2~~beginarrayl #1\hline #2endarraydefSmathsfStrongPrefdefWmathsfWeakPrefdeftooleftrightarrow
fitch~5.~S(a,b)~6.~S (a,b)tooneg W(b,a)\~7.~negW(b,a)\~8.~W(a,b)vee W(b,a)\fitch~9.~W(b,a)10.~bot\11.~neg S(b,a)\colorredfitch12.~W(a,b)fitch13.~S(b,a)~~vdots\~~vdots\16.~bot\17.~lnotS(b,a)\18.~neg S(b,a)$$
answered Jul 24 at 5:19
Graham Kemp
80.1k43275
edited Jul 24 at 5:29
answered Jul 24 at 5:19
Graham Kemp
80.1k43275
answered Jul 24 at 5:19
Graham Kemp
80.1k43275
answered Jul 24 at 5:19
Graham Kemp
80.1k43275
80.1k43275
add a comment |Â
add a comment |Â
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
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2861006%2ffitch-logic-proof%23new-answer', 'question_page');
);
Post as a guest
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
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
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
Use negation introduction there.
– Graham Kemp
Jul 24 at 5:31
Did the advice help?
– Graham Kemp
Jul 24 at 13:41
@GrahamKemp Thank you for your help! However, I'm still stuck deriving a contradiction. I'm thinking of obtaining ~StrongPref(b,a) from StrongPref(a,b) ⟷ ~WeakPref(b,a) and WeakPref(a,b), but I'm not sure how to start.
– Laur
Jul 24 at 15:55
@GrahamKemp Is StrongPref(a,b) ↔ StrongPref(b,a) an assumption?
– Laur
Jul 24 at 22:42
Use Universal Elimination on premise 3: $forall x~forall y~(textsfStrongPref(x,y)leftrightarrowlnottextsfWeakPref(y,x))$ to obtain a useful biconditional to use with the assumptions of $textsfStrongPref(b,a)$ and $textsfWeakPref(a,b)$ .
– Graham Kemp
Jul 24 at 23:18