Mixing
![Calculate x/y coordinates of an overlayed image when the underlying image is resized. [closed]](https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEhZCTB4-bb-s-32SAm6ytjzFOU06cH9o8q-a_wq_UnH6lcd8hvws23CmBWHM6g256LzTX9yK1EiCCzTC1NSgtxlNk_J9hdr9bA3tD0Nqntbl521j4bLAm_uXPANuWLBhcCKTKzns2gaUodx/s72-c/1.jpg)
Using Fitch to proof ∀x Indiff(x,x). Help
Clash Royale CLAN TAG#URR8PPP
up vote
1
down vote
favorite
I am having a hard time solving this Fitch Proof.
Goal: ∀x Indiff(x,x)
I have to proof this goal using the following four premises: (might not need all of them)
P1: ∀x∀y(WeakPref(x,y)∨WeakPref(y,x))
P2: ∀x∀y∀z((WeakPref(x,y)∧WeakPref(y,z))→WeakPref(x,z))
P3: ∀x∀y(StrongPref(x,y)↔ ¬WeakPref(y,x))
P4: ∀x∀y(Indiff(x,y)↔(WeakPref(y,x)∧WeakPref(x,y)))
Here is how far I've gotten right now
I was stuck with how to end the proof because Fitch states the last sentence is of the wrong form, but if I delete the premise in the subproof, I have no idea how to bring out ∀x Indiff(x,x).
Any suggestion is appreciated.
Thank you!
logic philosophy
asked Jul 22 at 1:39
Holly Feng
234
add a comment |Â
up vote
1
down vote
favorite
I am having a hard time solving this Fitch Proof.
Goal: ∀x Indiff(x,x)
I have to proof this goal using the following four premises: (might not need all of them)
P1: ∀x∀y(WeakPref(x,y)∨WeakPref(y,x))
P2: ∀x∀y∀z((WeakPref(x,y)∧WeakPref(y,z))→WeakPref(x,z))
P3: ∀x∀y(StrongPref(x,y)↔ ¬WeakPref(y,x))
P4: ∀x∀y(Indiff(x,y)↔(WeakPref(y,x)∧WeakPref(x,y)))
Here is how far I've gotten right now
I was stuck with how to end the proof because Fitch states the last sentence is of the wrong form, but if I delete the premise in the subproof, I have no idea how to bring out ∀x Indiff(x,x).
Any suggestion is appreciated.
Thank you!
logic philosophy
asked Jul 22 at 1:39
Holly Feng
234
To end up with a single variable, you could try introducing a single constant instead of two different ones. (But you haven't done the work to be able to derive the desired conclusion even if you do this.)
– spaceisdarkgreen
Jul 22 at 2:13
@HollyFeng How have you progressed with this?
– Graham Kemp
Jul 22 at 10:50
@GrahamKemp Not yet finish. I tried introducing a single variable and it did work (picture above). But I was stuck with how to end the proof because Fitch states the last sentence is of the wrong form unless I delete the premise in the subproof. But if so, I have no idea how to derive Indiff(a,a).
– Holly Feng
Jul 22 at 15:13
No. The witness needs to be completely arbitrary; just $boxed a$ with no assumptions. From there you use Universal Elimination as you have. Next you must derive $textWeakPref(a,a)wedge textWeakPref(a,a)$ from $textWeakPref(a,a)vee textWeakPref(a,a)$. Finish with deriving $textIndiff(a,a)$ as you have. Universal Introduction will then work.
– Graham Kemp
Jul 22 at 16:05
@GrahamKemp Thank you so much. I finally figured it out!
– Holly Feng
Jul 22 at 16:35
add a comment |Â
up vote
1
down vote
favorite
up vote
1
down vote
favorite
I am having a hard time solving this Fitch Proof.
Goal: ∀x Indiff(x,x)
I have to proof this goal using the following four premises: (might not need all of them)
P1: ∀x∀y(WeakPref(x,y)∨WeakPref(y,x))
P2: ∀x∀y∀z((WeakPref(x,y)∧WeakPref(y,z))→WeakPref(x,z))
P3: ∀x∀y(StrongPref(x,y)↔ ¬WeakPref(y,x))
P4: ∀x∀y(Indiff(x,y)↔(WeakPref(y,x)∧WeakPref(x,y)))
Here is how far I've gotten right now
I was stuck with how to end the proof because Fitch states the last sentence is of the wrong form, but if I delete the premise in the subproof, I have no idea how to bring out ∀x Indiff(x,x).
Any suggestion is appreciated.
Thank you!
logic philosophy
asked Jul 22 at 1:39
Holly Feng
234
I am having a hard time solving this Fitch Proof.
Goal: ∀x Indiff(x,x)
I have to proof this goal using the following four premises: (might not need all of them)
P1: ∀x∀y(WeakPref(x,y)∨WeakPref(y,x))
P2: ∀x∀y∀z((WeakPref(x,y)∧WeakPref(y,z))→WeakPref(x,z))
P3: ∀x∀y(StrongPref(x,y)↔ ¬WeakPref(y,x))
P4: ∀x∀y(Indiff(x,y)↔(WeakPref(y,x)∧WeakPref(x,y)))
Here is how far I've gotten right now
I was stuck with how to end the proof because Fitch states the last sentence is of the wrong form, but if I delete the premise in the subproof, I have no idea how to bring out ∀x Indiff(x,x).
Any suggestion is appreciated.
Thank you!
logic philosophy
asked Jul 22 at 1:39
Holly Feng
234
edited Jul 22 at 15:11
asked Jul 22 at 1:39
Holly Feng
234
asked Jul 22 at 1:39
Holly Feng
234
asked Jul 22 at 1:39
Holly Feng
234
234
To end up with a single variable, you could try introducing a single constant instead of two different ones. (But you haven't done the work to be able to derive the desired conclusion even if you do this.)
– spaceisdarkgreen
Jul 22 at 2:13
@HollyFeng How have you progressed with this?
– Graham Kemp
Jul 22 at 10:50
@GrahamKemp Not yet finish. I tried introducing a single variable and it did work (picture above). But I was stuck with how to end the proof because Fitch states the last sentence is of the wrong form unless I delete the premise in the subproof. But if so, I have no idea how to derive Indiff(a,a).
– Holly Feng
Jul 22 at 15:13
No. The witness needs to be completely arbitrary; just $boxed a$ with no assumptions. From there you use Universal Elimination as you have. Next you must derive $textWeakPref(a,a)wedge textWeakPref(a,a)$ from $textWeakPref(a,a)vee textWeakPref(a,a)$. Finish with deriving $textIndiff(a,a)$ as you have. Universal Introduction will then work.
– Graham Kemp
Jul 22 at 16:05
@GrahamKemp Thank you so much. I finally figured it out!
– Holly Feng
Jul 22 at 16:35
add a comment |Â
To end up with a single variable, you could try introducing a single constant instead of two different ones. (But you haven't done the work to be able to derive the desired conclusion even if you do this.)
– spaceisdarkgreen
Jul 22 at 2:13
@HollyFeng How have you progressed with this?
– Graham Kemp
Jul 22 at 10:50
@GrahamKemp Not yet finish. I tried introducing a single variable and it did work (picture above). But I was stuck with how to end the proof because Fitch states the last sentence is of the wrong form unless I delete the premise in the subproof. But if so, I have no idea how to derive Indiff(a,a).
– Holly Feng
Jul 22 at 15:13
No. The witness needs to be completely arbitrary; just $boxed a$ with no assumptions. From there you use Universal Elimination as you have. Next you must derive $textWeakPref(a,a)wedge textWeakPref(a,a)$ from $textWeakPref(a,a)vee textWeakPref(a,a)$. Finish with deriving $textIndiff(a,a)$ as you have. Universal Introduction will then work.
– Graham Kemp
Jul 22 at 16:05
@GrahamKemp Thank you so much. I finally figured it out!
– Holly Feng
Jul 22 at 16:35
To end up with a single variable, you could try introducing a single constant instead of two different ones. (But you haven't done the work to be able to derive the desired conclusion even if you do this.)
– spaceisdarkgreen
Jul 22 at 2:13
To end up with a single variable, you could try introducing a single constant instead of two different ones. (But you haven't done the work to be able to derive the desired conclusion even if you do this.)
– spaceisdarkgreen
Jul 22 at 2:13
@HollyFeng How have you progressed with this?
– Graham Kemp
Jul 22 at 10:50
@HollyFeng How have you progressed with this?
– Graham Kemp
Jul 22 at 10:50
@GrahamKemp Not yet finish. I tried introducing a single variable and it did work (picture above). But I was stuck with how to end the proof because Fitch states the last sentence is of the wrong form unless I delete the premise in the subproof. But if so, I have no idea how to derive Indiff(a,a).
– Holly Feng
Jul 22 at 15:13
@GrahamKemp Not yet finish. I tried introducing a single variable and it did work (picture above). But I was stuck with how to end the proof because Fitch states the last sentence is of the wrong form unless I delete the premise in the subproof. But if so, I have no idea how to derive Indiff(a,a).
– Holly Feng
Jul 22 at 15:13
No. The witness needs to be completely arbitrary; just $boxed a$ with no assumptions. From there you use Universal Elimination as you have. Next you must derive $textWeakPref(a,a)wedge textWeakPref(a,a)$ from $textWeakPref(a,a)vee textWeakPref(a,a)$. Finish with deriving $textIndiff(a,a)$ as you have. Universal Introduction will then work.
– Graham Kemp
Jul 22 at 16:05
No. The witness needs to be completely arbitrary; just $boxed a$ with no assumptions. From there you use Universal Elimination as you have. Next you must derive $textWeakPref(a,a)wedge textWeakPref(a,a)$ from $textWeakPref(a,a)vee textWeakPref(a,a)$. Finish with deriving $textIndiff(a,a)$ as you have. Universal Introduction will then work.
– Graham Kemp
Jul 22 at 16:05
@GrahamKemp Thank you so much. I finally figured it out!
– Holly Feng
Jul 22 at 16:35
@GrahamKemp Thank you so much. I finally figured it out!
– Holly Feng
Jul 22 at 16:35
add a comment |Â
1 Answer
1
active
oldest
votes
up vote
0
down vote
accepted
If you want to introduce a single universal quantifier at the end, then begin by eliminating both universals in each premise to the same arbitrary witness.
$beginarrayforall x~forall y ~Q(x,y)\forall x~forall y ~R(x,y)\hline beginarrayboxed c\hline forall y~Q(c,y)\Q(c,c)\ forall y~ R(c,y)\ R(c,c)\~~vdots\ P(c,c)endarray\forall x~P(x,x)endarray$
Now which premises you choose and what argument you make with them is left up to you, but as a hint: you do only need two of the four.
@GrahamKemp Not yet finish. I tried introducing a single variable and it did work (picture above). But I was stuck with how to end the proof because Fitch states the last sentence is of the wrong form unless I delete the premise in the subproof. But if so, I have no idea how to derive Indiff(a,a).
The witness needs to be arbitrary for the required universal introduction; no assumption must be made with it. Â You then use universal elimination, and so derive $textWeakPref(c,c)landtextWeakPref(c,c)$ from $textWeakPref(c,c)lortextWeakPref(c,c)$ to prepare for the biconditional elimination.
$defotoleftrightarrowbeginarrayforall x~forall y ~(textWeakPref(x,y)lortextWeakPref(y,x))\forall x~forall y~(textStrongPref(x,y)to lnottextWeakPref(y,x))\forall x~forall y ~(textIndiff(x,y)oto(textWeakPref(x,y)landtextWeakPref(y,x)))\hline beginarrayboxed c\hline forall y~(textWeakPref(c,y)lortextWeakPref(y,c))\textWeakPref(c,c)lortextWeakPref(c,c)\forall y~(textStrongPref(c,y)oto lnottextWeakPref(y,c))\textStrongPref(c,c)otolnottextWeakPref(c,c)\ forall y~ (textIndiff(c,y)oto(textWeakPref(c,y)land textWeakPref(y,c)))\ textIndiff(c,c)oto(textWeakPref(c,c)landtextWeakPref(c,c))\~~vdots\ textWeakPref(c,c)landtextWeakPref(c,c)\textIndiff(c,c)endarray\forall x~textIndiff(x,x)endarray$
answered Jul 22 at 3:04
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
0
down vote
accepted
If you want to introduce a single universal quantifier at the end, then begin by eliminating both universals in each premise to the same arbitrary witness.
$beginarrayforall x~forall y ~Q(x,y)\forall x~forall y ~R(x,y)\hline beginarrayboxed c\hline forall y~Q(c,y)\Q(c,c)\ forall y~ R(c,y)\ R(c,c)\~~vdots\ P(c,c)endarray\forall x~P(x,x)endarray$
Now which premises you choose and what argument you make with them is left up to you, but as a hint: you do only need two of the four.
@GrahamKemp Not yet finish. I tried introducing a single variable and it did work (picture above). But I was stuck with how to end the proof because Fitch states the last sentence is of the wrong form unless I delete the premise in the subproof. But if so, I have no idea how to derive Indiff(a,a).
The witness needs to be arbitrary for the required universal introduction; no assumption must be made with it. Â You then use universal elimination, and so derive $textWeakPref(c,c)landtextWeakPref(c,c)$ from $textWeakPref(c,c)lortextWeakPref(c,c)$ to prepare for the biconditional elimination.
$defotoleftrightarrowbeginarrayforall x~forall y ~(textWeakPref(x,y)lortextWeakPref(y,x))\forall x~forall y~(textStrongPref(x,y)to lnottextWeakPref(y,x))\forall x~forall y ~(textIndiff(x,y)oto(textWeakPref(x,y)landtextWeakPref(y,x)))\hline beginarrayboxed c\hline forall y~(textWeakPref(c,y)lortextWeakPref(y,c))\textWeakPref(c,c)lortextWeakPref(c,c)\forall y~(textStrongPref(c,y)oto lnottextWeakPref(y,c))\textStrongPref(c,c)otolnottextWeakPref(c,c)\ forall y~ (textIndiff(c,y)oto(textWeakPref(c,y)land textWeakPref(y,c)))\ textIndiff(c,c)oto(textWeakPref(c,c)landtextWeakPref(c,c))\~~vdots\ textWeakPref(c,c)landtextWeakPref(c,c)\textIndiff(c,c)endarray\forall x~textIndiff(x,x)endarray$
answered Jul 22 at 3:04
Graham Kemp
80.1k43275
add a comment |Â
up vote
0
down vote
accepted
If you want to introduce a single universal quantifier at the end, then begin by eliminating both universals in each premise to the same arbitrary witness.
$beginarrayforall x~forall y ~Q(x,y)\forall x~forall y ~R(x,y)\hline beginarrayboxed c\hline forall y~Q(c,y)\Q(c,c)\ forall y~ R(c,y)\ R(c,c)\~~vdots\ P(c,c)endarray\forall x~P(x,x)endarray$
Now which premises you choose and what argument you make with them is left up to you, but as a hint: you do only need two of the four.
@GrahamKemp Not yet finish. I tried introducing a single variable and it did work (picture above). But I was stuck with how to end the proof because Fitch states the last sentence is of the wrong form unless I delete the premise in the subproof. But if so, I have no idea how to derive Indiff(a,a).
The witness needs to be arbitrary for the required universal introduction; no assumption must be made with it. Â You then use universal elimination, and so derive $textWeakPref(c,c)landtextWeakPref(c,c)$ from $textWeakPref(c,c)lortextWeakPref(c,c)$ to prepare for the biconditional elimination.
$defotoleftrightarrowbeginarrayforall x~forall y ~(textWeakPref(x,y)lortextWeakPref(y,x))\forall x~forall y~(textStrongPref(x,y)to lnottextWeakPref(y,x))\forall x~forall y ~(textIndiff(x,y)oto(textWeakPref(x,y)landtextWeakPref(y,x)))\hline beginarrayboxed c\hline forall y~(textWeakPref(c,y)lortextWeakPref(y,c))\textWeakPref(c,c)lortextWeakPref(c,c)\forall y~(textStrongPref(c,y)oto lnottextWeakPref(y,c))\textStrongPref(c,c)otolnottextWeakPref(c,c)\ forall y~ (textIndiff(c,y)oto(textWeakPref(c,y)land textWeakPref(y,c)))\ textIndiff(c,c)oto(textWeakPref(c,c)landtextWeakPref(c,c))\~~vdots\ textWeakPref(c,c)landtextWeakPref(c,c)\textIndiff(c,c)endarray\forall x~textIndiff(x,x)endarray$
answered Jul 22 at 3:04
Graham Kemp
80.1k43275
add a comment |Â
up vote
0
down vote
accepted
up vote
0
down vote
accepted
If you want to introduce a single universal quantifier at the end, then begin by eliminating both universals in each premise to the same arbitrary witness.
$beginarrayforall x~forall y ~Q(x,y)\forall x~forall y ~R(x,y)\hline beginarrayboxed c\hline forall y~Q(c,y)\Q(c,c)\ forall y~ R(c,y)\ R(c,c)\~~vdots\ P(c,c)endarray\forall x~P(x,x)endarray$
Now which premises you choose and what argument you make with them is left up to you, but as a hint: you do only need two of the four.
@GrahamKemp Not yet finish. I tried introducing a single variable and it did work (picture above). But I was stuck with how to end the proof because Fitch states the last sentence is of the wrong form unless I delete the premise in the subproof. But if so, I have no idea how to derive Indiff(a,a).
The witness needs to be arbitrary for the required universal introduction; no assumption must be made with it. Â You then use universal elimination, and so derive $textWeakPref(c,c)landtextWeakPref(c,c)$ from $textWeakPref(c,c)lortextWeakPref(c,c)$ to prepare for the biconditional elimination.
$defotoleftrightarrowbeginarrayforall x~forall y ~(textWeakPref(x,y)lortextWeakPref(y,x))\forall x~forall y~(textStrongPref(x,y)to lnottextWeakPref(y,x))\forall x~forall y ~(textIndiff(x,y)oto(textWeakPref(x,y)landtextWeakPref(y,x)))\hline beginarrayboxed c\hline forall y~(textWeakPref(c,y)lortextWeakPref(y,c))\textWeakPref(c,c)lortextWeakPref(c,c)\forall y~(textStrongPref(c,y)oto lnottextWeakPref(y,c))\textStrongPref(c,c)otolnottextWeakPref(c,c)\ forall y~ (textIndiff(c,y)oto(textWeakPref(c,y)land textWeakPref(y,c)))\ textIndiff(c,c)oto(textWeakPref(c,c)landtextWeakPref(c,c))\~~vdots\ textWeakPref(c,c)landtextWeakPref(c,c)\textIndiff(c,c)endarray\forall x~textIndiff(x,x)endarray$
answered Jul 22 at 3:04
Graham Kemp
80.1k43275
If you want to introduce a single universal quantifier at the end, then begin by eliminating both universals in each premise to the same arbitrary witness.
$beginarrayforall x~forall y ~Q(x,y)\forall x~forall y ~R(x,y)\hline beginarrayboxed c\hline forall y~Q(c,y)\Q(c,c)\ forall y~ R(c,y)\ R(c,c)\~~vdots\ P(c,c)endarray\forall x~P(x,x)endarray$
Now which premises you choose and what argument you make with them is left up to you, but as a hint: you do only need two of the four.
@GrahamKemp Not yet finish. I tried introducing a single variable and it did work (picture above). But I was stuck with how to end the proof because Fitch states the last sentence is of the wrong form unless I delete the premise in the subproof. But if so, I have no idea how to derive Indiff(a,a).
The witness needs to be arbitrary for the required universal introduction; no assumption must be made with it. Â You then use universal elimination, and so derive $textWeakPref(c,c)landtextWeakPref(c,c)$ from $textWeakPref(c,c)lortextWeakPref(c,c)$ to prepare for the biconditional elimination.
$defotoleftrightarrowbeginarrayforall x~forall y ~(textWeakPref(x,y)lortextWeakPref(y,x))\forall x~forall y~(textStrongPref(x,y)to lnottextWeakPref(y,x))\forall x~forall y ~(textIndiff(x,y)oto(textWeakPref(x,y)landtextWeakPref(y,x)))\hline beginarrayboxed c\hline forall y~(textWeakPref(c,y)lortextWeakPref(y,c))\textWeakPref(c,c)lortextWeakPref(c,c)\forall y~(textStrongPref(c,y)oto lnottextWeakPref(y,c))\textStrongPref(c,c)otolnottextWeakPref(c,c)\ forall y~ (textIndiff(c,y)oto(textWeakPref(c,y)land textWeakPref(y,c)))\ textIndiff(c,c)oto(textWeakPref(c,c)landtextWeakPref(c,c))\~~vdots\ textWeakPref(c,c)landtextWeakPref(c,c)\textIndiff(c,c)endarray\forall x~textIndiff(x,x)endarray$
answered Jul 22 at 3:04
Graham Kemp
80.1k43275
edited Jul 22 at 16:38
answered Jul 22 at 3:04
Graham Kemp
80.1k43275
answered Jul 22 at 3:04
Graham Kemp
80.1k43275
answered Jul 22 at 3:04
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%2f2859019%2fusing-fitch-to-proof-%25e2%2588%2580x-indiffx-x-help%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
To end up with a single variable, you could try introducing a single constant instead of two different ones. (But you haven't done the work to be able to derive the desired conclusion even if you do this.)
– spaceisdarkgreen
Jul 22 at 2:13
@HollyFeng How have you progressed with this?
– Graham Kemp
Jul 22 at 10:50
@GrahamKemp Not yet finish. I tried introducing a single variable and it did work (picture above). But I was stuck with how to end the proof because Fitch states the last sentence is of the wrong form unless I delete the premise in the subproof. But if so, I have no idea how to derive Indiff(a,a).
– Holly Feng
Jul 22 at 15:13
No. The witness needs to be completely arbitrary; just $boxed a$ with no assumptions. From there you use Universal Elimination as you have. Next you must derive $textWeakPref(a,a)wedge textWeakPref(a,a)$ from $textWeakPref(a,a)vee textWeakPref(a,a)$. Finish with deriving $textIndiff(a,a)$ as you have. Universal Introduction will then work.
– Graham Kemp
Jul 22 at 16:05
@GrahamKemp Thank you so much. I finally figured it out!
– Holly Feng
Jul 22 at 16:35