License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2021.8
URN: urn:nbn:de:0030-drops-142461
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14246/
de Jong, Tom ;
Escardó, Martín Hötzel
Predicative Aspects of Order Theory in Univalent Foundations
Abstract
We investigate predicative aspects of order theory in constructive univalent foundations. By predicative and constructive, we respectively mean that we do not assume Voevodsky’s propositional resizing axioms or excluded middle. Our work complements existing work on predicative mathematics by exploring what cannot be done predicatively in univalent foundations. Our first main result is that nontrivial (directed or bounded) complete posets are necessarily large. That is, if such a nontrivial poset is small, then weak propositional resizing holds. It is possible to derive full propositional resizing if we strengthen nontriviality to positivity. The distinction between nontriviality and positivity is analogous to the distinction between nonemptiness and inhabitedness. We prove our results for a general class of posets, which includes directed complete posets, bounded complete posets and sup-lattices, using a technical notion of a δ_V-complete poset. We also show that nontrivial locally small δ_V-complete posets necessarily lack decidable equality. Specifically, we derive weak excluded middle from assuming a nontrivial locally small δ_V-complete poset with decidable equality. Moreover, if we assume positivity instead of nontriviality, then we can derive full excluded middle. Secondly, we show that each of Zorn’s lemma, Tarski’s greatest fixed point theorem and Pataraia’s lemma implies propositional resizing. Hence, these principles are inherently impredicative and a predicative development of order theory must therefore do without them. Finally, we clarify, in our predicative setting, the relation between the traditional definition of sup-lattice that requires suprema for all subsets and our definition that asks for suprema of all small families.
BibTeX - Entry
@InProceedings{dejong_et_al:LIPIcs.FSCD.2021.8,
author = {de Jong, Tom and Escard\'{o}, Mart{\'\i}n H\"{o}tzel},
title = {{Predicative Aspects of Order Theory in Univalent Foundations}},
booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
pages = {8:1--8:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-191-7},
ISSN = {1868-8969},
year = {2021},
volume = {195},
editor = {Kobayashi, Naoki},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/14246},
URN = {urn:nbn:de:0030-drops-142461},
doi = {10.4230/LIPIcs.FSCD.2021.8},
annote = {Keywords: order theory, constructivity, predicativity, univalent foundations}
}
|
Keywords: |
|
order theory, constructivity, predicativity, univalent foundations |
|
Collection: |
|
6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021) |
|
Issue Date: |
|
2021 |
|
Date of publication: |
|
06.07.2021 |
