Fitch Arrow Proofs [closed]

Question

Using the FITCH program and the FITCH derivation rules you should make a proof or derivation of C10 from P5 through P11.

P5: ∀x∀y(StrongPref(x,y)→ ¬StrongPref(y,x))

P6: ∀x∀y∀z((StrongPref(x,y)∧StrongPref(y,z))→StrongPref(x,z))

P7: ∀xIndiff(x,x)

P8: ∀x∀y(Indiff(x,y)→Indiff(y,x))

P9: ∀x∀y∀z((StrongPref(x,y)∧Indiff(y,z))→StrongPref(x,z))

P10: ∀x∀y(StrongPref(x,y)∨Indiff(x,y)∨StrongPref(y,x))

P11: ∀x∀y(WeakPref(x,y)↔(StrongPref(x,y)∨Indiff(x,y)))

C10: ∀x∀y∀z((Indiff(x,y)∧StrongPref(z,x))→StrongPref(z,y))

I genuinely am stuck and don't even know where to start.. Someone save me :(

Answer 1

One of the first things to consider is the goal you are trying to show:

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

Note that it is a conditional. So we may want to assume the antecedent of that conditional to start the proof. We may start by assuming the following:

Indiff(a,b)∧StrongPref(c,a)

From here we want to derive

StrongPref(c,b)

If we can derive that then we can derive the following using conditional introduction:

(Indiff(a,b)∧StrongPref(c,a)) → StrongPref(c,b)

If we get that far, the only thing left to do is introduce the universal quantifiers to finish the proof.

Don't let the many premises overwhelm you. We may not need all of them. Premise 9 looks promising:

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

It has both the StrongPref and Indiff predicates in a conjunction, but in reverse order. One can easily use conjunction elimination and conjunction introduction to put them in the right order.

It also has StrongPref(x,y) and StrongPref(x,z) and we want StrongPref(c,a) and StrongPref(c,b) so when we do the universal elimination we might try using the name c for the variable x and the name b for the variable y and the name a for the variable z.

If the Fitch proof checker accepts our steps then this should conclude the proof.