Arithmetic on Finite Sets
Recall 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.
Arithmetic on Finite Sets
Recall 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, and s is the successor function on n.
It is also possible to develop a similar list of axioms for finite sets such as:
{0}
{0, 1, 2, 3}
{0, 1, 2, ... 1x10603}
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 function s.
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 last number, 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 s is defined on all of n. FA4 states that the successor is defined on all of n but max, which has no successor. In this latter case, we call s a partial function on n, that is, s is defined only on a proper subset of n. Informally, we say that s(a) is undefined for a=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:
PA5 ALL(a):ALL(b):[a e n & b e n => [s(a)=s(b) => a=b]]
FA7 ALL(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 set n respectively. For the inductive step in the case of a finite set n (FA8), we have prove that, in addition to be being an element of a, the successor of b must also be defined. In the case of the infinite set n (PA6), the successor will be defined for all elements of n.
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.