# Language, Proof and Logic Exercise 14.13 (Fitch)

Having trouble proving this. I know how to prove the first conjunct of the conclusion, but not the second one. Picture shown is the attempt proof of the second conjunct (rules haven't been added yet). I have a feeling that we need to use ∀Intro for the second conjunct of conclusion as well as ∀z (Cube(z) → (z = x v z = y)) part of premise.

• Welcome to SE Philosophy! Thanks for your contribution. Please take a quick moment to take the tour or find help. You can perform searches here or seek additional clarification at the meta site. Don't forget, when someone has answered your question, you can click on the checkmark to reward the user!
– J D
Commented Nov 24, 2019 at 15:10

I have a feeling that we need to use ∀Intro for the second conjunct of conclusion as well as ∀z (Cube(z) → (z = x v z = y)) part of premise.

Yes, you need to apply Universal Elimination thrice, once to each arbitrary term.

You can then derive three disjunctions through Conditional Eliminations.

Up next is a nested disjunction elimination, where you use equality eliminations and disjunction introduction; you are aiming to obtain `a=b v a=c v b=c` at the end of each sub-proof.

Recall, `a=d` and `b=d` entails `a=b` by Equality Elimination.

And so on.