Natural deduction, true implies something

Question

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?

Answer 1

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.

Answer 2

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

Answer 3

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}