Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
A Constructive Examination of a Russell-style Ramified Type Theory
Stockholms universitet, Naturvetenskapliga fakulteten, Matematiska institutionen.
Antal upphovsmän: 12018 (Engelska)Ingår i: Bulletin of Symbolic Logic, ISSN 1079-8986, E-ISSN 1943-5894, Vol. 24, nr 1, s. 90-106Artikel i tidskrift (Refereegranskat) Published
Abstract [en]

In this article we examine the natural interpretation of a ramified type hierarchy into Martin-Lof 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 mathematical analysis in the style of Bishop. We present a ramified type theory suitable for this purpose. One may regard the results of this article as an alternative solution to the problem of the proliferation of levels of real numbers in 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.

Ort, förlag, år, upplaga, sidor
2018. Vol. 24, nr 1, s. 90-106
Nyckelord [en]
ramified type theory, intuitionistic logic, reducibility axiom
Nationell ämneskategori
Matematik Data- och informationsvetenskap
Identifikatorer
URN: urn:nbn:se:su:diva-156694DOI: 10.1017/bsl.2018.4ISI: 000431008000003OAI: oai:DiVA.org:su-156694DiVA, id: diva2:1211232
Tillgänglig från: 2018-05-30 Skapad: 2018-05-30 Senast uppdaterad: 2022-02-26Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas i DiVA

Övriga länkar

Förlagets fulltextarXiv:1704.06812

Person

Palmgren, Erik

Sök vidare i DiVA

Av författaren/redaktören
Palmgren, Erik
Av organisationen
Matematiska institutionen
I samma tidskrift
Bulletin of Symbolic Logic
MatematikData- och informationsvetenskap

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetricpoäng

doi
urn-nbn
Totalt: 4457 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf