Graduate studies at Western
Studia Logica 47 (2):129 - 143 (1988)
|Abstract||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.|
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
|Through your library||Configure|
Similar books and articles
J. Roger Hindley (1986). Introduction to Combinators and [Lambda]-Calculus. Cambridge University Press.
M. W. Bunder (1979). $\Lambda$-Elimination in Illative Combinatory Logic. Notre Dame Journal of Formal Logic 20 (3):628-630.
Sabine Broda & Luís Damas (1997). Compact Bracket Abstraction in Combinatory Logic. Journal of Symbolic Logic 62 (3):729-740.
M. W. Bunder (1982). Illative Combinatory Logic Without Equality as a Primitive Predicate. Notre Dame Journal of Formal Logic 23 (1):62-70.
Katalin Bimbó (2000). Investigation Into Combinatory Systems with Dual Combinators. Studia Logica 66 (2):285-296.
M. W. Bunder (1983). A Weak Absolute Consistency Proof for Some Systems of Illative Combinatory Logic. Journal of Symbolic Logic 48 (3):771-776.
Katalin Bimbó (2003). The Church-Rosser Property in Dual Combinatory Logic. Journal of Symbolic Logic 68 (1):132-152.
Katalin Bombó (2005). The Church-Rosser Property in Symmetric Combinatory Logic. Journal of Symbolic Logic 70 (2):536 - 556.
Wil Dekkers, Martin Bunder & Henk Barendregt (1998). Completeness of the Propositions-as-Types Interpretation of Intuitionistic Logic Into Illative Combinatory Logic. Journal of Symbolic Logic 63 (3):869-890.
Henk Barendregt, Martin Bunder & Wil Dekkers (1993). Systems of Illative Combinatory Logic Complete for First-Order Propositional and Predicate Calculus. Journal of Symbolic Logic 58 (3):769-788.
Added to index2009-01-28
Total downloads8 ( #131,868 of 739,404 )
Recent downloads (6 months)1 ( #61,680 of 739,404 )
How can I increase my downloads?