Switch to: References

Add citations

You must login to add citations.
  1. Bunder’s paradox.Michael Caie - 2020 - Review of Symbolic Logic 13 (4):829-844.
    Systems ofillative logicare logical calculi formulated in the untypedλ-calculus supplemented with certain logical constants.1In this short paper, I consider a paradox that arises in illative logic. I note two prima facie attractive ways of resolving the paradox. The first is well known to be consistent, and I briefly outline a now standard construction used by Scott and Aczel that establishes this. The second, however, has been thought to be inconsistent. I show that this isn’t so, by providing a nonempty class (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Pure type systems with more liberal rules.Martin Bunder & Wil Dekkers - 2001 - Journal of Symbolic Logic 66 (4):1561-1580.
    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 (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations