Natural deduction, true implies something Show by natural deduction
$$T \implies (\exists y (y + y = 2x))$$.
How do I begin a natural deduction proof like this?  I am given the premise true, but I don't see how to proceed?
 A: Hint
We need the first-order axioms for arithmetic; see Peano axioms.
1) $2x=x \cdot S(1)$ --- by definition of $2$
2) $x \cdot S(1) = (x \cdot 1)+x$ --- by 2nd Ax for mult
3) $(x \cdot 1) + x = (x \cdot S(0)) + x$ --- by def of $1$
4) $(x \cdot S(0)) + x = [(x \cdot 0)+x] + x$ --- by 2nd Ax for mult
5) $[(x \cdot 0)+x] + x = (0+x)+x$ --- by 1st Ax for mult
6) $(0+x)+x = x+x$ --- by 1st Ax for sum
In conclusion, by transitivity of $=$ :

7) $2x=x+x$.

8) $\exists y \ (2x=y+y)$ --- by $\exists$-intro


$\top \to \exists y \ (2x=y+y)$ --- by $\to$-intro.


Let $\mathsf {PA}$ the collection of Peano axioms; the above proof shows that:

$\mathsf {PA} \vdash \top \to \exists y \ (2x=y+y)$.

A: The expression you're trying to prove is equivalent to
$$(\forall y)(y+y\neq2x)\implies\lnot T$$
Now, to prove this:
$$(\forall y)(y+y\neq2x)\implies x+x\neq 2x\implies\lnot T$$
Note you need to justify $(\forall x)(x+x=2x)$ which depending on what you can assume may be able to just be taken for granted.
A: Existential Introduction doesn't require that all the variables of the expression be bound by the quantifier. Therefore:
\begin{array}{l}
& x+x=x+x & \text{ Identity Introduction }\\
& x+x = 2x & \text{ Addition }\\
& \exists y[y+y=2x] & \text{ Existential Introduction }\\
\end{array}
