1
$\begingroup$

I have to use natural deduction on the following 2 sequents: $$t_1=t_2 \vdash (t+t_1)=(t+t_2)$$ $$(x=0)\lor ((x+x)>0)\vdash (y=(x+x))\to ((y>0)\lor (y=0+x))$$

At first I thought that the first one is pretty easy, but I am stuck. $$t_1=t_2 \vdash (t+t_1)=(t+t_2)$$ $t_1=t_2 \qquad \qquad \qquad \qquad \text{premise} \\ (t+t_1)=(t+t_1)\qquad \qquad =_i \\ (t+t_2)=(t+t_2) \qquad \qquad =_e 1,2 \\ $

Now I am stuck at this point. I also tried to use $\lor_e$ after $\lor_i$, but I dont know how i can prove that.

The second one is a bit harder, but I have an idea. $$(x=0)\lor ((x+x)>0)\vdash (y=(x+x))\to ((y>0)\lor (y=0+x))$$ $(x=0)\lor ((x+x)>0) \qquad \qquad \ \ \text{premise} \\ \\ \_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\_\ \\ (y=(x+x)) \qquad \qquad \qquad \qquad \text{assumption}$

The next step is the $\lor_e$ , where i want to show that $(x=0)\to y>0$ and $((x+x)> 0)\to y>0)$. But that is impossible, since the first implication never holds.

Can somebody help me with my problem?

Thank you

$\endgroup$
1
$\begingroup$

For the first one :

1) $\vdash t+t_2=t+t_2$ --- by $=$-intro

2) $t_1=t_2 \vdash t_2=t_1$ --- from 1) by $(=\text{symmetric})$ : $s=t \vdash t=s$, derivable with $=$-intro and $=$-elim

3) $t_2=t_1, \ t+t_2=t+t_2 \ \vdash t+t_1=t+t_2$ --- by $=$-elim : $s=t, ϕ[s/x] \vdash ϕ[t/x]$, with $s,t$ terms substitutable for $x$ in $ϕ$, and $ϕ$ a formula : use $t+x=t+t_2$ as $ϕ$, $t_2$ as $s$ and $t_1$ as $t$.

4) $t_1=t_2 \ \vdash t+t_1=t+t_2$ --- from 1), 2) and 3).

Note : the same derivation can be used for any term $r$; thus we can generalize it to the derived rule: $(=\text{term})$ : $s=t \vdash r[s/x]=r[t/x]$.


For the 2nd one, we can split it into two sub-derivations:

1) $x=0, \ y=x+x \vdash y=0+x$ --- by $=$-elim, with $y=z+x$ as $ϕ$

2) $x=0, \ y=x+x \vdash (y >0) \lor (y=0+x)$ --- from 1) by $\lor$-intro

3) $x=0 \vdash (y=x+x) \to ((y >0) \lor (y=0+x))$ --- from 2) by $\to$-intro.

In the same way, we can derive :

4) $(x+x)>0 ⊢ (y=x+x) → ((y>0) ∨ (y=0+x))$

and then conclude by $\lor$-elim from : $(x=0) \lor (x+x)>0$.

$\endgroup$
1
$\begingroup$

You write:

At first I thought that the first one is pretty easy, but I am stuck. $$t_1=t_2 \vdash (t+t_1)=(t+t_2)$$ $t_1=t_2 \qquad \qquad \qquad \qquad \text{premise} \\ (t+t_1)=(t+t_1)\qquad \qquad =_i \\ (t+t_2)=(t+t_2) \qquad \qquad =_e 1,2 \\ $

Actually, it's very easy: when doing $=_e$ using $t_1=t_2$, you do not have to replace all instances of $t_1$ with $t_2$: you can just replace some of them. So, if you just replace the second $t_1$ in $(t+t_1)=(t+t_1)$ with $t_2$, you end up with the desired conclusion:

$t_1=t_2 \qquad \qquad \qquad \qquad \text{premise} \\ (t+t_1)=(t+t_1)\qquad \qquad =_i \\ (t+t_1)=(t+t_2) \qquad \qquad =_e 1,2 \\ $

$\endgroup$

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.