University of Wollongong
Browse

Pure type systems with more liberal rules

Download (425.8 kB)
journal contribution
posted on 2024-11-15, 07:09 authored by Martin BunderMartin Bunder, Wil Dekkers
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.

History

Citation

Bunder, M. & Dekkers, W. (2001). Pure type systems with more liberal rules. Journal of Symbolic Logic, 66 (4), 1561-1580.

Journal title

Journal of Symbolic Logic

Volume

66

Issue

4

Pagination

1561-1580

Publisher website/DOI

Language

English

RIS ID

6384

Usage metrics

    Categories

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC