Proving transitivity of Strict Preference Patrick Suppes in his book Introduction to Logic on page 63 asks a reader to proof a statement
$$\forall x\forall y\forall z(xPy\land yPz\to xPz)$$ from the theory which he calls "Theory of rational behavior". The statement is based on the notion of weak preference $xQy$, its two properties (lines 1 and 2) and a definition of strict preference $xPy$ (line 3):
$$\begin{array}{p}
\{1\}&(1)&\forall x\forall y\forall z(xQy\land yQz\to xQz)&\text{Transitive property} \\
\{2\}&(2)&\forall x\forall y(xQy \lor yQx)&\text{Axiom of order}\\
\{3\}&(3)&\forall x\forall y(xPy\leftrightarrow \neg yQx)&\text{Definition of strict preferece}\\
\{4\}&(4) & xPy\land yPz & \text{Assumption} \\
\{3,4\}&(5) & \neg yQx\land \neg zQy & \text{from (3)(4) using U.S.} \\
\{2,3,4\}&(6) & xQy & \text{from (2)(5) using U.S.} \\
\{2,3,4\}&(7) & yQz & \text{from (2)(5) using U.S.} \\
\{1,2,3,4\}&(8) & xQz & \text{from (1)(6)(7)} \\
\end{array}
$$
U.S. stands here for the Rule of Universal Specification
$xPz$ is equal to $\neg zQx$ by the definition of strict preference on line $3$. So we want to show that $\neg zQx$ logically follows from the premises $\{1,2,3,4\}$ and then use conditioning on line $(4)$ and The Rule of Universal Generalisation to prove the given statement. But from $xQz\land(xQz \lor zQx)$ we cannot conclude $\neg zQx$ because according to the Axiom of order both $xQz$ and $zQx$ can be true together.
I've tried the method of interpretations to check validity of the statement that has to be proven but haven't found any, such that its antecedent would be true and conclusion would be false.
If my derivation is fine so far, I'm looking for tips which will help me to get to the finish line here. Will appreciate any feedback.
 A: I came to the same conclusion using your approach, namely, that the axiom of order wasn't enough to prove $\neg zQx$. However, I found that it could be accomplished by using the transitive property along with modus tollens. That leads to the following idea: $\neg yQx \to (yQz \to \neg zQx)$. That's a summary of lines 14 through 17:
\begin{array}{l}
& \{1\} & 1. & x\forall y\forall z(xQy\land yQz\to xQz) & \text{ Transitive property }\\
& \{2\} & 2. & \forall x\forall y(xQy \lor yQx) & \text{ Axiom of order }\\
& \{3\} & 3. & \forall x\forall y(xPy\leftrightarrow \neg yQx) & \text{ Definition of strict preference }\\
& \{4\} & 4. & aPb\land bPc & \text{ Assum. }\\
& \{4\} & 5. & aPb & \text{ $\land$E }\\
& \{4\} & 6. & bPc & \text{ $\land$E }\\
& \{3\} & 7. & aPb\leftrightarrow \neg bQa & \text{ 3 UE }\\
& \{3\} & 8. & bPc\leftrightarrow \neg cQb & \text{ 3 UE }\\
& \{3,4\} & 9. & \neg bQa & \text{ 7 $\leftrightarrow$E, 5,7 MP }\\
& \{3,4\} & 10. & \neg cQb & \text{ 8 $\leftrightarrow$E, 6,8 MP }\\
& \{2\} & 11. & bQc \lor cQb & \text{ 2 UE }\\
& \{2\} & 12. & \neg cQb \to bQc & \text{ 11 MI }\\
& \{2,3,4\} & 13. & bQc & \text{ 10,12 MP }\\
& \{1\} & 14. & (bQc \land cQa) \to bQa & \text{ 1 UE }\\
& \{1,3,4\} & 15. & \neg (bQc \land cQa) & \text{ 9,14 MT }\\
& \{1,3,4\} & 16. & \neg bQc \lor \neg cQa & \text{ 15 DM }\\
& \{1,3,4\} & 17. & bQc \to \neg cQa & \text{ 16 MI }\\
& \{1,2,3,4\} & 18. & \neg cQa & \text{ 13,17 MP }\\
& \{3\} & 19. & \neg cQa \to aPc & \text{ 3 UE, $\leftrightarrow$E }\\
& \{1,2,3,4\} & 20. & aPc & \text{ 18,19 MP }\\
& \{1,2,3\} & 21. & (aPb\land bPc) \to aPc & \text{ 4,20 CP }\\
& \{1,2,3\} & 22. & \forall x\forall y\forall z(xPy\land yPz\to xPz) & \text{ 22 UI }\\
\end{array}
A: Do a proof by contradiction, i.e. continue with:
$$\begin{array}{p}
\{9\}&(9)&\neg xPz&\text{Assumption} \\
\{3,9\}&(2)&zQx&\text{from (3)(9)}\\
\{1,2,3,4,9\}&(10)&zQy&\text{from (1)(6)(10)}\\
\{3,4\}&(11) & \neg zQy & \text{from (5)} \\
\{1,2,3,4,9\}&(12) & \bot & \text{from (10)(11)} \\
\{1,2,3,4\}&(13) & xPz & \text{from (12) using proof by Contradiction} \\
\end{array}
$$
(I wasn't sure how proof by Contradiction works in your system ... but you get the idea)
