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
Partiality and Choice: Foundational Contributions
Stockholm University, Faculty of Science, Department of Mathematics.
2005 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

The subject of the thesis is foundational aspects of partial functions (Papers 1, 2 & 4) and some choice principles (Papers 3 & 4) in the context of constructive mathematics.

Paper 1 studies the inversion functions of commutative rings. The foundational problem of having them only partially defined is overcome by extending them to total functions. This cannot be done constructively unless the rings themselves are extended at the same time. We study such extensions, called wheels. It is investigated how identities for wheels relate to identities for commutative rings.

Paper 2 studies the foundations of partial functions in Martin-Löf's type theory according to the view of subsets as propositional functions, in particular in connection with equivalence relations that the functions are supposed to preserve. The first and second isomorphism theorems of algebra are verified, showing that our approach is flexible enough for some natural mathematical proofs to be carried out.

Paper 3 shows that the difference between the principles of intensional and extensional choice can be described as the principle of excluded middle plus a certain mild extensionality principle, which follows from the principle that functions are identical if they are identical at every point.

Paper 4 studies a constructive calculus of indefinite and definite descriptions. It has the property that it can be interpreted straightforwardly in type theory with all terms referring to individuals. In this respect it differs from other constructive calculi of descriptions, which are known to be conservative extensions of description-free calculi but for which descriptions cannot be interpreted as referring to individuals in general.

The appendix includes a predicative version of Birkhoff's theorem. It states that if a class of algebras is closed under homomorphic images, subalgebras and products and contains a set-indexed family of algebras that satisfies the same identities as the class, then the class can be axiomatized by a set of equations.

Place, publisher, year, edition, pages
Stockholm: Matematiska institutionen , 2005. , 132 p.
National Category
Mathematics
Identifiers
URN: urn:nbn:se:su:diva-475ISBN: 91-7155-020-8 (print)OAI: oai:DiVA.org:su-475DiVA: diva2:194366
Public defence
2005-06-02, sal 14, hus 5, Kräftriket, Stockholm, 10:00
Opponent
Supervisors
Available from: 2005-04-26 Created: 2005-04-26Bibliographically approved
List of papers
1. Wheels - on division by zero
Open this publication in new window or tab >>Wheels - on division by zero
2004 In: Mathematical Structures in Computer Science, ISSN 0960-1295, Vol. 14, no 1, 143-184 p.Article in journal (Refereed) Published
Identifiers
urn:nbn:se:su:diva-23754 (URN)
Note
Part of urn:nbn:se:su:diva-475Available from: 2005-04-26 Created: 2005-04-26Bibliographically approved
2. Subsets, quotients and partial functions in Martin-Löf's Type Theory
Open this publication in new window or tab >>Subsets, quotients and partial functions in Martin-Löf's Type Theory
2003 In: Types for Proofs and Programs: TYPES 2002, Selected Papers, LNCS 2646, Springer , 2003, 78-94 p.Chapter in book (Other academic) Published
Place, publisher, year, edition, pages
Springer, 2003
Identifiers
urn:nbn:se:su:diva-23755 (URN)3-540-14031-X (ISBN)
Note
Part of urn:nbn:se:su:diva-475Available from: 2005-04-26 Created: 2005-04-26Bibliographically approved
3. EM + Ext_ + ACint is equivalent to ACext
Open this publication in new window or tab >>EM + Ext_ + ACint is equivalent to ACext
2004 In: Mathematical Logic Quarterly, Vol. 50, no 3, 236-240 p.Article in journal (Refereed) Published
Identifiers
urn:nbn:se:su:diva-23756 (URN)
Note
Part of urn:nbn:se:su:diva-475Available from: 2005-04-26 Created: 2005-04-26Bibliographically approved
4. Interpreting descriptions in intensional type theory
Open this publication in new window or tab >>Interpreting descriptions in intensional type theory
2005 In: The Journal of Symbolic Logic, Vol. 70, no 2, 488-514 p.Article in journal (Refereed) Published
Identifiers
urn:nbn:se:su:diva-23757 (URN)
Note
Part of urn:nbn:se:su:diva-475Available from: 2005-04-26 Created: 2005-04-26Bibliographically approved

Open Access in DiVA

fulltext(923 kB)1439 downloads
File information
File name FULLTEXT01.pdfFile size 923 kBChecksum SHA-1
fae260d95a13ba222feb81d6d2e8ab1521f1ac92e9979de094fc39cfe142940c5e6df07f
Type fulltextMimetype application/pdf
errata(21 kB)26 downloads
File information
File name ERRATA01.pdfFile size 21 kBChecksum SHA-1
23b84725d7f115d4462a72f722a87216f4b2e4340992a17054c77ae7a0615b17f0d8a790
Type errataMimetype application/pdf

By organisation
Department of Mathematics
Mathematics

Search outside of DiVA

GoogleGoogle Scholar
Total: 1439 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 2203 hits
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