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

Question

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!

Answer 1

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