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.

  • $\begingroup$ In your title you speak of irreflexive transitive sets. That is confusing. You most probably mean irreflexive transitive relations. I have never heard of irreflexive sets. I have heard of transitive sets, but those are sets $x$ that satisfy $z\in y\in x\implies z\in x$. $\endgroup$ – drhab Jun 10 '18 at 11:08
  • $\begingroup$ I am sorry, yes, the error is in the wording. I will correct it $\endgroup$ – JPR Jun 10 '18 at 11:12
  • 1
    $\begingroup$ I found my mistake. The formalization of no three-cycle is not $$\forall x \forall y \forall z \neg (Rxy \land Ryz \rightarrow Rzx)$$, but $$\forall x \forall y \forall z \neg (Rxy \land Ryz \land Rzx)$$ $\endgroup$ – JPR Jun 10 '18 at 14:29

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.


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}$


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.