Using Fitch to proof ∀x Indiff(x,x). Help

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!

• 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 '18 at 2:13
• @HollyFeng How have you progressed with this? – Graham Kemp Jul 22 '18 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 '18 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 $\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. – Graham Kemp Jul 22 '18 at 16:05
• @GrahamKemp Thank you so much. I finally figured it out! – Holly Feng Jul 22 '18 at 16:35

$\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}$
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}$