Theories of types and names with positive stratified comprehension

Studia Logica 62 (2):215-242 (1999)
  Copy   BIBTEX


We introduce a certain extension of -calculus, and show that it has the Church-Rosser property. The associated open-term extensional combinatory algebra is used as a basis to construct models for theories of Explict Mathematics (formulated in the language of "types and names") with positive stratified comprehension. In such models, types are interpreted as collections of solutions (of terms) w.r. to a set of numerals. Exploiting extensionality, we prove some consistency results for special ontological axioms which are refutable under elementary comprehension.



    Upload a copy of this work     Papers currently archived: 89,330

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

Sharpening ockham's razor.Anne Cutler & Dennis Norris - 1999 - Behavioral and Brain Sciences 22 (1):40-41.
Stratified languages.A. Pétry - 1992 - Journal of Symbolic Logic 57 (4):1366-1376.
Relating Quine's NF to Feferman's EM.Andrea Cantini - 1999 - Studia Logica 62 (2):141-162.
Positive abstraction and extensionality.Roland Hinnion & Thierry Libert - 2003 - Journal of Symbolic Logic 68 (3):828-836.
Power types in explicit mathematics?Gerhard Jäger - 1997 - Journal of Symbolic Logic 62 (4):1142-1146.
Uniform inseparability in explicit mathematics.Andrea Cantini & Pierluigi Minari - 1999 - Journal of Symbolic Logic 64 (1):313-326.


Added to PP

32 (#425,006)

6 months
2 (#638,860)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Pierluigi Minari
Università degli Studi di Firenze

Citations of this work

The axiom of choice and combinatory logic.Andrea Cantini - 2003 - Journal of Symbolic Logic 68 (4):1091-1108.

Add more citations

References found in this work

Constructivism in mathematics: an introduction.A. S. Troelstra - 1988 - New York, N.Y.: Sole distributors for the U.S.A. and Canada, Elsevier Science Pub. Co.. Edited by D. van Dalen.
The lambda calculus: its syntax and semantics.Hendrik Pieter Barendregt - 1981 - New York, N.Y.: Sole distributors for the U.S.A. and Canada, Elsevier Science Pub. Co..

View all 6 references / Add more references