Predicative Aspects of Order Theory in Univalent Foundations

DOI10.4230/LIPICS.FSCD.2021.8arXiv2102.08812OpenAlexW3183788908MaRDI QIDQ6159924FDOQ6159924

Authors: Tom J. de Jong, Martín Escardo 

Publication date: 23 June 2023

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 $delt{a}_{mathcalV}$-complete poset. We also show that nontrivial locally small $delt{a}_{mathcalV}$-complete posets necessarily lack decidable equality. Specifically, we derive weak excluded middle from assuming a nontrivial locally small $delt{a}_{mathcalV}$-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.

Full work available at URL: https://arxiv.org/abs/2102.08812

Recommendations

• Extensions of ordered theories by generic predicates
• On the well-foundedness of adequate orders used for construction of complete unfolding prefixes
• Univalent foundations as structuralist foundations
• A Note on (Meta)predicative Wellordering Proofs
• Univalent foundations of mathematics and paraconsistency
• scientific article; zbMATH DE number 7408867
• Preorders, Partial Semigroups, and Quantales
• Decidable Theories of the Ordering of Natural Numbers with Unary Predicates
• Theories and ordinals in proof theory
• On decidability of monadic logic of order over the naturals extended by monadic predicates

zbMATH Keywords

order theorypredicativityconstructivityunivalent foundations

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of computing (68Qxx) Computer science (68-XX)

Cited In (8)

• Title not available (Why is that?)
• On Small Types in Univalent Foundations
• A Note on (Meta)predicative Wellordering Proofs
• On the well-foundedness of adequate orders used for construction of complete unfolding prefixes
• Apartness, sharp elements, and the Scott topology of domains
• Sharp elements and apartness in domains
• The Scott model of PCF in univalent type theory
• Title not available (Why is that?)

This page was built for publication: Predicative Aspects of Order Theory in Univalent Foundations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6159924)