Fitch natural deduction proof of ∀x∀y∀z((S(x,y) ∧ S(y,z)) → S(x,z)), ∀x¬S(x,x) ⊢ ∀x∀y (S(x,y) → ¬S(y,x))

Question

I'm trying to prove this sequent but I keep getting stuck. Working with multiple variables as well as quantifiers is confusing me quite a bit. My effort so far is below - you will see that I am trying to get to the proof on line 12 (through lines 7 to 11), but I am not sure how to deduce that with the give combination of variables. I am aware that section 8 to 10 does not make sense - I am just trying to use all the premises that were provided, but I'm not sure where that part fits in.

As you can see, I am replacing variables x, y and z with concrete values a, b and c respectively. I don't know if I am interpreting this incorrectly though.

I'm pretty sure I'm missing something obvious here - any help will be appreciated, thanks!

Answer 1

I think I just figured it out - it seems like you can name your variables as you wish - you don't have to use different concrete values for different variables. My solution is below:

Can someone please just double check my logic?

Thanks!