I have some trouble with proving stuff with natural deduction formalism. Let $R$ be a binary relation. For instance I want to prove
$\phi,\psi \vdash \theta$
$\phi : \forall x \forall y \forall z ((R(x,y) \wedge R(y,z) \rightarrow R(x,z))$. (i.e. $R$ is transitive).
$\psi : \forall x \neg R(x,y)$. (i.e. $R$ is irreflexive).
$\theta : \forall x \forall y (R(x,y) \rightarrow \neg R(y,x))$. (meaning $R$ is asymmetric).

So I first try to make a usual proof :
1) Assume $R$ is not antisymmetric. So $\exists x \exists y R(x,y)\wedge R(y,x)$.
2)But one assumption is that $R$ is transitive so $\exists x R(x,x)$.
3)$\exists x R(x,x)$ and $\psi$ produce a contradiction $\bot$.

But then I don't get how to translate each step in natural deduction.


so fist I assume $\theta$ is wrong so I think I should start by using the classical absurd :

${\phi,\psi,\neg \theta \vdash \bot}$
$\overline{\phi,\psi \vdash \theta}$

then with some steps I don't really know, I should have :

${\phi, \psi, (R(a,b) \wedge R(b,a)) \vdash \bot}$
$\overline{\phi, \psi, \exists x \exists y (R(x,y) \wedge R(y,x)) \vdash \bot}$
. . .

$\overline{\phi,\psi,\neg \theta \vdash \bot}$
$\overline{\phi,\psi \vdash \theta}$

also how do you eliminate the double $\exists$ on the left of the sequent?

  • $\begingroup$ At which step of the translation do you get stuck? Do you know how to work with natural deduction? $\endgroup$ Commented Jan 25, 2019 at 14:21

2 Answers 2



Start from assumption 1) : $∃x∃y(R(x,y)∧R(y,x))$ and apply double $\exists$-elim :

2) $R(a,b) ∧ R(b,a)$ --- assumed for $\exists$-elim.

From transitivity ($\phi$), by $\forall$-elim, we get :

3) $R(a,b) ∧ R(b,a) → R(a,a)$.

Thus, with 2) :

4) $R(a,a)$.

From irreflexivity ($\psi$ : you have a typo) we get, by $\forall$-elim :

5) $\lnot R(a,a)$.

Now we have a contradiction : $\bot$ and we can close the double $\exists$-elim deriving :

6) $\bot$.

In this way we have : $\lnot ∃x∃y(R(x,y)∧R(y,x))$.

Now we are left with the boring part : to derive the equivalent $∀x∀y(R(x,y) → ¬R(y,x)$.

  • $\begingroup$ In the deduction tree, are you going from up to down or from down to up (see edit)? $\endgroup$
    – roi_saumon
    Commented Jan 25, 2019 at 15:45
  • $\begingroup$ @roi_saumon - I'm going up-down. From the premises to the conclusion. $\endgroup$ Commented Jan 25, 2019 at 17:16


also how do you eliminate the double ∃ on the left of the sequent?

Do not even introduce existentials.   You are not dealing with existential witnesses but arbitrary terms.

$\phi,\psi,$ and $\theta$ are each composed only of universal quantified statements.   That contraindicates pulling existential rules out of the toolbox.

Rather your proof should be structured around universal eliminations and universal introductions.   Work entirely with these arbitrary assumptions.

Now, there is a negation elimination/introduction involved (a proof of contradiction), but that is best placed within the context of those arbitrary assumptions.

Here is the skeleton of the fitch style proof. $$\def\R{\mathrm R}\fitch{\forall x\forall y\forall z~(x\R y\land y\R z\to x\R z)\\\forall x~\lnot x\R x}{\fitch{[a]}{\fitch{[b]}{\fitch{a\R b}{\fitch{b\R a}{a\R b\land b\R a\\\vdots\quad\text{somehow}\\\bot}\\\lnot b\R a}\\a\R b\to\lnot b\R a}\\\forall y~(a\R y\to \lnot y\R a)}\\\forall x\forall y~(x\R y\to\lnot y\R x)}$$


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .