I am having a hard time finishing this proof. Here is how far I've gotten.
I was stuck at almost the end of the proof. The first thing is that, I am pretty confused why the step 23 isn't checked out because it seems is of the correct form. The second thing is that, in step 24-27, I have no idea how to deal with WeakPref(c,b) so as to bring out ¬WeakPref(b,c) which is necessary to derive the last part of the goal.
Any help is appreciated.
Thank you
Okay, use the assumption of $\text{InDiff}(a,b)\land\text{StrongPref}(c,a)$ to derive $\lnot\text{WeakPref}(a,c)$ (as you did) and $\color{blue}{\text{WeakPref}(a,b)}$. Next assume $\color{blue}{\text{WeakPref}(b,c)}$ to derive $\color{blue}{\text{WeakPref}(a,c)}$ , which contradicts the earlier derivation. Thus deducing that $\lnot\text{WeakPref}(b,c)$, and from that derive $\text{StrongPref}(c,b)$ as required.
$$\def\I{\textsf{Indiff}}\def\W{\textsf{WeakPref}}\def\S{\textsf{StrongPref}}\def\fitch#1#2{~~\begin{array}{|l} #1\\\hline #2\end{array}}\def\too{\leftrightarrow}\def\hide#1{\vdots} {\fitch{~\forall x~\forall y~(\W(x,y)\vee \W(y,x))\\~\forall x~\forall y~\forall z~ ((\W(x,y)\wedge \W(y,z))\to \W(x,z))\\~\forall x~\forall y~(\S(x,y)\too\neg \W(y,x))\\~\forall x~\forall y~(\I(x, y)\too (\W(x,y)\wedge \W(y,x)))}{\fitch{~\boxed a}{\fitch{~\boxed b}{\fitch{~\boxed c}{~ \hide{(\W(a,b)\wedge \W(b,c))\to \W(a,c)}\\~ \hide{\S(c,a)\too\lnot \W(a, c)}\\~ \hide{\I(a,b)\too (\W(a,b)\wedge \W(b,a))}\\\fitch{~\I(a,b)\wedge \S(c,a)}{~ \hide{\S(c,a)}\\~ \neg \W(a,c)\\~ \hide{\I(a,b)}\\~ \hide{\W(a,b)\wedge \W(b,a)} \\~ \W(a,b)\\\fitch{\W(b,c)}{\hide{\W(a,b)\wedge \W(b,c)}\\\W(a, c)\\\bot}\\\neg \W(b,c)\\~\S(c,b)}\\~(\I(a,b)\wedge \S(c,a))\to \S(c,b)}}}\\\therefore~\forall x~\forall y~\forall z~((\I(x,y)\wedge \S(z,x))\to \S(z,y))}}$$