Formal Proof in Peano Arithmetic that exp(3,2) = 9

Language & Numerals

• Constant: 0
• Function symbols: S(x), +(x,y), ⋅(x,y), exp(x,y)
• Numerals:
  • 1 ≔ S(0)
  • 2 ≔ S(S(0))
  • 3 ≔ S(S(S(0)))
  • 9 ≔ S(S(S(S(S(S(S(S(S(0)))))))))

---

Axioms of PA

Addition

1. ∀x [x + 0 = x]
2. ∀x ∀y [x + S(y) = S(x + y)]

Multiplication

1. ∀x [x ⋅ 0 = 0]
2. ∀x ∀y [x ⋅ S(y) = x ⋅ y + x]

Exponentiation

1. ∀x [exp(x,0) = 1]
2. ∀x ∀y [exp(x,S(y)) = exp(x,y) ⋅ x]

---

Proof of exp(3,2) = 9

Let a ≔ 3, b ≔ 2, c ≔ 9.

Phase 1: Show exp(a,1) = 3

1. From exponentiation axiom (instantiate x≔a): exp(a,0) = 1.
2. From exponentiation axiom (instantiate x≔a,y≔0): exp(a,1) = exp(a,0) ⋅ a = 1 ⋅ 3.
3. Compute 1 ⋅ 3 via multiplication and addition:
   1. 1 ⋅ 0 = 0
   2. 1 ⋅ 1 = (1 ⋅ 0) + 1 = 0 + 1 = 1
   3. 1 ⋅ 2 = (1 ⋅ 1) + 1 = 1 + 1 = 2
   4. 1 ⋅ 3 = (1 ⋅ 2) + 1 = 2 + 1 = 3
4. Therefore exp(a,1) = 3.

Phase 2: Show exp(a,2) = 9

1. From exponentiation axiom (instantiate x≔a,y≔1): exp(a,2) = exp(a,1) ⋅ a = 3 ⋅ 3.
2. Compute 3 ⋅ 3 via multiplication and addition:
   1. 3 ⋅ 0 = 0
   2. 3 ⋅ 1 = (3 ⋅ 0) + 3 = 0 + 3 = 3
   3. 3 ⋅ 2 = (3 ⋅ 1) + 3 = 3 + 3 = 6
   4. 3 ⋅ 3 = (3 ⋅ 2) + 3 = 6 + 3 = 9
3. Therefore exp(a,2) = 9.

---

Conclusion

We have derived in PA:

exp(S(S(S(0))), S(S(0))) = S(S(S(S(S(S(S(S(S(0)))))))))

That is, 3² = 9.