Proving the conjecture ∀x.x+0=x with some predefined axioms

Question

I saw this problem:

$$∀x.x+0=x $$

in a introduction to logic text book but I am unsure how to go about solving it.

The book provides the following axioms:

$A1: nat(0)$

$A2: nat(T) ⊢ nat(s(T))$

$A3: nat(T), nat(U) ⊢ nat(T+U)$

$A4: nat(T), nat(U) ⊢ nat(T · U)$

$A5: 1=s(0)$

$A6: ∀x. 0+x=x$

$A7: ∀x.∀y.s(x)+y=s(x+y)$

$A8: ∀x.0·x = 0$

$A9: ∀x.∀y.s(x)·y = y + x · y$

---

Here is my attempt so far, if it is totally on the wrong track feel free to start from scratch :)

    __________________
  1.| nat(a)          | assumption
  2.| nat(0)          | A1 nat(0)
  3.| ∀x1. 0+x1=x1    | A6 ∀x.0+x=x
  4.| 0+a=a           | ∀-elim 3,1
  5.| 0+a=0+a         | =-into              
  6.| a=0+a           | =-elim-1 5,4
  7.| a=a             | =-intro
    | ...             |
  8.| a=a+0           | 
  9.| a+0=a           | =-elim-1 7,8
     ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
 10.  ∀x.x+0=x          ∀-intro 1-7

Thank you guys especially @Brams28 I have managed to prove it using induction

Answer 1

To be complete there should be something to tell us the names of the naturals generated by $A2$, I'll call it $N2$ in the following (i.e. $2=s(1)$, $3=s(2)$, etc.)

But anyway, I think this can be done by repeated usage of $A6,A7$ (and of course $A1,A2,A3$ as they are constantly used by the process described below, I will not mention them explicitely).

$1+0\ \stackrel{N2}=\ s(0)+0\ \stackrel{A7}=\ s(0+0)\ \stackrel{A6}=\ s(0)\ \stackrel{N2}=\ 1\tag{B1}$

$2+0\ \stackrel{N2}=\ s(1)+0\ \stackrel{A7}=\ s(1+0)\ \stackrel{B1}=\ s(1)\ \stackrel{N2}=\ 2\tag{B2}$

$3+0\ \stackrel{N2}=\ s(2)+0\ \stackrel{A7}=\ s(2+0)\ \stackrel{B2}=\ s(2)\ \stackrel{N2}=\ 3\tag{B3}$

and so on either directly until we reach $x$...

or by induction: $s(x)+0\ \stackrel{A7}=\ s(x+0)\ \stackrel{induction}=\ s(x)$

---

@GrahamKemp

$1.x=x$ can be deducted from $1.y\ \stackrel{N2}=\ s(0).y\ \stackrel{A9}=\ y+0.y\ \stackrel{(*)}=\ y+0\ \stackrel{B\infty}=\ y$

And for $(*)\ :\ 0.y=0$ we do like we have done by induction for $+$ but this time for $\times$ starting from repeated usage of $A8,A9$.

Answer 2

Use $A9$ and $\forall \textsf{elim}$ twice to get $s(0)\cdot a = a+ 0\cdot a$, then use $A5$ and $\forall\text{elim}$ on $A8$ to get $1\cdot a=a+0$.

However, do you have any axiom telling you that $\forall x.1\cdot x=x$ ?

Answer 3

Something is going wrong here. $\forall x.\ x + 0 = x$ is not provable in your system.

The given axioms are in effect a fragment of the standard weak "Robinson Arithmetic", so called Q (actually yours is the mirror image that you get by reversing the usual order of terms of an addition and of a multiplication, but let's not fuss about that).

Famously,not even full Q (in your mirror version), so with your axioms $\forall x.\ 0 + x = x$ etc., can prove $\forall x.\ x + 0 = x$.

There's a simple model-theoretic proof of this: see, for example, my Introduction to Godel's Theorems (CUP, 2nd edn), Theorem 10.8. (The idea is that you take the standard numbers, and add a couple of rogue elements to get a model that still makes axioms true, but the behaviour of the rogue elements makes addition non-commutative. But judging from the OP's comments on another answer, I don't think going into details will be helpful right here.)