I Formal derivation of statement from Peano Arithmetic system

[cianfa72]

TL;DR Summary

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.

 

[cianfa72]

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.

No, I meant Hilbert-style proof system hence not natural deduction system. Therefore rules (or axiom schemes) for Universal Instantiation UI (aka Universal Elimination) and Universal Generalization UG (aka Universal Introduction) are included as well.

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.

Good, I asked chatGPT for this.

Axioms / Schemas and Rules used​

1. Addition zero axiom (PA): ∀z ( z + 0 = z ).
2. Equality substitution (congruence) schema (for + in second argument): for any terms u,v,w
   u = v → ( w + u = w + v ).
   (We will apply instances of this schema; this is a standard equality congruence axiom.)
3. Equality symmetry: a = b → b = a.
4. Equality transitivity: (a = b ∧ b = c) → a = c.
   (In Hilbert systems you may treat transitivity as derivable from equality axioms; I cite it as a step.)
5. Logical rules: Modus Ponens (MP), Universal Instantiation (UI): from ∀z φ(z) infer φ(t) for any term t, and Universal Generalization (UG): from φ(v) infer ∀v φ(v) provided v is not free in any open assumption.

Formal derivation (numbered)​

1. ∀z ( z + 0 = z ).
   justification: PA axiom (Addition zero).
2. y + 0 = y.
   justification: from (1) by Universal Instantiation (UI) with term y.
   (Instance: apply ∀z (z+0=z) to z := y.)
3. x + (y + 0) = x + y.
   justification: from (2) and the equality substitution (congruence) axiom by MP.
   • More precisely: take the congruence axiom instance (y + 0) = y → ( x + (y + 0) = x + y ) (choose u := y+0, v := y, w := x).
   • From (2) and that instance, apply MP to get the displayed formula.
4. (x + y) + 0 = x + y.
   justification: from (1) by UI with term x + y.
   (Instance: apply ∀z (z+0=z) to z := x + y.)
5. x + y = (x + y) + 0.
   justification: from (4) by Equality Symmetry (instance: (x+y)+0 = x+y → x+y = (x+y)+0), apply MP.
6. x + (y + 0) = (x + y) + 0.
   justification: from (3) and (5) by Equality Transitivity.
   • We have x + (y + 0) = x + y (line 3) and x + y = (x + y) + 0 (line 5).
   • Using transitivity we infer x + (y + 0) = (x + y) + 0.
7. ∀y ( x + (y + 0) = (x + y) + 0 ).
   justification: from (6) by Universal Generalization (UG)on y.
   • Side condition: y is not free in any open assumption (none are), so UG is permitted.
8. ∀x ∀y ( x + (y + 0) = (x + y) + 0 ).
   justification: from (7) by UGon x.
   • Again side conditions hold.

Line 8 is exactly the desired formula. QED.

---

Remarks (about subtle points)

• Steps 2 and 4 are UI applications of the single addition-zero axiom ∀z (z+0=z). This is the Universal Instantiation rule (UI), not a separate "axiom instance" in the sense of schema substitution — though some presentations blur the distinction because ∀z φ(z) is an axiom schema and one commonly writes down its instance φ(t). I have written both the axiom and the UI steps explicitly to avoid that ambiguity.
• The equality substitution step (line 3) used an instance of the equality congruence axiom for + (substituting equal terms into a function’s argument). In a precise Hilbert system this is either an axiom schema or derived from equality axioms; I treated it as the usual axiom instance: (y+0)=y → (x+(y+0)=x+y).
• UG was applied only to formulas derived purely from axioms (no extra assumptions), so the usual side-conditions for UG are satisfied.

As far as I can tell, Universal Instantiation UI applies only to axioms (well-formed formulas in the object language) to get an axiom instantiated using terms from the object language (i.e. UI doesn't apply to axiom schemes at all).

Regarding axiom schemes, instead, since they are basically templates with placeholder variables, one can substitute terms and/or formulas (from the object language) for the schema placeholder variables to get an axiom scheme's instance.

 

[berkeman]

Thread is closed for Moderation.