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$ – Mees de Vries Jan 25 at 14:21


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 Jan 25 at 15:45
  • $\begingroup$ @roi_saumon - I'm going up-down. From the premises to the conclusion. $\endgroup$ – Mauro ALLEGRANZA Jan 25 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)}$$


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.