In the early thirties, Church developed predicate calculus within a system based on lambda calculus. Rosser and Kleene developed Arithmetic within this system, but using a Godelization technique showed the system to be inconsistent.Alternative systems to that of Church have been developed, but so far more complex definitions of the natural numbers have had to be used. The present paper based on a system of illative combinatory logic developed previously by the author, does allow the use of the Church numerals. (...) Given a new definition of equality all the Peano-type axioms of Mendelson except one can be derived. A rather weak extra axiom allows the proof of the remaining Peano axiom. Note. The illative combinatory logic used in this paper is similar to the logic employed in computer languages such as ML. (shrink)

Pure Type Systems, PTSs, were introduced as a generalization of the type systems of Barendregt's lambda cube and were designed to provide a foundation for actual proof assistants which will verify proofs. Systems of illative combinatory logic or lambda calculus, ICLs, were introduced by Curry and Church as a foundation for logic and mathematics. In an earlier paper we considered two changes to the rules of the PTSs which made these rules more like ICL rules. This led to four kinds (...) of PTSs. Most importantly PTSs are about statements of the form M:A, where M is a term and A a type. In ICLs there are no explicit types and the statements are terms. In this paper we show that for each of the four forms of PTS there is an equivalent form of ICL, sometimes if certain conditions hold. (shrink)

Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. The paper considers systems of illative combinatory logic that are sound for first-order propositional and predicate calculus. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators or, in a more direct way, in which derivations are not translated. Both translations are (...) closely related in a canonical way. The two direct translations turn out to be complete. The paper fulfills the program of Church [1932], [1933] and Curry [1930] to base logic on a consistent system of λ-terms or combinators. Hitherto this program had failed because systems of ICL were either too weak (to provide a sound interpretation) or too strong (sometimes even inconsistent). (shrink)