1
$\begingroup$

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

enter image description here

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!

$\endgroup$
  • $\begingroup$ 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.) $\endgroup$ – spaceisdarkgreen Jul 22 '18 at 2:13
  • $\begingroup$ @HollyFeng How have you progressed with this? $\endgroup$ – Graham Kemp Jul 22 '18 at 10:50
  • $\begingroup$ @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). $\endgroup$ – Holly Feng Jul 22 '18 at 15:13
  • $\begingroup$ 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 $\text{WeakPref}(a,a)\wedge \text{WeakPref}(a,a)$ from $\text{WeakPref}(a,a)\vee \text{WeakPref}(a,a)$. Finish with deriving $\text{Indiff}(a,a)$ as you have. Universal Introduction will then work. $\endgroup$ – Graham Kemp Jul 22 '18 at 16:05
  • $\begingroup$ @GrahamKemp Thank you so much. I finally figured it out! $\endgroup$ – Holly Feng Jul 22 '18 at 16:35
0
$\begingroup$

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.

$\begin{array}{|l}\forall x~\forall y ~Q(x,y)\\\forall x~\forall y ~R(x,y)\\\hline \begin{array}{|l}\boxed c\\\hline \forall y~Q(c,y)\\Q(c,c)\\ \forall y~ R(c,y)\\ R(c,c)\\~~\vdots\\ P(c,c)\end{array}\\\forall x~P(x,x)\end{array}$

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 $\text{WeakPref}(c,c)\land\text{WeakPref}(c,c)$ from $\text{WeakPref}(c,c)\lor\text{WeakPref}(c,c)$ to prepare for the biconditional elimination.

$\def\oto{\leftrightarrow}\begin{array}{|l}\forall x~\forall y ~(\text{WeakPref}(x,y)\lor\text{WeakPref}(y,x))\\\forall x~\forall y~(\text{StrongPref}(x,y)\to \lnot\text{WeakPref}(y,x))\\\forall x~\forall y ~(\text{Indiff}(x,y)\oto(\text{WeakPref}(x,y)\land\text{WeakPref}(y,x)))\\\hline \begin{array}{|l}\boxed c\\\hline \forall y~(\text{WeakPref}(c,y)\lor\text{WeakPref}(y,c))\\\text{WeakPref}(c,c)\lor\text{WeakPref}(c,c)\\\forall y~(\text{StrongPref}(c,y)\oto \lnot\text{WeakPref}(y,c))\\\text{StrongPref}(c,c)\oto\lnot\text{WeakPref}(c,c)\\ \forall y~ (\text{Indiff}(c,y)\oto(\text{WeakPref}(c,y)\land \text{WeakPref}(y,c)))\\ \text{Indiff}(c,c)\oto(\text{WeakPref}(c,c)\land\text{WeakPref}(c,c))\\~~\vdots\\ \text{WeakPref}(c,c)\land\text{WeakPref}(c,c)\\\text{Indiff}(c,c)\end{array}\\\forall x~\text{Indiff}(x,x)\end{array}$

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.