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.
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.
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.
A critical question in cognitive science concerns how numerical knowledge develops. One essential component of an adult concept of number is ordinality: the greater than and less than relationships ...between numbers. Here it is shown in two experiments that 11-month-old infants successfully discriminated, whereas 9-month-old infants failed to discriminate, sequences of numerosities that descended in numerical value from sequences that increased in numerical value. These results suggest that by 11 months of age infants possess the ability to appreciate the greater than and less than relations between numerical values but that this ability develops between 9 and 11 months of age. In an additional experiment 9-month-old infants succeeded at discriminating the ordinal direction of sequences that varied in the size of a single square rather than in number, suggesting that a capacity for non-numerical ordinal judgments may develop before a capacity for ordinal numerical judgments. These data raise many questions about how infants represent number and what happens between 9 and 11 months to support ordinal numerical judgments.
PDF
