PaperlayerView exact revision on arXiv

Source-linked AI summary

Compact totally separated types

Martín Hötzel Escardó

arXiv:2609.10447v3math.LOcs.LOmath.GN

TL;DR

The paper asks which infinite types can be exhaustively searched in finite time, a question viewed through topology as compactness. It interprets ordinal codes in discrete and compact ways, obtaining constructive distinctions between trichotomy and compactness with least elements for complemented subsets.

  • Problem

    The paper asks which infinite types admit an exhaustive mechanical search in finite time, framing the question as compactness.

    Source: §1 · p. 2

  • Method

    The paper interprets ordinal codes in discrete and compact ways, using Brouwer codes and a generalized construction with an extended sum.

    Source: §1 · pp. 4–5, §8.1 · p. 76

  • Results

    Constructively, the discrete interpretations are trichotomous while the compact ordinals have least elements for non-empty complemented subsets, and these properties do not coincide.

    Source: §1 · p. 4, §8.1 · p. 76

  • Takeaways & Limitations

    The paired interpretations show that ordinals identified classically can behave differently constructively, with the discrete-to-compact embedding not necessarily a bijection.

    Source: §1 · p. 4

    Without further axioms, the theory cannot prove an infinite generalization of compactness preservation for products, even for countable products.

    Source: §4.3 · p. 27

Abstract

from arXiv · show

Perhaps surprisingly, there are infinite types that can be exhaustively searched mechanically in finite time. We use ideas from topology to build plenty of them, referring to searchable types as compact types, and we use ordinals to measure their logical complexity. We consider two systems of ordinal notations under which a single notation denotes both a discrete ordinal and a compact one, with an embedding of the former into the latter whose image has empty complement. A boolean valued function decides which points in the image of the embedding are isolated and which are topological limit points. The first system consists of the traditional Brouwer codes and the second is an inductive-recursive universe generalizing them. The discrete ordinals so obtained are trichotomous, and the compact ones have the least element property for complemented subsets, but these two desirable properties cannot be fulfilled simultaneously in a constructive setting. The ordinals obtained from Brouwer codes further enjoy a boolean Leibniz principle, which has the notion of total separatedness as its topological counterpart. This extends previous work from G\"odel's system T to intensional Martin-L\"of type theory with univalent universes, and is formalized in Agda in the TypeTopology repository.

1. Introduction

The paper asks which infinite types can be exhaustively searched in finite time, treating types with this searchability property as compact. It develops constructive ordinal interpretations that distinguish trichotomous discrete ordinals from compact ordinals with least elements for complemented subsets.

1. Introduction

  • Searchability asks whether a boolean-valued function on a type has a root or can be determined to have none; topology frames this as compactness, while logic connects it to choice.Requiring the search property for every type in a universe amounts to global choice.Source: §1 · p. 2
  • The conatural type of decreasing binary sequences is an infinite compact example, but boolean compactness reflects topological compactness faithfully only for totally separated types.Total separatedness means boolean-valued functions separate points; a broader Sierpiński-like formulation is suggested but not studied.Source: §1 · p. 3
  • Constructively, trichotomy and compactness with the least-element property for complemented subsets occur in different ordinal interpretations, rather than together.Trichotomous ordinals are discrete, and in the topological topos compact discrete objects are necessarily finite.Source: §1 · pp. 3–4
  • Ordinal codes receive two interpretations: one yields trichotomous ordinals, and the other yields compact totally separated ordinals with the least-element property for complemented subsets.The first interpretation embeds into the second with image having empty complement.Source: §1 · p. 4
  • The paper uses Brouwer codes and an inductive-recursive universe whose sum constructor can branch over any previously constructed discrete ordinal.The extended sum is a key ingredient in the compact totally separated interpretation; total separatedness is not guaranteed for the more general inductive-recursive compact interpretation.Source: §1 · pp. 4–5
  • The work develops its results internally in intensional Martin-Löf type theory without assuming Brouwerian continuity principles or continuity of the boolean-valued search function.The results hold in all topos models of univalent type theory and are formalized in Agda in TypeTopology.Source: §1 · pp. 2, 5

