In a previous blog post, we showed an implementation of a subset formal system of Peano’s axioms that could represent numbers and the addition operator. In a blog post before that, we showed and implemented a formal system that could represent numbers and the addition operator at a more basic level.
This blog post will show yet another way to represent numbers and arithmetic operations such as addition, subtraction, multiplication, and division. Finally, we’ll extend this system to also support complex arithmetic operations (combining the previous basic operations).
Numbers
We start with the same rules as before, which allows us to represent numbers:
# Zero is a natural number
rTmZ : 0
tmZ : rTmZ
# Successor
rTmS : S(x)
# Few numbers needed for the proofs
tm1 : rTmS x=tmZ
tm2 : rTmS x=tm1
tm3 : rTmS x=tm2
tm4 : rTmS x=tm3
tm5 : rTmS x=tm4
Simple arithmetical expressions
Instead of working at the equational level, we lift the representation and allow the object level to express implication. Here’s an example of how addition can be represented:
# Addition
rAZ : ADD(x,0)=>x
rAS : ADD(x,y)=>z -> ADD(x,S(y))=>S(z)
We can represent the same rules in natural deduction style:
For example, we can now show that 
tADD20 : rAZ x=tm2
tADD21 : rAS x=tm2;y=tmZ;z=tm2 tADD20
tADD22 : rAS x=tm2;y=tm1;z=tm3 tADD21
The theorem tADD22 produces ADD(S(S(0)),S(S(0)))=>S(S(S(S(0)))).
Rules for subtraction, multiplication and division respectively can be represented similarly:
# Subtraction
rSZ : SUB(x,0)=>x
rSS : SUB(x,y)=>z -> SUB(S(x),S(y))=>z
# Multiplication
rMZ : MUL(x,0)=>0
rMS : MUL(x,y)=>z -> ADD(x,z)=>w -> MUL(x,S(y))=>w
# Division
rDZ : DIV(a,d)=>(0,a)
# The inequality check 0 <= r < d is redundant because of subtraction
rDS : DIV(a,d)=>(q,r) -> SUB(r,d)=>x -> DIV(a,d)=>(S(q),x)
With some example evaluations:
# Subtraction example (3-2=1)
tSUB10 : rSZ x=tm1
tSUB21 : rSS x=tm1;y=tmZ;z=tm1 tSUB10
tSUB32 : rSS x=tm2;y=tm1;z=tm1 tSUB21
# Multiplication example (2*2=4)
tMUL20 : rMZ x=tm2
tMUL21 : rMS x=tm2;y=tmZ;z=tmZ;w=tm2 tMUL20 tADD20
tMUL22 : rMS x=tm2;y=tm1;z=tm2;w=tm4 tMUL21 tADD22
# Division example (3/2=1r1)
tDIV32step1 : rDZ a=tm3;d=tm2
tDIV32 : rDS a=tm3;d=tm2;q=tmZ;r=tm3;x=tm1 tDIV32step1 tSUB32
These produce the following theorems:
tSUB32 : SUB(S(S(S(0))),S(S(0)))=>S(0)
tMUL22 : MUL(S(S(0)),S(S(0)))=>S(S(S(S(0))))
tDIV32 : DIV(S(S(S(0))),S(S(0)))=>(S(0),S(0))Complex arithmetical expressions
As it is, the current system allows us to evaluate simple expressions, but not complex ones such as 
rAS' : x=>a -> y=>b -> ADD(x,y)=>ADD(a,b)
rSS' : x=>a -> y=>b -> SUB(x,y)=>SUB(a,b)
rMS' : x=>a -> y=>b -> MUL(x,y)=>MUL(a,b)
rDS' : x=>a -> y=>b -> DIV(x,y)=>DIV(a,b)
The idea is, to evaluate ADD(SUB(3,2),MUL(2,2)), we need to show that SUB(3,2) evaluates to 1, i.e. SUB(3,2)=>1, and also show that MUL(2,2)=>4. If we do that, we can conclude that ADD(SUB(3,2),MUL(2,2)) evaluates to ADD(1,4).
To be able to replace x, a, y, and b with some of the operations, we will also need a way to represent terms:
rTmAD : ADD(x,y)
rTmSU : SUB(x,y)
rTmMU : MUL(x,y)
rTmDI : DIV(x,y)
Now we are able to represent
tmSUB(SSS0,SS0) : rTmSU x=tm3;y=tm2
tmMUL(SS0,SS0) : rTmMU x=tm2;y=tm2
tComplexEg1 : rAS' x=tmSUB(SSS0,SS0);a=tm1;y=tmMUL(SS0,SS0);b=tm4 tSUB32 tMUL22
The theorem tComplexEg1 represents the following deduction which states that 
ADD(SUB(S(S(S(0))),S(S(0))),MUL(S(S(0)),S(S(0))))=>ADD(S(0),S(S(S(S(0)))))Extending the system with implications
As it is right now, we cannot reduce tComplexEg1 any further, i.e. we showed that 
To be able to do that, we will extend the system with the following rules (identity and hypothetical syllogism) for manipulating implications:
rId : x=>x
rHs : a=>b -> b=>c -> a=>c
Our proof will rely on the following lemmas (more specifically, tADD14 which proves that 
tADD10 : rAZ x=tm1
tADD11 : rAS x=tm1;y=tmZ;z=tm1 tADD10
tADD12 : rAS x=tm1;y=tm1;z=tm2 tADD11
tADD13 : rAS x=tm1;y=tm2;z=tm3 tADD12
tADD14 : rAS x=tm1;y=tm3;z=tm4 tADD13
Finally, we are now able to show that 
tmADD(SUB(SSS0,SS0),MUL(SS0,SS0)) : rTmAD x=tmSUB(SSS0,SS0);y=tmMUL(SS0,SS0)
tmADD(S0,SSSS0) : rTmAD x=tm1;y=tm4
tComplexEg2 : rHs a=tmADD(SUB(SSS0,SS0),MUL(SS0,SS0));b=tmADD(S0,SSSS0);c=tm5 tComplexEg1 tADD14
This produces the following proof for tComplexEg2:
ADD(SUB(S(S(S(0))),S(S(0))),MUL(S(S(0)),S(S(0))))=>S(S(S(S(S(0)))))The expression S(S(S(S(S(0))))) represents the number 5 and can not be reduced any further.
Conclusion
As we’ve seen, there are a lot of ways to represent numbers and operations. It is a common thing to start with a very basic system and then extend it with additional features – this approach can be seen all across mathematics, though this “linearity” is unnatural as usually a lot of trial & error is done before coming up with a clear picture of how the system should look like. Working with implications like we did here (i.e. lifting them at the object level) is also pretty common and allows for a lot of flexibility.
Some further example ideas for extending could be to add support for integers, fractions, etc.
Budge-TP allows us to express all of these systems, play around with them and understand and analyze them. This is what makes it useful as a theorem prover – getting a deeper insight into a formal system, which is even better for expanding our knowledge of how things work.
bor0's blog 