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!

enter image description here

  • See your previous post. Jun 20, 2019 at 6:52
  • Possible duplicate of Fitch Arrow Proofs
    – Conifold
    Jun 20, 2019 at 7:34
  • 2
    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
  • 1
    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 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.

enter image description here

enter image description here

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

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .