Arithmetic on Finite SetsRecall that, using only Peano's Axioms (listed below in DC Proof format) plus the rules and axioms of logic and set theory, we can develop the laws of arithmetic for natural numbers.

**PA1**
Set(n)

**PA2**
0
e
n

**PA3**
ALL(a):[a
e
n
=>
s(a)
e
n]

**PA4**
ALL(a):[a
e
n
=>
~s(a)=0]

**PA5**
ALL(a):ALL(b):[a
e
n
&
b
e
n
=>
[s(a)=s(b)
=> a=b]]

**PA6**
ALL(a):[Set(a)
& ALL(b):[b
e
a
=> b
e
n]

=>
[0
e
a
& ALL(b):[b
e
a
=>
s(b)
e
a]

=>
ALL(b):[b
e
n
=>
b
e
a]]]

where

n= {0, 1, 2, ...} is the infinite set of natural numbers, andsis the successor function onn.It is also possible to develop a similar list of axioms for finite sets such as:

{0}

{0, 1, 2, 3}

{0,
1, 2, ... 1x10^{603}}

The axioms for Finite Arithmetic include:

**FA1**
Set(n)

**FA2**
0
e
n

**FA3**
max
e
n

**FA4**
ALL(a):[a
e
n
=>
[~a=max
=>
s(a)
e
n]]

**FA5**
~s(max)
e
n

**FA6**
ALL(a):[a
e
n
=>
~s(a)=0]

**FA7**
ALL(a):ALL(b):[a
e n & b
e n &
s(a)
e n => [s(a)=s(b) => a=b]]

**FA8**
ALL(a):[Set(a)
& ALL(b):[b
e
a
=> b
e
n]

=>
[0
e
a
& ALL(b):[b
e
a
&
s(b)
e
n
=>
s(b)
e
a]

=>
ALL(b):[b
e
n
=>
b
e
a]]]

where

n= {0, 1, 2, ...max} is a finite set with successor functions.Let us now compare these two remarkably similar sets of axioms.

The axioms of finite arithmetic have only two axioms (axioms 3 and 5) that have no analogs in Peano's Axioms. Axiom 3 introduces the

lastnumber,max. (There is no last number in an infinite set.)

**FA3**
max
e
n

Axiom 5 states that max has no successor.

**FA5**
~s(max)
e
n

Apart from these two axioms, the other axioms are identical or very similar to those in the Peano's Axioms.

Axioms 1 and 2 are identical. In both cases, 0 is an element of set

n.

**PA1,
FA1**
Set(n)

**PA2,
FA2**
0
e
n

Compare PA3 and FA4:

**PA3**
ALL(a):[a
e
n
=>
s(a)
e
n]

**FA4**
ALL(a):[a
e
n
=>
**[~a =**** max**
**=>**
s(a)
e
n**]**]

The only difference is highlighted in bold (in FA4). PA3 states that the successor function

sis defined on all ofn. FA4 states that the successor is defined on all ofnbutmax, which has no successor. In this latter case, we callsapartial functiononn, that is,sis defined only on a proper subset ofn. Informally, we say thats(a)isundefinedfora=max[1].PA4 and FA6 are identical.

**PA4,
FA6**
ALL(a):[a
e
n
=>
~s(a)=0]

These two axioms state that 0 is not predecessor.

Compare PA5 and FA7:

PA5ALL(a):ALL(b):[a e n & b e n => [s(a)=s(b) => a=b]]

FA7ALL(a):ALL(b):[a e n & b e n&s(a) e n=> [s(a)=s(b) => a=b]]

The only difference is highlighted in bold (in FA7). These two axioms state that predecessors are unique.

Compare PA6 and FA8:

**PA6**
ALL(a):[Set(a)
& ALL(b):[b
e
a
=> b
e
n]

=>
[0
e
a
& ALL(b):[b
e
a
=>
s(b)
e
a]

=>
ALL(b):[b
e
n
=>
b
e
a]]]

**FA8**
ALL(a):[Set(a)
& ALL(b):[b
e
a
=> b
e
n]

=>
[0
e
a
& ALL(b):[b
e
a
**&
****s****(b)**
**e
****n**
=>
s(b)
e
a]

=>
ALL(b):[b
e
n
=>
b
e
a]]]

The only difference is highlighted in bold (in FA8). These two axioms represent the Principal of Mathematical Induction for the infinite set

n, and the finite setnrespectively. For the inductive step in the case of a finite setn(FA8), we have prove that, in addition to be being an element of a, the successor ofbmust also be defined. In the case of the infinite setn(PA6), the successor will be defined forallelements ofn.To develop the laws of arithmetic in either system, we must define addition. We can construct (i.e. prove the existence of) the add function using either Peano's Axioms or the axioms of finite arithmetic above, along with the rules and axioms of logic and set theory. From Peano's axioms, we can construct a function + such that:

**PA+1**
ALL(a):[a
e
n
=>
a+0=a]

**PA+2**
ALL(a):ALL(b):ALL(c):[a
e
n
&
b
e
n
&
c
e
n

=>
[a+b=c => a+s(b)=s(c)]

From the axioms of finite arithmetic, we can construct a function + such that:

**FA+1**
ALL(a):[a
e
n
=>
a+0=a]

**FA+2**
ALL(a):ALL(b):[a
e
n
& b
e
n
& c
e
n
**
&
s(b)
e n &
s(c)
e n**

=>
[a+b=c
=>
a+s(b)=s(c)]

Differences are highlighted in bold (in FA+2). Before we can increment a sum in finite arithmetic, we must determine that the successors actually exist.

See formal proof of the construction of the add function based on the axioms of finite arithmetic (makes using of prefix notation, i.e.

add(x,y) =x+y).

1. Other, somewhat less satisfying attempts to develop finite arithmetic have been based on what amounts to changing the specifications by arbitrarily assigning a successor to max, or adding another element to the co-domain to which all unassigned elements of the domain can be mapped.