Natural Deduction Proof that irreflexive, transitive relations on a Set S are not three-cycles

Question

I am looking for a natural deduction proof for above question. I have formalized the argument in the following way:

$$ \forall x \neg Rxx, \ \forall x\forall y \forall z (Rxy\land Ryz \rightarrow Rxz) \vdash \forall x \forall y \forall z \neg(Rxy\land Ryz \rightarrow Rzx) $$ I may have made an error in the formalization, and if this is the case I would be very happy for anybody to point this out. I currently have problems with showing that a relation is not three-cycle when there are no elements a,b,c such that $$ \neg (Rab\land Rbc) $$ I have already managed to show this from the premises, with only $$ Rab \land Rbc \rightarrow Rca $$ as undischarged premiss.

Answer 1

Suppose that $R\subseteq S\times S$ is a relation on $S$ that is irreflexive and transitive.

Now if $\langle x,y\rangle,\langle y,z\rangle,\langle z,x\rangle\in R$ then the transitivity of $R$ will lead to the conclusion $\langle x,x\rangle\in R$ contradicting that $R$ is irreflexive.

Our conclusion is that no elements $x,y,z\in S$ exist such that $\langle x,y\rangle,\langle y,z\rangle,\langle z,x\rangle\in R$.

In words: $R$ does not contain any $3$-cycles if it is irreflexive and transitive.

Answer 2

drhab's proof can be easily formalized:

$\def\fitch#1#2{\begin{array}{|l}#1 \\ \hline #2\end{array}}$

$\fitch{ 1. \forall x \ \neg R(x,x) \land \forall x \forall y \forall z((R(x,y) \land R(y,z)) \rightarrow R(x,z)) \quad \text{ Assumption}}{ 2.\forall x \ \neg R(x,x) \quad \land \text{ Elim} \ 1\\ 3.\forall x \forall y \forall z((R(x,y) \land R(y,z)) \rightarrow R(x,z)) \quad \land \text{ Elim} \ 1\\ \fitch{ 4. \exists x \exists y \exists z (R(x,y) \land R(y,z) \land R(z,x)) \quad \text{ Assumption}}{ \fitch{ 5. R(a,b) \land R(b,c) \land R(c,a)\quad \text{ Assumption}}{ 6. R(a,b) \land R(b,c) \quad \land \text{ Elim } 5\\ 7. (R(a,b) \land R(b,c)) \rightarrow R(a,c) \quad \forall \text{ Elim } 3\\ 8. R(a,c) \quad \rightarrow \text{ Elim } 6,7\\ 9. R(c,a) \quad \land \text{ Elim } 5\\ 10. R(a,c) \land R(c,a) \quad \land \text{ Intro } 8,9\\ 11. (R(a,c) \land R(c,a)) \rightarrow R(a,a) \quad \forall \text{ Elim } 3\\ 12. R(a,a) \quad \rightarrow \text{ Elim } 10,11\\ 13. \neg R(a,a) \quad \forall \text{ Elim } 2\\ 14. \bot \quad \bot \text{ Intro } 12,13}\\ 15. \bot \quad \exists \text{ Elim } 4, 5-14} \\ 16. \neg \exists x \exists y \exists z (R(x,y) \land R(y,z) \land R(z,x)) \quad \neg \text{ Intro } 4-15}$