2. Preliminaries

The preliminaries establish the constructive type-theoretic framework and terminology, along with principles that later results use or identify as taboos. They leave excluded middle, LPO, and WLPO undecided, assume no Brouwerian continuity, and define maps of sums and preservation of component-map properties.

2. Preliminaries

  • The paper works constructively in intensional Martin-Löf type theory with standard type formers and a hierarchy of universes, adopting the HoTT Book foundation.The framework includes empty, one- and two-element types, natural numbers, products, sums, W types, identity types, and universes.Source: §2 · p. 6, §2.1 · p. 6

2.1. Our type theory.

  • Here, a type is decidable when it is inhabited or empty, while a type is discrete when it has decidable equality.The paper distinguishes its use of “decidable” from literature that uses the term for decidable equality.Source: §2.1 · p. 6

2.2. Univalent foundations.

  • Univalence and set quotients provide extensionality principles, propositional truncations, and set replacement; full univalence is assumed from Section 5 onward.The paper treats assumptions explicitly in its Agda development; earlier sections use only extensionality consequences of univalence. Truncation distinguishes inhabitation from non-emptiness, which means ¬¬X.Source: §2.2 · pp. 6–7

2.3. Constructive mathematics.

  • ¬¬-separated types are sets, and tight apartness implies ¬¬-separatedness.The proof of the lemma uses Hedberg’s theorem: a weakly constant endofunction on each identity type makes points homotopy isolated.Source: §2.3 · p. 10
  • Extreme density means that no point lies outside a map’s image; it yields right-cancellation into ¬¬-separated types, and 2 → Ω is extremely dense.With excluded middle, extreme density is equivalent to surjectivity and is stronger than topological density.Source: §2.3 · p. 11
  • Global choice, excluded middle, LPO, and WLPO are constructive taboos considered in the paper; global choice is not assumed and is stronger than the axiom of choice.LPO decides whether a binary sequence ever takes value 0, while WLPO decides whether it takes value 1 everywhere.Source: §2.3 · pp. 11–12
  • Excluded middle, LPO, and WLPO are left undecided: continuity is not assumed, so the results remain compatible with classical mathematics and hold in every model of the foundation.The section distinguishes “fails constructively” (implies a taboo) from being false (implies the empty type).Source: §2.3 · p. 12
  • WLPO is equivalent to a discontinuous function N∞→N, while ¬WLPO entails that every such function is ¬¬-continuous; this remark inspires Definition 7.14.Markov’s principle, which is not assumed, would allow removal of the double negation.Source: §2.3 · p. 13

2.4. Retracts and maps of sums.

  • A map of sums applies a base map to each index and a corresponding fiber map, preserving equivalence, embedding, extreme density, and retraction under the stated componentwise conditions.A retract is specified by a retraction and section whose composite is the identity; for retractions of sums, the base map is the identity and each fiber map is a retraction.Source: §2.4 · p. 13

3. Totally separated types

This section defines and characterizes discrete and totally separated types using decidability and separation by 2-valued maps, and examines their relationships and closure properties constructively. It gives a sufficient condition for sums to be totally separated, constructs a universal totally separated reflection for every type, and shows that the Cantor type’s retract N∞ is discrete, implying WLPO.

3.1. Discrete types and isolated points.

  • In N∞, finite points are isolated, ∞ is isolated iff WLPO, and N∞ is discrete iff WLPO; N + 1 embeds extremely densely into N∞.The embedding sends natural numbers to finite points and the added point to ∞.Source: §3.1 · p. 14

