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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.