Arithmetic based on the Church numerals in illative combinatory logic (Q1115414): Difference between revisions
From MaRDI portal
Changed an Item |
Set profile property. |
||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank |
Revision as of 03:15, 5 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Arithmetic based on the Church numerals in illative combinatory logic |
scientific article |
Statements
Arithmetic based on the Church numerals in illative combinatory logic (English)
0 references
1988
0 references
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.
0 references
Arithmetic
0 references
Church numerals
0 references
illative combinatory logic
0 references
Peano-type axioms of Mendelson
0 references
predecessor relation
0 references