translating a usual proof into natural deduction.

Question

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$
Where
$\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.

edit

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?

Answer 1

Hint

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)$.

Answer 2

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

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