3.2. Totally separated types.

  • A type is totally separated when maps to 2 distinguish every pair of distinct points; every discrete type is totally separated, and every totally separated type is a set and ¬¬-separated.Source: §3.2 · p. 17
  • Total separatedness is equivalent to each point having a singleton quasi-component, the evaluation map X → 2^(2^X) being an embedding, and the apartness relation ♯2 being tight.Source: §3.2 · p. 18
  • Total separatedness is closed under retracts, binary products, arbitrary products, and sums indexed by discrete types, including binary sums.Source: §3.2 · p. 19
  • Constructively, total separatedness is not closed under dependent sums: Σx:N∞ 2^(x=∞) has a totally separated index and fibers, but its total separatedness implies ¬¬WLPO.Source: §3.2 · pp. 17, 20
  • The converse that every totally separated type is discrete fails constructively: 2^N is totally separated, but its discreteness implies WLPO.Source: §3.2 · p. 20
  • The Cantor type 2^N is totally separated, and its retract N∞ is discrete, which implies WLPO.Source: §3.2 · p. 21
  • If each A u is totally separated for u : N∞ and A ∞ is a proposition, then the sum ΣA is totally separated.Source: §3.2 · p. 21
  • Every type X has a totally separated reflection T X, and maps from X to any totally separated type factor uniquely through it.The reflector is the image of evalX, is surjective, and identifies x and y exactly when x =₂ y.Source: §3.2 · p. 21
  • Boolean-valued functions on X are in canonical bijection with boolean-valued functions on T X.Source: §3.2 · p. 22

4. Compact types

This section develops compactness and its variants, including their interactions with discreteness and total separatedness, and establishes closure properties and a micro-Tychonoff theorem for proposition-indexed products of compact pointed types. It also presents extended sums along embeddings as a construction of new compact types, alongside examples and limitations of these methods.

4.1. Definitions and first examples.

  • A type is compact when root existence is decidable for every Boolean-valued map; equivalently, sums of complemented families are decidable, and every compact type is decidable.The definition also has ∃-compact and Π-compact variants, obtained by changing the root-existence condition.Source: §4.1 · pp. 22–23
  • Every finite type is compact, while compactness and ∃-compactness of N are equivalent to LPO, and Π-compactness of N is equivalent to WLPO.Every type in a universe is compact if and only if global choice holds for that universe; the paper notes that global choice is constructively unacceptable and inconsistent with univalence [44, Corollary 3.2.7].Source: §4.1 · p. 23

4.2. Compact pointed types.

  • A type X is compact and pointed iff, for every Boolean-valued map p : X → 2, there is x0 such that p x0 = 1 implies p x = 1 for every x : X.Source: §4.2 · p. 24

4.3. Closure properties of compact types.

  • Compact types are closed under finite sums, dependent sums over compact bases, retracts, surjective images, and totally separated reflection; pointed compactness is preserved by retracts, sums, and surjective images.The results also give compactness of binary products and images of maps from compact types.Source: §4.3 · pp. 25–26
  • Without further axioms, compactness of countably infinite products cannot be proved in this type theory; compactness of 2^N is independent across the cited models.Under the unadopted Brouwerian principle that maps from 2^N to discrete types are uniformly continuous, every uniformly continuous Boolean-valued map on 2^N has a universal witness and root existence is decidable.Source: §4.3 · pp. 27–28

4.4. ∃-compactness and Π-compactness.

  • ∃-compactness and Π-compactness are propositions, compactness implies ∃-compactness, and ∃-compactness implies Π-compactness.For ∃-compact types, root existence is ¬¬-stable; Π-compactness is equivalent to the constant-1 map being isolated in 2^X, and both weaker notions are preserved by the totally separated reflection.Source: §4.4 · p. 28
  • A proposition is ∃-compact exactly when decidable; moreover, ∃-compact types have decidable truncation, non-empty ∃-compact types are inhabited, and Π-compact types have decidable negation.These properties follow by applying the compactness definitions to constant boolean-valued functions.Source: §4.4 · p. 30
  • An inhabited type is ∃-compact exactly when every boolean-valued function has a universal witness; an ∃-compact type is either empty or has this property.The universal witness may be available only in an unspecified way.Source: §4.4 · p. 30
  • A type is Π-compact exactly when every boolean-valued function on it has an infimum, which decides whether that function is constantly 1.The infimum is 1 precisely when all function values are 1.Source: §4.4 · p. 31
  • A type is ∃-compact exactly when every projection Y × X → Y sends complemented subsets to complemented subsets.Membership in the image is decided by ∃x:X p(y, x) = 0.Source: §4.4 · p. 31

4.5. Interplay between the notions.

  • Π-compactness of X with discrete fibers Y x makes the dependent product discrete; if X is compact, its discreteness strengthens to total separatedness.Source: §4.5 · p. 32
  • For disconnected Y, Π-compactness of Y^X implies X is Π-compact; if X is totally separated, it implies X is discrete, and otherwise the totally separated reflection T X is discrete.The paper also derives WLPO from Π-compactness of a simple type or of 2^N∞.Source: §4.5 · pp. 32–33

4.6. The micro-Tychonoff theorem.

  • If X is a proposition and every Y x is compact pointed, then the product of the family is compact pointed.The theorem restricts the index type to a proposition and requires each indexed type to be pointed.Source: §4.6 · p. 33
  • For a constant family, Y^X is compact pointed whenever pointedness of X implies compact pointedness of Y, whether or not X holds.Source: §4.6 · p. 34
  • The exponential NLPO is compact pointed, while its compactness holds independently of LPO, unlike compactness of N.LPO implies that N is compact pointed, allowing the micro-Tychonoff theorem to apply.Source: §4.6 · p. 34
  • Products of compact pointed types indexed by a proposition are compact pointed, and the result extends to subtypes of finite types; pointedness is essential constructively.Without pointedness, plain compactness would imply weak excluded middle.Source: §4.6 · pp. 34–35

4.7. Extension of families of compact types along embeddings.

  • In the N→N∞ construction, the Π-extension permits extending Y without checking whether its argument is ∞; along the embedding it recovers Y up to equivalence, and elsewhere yields the unit type.The extended sum generalizes the squashed sum to embeddings into compact pointed types and indexed families of compact pointed types.Source: §4.7 · p. 36
  • For an embedding into a compact pointed type, extending a family of compact pointed types and taking its sum again yields a compact pointed type.The fibers of the embedding are propositions, so the micro-Tychonoff theorem applies to the products defining the extension.Source: §4.7 · p. 36
  • Fiberwise Π-extensions preserve total separatedness for arbitrary maps, and pointwise retractions induce retractions of both extensions and extended sums.These closure properties support further compact-type constructions.Source: §4.7 · pp. 36–37
  • The extended sum of the constant family at 2^N along N ↪ N∞ is equivalent to the type of delayed binary sequences, which is itself equivalent to 2^N.More generally, extended sums along this embedding generalize the delay monad to countable families whose types may depend on their arrival time.Source: §4.7 · pp. 37, 39
  • For every natural number k, the type of decreasing sequences of natural numbers bounded by k is compact and totally separated.The construction identifies this type with an iterated extended-sum operation on the unit type.Source: §4.7 · p. 39

5. Equipping compact types with well-orders

This section develops ordinal theory and arithmetic for well-orders carried by compact types, including extended sums and suprema, and examines trichotomy and constructive limits on extensionality. It establishes preservation of well-order and compactness properties for these constructions, and shows that extended suprema are least upper bounds and preserve compact pointedness under stated conditions.

5.1. Ordinals in type theory.

  • A relation is well-founded exactly when transfinite induction holds; an ordinal has a proposition-valued, transitive, well-founded, extensional order, and its carrier is automatically a set.Source: §5.1 · pp. 40–41

5.2. Trichotomy.

  • Trichotomy implies discreteness; requiring all discrete ordinals to be trichotomous is equivalent to excluded middle, although Brouwer codes yield trichotomous ordinals without it.Source: §5.2 · p. 43

5.3. Ordinal arithmetic.

  • Ordinal addition concatenates well-orders, while multiplication is a lexicographic sum indexed by its right operand; such sums are ordinals when fibers are constant, indices trichotomous, or summands topped.The ordinal N∞ is topped by its largest element ∞.Source: §5.3 · pp. 43–46
  • Constructively, extensionality of every arbitrary lexicographic sum would imply excluded middle, so arbitrary indexed sums need not be ordinals.Source: §5.3 · p. 45
  • Ordinal addition, multiplication, and indexed sums preserve topped ordinals and trichotomous ordinals.Constructively, N∞ has a top but is not a successor ordinal because its top is not isolated.Source: §5.3 · p. 47

5.4. Extended sums.

  • Extending an ordinal family along an embedding gives a well-order at each point, and preserves toppedness when every member is topped.The construction restricts back to the original family along the embedding.Source: §5.4 · p. 48
  • Under univalence, ordinals and totally separated ordinals are algebraically injective.This follows from the extension construction and, for total separatedness, the corresponding result for types.Source: §5.4 · p. 49
  • For a family of topped ordinals indexed by N, the comparison map from the successor sum to the extended sum is an extremely dense, order-preserving, order-reflecting embedding.Source: §5.4 · p. 50

5.5. Extended suprema.

  • The supremum of any family of ordinals is an ordinal and its least upper bound; the map from the family’s sum onto it is surjective.Set replacement is assumed for the general existence of least upper bounds.Source: §5.5 · p. 51
  • Suprema of compact pointed ordinals remain compact pointed for compact pointed index types, including suprema of families extended along embeddings into such types.Source: §5.5 · pp. 51–52

6. Compact totally separated ordinals from Brouwer codes

This section develops and compares five Brouwer-code ordinal interpretations, examining how compactness, total separatedness, trichotomy, and discreteness vary across them. It focuses on the discrete fifth interpretation and the compact totally separated interpretation, including their comparison map and its relation to LPO.

6. Compact totally separated ordinals from Brouwer codes

  • The final interpretation embeds each code’s discrete ordinal extremely densely into its compact totally separated ordinal, an equivalence classically but not constructively.The image has empty complement, while a boolean-valued function distinguishes isolated image points from topological limit points.Source: §6 · p. 52

6.1. The standard interpretation.

  • The standard interpretation constructively yields neither compact nor trichotomous ordinals; universal compactness or trichotomy would imply LPO.Indeed, trichotomy of a single code constructed from a conatural number can decide whether that number is finite.Source: §6.1 · pp. 53–54

6.2. Three non-standard interpretations.

  • The three non-standard interpretations yield, respectively, trichotomous ordinals, compact totally separated ordinals that retract from 2^N, and compact ordinals.The first interpretation is discrete; compactness of the second is proved directly and does not follow from its retraction from 2^N.Source: §6.2 · pp. 55–56
  • Constructively, universal compactness of the trichotomous interpretation implies LPO, while universal total separatedness of the compact interpretation implies ¬¬WLPO.Compact pointed totally separated types need not remain totally separated under suprema: the paper gives a family whose supremum’s total separatedness implies ¬¬WLPO.Source: §6.2 · p. 56

6.3. Comparing the four interpretations.

  • Assuming excluded middle, the four interpretations are ordered so that the compact totally separated interpretation gives the largest ordinal.The comparison relies on excluded middle, including to make ordinal successor monotone and to bound suprema by corresponding sums.Source: §6.3 · p. 59
  • A universal standard-to-trichotomous comparison implies LPO, while the corresponding compact-totally-separated comparison implies ¬¬WLPO; whether the other two comparisons imply a constructive taboo remains open.The unresolved comparisons are standard-to-compact-totally-separated and trichotomous-to-discrete interpretations.Source: §6.3 · p. 60

6.4. A fifth interpretation.

  • The fifth interpretation is trichotomous and discrete for every code, but universally compact exactly under LPO; universal discreteness would imply WLPO.Trichotomy has no counterpart for the compact totally separated interpretation, since trichotomy implies discreteness.Source: §6.4 · pp. 61–62
  • For every Brouwer code, the comparison map from the fifth interpretation to the compact totally separated one is an embedding, extremely dense, order-preserving, and order-reflecting.For b=L(λi. Z), the map is the inclusion N+1 into N∞, and it is an equivalence exactly when LPO holds.Source: §6.4 · pp. 62–63
  • For b=L(λi. Z), the added point of N+1 is isolated, whereas ∞ in N∞ is isolated exactly when WLPO holds.The compact interpretation is always compact and totally separated, while its discreteness for every code is equivalent to WLPO.Source: §6.4 · pp. 61–63

6.5. The least element property.

  • For every Brouwer code, the compact interpretation has infima of complemented subsets, so every non-empty complemented subset has a least element; the discrete interpretation has this property universally exactly under LPO.Having infima strengthens pointed compactness.Source: §6.5 · p. 65

