A complete, decidable arithmetic. The system Aoo
S. W. P. Steen · Cambridge University Press eBooks · 1972
The system A oo In this chapter we construct the formal system A oo . It is a very simple arithmetic with familiar fundamental concepts. These are: the natural number zero , the successor function , the operation of repeatedly applying a function, the operation of forming functions by abstraction, equality and inequality between numerical expressions, and the logical connectives, conjunction and disjunction. The atomic statements are equations and inequations between numerical terms, compound statements are built up from atomic statements by conjunction and disjunction. Negation, material implication and material equivalence are definable, but existential quantification and universal quantification are unrepresentable. We give definitions of A oo - truth and of A oo - falsity for closed A oo -statements, and show that they are exclusive properties. We also show that a closed A oo -statement is A oo -true if and only if it is an A oo -theorem. Thus the system A oo is consistent in the sense that A oo -theorems are A oo -true; and is complete in the sense that A oo -true A oo -statements are A oo -theorems. We give a procedure which applied to a closed A oo -statement will terminate and tell us whether it is A oo -true or is A oo -false. Thus the system A oo is decidable. The A oo -rules of formation To construct the system A oo we first list the A oo -signs and attach a type to each proper A oo -symbol and give each A oo -symbol a name which will assist the reader in understanding how the system was first conceived. Parentheses round type symbols are usually omitted by association to the left as explained in Ch. 1. (See table overleaf.)