Commutative multiple successor recursive arithmetics.

Recursive arithmetics are usually based on three initial functions, namely the zero, successor and identity functions. In this thesis recursive arithmetics are considered which instead of having just one successor function have a number of different successor functions. These will be represented by Sv where v ranges from 1 to n. The system is made commutative by stipulating that SuSvx = SvSux for all u and v. The notion of a primitive recursive function is introduced into this arithmetic and various basic functions are defined. Another recursive arithmetic is then constructed in which the elements are ordered sets of natural numbers. It is shown that a complete isomorphism, both functional and deductive, exists between this arithmetic and the arithmetic with n successors. It is then shown by using this isomorphism that a proof can be constructed of the key equation x + (y - x) = y + (x - y) in multiple successor recursive arithmetic. A formal equation calculus is then developed for multiple successor recursive arithmetic in which the proof of the key equation given above is derived without resource to a doubly recursive uniqueness rule. The properties of the basic primitive recursive functions are also established. The problem of avoiding irregular models of this equation calculus is then examined and it is shown that this can be done by using relatively simple axioms. An inequality relationship is then defined and it is shown that with respect to this relationship the numbers of a multiple successor recursive arithmetic form a lattice. It is then shown that this lattice is modular and distributive. The problem of introducing limited universal and existential quantifiers is then considered. It is shown that this can be done in an arithmetic of ordered sets and hence, by the isomorphism established earlier, they can also be introduced into a multiple successor recursive arithmetic. Three different logical models in multiple successor recursive arithmetic are then considered. The models are of classical two-valued logic, a modified form of Heyting's intuitionist logic, and a many-valued logic. The connection between these models is examined.