Pure type systems with more liberal rules

Journal of Symbolic Logic 66 (4):1561-1580 (2001)
  Copy   BIBTEX


Pure Type Systems, PTSs, introduced as a generalisation of the type systems of Barendregt's lambda-cube, provide a foundation for actual proof assistants, aiming at the mechanic verification of formal proofs. In this paper we consider simplifications of some of the rules of PTSs. This is of independent interest for PTSs as this produces more flexible PTS-like systems, but it will also help, in a later paper, to bridge the gap between PTSs and systems of Illative Combinatory Logic. First we consider a simplification of the start and weakening rules of PTSs, which allows contexts to be sets of statements, and a generalisation of the conversion rule. The resulting Set-modified PTSs or SPTSs, though essentially equivalent to PTSs, are closer to standard logical systems. A simplification of the abstraction rule results in Abstraction-modified PTSs or APTSs. These turn out to be equivalent to standard PTSs if and only if a condition (*) holds. Finally we consider SAPTSs which have both modifications



    Upload a copy of this work     Papers currently archived: 93,069

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.


Added to PP

33 (#500,033)

6 months
10 (#308,797)

Historical graph of downloads
How can I increase my downloads?