Formal derivation of statement from Peano Arithmetic system

[cianfa72]

TL;DR

About the formal derivation of a (meta)-statement from axioms of Peano Arithmetic formal system

I was reading a Bachelor thesis on Peano Arithmetic (PA). PA has the following axioms (not including the induction schema):
$$\begin{align}
& (A1) ~~~~ \forall x \neg (x + 1 = 0) \nonumber \\
& (A2) ~~~~ \forall xy (x + 1 =y + 1 \to x = y) \nonumber \\
& (A3) ~~~~ \forall x (x + 0 = x) \nonumber \\
& (A4) ~~~~ \forall xy (x + (y +1) = (x + y ) + 1) \nonumber \\
& (A5) ~~~~ \forall x (x \cdot 0 = 0) \nonumber \\
& (A6) ~~~~ \forall xy (x \cdot (y + 1) = (x \cdot y) + x) \nonumber
\end{align}
$$
The thesis claims the (meta)-statement $\text{PA} \vdash \varphi(0)$ where $\varphi(z)$ is the open well-formed formula (wff) $$\forall xy (x + (y + z) = (x + y) + z)$$ However I'm not sure how, from a formal viewpoint, it follows from axiom A3. Can you kindly help me ?

 

[mad mathematician]

You need to use induction on z and to invoke an instance of A4.

 

[cianfa72]

You need to use induction on z and to invoke an instance of A4.

Sorry, could you be more explicit about this ? Thanks.

 

[mad mathematician]

You want to use A4 to prove associativity of addition, so
we have for z=1: (x+y)+1=x+(y+1) this is an instantiation of axiom A4.
Now we use induction: suppose for z=n we have (x+y)+n=x+(y+n), now for z=n+1 we get: ((x+y)+(n+1))=((x+y)+n)+1=(x+(y+n))+1=x+((y+n)+1)=x+(y+(n+1)).
In the first equality (lhs) I used instantiation of A4, in the second equality it's the hypothesis of induction, the third equality is another instantiation of A4, and also the last equality is an instantiation of A4.

So we proved the associative of addition in PA, i.e $\varphi(z)$, $\varphi(0)$ is just the claim that x+y=x+y, which follows as always from reflexivity of '=', identity.

 

[cianfa72]

You want to use A4 to prove associativity of addition, so
we have for z=1: (x+y)+1=x+(y+1) this is an instantiation of axiom A4.
Now we use induction: suppose for z=n we have (x+y)+n=x+(y+n), now for z=n+1 we get: ((x+y)+(n+1))=((x+y)+n)+1=(x+(y+n))+1=x+((y+n)+1)=x+(y+(n+1)).
In the first equality (lhs) I used instantiation of A4, in the second equality it's the hypothesis of induction, the third equality is another instantiation of A4, and also the last equality is an instantiation of A4.

Sorry just to be sure: what you said in bold is an instance of axiom A4, you meant that formally (x+y)+1=x+(y+1) is the instance of A4 where the name of variables entering it are actually x and y. Furthermore the universal closure $\forall xy$ (or $\forall x \forall y$) is implicitly understood.

On the other hand, for the first equality (LHS) you used the instantiation of A4 where the variables' name are (x + y) and n respectively (note that n should be actually a standard numeral term of the underlying formal language).

So we proved the associative of addition in PA, i.e $\varphi(z)$, $\varphi(0)$ is just the claim that x+y=x+y, which follows as always from reflexivity of '=', identity.

Ah ok, that's right. However that thesis claims that $PA \vdash \varphi(0)$ follows from axiom A3 (i.e. there is a formal proof from it), I don't see how though...

 

[mad mathematician]

Sorry just to be sure: when you said in bold is an instance of axiom A4, you meant that formally (x+y)+1=x+(y+1) is the instance of A4 where the name of variables entering it are actually x and y. Furthermore the universal closure $\forall xy$ (or $\forall x \forall y$) is implicitly understood.


Ah ok, that's right. However that thesis claims that $PA \vdash \varphi(0)$ follows from axiom A3 (i.e. there is a formal proof from it), I do not see why though...

In my derivation I forgot to mention that I use y+0=y; acknowledged we proved already x+(y+z)=(x+y)+z plug z=0, and get: x+(y+0)=(x+y)+0; now from the axiom A3 we have: y+0=y and (x+y)+0=(x+y), and you proved that also $\varphi(0)$ follows from A3.

 

[cianfa72]

In my derivation I forgot to mention that I use y+0=y; acknowledged we proved already x+(y+z)=(x+y)+z plug z=0, and get: x+(y+0)=(x+y)+0; now from the axiom A3 we have: y+0=y and (x+y)+0=(x+y), and you proved that also $\varphi(0)$ follows from A3.

From my understanding, using the Hilbert-style proof system (no natural deduction system), we have:

line 1: $\forall y (y+0=y)$ is an instantiation of A3 axiom schema where the placeholder entering it is instantiated using $y$

line 2: $\forall xy ((x+y)+0=x+y)$ is an instantiation of A3 axiom schema where the placeholder entering it is instantiated using $x + y$

line 3: $\forall xy (y+0=y \to x + (y+0) = x + y)$ is an instantiation of substitution axiom schema $\forall ab (a=b \to F(a) = F(b))$ with $F(t) = x + t$ where placeholders entering it are $y+0$ and $y$ respectively.

line 4: by MP inference rule on line 1,3 we get $\forall xy (x + (y+0) = x +y)$

line 5: $\forall xy ( (x+y)+0 = x+y) \to ( (x+y = x + (y+0)) \to ((x+y)+0 = x+(y+0) ) ) )$ is an instantiation of transitivity of equality axiom scheme $\forall pqr ( (p = q) \to ( (q = r) \to (p = r) ) )$ where the placeholders are $p: \forall xy ((x+y)+0)$, $q: \forall xy (x+y)$, $r: \forall xy (x + (y+0))$.

line 6: by MP applied twice on line 2,5,4 then $\forall xy (x+(y+0)=(x+y)+0)$ follows, i.e. $\varphi(0)$.

 

[mad mathematician]

When you say that you use a Hilbert system without natural deduction, do you mean that you can't use rules that are specific to the quantifiers? such as universal elimination etc.
A rigorous and exact solution will be to eliminate a quantifier and after that introduce a quantifier.
BTW, I am pretty sure the software tarski or chatGPT can handle the proof of this claim with ease.

 

[berkeman]

Thread is closed for Moderation.

 

[PeterDonis]

Thread reopened after a post with an unacceptable reference (ChatGPT) has been deleted.

 

[cianfa72]

After reviewing it, this is my formal deduction of the sentence $\varphi(0)$ in first-order Peano Arithmetic (PA) formalized by using Hilbert-style proof (or deduction) system.

PA non-logical axiom schemas:
(A1) ∀z (z + 0 = z) - addition zero axiom
(A2) u = v → (w + u = w + v) - equality substitution axiom schema for function +
(A3) u = v → v = u - equality symmetry axiom schema
(A4) (u = v ∧ v = w) → u = w - equality transitivity axiom schema

Hilbert-style inference rules:
(I1) Modus Ponens MP
(I2) Universal Instantiation UI
(I3) Universal Generalization UG

Formal deduction of $\varphi(0)$ :

1. ∀z (z + 0 = z)
   PA axiom (Addition zero axiom)
2. y + 0 = y
   from (1) by Universal Instantiation (UI) with term y (by UI instantiation of ∀z (z+0=z) with z := y)
3. x + (y + 0) = x + y
   from (2) and the equality substitution (congruence) axiom by MP. Equality substitution axiom schema’s instance y + 0 = y → (x + (y + 0) = x + y) (by substituting u := y+0, v := y, w := x); from (2) apply MP to infer the wff.
4. (x + y) + 0 = x + y
   from (1) by UI with term x + y (by UI instantiation of ∀z (z+0=z) with z := x + y)
5. x + y = (x + y) + 0
   from (4) and Equality symmetry axiom schema’s instance (by substituting u:= (x+y)+0, v:= x+y) apply MP to infer the wff.
6. x + (y + 0) = (x + y) + 0
   from (3) and (5) by Equality transitivity axiom schema’s instance (by substituting u:= x + (y + 0), v:= x + y, w:= (x + y) + 0) apply MP to infer the wff.
7. ∀y ( x + (y + 0) = (x + y) + 0 )
   from (6) by Universal Generalization (UG) on y (y is not free in any open assumption (none are), so UG is permitted)
8. ∀x ∀y ( x + (y + 0) = (x + y) + 0 )
   from (7) by UG on x (x is not free in any open assumption (none are), so UG is permitted)

Line 8 is indeed $\varphi(0)$ :

Some points to highlight:

• the list of PA arithmetic axiom schemas are at metalanguage level, so u,v,w are metavariables acting as placeholders for object-language terms (i.e. for constant, variables, functions and wffs of PA object language).
• The instantiation of an axiom schema isn't obtained by applying UI inference rule. It is rather a syntactic substitution at metalanguage level.

Do you think I got it right ?