uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • 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
Some proof-theoretic properties of PHL and related systems
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Mathematics. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Mathematics, Algebra, Geometry and Logic.
2010 (English)Report (Other academic)
Place, publisher, year, edition, pages
2010.
Series
U.U.D.M. report / Uppsala University, Department of Mathematics, ISSN 1101-3591 ; 2010:18
National Category
Mathematics
Identifiers
URN: urn:nbn:se:uu:diva-135771OAI: oai:DiVA.org:uu-135771DiVA: diva2:375559
Available from: 2010-12-08 Created: 2010-12-08 Last updated: 2011-12-15Bibliographically approved
In thesis
1. On Constructive Sets and Partial Structures
Open this publication in new window or tab >>On Constructive Sets and Partial Structures
2011 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

The first three papers in this thesis study the formalisation of a set in type theory as a data type with an equivalence relation – an object usually known as a setoid. The corresponding formalisation of a locally small category is called an E-category.

In Paper I, we show that type theory without universes is insufficient for proving that some expected properties hold of the E-category of setoids, but that a minimal universe is sufficient.

In Paper II, we show that although the collection of all E-categories does not form a category, we can introduce a type-theoretic version of bicategories, and the E-categories form such an E-bicategory.

In Paper III, we consider the setoids inside a type-theoretic universe. The axiom of unique substitutions is proposed and used to show that these form a small category (that is, a category witha setoid of objects and a single setoid of all arrows). We demonstrate that this construction can not be carried out without adding some new axiom to type theory. We also show that the axiom of unique substitutions is strictly weaker than the axiom of unique identity proofs.

In Paper IV, we investigate partial equivalence relations, also known as partial setoids, in Heyting arithmetic in all finite types, and adapt the result that the extensional axiom of choice is equivalent to the combination of the intensional axiom of choice, classical logic, and an extensionality axiom.

In Paper V, we investigate PHL, a logic of partial terms, and prove a cut elimination theorem for it and for a related calculus.

Place, publisher, year, edition, pages
Uppsala: Department of Mathematics, 2011. 33 p.
Series
Uppsala Dissertations in Mathematics, ISSN 1401-2049 ; 74
National Category
Algebra and Logic
Research subject
Mathematical Logic
Identifiers
urn:nbn:se:uu:diva-160605 (URN)978-91-506-2245-4 (ISBN)
Public defence
2011-12-13, Polhemsalen, Ångströmlaboratoriet, Lägerhyddsvägen 1, Uppsala, 13:15 (English)
Opponent
Supervisors
Available from: 2011-11-22 Created: 2011-10-27 Last updated: 2011-12-15Bibliographically approved

Open Access in DiVA

No full text

Authority records BETA

Wilander, Olov

Search in DiVA

By author/editor
Wilander, Olov
By organisation
Department of MathematicsAlgebra, Geometry and Logic
Mathematics

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

urn-nbn
Total: 579 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • 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