Multiplication of Natural Numbers is Provable
Theorem
Let $x, y \in \N$ be natural numbers.
Then there exists a formal proof of:
- $\sqbrk x \times \sqbrk y = \sqbrk {x \times y}$
in minimal arithmetic, where $\sqbrk a$ is the unary representation of $a$.
Proof
By Unary Representation of Natural Number, let $\sqbrk a$ denote the term $\map s {\dots \map s 0}$, where there are $a$ applications of the successor mapping to the constant $0$.
Proceed by induction on $y$.
Base Case
Let $y = 0$.
Then $\sqbrk y = 0$.
The following is a formal proof:
By the tableau method of natural deduction:
Line | Pool | Formula | Rule | Depends upon | Notes | |
---|---|---|---|---|---|---|
1 | $\forall a: a \times 0 = 0$ | Axiom $\text M 5$ | ||||
2 | $\sqbrk x \times 0 = 0$ | Universal Instantiation |
But $x \times 0 = 0$.
Therefore, $\sqbrk {x \times 0} = \sqbrk 0$.
Thus, the proof above is a formal proof of $\sqbrk x \times 0 = \sqbrk {x \times 0}$.
$\Box$
Induction Step
Let there exist a formal proof of $\sqbrk x \times \sqbrk y = \sqbrk {x \times y}$.
Then the following is a formal proof:
By the tableau method of natural deduction:
Line | Pool | Formula | Rule | Depends upon | Notes | |
---|---|---|---|---|---|---|
1 | $\sqbrk x \times \sqbrk y = \sqbrk {x \times y}$ | Theorem Introduction | (None) | Induction hypothesis | ||
2 | $\forall a, b: a = b \implies a + \sqbrk x = b + \sqbrk x$ | Theorem Introduction | (None) | Substitution Property of Equality | ||
3 | $\sqbrk x \times \sqbrk y = \sqbrk {x \times y} \implies \paren {\sqbrk x \times \sqbrk y} + \sqbrk x = \sqbrk {x \times y} + \sqbrk x$ | Universal Instantiation | 2 | |||
4 | $\paren {\sqbrk x \times \sqbrk y} + \sqbrk x = \sqbrk {x \times y} + \sqbrk x$ | Modus Ponendo Ponens | 3, 2 | |||
5 | $\forall a, b: a \times \map s b = \paren {a \times b} + a$ | Axiom $\text M 6$ | ||||
6 | $\sqbrk x \times \map s {\sqbrk y} = \paren {\sqbrk x \times \sqbrk y} + \sqbrk x$ | Universal Instantiation | 5 | |||
7 | $\sqbrk x \times \map s {\sqbrk y} = \paren {\sqbrk x \times \sqbrk y} + \sqbrk x \land \paren {\sqbrk x \times \sqbrk y} + \sqbrk x = \sqbrk {x \times y} + \sqbrk x$ | Rule of Conjunction | 6, 4 | |||
8 | $\forall a,b,c: \paren {a = b} \land \paren {b = c} \implies a = c$ | Theorem Introduction | (None) | Equality is Transitive | ||
9 | $\sqbrk x \times \map s {\sqbrk y} = \paren {\sqbrk x \times \sqbrk y} + \sqbrk x \land \paren {\sqbrk x \times \sqbrk y} + \sqbrk x = \sqbrk {x \times y} + \sqbrk x \implies \sqbrk x \times \map s {\sqbrk y} = \sqbrk {x \times y} + \sqbrk x$ | Universal Instantiation | 8 | |||
10 | $\sqbrk x \times \map s {\sqbrk y} = \sqbrk {x \times y} + \sqbrk x$ | Modus Ponendo Ponens | 9, 7 | |||
11 | $\sqbrk {x \times y} + \sqbrk x = \sqbrk {\paren {x \times y} + x}$ | Theorem Introduction | (None) | Addition of Natural Numbers is Provable | ||
12 | $\sqbrk x \times \map s {\sqbrk y} = \sqbrk {x \times y} + \sqbrk x \land \sqbrk {x \times y} + \sqbrk x = \sqbrk {\paren {x \times y} + x}$ | Rule of Conjunction | 10, 11 | |||
13 | $\sqbrk x \times \map s {\sqbrk y} = \sqbrk {x \times y} + \sqbrk x \land \sqbrk {x \times y} + \sqbrk x = \sqbrk {\paren {x \times y} + x} \implies \sqbrk x \times \map s {\sqbrk y} = \sqbrk {\paren {x \times y} + x}$ | Universal Instantiation | 8 | |||
14 | $\sqbrk x \times \map s {\sqbrk y} = \sqbrk {\paren {x \times y} + x}$ | Modus Ponendo Ponens | 13, 12 |
Therefore, there exists a formal proof of $\sqbrk x \times \map s {\sqbrk y} = \sqbrk {\paren {x \times y} + x}$.
But $\sqbrk y$ consists of $y$ applications of the successor mapping to the constant $0$.
Thus, $\map s {\sqbrk y}$ consists of $y + 1 = \map s y$ mappings of $s$ to $0$.
As that is the unary representation of $\map s y$ it follows that:
- $\map s {\sqbrk y} = \sqbrk {\map s y}$
By definition of multiplication:
- $x \times \map s y = \paren {x \times y} + x$
Therefore, the above proof also proves:
- $\sqbrk x \times \sqbrk {\map s y} = \sqbrk {x \times \map s y}$
as the WFFs are syntactically identical.
$\Box$
Thus, by the Principle of Mathematical Induction, there exists such a formal proof for every $y \in \N$.
As $x$ was arbitrary, there exists such a formal proof for every $x, y \in \N$.
$\blacksquare$