7. An inductive-recursive universe of compact ordinals

This section introduces inductive-recursive ordinal codes with discrete and compact interpretations, relates them to Brouwer codes, and classifies image points as isolated or limit points. It also establishes constructive limitations concerning compactness, discreteness, least elements, and total separatedness, and shows that under ¬WLPO isolatedness of image points is decidable.

7.1. Ordinal expressions and their discrete interpretation.

  • Inductive-recursive codes allow sum branching indexed by an earlier-stage ordinal; their discrete interpretations are retracts of N and trichotomous, while compactness of all such interpretations is equivalent to LPO.Source: §7 · p. 66, §7.1 · pp. 66–67

7.2. The compact interpretation.

  • The compact interpretation K is compact, and its extremely dense embedding of the discrete interpretation preserves order; every non-empty complemented subset of K has a least element.Constructively, the embedding is an equivalence for every code iff LPO; universal discreteness of K implies WLPO, while universal least-element existence for complemented subsets of the discrete interpretations is equivalent to LPO.Source: §7.2 · pp. 68–69

7.3. Inclusion of Brouwer codes into inductive-recursive codes.

  • The embedding of Brouwer codes into inductive-recursive codes preserves both interpretations, but total separatedness of every compact interpretation would imply ¬¬WLPO, so these codes denote strictly more compact ordinals.Source: §7.3 · pp. 71–73

7.4. Isolated points and limit points.

  • A boolean-valued function defined by induction on each code classifies points in the embedding’s image as isolated or limit points.A limit point is defined as a point whose isolatedness implies WLPO; in N∞, finite points are isolated and ∞ is a limit point.Source: §7.4 · p. 73
  • The limit point indicator classifies every embedded point as isolated or a topological limit point, and under ¬WLPO isolatedness is decidable.The indicator’s value 0 marks isolated points; its value 1 marks limit points.Source: §7.4 · p. 73
  • Order limit points and topological limit points differ: (∞, 1) is an order successor but a topological limit point.Its isolatedness would imply WLPO through its first coordinate ∞, a limit point of N∞.Source: §7.4 · p. 74

8. Discussion

The discussion summarizes two ordinal-notation systems and their interpretations, the embedding between discrete and compact ordinals, the constructions’ reach, and their Agda formalization.

8.1. Summary of results.

  • The two systems relate discrete and compact interpretations by an embedding; comparisons among other interpretations require excluded middle.The embedding needs no assumption.Source: §8.1 · p. 76
  • The inductive-recursive system E extends Brouwer codes, indexes sums by previously constructed discrete ordinals, and preserves both interpretations under their inclusion.E’s compact interpretation is totally separated for every code, which implies ¬¬WLPO; Brouwer-code compact interpretations are totally separated without that condition.Source: §8.1 · p. 76
  • Every non-empty complemented subset of either system’s compact ordinals has a least element; a Boolean-valued function distinguishes isolated and limit points in the embedding’s image.The embedding is an equivalence for every code precisely when LPO holds.Source: §8.1 · pp. 76–77
  • The constructions rely on compactness closure properties, a micro-Tychonoff theorem for proposition-indexed families, extensions along embeddings, and ordinal sums and suprema.Source: §8.1 · p. 77

8.2. Reaching large compact ordinals.

  • Earlier work reached compact totally separated ordinals below ε0 in Gödel’s T; Normann proved this is the best possible bound there.For closed subsets of Baire space, a T-definable search functional entails countability and Cantor–Bendixson rank below ε0.Source: §8.2 · p. 77
  • Reproducing T’s ordinal-building constructions and evaluating codes via J−KΣ1 yields compact totally separated ordinals dominating every ordinal below φε00.Source: §8.2 · p. 77
  • System E denotes strictly more compact ordinals in general than the Brouwer-code system.Source: §8.2 · p. 77

8.3. Formalization.

  • The results were formalized in Agda with safe and without-K checks, no postulates, and explicit assumptions where needed.Source: §8.3 · p. 78
Loading 2609.10447v3…