Natural Deduction Proof that irreflexive, transitive relations on a Set S are not three-cycles 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.
 A: 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.
A: 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}$
