Creating a formal system which corresponds to multiplication (of natural numbers)

Question

I've begun studying mathematical logic with Hodel's 'An Introduction to Mathematical Logic', and have just learnt about formal systems and their components. In the textbook, Hodel gives as an example of a formal system the system 'ADD', whose theorems correspond to true statements about addition; it is defined as follows:

• Symbols: $| \,,+,=$
• Formulae: statements of the form $x+y=z$ where $x,y$, and $z$ are expressions in $|$
• Axiom: $|+|=||$
• Rules of Inference: $\frac{x+y=z}{x|+y=z|}$ (R1) and $\frac{x+y=z}{y+x=z}$ (R2)

As an exercise (exercise 3 of section 1.3 for those with the book), Hodel then asks the reader to create a formal system 'MULT', which has theorems corresponding to our standard notions of multiplication; he also asks the reader to prove within this system that $|| \times ||| = ||||||$.

I believe I have a solution to this, but I would be grateful if someone wouldn't mind checking it for me - I'm new to this area of maths so want to make sure my fundamentals are strong. My system is defined as follows:

• Symbols: $|\, , \times, + , =$
• Formulae: statements of the form $x\times y = z$ or $x+y=z$ where $x, y,$ and $z$ are expressions in $|$
• Axioms: $|+|=||$ (A1) and $| \times x = x$ (A2)
• Rules of inference: $\frac{x+y=z}{x|+y=z|}$ (R1), $\frac{x+y=z}{y+x=z}$ (R2), $\frac{x\times y=z}{x|\times y=z+y}$ (R3), and $\frac{x\times y=z}{y\times x=z}$ (R4)

and my proof that $\vdash_{\text{MULT}}|| \times ||| = ||||||$:

1. $|\times||=||$ (A2)
2. $||\times || = ||+||$ (R3)
3. $|+|=||$ (A1)
4. $||+| = |||$ (R1)
5. $|+|| = |||$ (R2)
6. $||+|| = |||| = || \times || $(R1 and step 2)
7. $||| \times || = ||||+||$ (R3)
8. $|| + || = ||||$ (step 6 and previous)
9. $||||+|| = |||||| = ||| \times ||$ (R1 twice and step 7)
10. $ || \times ||| = ||||||$ (R4) $\square$

What makes me doubt whether this is the simplest solution is that I have included all of ADD within my new system, however I suppose this does reflect how multiplication is defined in terms of iterated addition.

Improvements, corrections, and other solutions welcomed and greatly appreciated :)

Answer 1

Here's a solution: Reformulate A2 as: I x I = I. Then, the proof goes as follows:

1. I x I = I (A2)

2. II x I = II (R3)

3. III x I = III (R3)

4. I x III = III (R4)

5. II x III = IIIIII (R3)

Answer 2

Here is my solution:

• Symbols: $|, \cdot, =$
• Formulas of the form $a\cdot b = c$
• Axiom: $|\cdot|=|$
• Rules of inference: $\frac{a\cdot b = c}{a|\cdot b = b c} $ (R1) and $ \frac{a\cdot b = c}{a\cdot b| = ac}$ (R2)

Here is the proof:

1. $|\cdot|=|$ (Axiom)
2. $||\cdot|=||$ (R1)
3. $||\cdot||=||||$ (R2)
4. $||\cdot|||=||||||$ (R2)

Q.E.D.