Fitch Arrow Proofs [closed]

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 :(

closed as off-topic by Eliran, Conifold, Mauro ALLEGRANZA, Jishin Noben, curiousdanniiJun 18 at 0:39

This question appears to be off-topic. The users who voted to close gave this specific reason:

• "This question is missing context. Please improve the question by providing additional context, which ideally includes your thoughts on the problem and any attempts you have made to solve it. This information helps others identify where you have difficulties and helps them write answers appropriate to your experience level." – Eliran, Conifold, Mauro ALLEGRANZA, Jishin Noben, curiousdannii
If this question can be reworded to fit the rules in the help center, please edit the question.

• Show us what you tried and didn't work, and explain in more detail what you're having trouble with, then potential responders will be much more willing and able to to help you. You can't just expect others to do your entire homework for you. – lemontree Jun 17 at 1:33

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.