Natural deduction predicate logic for equality

Question

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

Answer 1

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