Axioms for Arithmetic
In this Chapter I shall consider three axioms systems, PC , PB and PQ. The first two employ, for every natural number n, a constant /c„, and the axioms of PB , say, express essentially that is and that / c „ i s xnn. So PB employs 2-ary terms formed with + and • , while PC expres ses the same facts with help of 3-ary predicates. Clearly, both PC and PB have infinitely many axioms. The system PQ , introduced by R.M.ROBINSON 50, uses only seven axioms which, instead of mirroring the tables of addi tion and multiplication, express their recursive definitions with help of a constant k0 and a function symbol s for successor. All three axiom systems turn out to be radically undecidable. Being finite, PQ then permits to apply an idea of CHURCH 36 in order to show that also the empty axiom system, i.e. elementary quantifier logic, is undecidable.