Fitch Proof - Arrow's logic of preferences

Question

I've been stumped on this one question in particular for several days now and I'm hoping to get some help on where I'm going wrong.

Given the following premises:

1. ∀x∀y(StrongPref(x,y)→ ¬StrongPref(y,x))
2. ∀x∀y∀z((StrongPref(x,y)∧StrongPref(y,z))→StrongPref(x,z))
3. ∀xIndiff(x,x)
4. ∀x∀y(Indiff(x,y)→Indiff(y,x))
5. ∀x∀y∀z((StrongPref(x,y)∧Indiff(y,z))→StrongPref(x,z))
6. ∀x∀y(StrongPref(x,y)∨Indiff(x,y)∨StrongPref(y,x))
7. ∀x∀y(WeakPref(x,y)↔(StrongPref(x,y)∨Indiff(x,y)))

Prove: (Not required to use all the premises)

∀x∀y∀z((Indiff(x,y) ∧ Indiff(y,z)) → Indiff(x,z))

---

Since we are trying to prove a conditional, my initial inclination is to assume Indiff(x,y) ∧ Indiff(y,z) and try to prove Indiff(x,z). Since none of the premises explicitly tells us much information about deriving Indiff, I figured it would be best to prove by contradition - that is, assuming ~Indiff(x,z) and deriving a contradiction.

I begin the proof by initializing the quantifiers, using c,d,e in place of x,y,z. Since only premises (5) and (6) give us some information about Indiff to work off of, I am thinking to initially use (6) and go through each case/combination of StrongPref(c,d) ∨ Indiff(c,d) ∨ StrongPref(d,c)and StrongPref(d,e) ∨ Indiff(d,e) ∨ StrongPref(e,d) in order to get c and e together (which seems unreasonable since that would mean doing 9 proofs but I'm getting desperate). Then, to get the contradictions, I used (5) to derive something of the form StrongPref(x,x) which we can get a contradiction from (1).

I am able to get contradictions for many of the cases, but I begin getting stuck when it comes to getting a contradiction in the case where we have both Indiff(c,d) and Indiff(d,e).

I have shown my work below (took out some of the repeated work for working contradictions to save space). I have a feeling I'm completely off since it seems unreasonable of have to do 9 subproofs, but I can't see another perspective to take. Any help would be much appreciated, thank you!

Answer 1

The following is a direct proof. I converted StrongPref to S and Indiff to I to use the syntax required by the proof checker associated with forallx.

After assuming the antecedent on line 5, I attempted to derive the consequent using premise 4. Premise 4 was a disjunction so I had to eliminate it. In each case I derived Iac. When that was done, I introduced the universal quantifiers.

---

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf