Prove in formal arithmetic: $\neg\exists x.x + \overline{3} = \overline{2}$

Question

I don't know how to convert such kind of expressions $\neg\exists x.P(x)$. Can anybody help me?

Prove in formal arithmetic: $\neg\exists x.x + \overline{3} = \overline{2}$ .

UPD: Everything I've achieved so far. Thanks to the people in the comments below, I know, that it is equivalent to $\forall x.\neg(x +\overline{3} = \overline{2}$)

Let's prove it by induction:

1. $P(0)$. Really, $\forall x.\neg(\overline{3} = \overline{2})$ is true.
2. I know, that $\forall x.P(x)$, where $P(x) = \neg(x + \overline{3} = \overline{2}).$ I need to prove it for $P(x') = (\neg(x + \overline{3} = \overline{2})).$

$P(x') = \neg(x' + \overline{3} = \overline{2}) = \neg((x + \overline{3})' = \overline{2})$ . How can I use here $P(x)$?

Axioms that can be used:

$(A1)\ a=b \to a=c \to b=c$

$(A2)\ a=b \to a'=b'$

$(A3)\ a'=b' \to a=b$

$(A4)\ \neg a' = 0$

$(A5)\ a+0 = a$

$(A6)\ a+b' = (a+b)'$

$(A7)\ a\cdot 0 = 0$

$(A8)\ a\cdot b' = a \cdot b + a$

Also allowed predicate-logic axioms and first-order-logic axioms.

Answer 1

You don't need induction. Just do a proof by contradiction.

For simplicity I am going to use $0,1,2,3$ where $1=0', 2=1'$, and $3 = 2'$.

OK, let's assume $\exists x \ x + 3 = 2$. So, for some $a$:

$a + 3 = 2$

$a + 2' = 1'$ (by def. $3=2'$ and $2 = 1'$)

$(a+2)' = 1'$ (using $A6$ (I suppose you'll need $A1$ as well to make this super formal ... goes for most of next steps as well))

$a + 2 = 1$ (using $A3$)

$a+1' = 0'$ (by def. $2=1'$ and $1 = 0'$)

$(a+1)' = 0'$ (using $A6$)

$a + 1 = 0$ (using $A3$)

$a+0' = 0$ (by def. $1 = 0'$)

$(a+0)' = 0$ (using $A6$)

$\neg \ (a+0)' = 0$ ($A4$)

contradiction!

So, we run into a contradiction if we assume $\exists x \ x + 3 = 2$, and therefore $\neg \exists x \ x + 3 = 2$