Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
A Constructive Examination of a Russell-style Ramified Type Theory
Stockholm University, Faculty of Science, Department of Mathematics. (Matematisk logik)
2017 (English)Report (Other academic)
Abstract [en]

In this paper we examine the natural interpretation of a ramified type hierarchy into Martin-Löf type theory with an infinite sequence of universes. It is shown that under this predicative interpretation some useful special cases of Russell’s reducibility axiom are valid, namely functional reducibility. This is sufficient to make the type hierarchy usable for development of constructive mathematics. We present a ramified type theory suitable for this purpose. One may regard the results of this paper as an alternative solution to the problems of Russell’s theory, which avoids impredicativity, but instead imposes constructive logic. The intuitionistic ramified type theory introduced here, also suggests that there is a natural associated notion of predicative elementary topos. 

Place, publisher, year, edition, pages
2017. , 14 p.
Keyword [en]
Type theory, predicativity, Russell's type theory
National Category
Natural Sciences
Research subject
Mathematical Logic
Identifiers
URN: urn:nbn:se:su:diva-142058OAI: oai:DiVA.org:su-142058DiVA: diva2:1130097
Projects
Konstruktiva och kategoriteoretiska grundvalar för matematik
Funder
Swedish Research Council, 2015-03835
Available from: 2017-08-08 Created: 2017-08-08 Last updated: 2017-08-08

Open Access in DiVA

No full text

Other links

ArXiV
By organisation
Department of Mathematics
Natural Sciences

Search outside of DiVA

GoogleGoogle Scholar

CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf