# Fitch Proof - Arrow's logic of preferences

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!

• See your previous post. Jun 20, 2019 at 6:52
• Possible duplicate of Fitch Arrow Proofs Jun 20, 2019 at 7:34
• Thank you for taking notice - while the linked question uses the same premises/axioms, it's attempting to prove something completely different This question is asking to prove the transitivity of `Indiff`, whereas the other one is proving something with `StrongPref`
– rzy
Jun 20, 2019 at 8:01
• I agree. I don't see this as a duplicate. +1 for a clear presentation of what you have attempted. Jun 20, 2019 at 12:23

## 1 Answer

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