Arithmetic based on the Church numerals in illative combinatory logic (Q1115414)

Arithmetic was first developed within lambda calculus by Rosser and Kleene in a system of Church, which was later shown to be inconsistent. Some of this work could be rescued but not within the framework of predicate logic. The present paper has a new definition of equality which allows not only the Church numerals to be used, but also the set of all such to be defined, within the author's system of illative combinatory logic as outlined in Arch. Math. Logik Grundlagenforsch. 23, 99-107 (1983; Zbl 0537.03010). All the Peano-type axioms of Mendelson except one can be proved directly from this. A rather weak extra axiom suffices to derive the properties of a predecessor relation, which allow for the proof of the remaining Peano axiom.