In a constructive setting, no concrete formulation of ordinal numbers can simultaneously have all the properties one might be interested in; for example, being able to calculate limits of sequences ...is constructively incompatible with deciding extensional equality. Using homotopy type theory as the foundational setting, we develop an abstract framework for ordinal theory and establish a collection of desirable properties and constructions. We then study and compare three concrete implementations of ordinals in homotopy type theory: first, a notation system based on Cantor normal forms (binary trees); second, a refined version of Brouwer trees (infinitely-branching trees); and third, extensional well-founded orders.
Each of our three formulations has the central properties expected of ordinals, such as being equipped with an extensional and well-founded ordering as well as allowing basic arithmetic operations, but they differ with respect to what they make possible in addition. For example, for finite collections of ordinals, Cantor normal forms have decidable properties, but suprema of infinite collections cannot be computed. In contrast, extensional well-founded orders work well with infinite collections, but the price to pay is that almost all properties are undecidable. Brouwer trees, implemented as a quotient inductive-inductive type to ensure well-foundedness and extensionality, take the sweet spot in the middle by combining a restricted form of decidability with the ability to work with infinite increasing sequences.
Our three approaches are connected by canonical order-preserving functions from the “more decidable” to the “less decidable” notions, i.e. from Cantor normal forms to Brouwer trees, and from there to extensional well-founded orders. We have formalised the results on Cantor normal forms and Brouwer trees in cubical Agda, while extensional well-founded orders have been studied and formalised thoroughly by Escardó and his collaborators. Finally, we compare the computational efficiency of our implementations with the results reported by Berger.
•We introduce an abstract framework for approaches to ordinals in type theory.•Constructively, no single approach to ordinals combines all desirable properties.•We study three instances of the abstract framework, and their relationships.•All our approaches have extensional, well-founded orders, and arithmetic operations.•Most results are formalised in cubical Agda.
It is known that the maximal invariant set of a continuous iterative dynamical system in a compact Hausdorff space is equal to the intersection of its forward image sets, which we will call the {\it ...first minimal image set}. In this article, we investigate the corresponding relation for a class of discontinuous self maps that are on the verge of continuity, or {\it topologically almost continuous endomorphisms}. We prove that the iterative dynamics of a topologically almost continuous endomorphisms yields a chain of minimal image sets that attains a unique transfinite {\it length}, which we call the {\it maximal invariance order}, as it stabilizes itself at the maximal invariant set. We prove the converse, too. Given ordinal number $\xi$, there exists a topologically almost continuous endomorphism $f$ on a compact Hausdorff space $X$ with the maximal invariance order $\xi$. We also discuss some further results regarding the maximal invariance order as more layers of topological restrictions are added. KCI Citation Count: 0
In this paper three main results are presented: a bijection between natural sums and natural products, the completion of the axioms of Carruth for natural sums, and a new characterization of the ...natural sums in terms of Klaua’s integral ordinals. After introducing some preliminary results, we present two lemmas and a proposition for the proof of the existence of a bijection between natural products and natural sums. Then we prove the incompleteness of Carruth’s axioms by providing two counterexamples, and complete Carruth’s axioms by adding a fifth axiom. Finally, we introduce a characterization of natural sums in terms of Klaua’s integral ordinals and present two families of natural sums, which differ from Hessenberg’s sum.
A relational characterization of cop-win graphs was provided by Nowakowski and Winkler in their seminal paper on the game of Cops and Robbers. As a by-product of that characterization, each cop-win ...graph is assigned a unique ordinal, which we refer to as a CR-ordinal. For finite graphs, CR-ordinals correspond to the length of the game assuming optimal play, with the cop beginning the game in a least favourable initial position. For infinite graphs, however, the possible values of CR-ordinals have not been considered in the literature until the present work.
We classify the CR-ordinals of cop-win trees as either a finite ordinal, or those of the form α+ω, where α is a limit ordinal. For general infinite cop-win graphs, we provide an example whose CR-ordinal is not of this form. We finish with some problems on characterizing the CR-ordinals in the general case of cop-win graphs.
In his 1887's Mitteilungen zur Lehre von Transfiniten, Cantor seeks to prove inconsistency of infinitesimals. We provide a detailed analysis of his argument from both historical and mathematical ...perspective. We show that while his historical analysis are questionable, the mathematical part of the argument is false.
Celotno besedilo
Dostopno za:
DOBA, IZUM, KILJ, NUK, PILJ, PNG, SAZU, UILJ, UKNU, UL, UM, UPUK
To understand the meaning and function of the ordinal numbers in the myth of the races it is essential to have a full grasp of how the myth is composed and its structure is supposed to be perceived ...by a listener or reader. There is a general silence among Hesiod scholars about the meaning and function of the ordinal numbers in the myth. A tacit agreement may be inferred from such a silence: the ordinal numbers are implicitly taken to merely express the chronological order of the races. In this article, we examine each and every one of the ordinal numbers that appear in Hesiod’s myth. We demonstrate that the ordinal numbers preserve their hierarchical dimension even in the cases in which this appears to be less convincing.
For every well-founded tree 𝒯 having a unique root such that every non-maximal node of it has countable infinitely many immediate successors, we construct a ℒ∞-space X𝒯. We prove that, for each ...such tree 𝒯, the Calkin algebra of X𝒯 is homomorphic to C(𝒯), the algebra of continuous functions defined on 𝒯, equipped with the usual topology. We use this fact to conclude that, for every countable compact metric space K, there exists a ℒ∞-space whose Calkin algebra is isomorphic, as a Banach algebra, to C(K).
Natural Addition of Ordinals Koch, Sebastian
Formalized mathematics,
07/2019, Letnik:
27, Številka:
2
Journal Article
Recenzirano
Odprti dostop
In 3 the existence of the Cantor normal form of ordinals was proven in the Mizar system 6. In this article its uniqueness is proven and then used to formalize the natural sum of ordinals.
We present arguments showing that the standard notion of the support of a probabilistic Borel measure is not well defined in every topological space. Our goal is to create a “very inseparable” space ...and to show the existence of a family of closed sets such that each of them is of full measure, but their intersection is empty. The presented classic construction is credited to Jean Dieudonné and dates back to 1939. We also propose certain, up to our best knowledge, new simplifications.
The rank of a point-line geometry
Γ
is usually defined as the generating rank of
Γ
, namely the minimal cardinality of a generating set. However, when the subspace lattice of
Γ
satisfies the Exchange ...Property we can also try a different definition: consider all chains of subspaces of
Γ
and take the least upper bound of their lengths as the rank of
Γ
. If
Γ
is finitely generated then these two definitions yield the same number. On the other hand, as we shall show in this paper, if infinitely many points are needed to generate
Γ
then the rank as defined in the latter way is often (perhaps always) larger than the generating rank. So, if we like to keep the first definition we should accordingly discard the second one or modify it. We can modify it as follows: consider only well ordered chains instead of arbitrary chains. As we shall prove, the least upper bound of the lengths of well ordered chains of subspaces is indeed equal to the generating rank. According to this result, the (possibly infinite) rank of a polar space can be characterized as the least upper bound of the lengths of well ordered chains of singular subspaces; referring to arbitrary chains would be an error.
PDF
