Equivalences between Pure Type Systems and Systems of Illative Combinatory Logic

Notre Dame Journal of Formal Logic 46 (2):181-205 (2005)
  Copy   BIBTEX

Abstract

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

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 74,213

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Pure Type Systems with More Liberal Rules.Martin Bunder & Wil Dekkers - 2001 - Journal of Symbolic Logic 66 (4):1561-1580.
Modal Pure Type Systems.Tijn Borghuis - 1998 - Journal of Logic, Language and Information 7 (3):265-296.
Introduction to Combinatory Logic.J. Roger Hindley - 1972 - Cambridge University Press.
Consistency Notions in Illative Combinatory Logic.M. W. Bunder - 1977 - Journal of Symbolic Logic 42 (4):527-529.
A Paradox in Illative Combinatory Logic.M. W. Bunder - 1970 - Notre Dame Journal of Formal Logic 11 (4):467-470.
Scott's Models and Illative Combinatory Logic.M. W. Bunder - 1979 - Notre Dame Journal of Formal Logic 20 (3):609-612.
$\lambda$-Elimination in Illative Combinatory Logic.M. W. Bunder - 1979 - Notre Dame Journal of Formal Logic 20 (3):628-630.
Illative Combinatory Logic Without Equality as a Primitive Predicate.M. W. Bunder - 1982 - Notre Dame Journal of Formal Logic 23 (1):62-70.
Significance and Illative Combinatory Logics.M. W. Bunder - 1980 - Notre Dame Journal of Formal Logic 21 (2):380-384.
Combinatory Reduction Systems.Jan Willem Klop - 1963 - Mathematisch Centrum.

Analytics

Added to PP
2010-08-24

Downloads
216 (#56,258)

6 months
1 (#414,449)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Higher-Order Illative Combinatory Logic.Łukasz Czajka - 2013 - Journal of Symbolic Logic 78 (3):837-872.

Add more citations

References found in this work

Propositional and Predicate Calculuses Based on Combinatory Logic.M. W. Bunder - 1974 - Notre Dame Journal of Formal Logic 15 (1):25-34.
On the Proof Theory of Coquand's Calculus of Constructions.Jonathan P. Seldin - 1997 - Annals of Pure and Applied Logic 83 (1):23-101.
Frege Structures and the Notions of Proposition, Truth and Set.Peter Aczel - 1980 - Journal of Symbolic Logic 51 (1):244-246.
A Deduction Theorem for Restricted Generality.M. W. Bunder - 1973 - Notre Dame Journal of Formal Logic 14 (3):341-346.

View all 14 references / Add more references