13. Examples of Formal Proofs
We can use the formal proof system we have developed to revisit the axiomatic theories that we first considered semantically.
Group Theory
Recall that the set \(\Gamma_G\) of three sentences
\[\begin{align*} & \forall x \forall y \forall z (x \cdot (y \cdot z)) = ((x \cdot y) \cdot z) & \mbox{(Associativity)}\\ & \forall x \, ((x\cdot \mathbf{e}) = x \wedge (\mathbf{e} \cdot x) = x) & \mbox{(Identity)} \\ & \forall x \exists y \, ((x \cdot y) = \mathbf{e} \wedge (y \cdot x) = \mathbf{e}) & \mbox{(Inverse)} \end{align*}\]forms the group theory axioms. We can use formal proofs to establish a few theorems in the theory of \(\Gamma_G\).
The first proof is very short:
Theorem. \(\Gamma_G \vdash (\mathbf{e} \cdot \mathbf{e}) = \mathbf{e}\).
Proof.
1. ∀x ((x⋅e)=x) ⋀ (e⋅x)=x) PR 2. ((e⋅e)=e) ⋀ (e⋅e)=e) ∀E 1 3. (e⋅e)=e ⋀E 2
Other similarly basic theorems require longer proofs:
Theorem. \(\Gamma_G \vdash \forall x \, ((x \cdot x) = x \to x = \mathbf{e})\).
Proof.
1. ⎡ (g⋅g) = g AS 2. ⎢ ∀x ∃y ((x⋅y)=e ⋀ (y⋅x)=e) PR 3. ⎢ ∃y ((g⋅y)=e ⋀ (y⋅g)=e) ∀E 2 4. ⎢ ⎡ ((g⋅h)=e ⋀ (h⋅g)=e) AS 5. ⎢ ⎢ (g⋅h)=e ⋀E 4 6. ⎢ ⎢ ∀x ∀y ∀z (x⋅(y⋅z)) = ((x⋅y)⋅z) PR 7. ⎢ ⎢ ∀y ∀z (g⋅(y⋅z)) = ((g⋅y)⋅z) ∀E 6 8. ⎢ ⎢ ∀z (g⋅(g⋅z)) = ((g⋅g)⋅z) ∀E 7 9. ⎢ ⎢ (g⋅(g⋅h)) = ((g⋅g)⋅h) ∀E 8 10. ⎢ ⎢ (g⋅(g⋅h)) = (g⋅h) =E 1, 9 11. ⎢ ⎢ (g⋅e) = e =E 5, 10 12. ⎢ ⎢ ∀x ((x⋅e)=x) ⋀ (e⋅x)=x) PR 13. ⎢ ⎢ ((g⋅e)=g ⋀ (e⋅g)=g) ∀E 12 14. ⎢ ⎢ (g⋅e)=g ⋀E 13 15. ⎢ ⎣ g=e =E 14, 11 16. ⎣ g=e ∃E 3, 4-15 17. ((g⋅g)=g → g=e) →I 1-12 18. ∀x ((x⋅x)=x → x=e) ∀I 17
Another example of a basic theorem with a fairly long proof is the following.
Theorem. \(\Gamma_G \vdash \forall x \forall y \forall z ((x \cdot y) = (x \cdot z) \to y=z).\)
Proof.
1. ⎡ (g⋅h) = (g⋅i) AS 2. ⎢ ∀x ∃y ((x⋅y)=e ⋀ (y⋅x)=e) PR 3. ⎢ ∃y ((g⋅y)=e ⋀ (y⋅g)=e) ∀E 2 4. ⎢ ⎡ ((g⋅a)=e ⋀ (a⋅g)=e) AS 5. ⎢ ⎢ (a⋅g)=e ⋀E 4 6. ⎢ ⎢ (a⋅(g⋅h)) = (a⋅(g⋅h)) =I 7. ⎢ ⎢ (a⋅(g⋅h)) = (a⋅(g⋅i)) =E 1, 6 6. ⎢ ⎢ ∀x ∀y ∀z (x⋅(y⋅z)) = ((x⋅y)⋅z) PR 7. ⎢ ⎢ ∀y ∀z (a⋅(y⋅z)) = ((a⋅y)⋅z) ∀E 6 8. ⎢ ⎢ ∀z (a⋅(g⋅z)) = ((a⋅g)⋅z) ∀E 7 9. ⎢ ⎢ (a⋅(g⋅h)) = ((a⋅g)⋅h) ∀E 8 10. ⎢ ⎢ (a⋅(g⋅i)) = ((a⋅g)⋅i) ∀E 8 11. ⎢ ⎢ ((a⋅g)⋅h) = (a⋅(g⋅i)) =E 9, 7 12. ⎢ ⎢ ((a⋅g)⋅h) = ((a⋅g)⋅i) =E 10, 11 13. ⎢ ⎢ (e⋅h) = (e⋅i) =E 5, 12 14. ⎢ ⎢ ∀x ((x⋅e)=x) ⋀ (e⋅x)=x) PR 15. ⎢ ⎢ ((h⋅e)=h ⋀ (e⋅h)=h) ∀E 14 16. ⎢ ⎢ (e⋅h)=h ⋀E 15 17. ⎢ ⎢ ((i⋅e)=i ⋀ (e⋅i)=i) ∀E 14 18. ⎢ ⎢ (e⋅i)=i ⋀E 17 19. ⎢ ⎢ h = (e⋅i) =E 16, 13 20. ⎢ ⎣ h = i =E 18, 19 21. ⎣ h = i ∃E 3, 4-20 22. ((g⋅h)=(g⋅i) → h=i) →I 1-21 23. ∀z ((g⋅h)=(g⋅z) → h=z) ∀I 22 24. ∀y ∀z ((g⋅y)=(g⋅z) → y=z) ∀I 23 25. ∀x ∀y ∀z ((x⋅y)=(x⋅z) → y=z) ∀I 24
Peano Arithmetic
For a different kind of example, recall that the set \(\Gamma_{\mathrm{PA}}\) of Peano axioms for arithmetic include the two sentences
\[\begin{align*} & \forall x \, (x + \mathbf{0}) = x \quad \mbox{and} \\ & \forall x \forall y \, (x + S(y)) = S(x + y) \end{align*}\]as well as the induction axiom
\[(((0+0)=0 \wedge \forall x ((0+x)=x \to 0+S(x)=S(x))) \to \forall x 0+x=x).\]We can use these three axioms to establish the following basic theorem of arithmetic.
Theorem. \(\Gamma_{\mathrm{PA}} \vdash \forall x (\mathbf{0} + x) = x.\)
Proof.
1. ∀x (x+0) = x PR 2. (0+0) = 0 ∀E 1 3. ⎡ 0+n = n AS 4. ⎢ S(n) = S(n) =I 5. ⎢ S(0+n) = S(n) =E 3, 4 6. ⎢ ∀x ∀y (x+S(y)) = S(x+y) PR 7. ⎢ ∀y (0+S(y)) = S(0+y) ∀E 6 8. ⎢ (0+S(n)) = S(0+n) ∀E 7 9. ⎣ (0+S(n)) = S(n) =E 3, 8 10. ((0+n)=n → (0+S(n))=S(n)) →I 3-9 11. ∀x ((0+x)=x → (0+S(x))=S(x)) ∀I 10 12. ((0+0)=0 ⋀ ∀x ((0+x)=x → (0+S(x))=S(x))) ⋀I 2, 11 13. (((0+0)=0 ⋀ ∀x ((0+x)=x → (0+S(x))=S(x))) → ∀x (0+x)=x PR 14. ∀x (0+x)=x →E 13, 12
Similarly we can establish proofs for all of the sentences in the exercise at the end of Lecture 11.