Eat. Sleep. Math.

I'm Jesse. UCLA '15, McMaster University '18. I am now a PhD student at the University of Pittsburgh. This is my blog, where I talk about what I'm studying.

[eatsleepmath]

This paper is primarily concerned with a special case of one of the leading problems of mathematical logic, the problem of finding a regular procedure to determine the truth or falsity of any given logical formula. But in the course of this investigation it is necessary to use certain theorems on combinations which have an independent interest and are most conveniently set out by themselves beforehand.

Frank Ramsey, before proving Ramsey’s theorem

[eatsleepmath]

Hilbert complained about being driven out of Cantor's paradise. Well, set theories like ZF allow us to be driven out the minimal amount.

John McCarthy, as quoted by Paul B. Jackson in The QED Workshop II (technical report)

[eatsleepmath]

Fundamental for us is ZFC. I feel it is not something esoteric for you. Rather, most mathematicians “do not know” of ZFC just as Monsieur Jourdain in Molière's Bourgeois Gentilhomme “did not know” he was speaking in prose; or, in the same way that most of us use freely the law of the excluded middle, “A or ¬A”, without any scruples, because we do not even notice that we are using it. Many times, we can read but not understand (mathematical writings). However, I guarantee you will understand, though not necessarily be able to read (including most of my audience and unfortunately myself) the following paragraph: MONSIEUR JOURDAIN: Quoi? quand je dis: “Nicole, apportez-moimes pantoufles, et me donnez mon bonnet de nuit”, c’est de la prose? MAITRE DE PHILOSOPHIE: Oui, Monsieur. MONSIEUR JOURDAIN: Par ma foi! il y a plus de quarante ans queje dis de la prose sans que j’en susse rien, et je vous suis le plus obligé du monde de m’avoir appris cela.

Saharon Shelah, Logical Dreams

[eatsleepmath]

We do not expect, however, that all machine-generated proofs will 'look human'. For example, there exists a machine-generated proof that a certain formula is a single axiom for groups satisfying \(x^{19} = 1\) for all \(x\). This proof contains a formula 715 symbols long. No human will find that proof.

Michael Beeson, The Mechanization of Mathematics

[eatsleepmath]

Translations of higher-order logic to first-order logic

Efficient encodings of higher-order logic in first-order logic are an essential component of sledgehammer-type automation for higher-order theorem proving. In this post, I record some notes on basic techniques of translating HOL to FOL. All code snippets are in Lean (I also freely conflate Prop and bool).

1 Monomorphization and λ-lifting

1.1 Monomorphization

Monomorphization (i.e., eliminating polymorphism) is the process of (repeatedly) heuristically instantiating quantifications over Type.

For example, the theorem eq.symm is polymorphic:

theorem eq.symm : ∀ {α : Sort u} {a b : α}, a = b → b = a := λ {α : Sort u} {a b : α} (h : a = b), h ▸ rfl

and if the tactic state contains the types bool and ℕ, then monomorphization should produce the instances

lemma bool.eq.symm : ∀ {a b : bool}, a = b → b = a := by apply eq.symm lemma nat.eq.symm : ∀ {a b : ℕ}, a = b → b = a := by apply eq.symm

1.2 λ-lifting

Given a λ-term t := λ x, foo x, define a new function symbol fₜ and replace all occurences of t with fₜ. Furthermore, fₜ must be axiomatized with the first-order translation of foo: ∀ x, f x = ⟦foo⟧ x. Since λ-terms might be nested, λ-lifting might have to be performed recursively. Once all the new function symbols are axiomatized, anything provable about the λ-terms should be provable about the new function symbols.

For example:

def baz : ℕ → ℕ := λ z, 2 * z + 1 def foo : ℕ → ℕ := λ y, y + baz y def t : ℕ → ℕ := λ x, foo x --now we lift lambdas constant f_baz : ℕ → ℕ constant f_baz_spec : ∀ z, f_baz z = 2 * z + 1 constant f_foo : ℕ → ℕ constant f_foo_spec : ∀ y, f_foo y = y + f_baz y constant f_t : ℕ → ℕ constant f_t_spec : ∀ x, f_t x = f_foo x lemma sanity_check₁ : f_t 40 = 121 := by rw[f_t_spec, f_foo_spec, f_baz_spec]; refl lemma sanity_check₂ (w : ℕ) : f_t w = (w + 2 * w + 1) := by rw[f_t_spec, f_foo_spec, f_baz_spec]; refl lemma sanity_check₁' : f_t 40 = 121 := sanity_check₂ _

1.3 Encoding λ-terms with Curry combinators

In addition to λ-lifting, which was discussed above, one can encode λ-terms using the Curry combinators I,K,S,B,C. (Technically, S and K suffice, but at the cost of producing output exponential in the number of λ's.) The combinators are defined as follows: I x := x, K x y := x, S x y z := x z (y z), B x y z = x (y z), and C x y z = x z y.

The translation of λ-expressions to combinators is defined by the following rules:

(λ x, x) ↦ I x

(λ x, p) ↦ K p, where p does not depend on x

λ x, p x ↦ p, where p does not depend on x

λ x, p q ↦ B p (λ x, q), where p does not depend on x

λ x, p q ↦ C (λ x, p) q, where q does not depend on x

λ x, p q ↦ S (λ x, p) (λ x, q), where p and q depend on x.

2 Three translation schemes

This section roughly follows Section 2 of Meng and Paulson's Translating Higher-Order Clauses to First-Order Clauses. In the first paragraph they single out three criteria for a formula to have higher-order features: (1) arguments of type a function type or Prop, (2) variables of type a function type of Prop, and (3) no "higher-type instances of overloaded constants". (I remark that in dependent type theory, these all mean the same thing, because (1) and (2) are both instances of parameters of a Π-type, and (3) is an instance of a implicit parameter of a Π-type (e.g. eq.symm above).)

A translation scheme T assigns a first-order formula (the translation) to every higher-order formula. A translation scheme is sound if whenever the first-order formula T(ϕ) is provable, then the higher-order formula ϕ is provable also. We'll review three translation schemes; only the first is sound. (Interestingly, the sound translation is the least useful.)

2.1 Fully typed

The fully typed translation is due to Hurd, and it is sound. Essentially, we:

add a sort S_Type whose elements are types, equipped with type constructors (e.g. λ A B, A → B),

for every sort S, add a new function symbol ti_S : S → S_Type which assigns each term to its "type",

denote function application using a binary function @, so e.g. f x becomes @(f,x),

convert translated terms of type Prop (which will be FOL terms) to FOL formulas via a predicate B.

2.2 Partially typed

In the partially typed translation, the typing operation ti is removed, and only the types of functions in function calls are included (as an additional argument to the application operator @). In contrast to the fully typed translation, schematic/free variables and constants are translated to FOL variables and constant symbols (without additional typing data), and only function applications are typed.

Using Meng and Paulson's example, if we have (X Y : α) and an infix operation (λ A B, A ≤ B : α → α → Prop), then under the fully typed translation, (X ≤ Y) would become

ti(@(ti(@(ti(≤, α → α → Prop), ti(X, α)), α → Prop), ti(Y, α)), Prop)

while under the partially typed translation, the same term would become

@(@(≤, X, α → α → Prop), Y, α → Prop).

2.3 Constant typed

The constant typed translation retains the minimum type information required to ensure correct overloading of constants. That is, any polymorphic constants (e.g. ≤ above) are monomorphized with a type ascription. Again using their example, if (X Y : ℕ), then (X ≤ Y) translates to

@(@(le(ℕ), X), Y)

2.4 Unsoundness

When typing information is removed, unsoundness can creep in when proofs use ill-typed terms. The canonical example is given by translating a finite type F = A | B. In both the partially typed and constant typed translation, the type ascription in the theorem ∀ x : F, x = A ∨ x = B is erased, and so the external prover is allowed to e.g. combine this fact with the axiom of infinity on ℕ. It turns out that by blocking the translation of these sorts of facts, the unsound translations rule out many unsound proofs and, by virtue of their speed, return more successful proofs than the fully typed translation. Interestingly, the best performance was achieved by the constant-typed translation, which discards as much type information as possible.

3 Further reading

What we've covered is far from the state of the art. For HOL-FOL translations, the interested reader could look at e.g. Chapter 6 of Jasmin Blanchette's thesis (link). There's also been work on DTT-FOL translations and sledgehammers (see CoqHammer). In addition to delegating to first-order ATPs, there has also been successful work on delegating proof search to SMT solvers. This also involves translation to first-order logic; see Chapter 2 of Sascha Böhme's thesis (link) (for Isabelle/HOL) and SMTCoq.

[eatsleepmath]

A formalization of forcing and the unprovability of the continuum hypothesis

I'm pleased to announce that the Flypitch project has passed a major milestone: we have completed a formalization of the unprovability of the continuum hypothesis from ZFC (by way of forcing with Boolean-valued models). This required implementing, among other things, a deep embedding of first-order logic with a proof system, the Godel completeness theorem, Boolean-valued semantics for first-order logic, a Boolean-valued soundness theorem, constructing a Boolean-valued model of ZFC, and some delicate transfinite combinatorics.

A draft of our paper describing this result is available here. It has been submitted to ITP 2019.

Interestingly, in translating the forcing argument to dependent type theory, not much set theory was actually needed do forcing. We didn't even need to start with an existing standard model or end up with a two-valued model of ZFC. It turns out that the commonly-used Aczel-Werner encoding of ZFC into (dependent type theory + calculus of inductive constructions) is actually a special case of the recursive name-construction from forcing, which allowed us to easily construct forcing extensions—as long as one is willing to work in a many-valued logic; otherwise, you have to carry a generic filter around to collapse the names into a two-valued model.

Since one can also use forcing to show the consistency of CH, and we have already set up much of the required infrastructure, I expect that we will soon have a complete formal proof of the independence of the continuum hypothesis.

Our formalization is in the Lean theorem prover, which implements a hierarchy of type universes to handle proper classes. Our construction for Boolean-valued models of set theory is universe-polymorphic—it takes a type universe and constructs a model of set theory one universe level up. Every conceivable forcing argument can be carried out at the bottom level of the universe hierarchy Type 0, and each new model of set theory lives in the next universe of types Type 1, and thus informs the structure of any models of set theory formed from Type 1, which live in Type 2, and so on. To me, this is a striking illustration of the richness of Lean's metatheory (in a way, unsurprising, since it is mutually interpretable with ZFC + countable many inaccessibles).

I should mention that forcing with Boolean-valued models is very close in spirit to forcing using double-negation sheaves. Lean's category theory library is not quite ready to handle involved arguments about sheaves on sites, but it is under heavy development, and it is conceivable that we could soon have a formalization of Kripke-Joyal semantics, after which it will be easy, given our existing work, to complete the sheaf-theoretic forcing argument for negating CH (again, with no need to perform the cumulative hierarchy construction to extract an actual model of ZFC—the soundness theorem for intuitionistic logic implicit in the Kripke-Joyal semantics specialized to a soundness theorem for classical logic in a Boolean topos will be enough.)

[eatsleepmath]

I am interested in mathematical logic, but the subject requires a certain way of thinking that proves very difficult for me to swallow. For example, there is the "theorem" and "metatheorem" distinction that one does not encounter in other parts of mathematics. Is assigning truth values to propositions in propositional logic a "meta" concept? In elementary texts on logic one draws truth tables to verify tautologies like "p implies p". Would that count as a metatheorem?

A metatheorem is a theorem (in a metatheory) about some formal system (the object theory), rather than a theorem in that formal system. So, ‘p and q implies q and p’ is a theorem in propositional logic, while “ ‘p and q implies q and p’ is a theorem in propositional logic” is a metatheorem about propositional logic.

Both of your specific questions are about semantics of propositional logic, which I would classify as a “meta” concept (with propositional logic as the object theory). For your second question, the fact that a propositional formula is a theorem in propositional logic if and only if the truth-table algorithm returns “true” for every Boolean valuation is an instance of a completeness theorem, and so is indeed a metatheorem about propositional logic.

[eatsleepmath]

Why haven't we heard from you, and what made you switch to formal theorem proving?

Hi anon! I’ve been busy being a first-year PhD student and working on my latest project, which aims to formalize the independence of the continuum hypothesis.There are a number of reasons why I switched to formal theorem proving. Mainly, I wanted to work with Tom Hales, my new advisor, and he wanted to do formal theorem proving. It seemed interesting, so I learned it. So far, it’s been very fun---a unique blend of mathematics and software engineering.

[eatsleepmath]

Departing from the usual author's statement, I would like to say that I am not responsible for any of the mistakes in this document. Any mistakes here are the responsibility of the reader. If anybody wants to point out a mistake to me, I promise to respond by saying "but you know what I meant to say, don't you?

Arthur Miller, Descriptive set theory and forcing

[eatsleepmath]

[Nagel] did propose to me as a separate project the reading of W.V. Quine's proof of the completeness of propositional logic, that had appeared [...] in the Journal of Symbolic logic. This was a stupendous experience in my education, now because of the subject of the paper, but because it showed me vividly that new work in logic and more generally in mathematics, was being published, and that---with great difficulty---I could read and follow it. [...] As to the concept of completeness which was the focus of Quine's paper, it did not get through to me. I simply noted that the aim of the paper was to show that every tautology had a formal proof in the system of axioms presented, and I expended my utmost effort to check Quine's reasoning that this was so, without ever reflecting on why author and reader were making this effort. This strictly limited objective also kept me from wondering how the author thought of putting the steps of the proof together; the result was that I failed to get "the idea of the proof," the essential ingredient needed for discovery.

Leon Henkin, The discovery of my completeness proofs

[eatsleepmath]

Illustration by Carina Willbold

[eatsleepmath]

Reconstructing groups and rings from faithful actions

Groups and group actions

Let \(G \curvearrowright X\) be a faithful group action. It is not necessarily transitive, and the actions of \(G\) on its orbits do not have to be faithful either. For each orbit \(O\) of \(G \curvearrowright X\), let \(K_O\) be the kernel of the associated group homomorphism \(\phi_O : G \to \operatorname{Sym}(O)\). Faithfulness is equivalent to \(\bigcap_O K_O = 1\).

The motivating question is:

Question. How do we recognize the image \(G' \subseteq \operatorname{Sym}(X)\) of \(\phi_X : G \hookrightarrow \operatorname{Sym}(X)\)?

Clearly, a necessary condition for a permutation \(\sigma \in \operatorname{Sym}(X)\) to be in \(G'\) is for all the orbits of \(G \curvearrowright X\) to be invariant under \(\sigma\).

Generalizing slightly, note that \(G\) (and \(\operatorname{Sym}(X)\)) have a natural product action on any power \(X^{I}\) of \(X\), by \(g.(x_i)_{i \in I} \overset{\operatorname{df}}{=} (g.x_i)_{i \in I}\). We call an orbit of the product action on \(X^I\) an \(I\)-orbit of \(X\). For \(\sigma\) to belong to \(G'\), it is also necessary that for every \(I\), every \(I\)-orbit of \(X\) is \(\sigma\)-invariant.

Suppose that we restrict to the permutations with respect to which all the orbits of \(G\) are invariant. Unless if \(G\) is a product of the permutation groups of those orbits, the subgroup of all such permutations is larger than \(G\).

This leads to the next natural question:

Question 2. Can we specify a collection of index sets \((I_{\alpha})_{\alpha}\) such that \[\left\{\sigma \in \operatorname{Sym}(X) \operatorname{\big{|}} \text{for all $\alpha$, for every $I_{\alpha}$-orbit $O$, $O$ is $\sigma$-invariant}\right\} = G'?\]

So in the previous paragraph, we saw that the answer to this question is “no” if \((I_{\alpha})_{\alpha}\) is just \(\{1\}\).

Proposition. We can answer “yes” to Question 2 by putting \((I_{\alpha})_{\alpha} = \{|X|\}\).

Proof. Fix an enumeration \((x_i)_{i \in |X|}\). Its orbit \(O\left((x_i)_{i \in |X|}\right)\) is an \(|X|\)-orbit of \(X\), and looks like \[\left\{(g . x_i)_{i \in |X|} \operatorname{\big{|}} g \in G\right\}.\] If \(\sigma\) is a permutation such that \(O\left((x_i)_{i \in |X|}\right)\) is \(\sigma\)-invariant, then there exists some \(g \in G\) such that \[\sigma . (x_i)_{i \in |X|} = (\sigma . x_i)_{i \in |X|} = (g. x_i)_{i \in |X|}.\]

Therefore, for every \(x \in X\), \(\sigma(x) = g . x\), and so \(\sigma = \phi_X(g)\), where \(\phi_X\) is the action map \(G \to \operatorname{Sym}(X)\). \(\square\)

Actually, this previous argument works to reconstruct \(G'\) even when the action is not faithful, and in fact only requires just that one \(|X|\)-orbit, not any of the others.

Here is an alternate way of reconstructing \(G\). Recall that if \(G \curvearrowright X\) is a faithful and transitive action, then it is isomorphic as a \(G\)-set to the regular action \(G \curvearrowright G\), and \(\operatorname{Aut}_{G\text{-}\mathbf{Set}}(G \curvearrowright G) \simeq G\) (by looking at what the action does on the identity \(e_G\)).

Here’s the trick: we can define what it means for a permutation \(\sigma\) to be an automorphism of a \(G\)-set \(G \curvearrowright X\) by requiring \(\sigma\)-invariance for certain subsets of \(X \times X\).

Lemma. A permutation \(\sigma : X \to X\) is compatible with a \(G\)-action \(G \curvearrowright X\) (i.e. \(\sigma\) is \(G\)-equivariant) if and only if for every \(g \in G\), the graph \(\Gamma(g) \subseteq X \times X\), given by \(\Gamma(g) \overset{\operatorname{df}}{=} \left\{(x, g.x) \operatorname{\big{|}} x \in X \right\}\), is \(\sigma\)-invariant.

Proof. Suppose \(\sigma\) is already \(G\)-equivariant, so that for all \(x\) and for all \(g\), \(g. \sigma(x) = \sigma(g.x)\). Then for every \(g\), \(\sigma.(x, g.x)\) = \((\sigma(x), \sigma(g.x)) = (\sigma(x), g.\sigma(x)) \in \Gamma(g)\).

Conversely, suppose that for every \(g\), \(\Gamma(g)\) is \(\sigma\)-invariant. Then for every \(x \in X\), \(\sigma(x, g.x) = (\sigma x, \sigma(g.x)) \in \Gamma(g)\), which means that \(\sigma(g.x) = g.\sigma(x)\). \(\square\)

So, suppose that \(G\) acts faithfully on \(X\). As we mentioned in the beginning, this action doesn’t need to be faithful on any of the orbits. However, let’s look at the product action on \(X^X\). Fix an enumeration \((x_i)\) of \(X\), which will be an element of \(X^X\). Then \(G\)’s action on the orbit of \((x_i)\) is faithful: if \(g_1 \neq g_2\), then since the original action was faithful, there exists some \(x_j\) such that \(g_1. x_j \neq g_2.x_j\). Then \(g_1.(x_i)\) and \(g_2.(x_i)\) do not agree at the \(j\)th component, and so are not the same. Since an orbit is by definition transitive, \(G \curvearrowright O\left((x_i)\right)\) is faithful and transitive (and therefore we have found an isomorphic of \(G \curvearrowright G\) inside \(G \curvearrowright X^X\)!) Now, name the graphs of the action of each \(g \in G\) on \(O(\left((x_i)\right))\). These are subsets of \(X^{X \times X}\), and if they are simultaneously invariant under some \(\sigma \in \operatorname{Sym}(X)\), then \(\sigma\) acts as a \(G\)-set automorphism on \(O((x_i)_{i \in I})\) and as a \(G\)-set automorphism on \(X\).

So the subgroup of all such \(\sigma\) embeds via some map \(\psi\) into \(\operatorname{Aut}(O((x_i))) \simeq \operatorname{Aut}(G \curvearrowright G) \simeq G\).1

Conversely, let \(\rho \in \operatorname{Aut}(G \curvearrowright G)\). Then \(\rho\) is given by right-multiplication by some group element \(g\); chasing \(g\) through the isomorphism \(G \curvearrowright O((x_i)) \simeq G \curvearrowright G\) yields another group element \(g'\) such that right-multiplication by \(g'\) gives an automorphism \(\rho'\) of \(O((x_i))\), and \(\psi(\rho') = \rho\), showing that \(\psi\) is bijective, so the subgroup of all such \(\sigma\) is isomorphic to \(G\).

Rings and modules

The last thing I want to mention is that this all works equally well for rings and modules in place of groups and sets, and linear self-maps in place of permutations. Indeed, the two arguments presented above go through mutatis mutandis.

Proposition. Let \(R \curvearrowright M\) be an \(R\)-module. Fix an enumeration \((m_i)\) of \(M\). Then the image \(\phi_M(R)\) of the action map \(\phi_M : R \to \operatorname{End}(M)\) is equal to the following set: \[\left\{\sigma \in \operatorname{Hom}_{R\text{-}\operatorname{\mathbf{Mod}}}(M, M) \operatorname{\big{|}} O((m_i)) \text{ is $\sigma$-invariant under the product action} \right\}.\]

Proof. It is clear that for each \(r \in R\), scalar multiplication by \(r\) belongs to the set displayed above. Conversely, let \(\sigma\) belong to the set displayed above. Since \(O((m_i))\) is \(\sigma\)-invariant, there exists some \(r \in R\) such that \[\sigma.(m_i) = (\sigma . m_i) = (r . m_i),\] and so for every \(m \in M\), \(\sigma.m = r.m\). \(\square\)

Similarly, if \(R \curvearrowright M\) is faithful, then \(R\)’s product action on the orbit of \((m_i)\) is faithful and transitive, and thus \(O(m_i)\) is isomorphic to \(R \curvearrowright R\), which is isomorphic to \(R\). And \(\operatorname{Hom}_{R\text{-}\operatorname{\mathbf{Mod}}}(R, R)\) is again \(R\), so naming the graphs of the scalar multiplications does the trick as in the case for groups.

These isomorphisms are obtained as follows. We can choose a \(G\)-\(\mathbf{Set}\) isomorphism \(\iota : O((x_i)) \simeq G\). \(\iota\) induces by conjugation an isomorphism \(\operatorname{Aut}_{G\text{-}\mathbf{Set}}(O((x_i))) \simeq \operatorname{Aut}_{G\text{-}\mathbf{Set}}(G)\), and then there is a canonical isomorphism \(G \to \operatorname{Aut}_{G \text{-}\mathbf{Set}}(G)\) by right-multiplication.↩

[twocubes]

[eatsleepmath]

Is "First Order Categorical Logic" by Makkai & Reyes worth keeping in my digital library in case I one day decide to study that subject? I imagine it might be hopelessly dated or simply not the best source to learn that material from, but I just don't know.

The book is still the essential reference for fundamental results in categorical first-order logic. They go to the trouble of spelling out proofs for "obvious" results (like a category-theoretic completeness theorem for logical categories) that are, in practice, rather gruesome to prove. For that reason, the book is still very valuable.Furthermore, I think this is one of the first places, if not the first, where pretoposes and classifying toposes are studied. A streamlined exposition for these can be found in the Elephant, but the details can be found written very clearly in Makkai-Reyes.

[eatsleepmath]

Hyperimaginaries, pseudometrics, and uniform spaces

On one hand, there’s a well-known correspondence between pseudometrics and uniform structures; on the other hand, the type defining a type-definable equivalence relation looks like a collection of entourages defining a uniformity. Indeed, passing through the correspondence, type-definable equivalence relations are precisely the distance-0-apart equivalence relation of their corresponding pseudometric, and this is how one can treat hyperimaginaries on equal footing with imaginary sorts (by viewing a discrete first-order structure as a continuous first-order structure.) Apparently, this was one of the motivations for IBY to develop continuous logic.

At some point, I was interested in this, and wrote it down to understand it. What follows are my notes.

The classic reference for uniform structures is Bourbaki’s Topologie Générale, Chapter II, which we will closely follow.

Definition. A pseudometric on a set \(X\) is a function \(X \times X \overset{f}{\to} \overline{\mathbb{R}}\) from \(X \times X\) to the extended real line \(\overline{R} = \mathbb{R} \cup \{+\infty\}\) which satisfies all the properties of a metric (symmetric, positivity, triangle inequality) except that \(f(x,y) = 0\) does not necessarily imply that \(x = y\).

Definition. Let \(X\) be a set. A uniform structure, or uniformity, on \(X\) consists of a collection \(\Phi\) of reflexive relations \(U \subseteq X \times X\) satisfying the following conditions:

\(\Phi\) is a filter.

If \(U \in \Phi\), then there is a \(V \in \Phi\) such that \[V \circ V \overset{\operatorname{df}}{=} \{(x,z) \operatorname{\big{|}} \exists y \in X \text{ s.t. } (x,y) \in V \land (y,z) \in V\}.\]

The members \(U\) of the uniformity \(\Phi\) are sometimes called entourages. Every uniformity \(\Phi\) can be given a filter base consisting of symmetric \(U\)’s.

Families of pseudometrics induce uniformities:

Proposition. (Section 9.2 in Topologie Générale) Let \(f\) be a pseudometric on a set \(X\). For each \(a > 0\), set \(U_{a} \overset{\operatorname{df}}{=} f^{-1}([0,a])\). Then the collection \((U_a)_{a \in \mathbb{R}^+}\) forms a filter base for a uniform structure \(\mathscr{U}\) on \(X\).

Proof. Let \(U'\) contain \(U_a\) and \(U''\) contain \(U_b\). Then \(U' \cap U''\) contains \(U_a \cap U_b = U_{\min(a,b)}\). By definition \(\mathscr{U}\) is also upwards-closed. By the triangle inequality, \(U_a\) contains \(U_{\frac{a}{2}} \circ U_{\frac{a}{2}}\). \(\square\)

Definition. (9.2.2 in ) Given a pseudometric \(f\) on a set \(X\), the uniformity defined by \(f\) is the uniformity on \(X\) which has a filter base of entourages the family of sets \(f^{-1}([0,a])\) where \(a \in \mathbb{R}^+\).

(This amounts to taking the inverse image under \(f\) of the neighborhood filter of \(0\) in the subspace \([0, +\infty)\) of \(\mathbb{R}\).)

We say that two pseudometrics on \(X\) are equivalent if they define the same uniformity.

Definition. (9.2.3 in Topologie Générale) If \((f_i)_{i \in I}\) is a family of pseudometrics on a set \(X\), then the least upper bound of the set of uniformities defined on \(X\) by the pseudometrics \(f_i\) is called the uniformity defined by the family \((f_i)\).

Two families of pseudometrics are said to be equivalent if they define the same uniformity on \(X\).

Remark. (9.3 in Topologie Générale) Let \(\mathscr{U}\) be generated by the family of pseudometrics \((f_i)\). \(\mathscr{U}\) is Hausdorff if and only if every pair of points \((x,y)\) is separated by some \(f_i\).

Every uniformity is induced by some family of pseudometrics

Importantly, any uniform structure can be realized as the uniformity induced by a family of pseudometrics.

Lemma. (9.4.2 in Topologie Générale) If a uniformity \(\mathscr{U}\) on \(X\) has a countable filter base, then there is a pseudometric \(f\) on \(X\) such that \(\mathscr{U}\) is identical with the uniformity defined by \(f\).

Proof. Let \((V_n)\) be a countable filter base for \(\mathscr{U}\). Define inductively a sequence \((U_n)\) of symmetric entourages of \(\mathscr{U}\) such that

\(U_1 \subset V_1\), and

\(U_{n+1} \circ U_{n+1} \circ U_{n+1} \subset U_n \cap V_n\).

(How? Take \(U_{n+1}\) to be the entourage \(V\) such that \(V \circ V \subset V'\), where \(V'\) is the entourage such that \(V' \circ V' \subseteq U_n \cap V_n \in \mathscr{U}\).)

Claim. This \((U_n)\) again is a filter base for a uniformity which coincides with \(\mathscr{U}\).

Proof.

Each member of \(U_n\) clearly contains the diagonal.

Since the \(U_n\) were symmetric, any the reverse \(U'^{-1}\) of any \(U'\) containing \(U_i\) again contains \(U_i\).

If \(U' \subseteq U_n\), and \(U_n\) contains \(U_{n+1} \circ U_{n+1} \circ U_{n+1}\), then it is easy to check that this must also contain \(U_{n+1} \circ U_{n+1}\).

Why is the filter generated by \((U_n)\) again \(\mathscr{U}\)? It suffices to check that each \(U \in \mathscr{U}\) contains some \(U_n\). Let \(U \in \mathscr{U}\). Since \(\mathscr{U}\) is generated by the countable filter base \((V_n)\), \(U\) contains \(V_k\) for some \(k\), and by construction \(V_k\) contains \(V_k \cap U_k\), which contains \(U_{k + 1} \circ U_{k + 1} \circ U_{k+1} \supset U_{k+1}\).

\(\square\)

Now, we have obtained in place of the countable filter base \((V_n)\) of \(\mathscr{U}\) an equivalent countable filtration \((U_n)\) which is also a filter base of \(\mathscr{U}\).

We can therefore associate a natural valuation \(v(x,y)\) to every pair \((x,y) \in X \times X\), defined by \[v(x,y) \overset{\operatorname{df}}{=} n - 1,\] where \(n\) is the index of the first \(U_n\) such that \((x,y) \not \in U_n\).

In case \((x,y) \in \bigcap_n U_n\), we say that \(v(x,y) = \infty\).

Define as follows the real-valued function \(g\) on \(X \times X\), by \[g(x,y) \overset{\operatorname{df}}{=} 2^{-v(x,y)},\] so in case \((x,y) \in \bigcap_{n} U_n\), \(g(x,y) = 1\).

\(g\) is symmetric because each \(U_k\) was, positive by definition, and \(g^{-1}(\{0\})\) contains the diagonal relation \(\Delta_X \subseteq X \times X\) because every \(V \in \mathscr{U}\) contained \(\Delta_X\).

\(g\) does not a priori satisfy the triangle inequality. (If it did, then for each \(x,y,\) and \(z\) and each value \(c - 1\) for \((x,y)\) there would only be finitely many values \(a - 1\) and \(b - 1\) for \((x,z)\) and \((z,y)\), which is quite strong.)

However, we can build something out of \(g\) which does. Define as follows the real-valued function \(f\) by

\[f(x,y) = \inf \left\{\sum_{i = 0}^{p - 1} g(z_i. z_{i + 1}) \right\},\] (where the inf is taken over over all finite sequences \((z_i)_{0 \leq i \leq p}\), \(p \in \mathbb{N}\), with \(z_0 = x, z_p = y\))

Claim. \(f\) is a pseudometric which satisfies the inequalities \[\frac{1}{2} g(x,y) \leq f(x,y) \leq g(x,y).\]

Proof.

(Symmetry.) If \(f(y,x) = a\) is approximated by a sequence of finite sequences \((z_j \leq p_i)_{i \in I}\), then by reversing the sequences and using the symmetry of \(g\), \(a = f(x,y)\) also.

(Positivity.) \(f(x,y)\) is an inf of sums of nonnegative numbers.

(Triangle inequality.) Let \(x,y,z \in X\). When we write e.g. “\(x \to z\)” we mean to index finite paths starting at \(x\) and ending at \(z\). We have: \[\inf_{x \to z} \left\{ \sum_{i = 0}^{p-1} g(z_i. z_{i + 1}) \right\} + \inf_{z \to y} \left\{ \sum_{i = 0}^{p - 1} g(z_i. z_{i + 1})\right\}\] \[= \inf_{x \to z \to y} \left\{ \sum_{i = 0}^{p-1} g(z_i. z_{i+1}) \right\} \geq \inf_{x \to y} \left\{ \sum_{i = 0}^{p-1} g(z_i. z_{i+1})\right\} = f(x,y),\] where the latter inequality holds because the infimum on the right is being computed over at least all the paths the infimum on the left is being computed over, and the former equality holds because the two infima are independent (the paths \(x \to z \to y\) split into the product \((x \to z) \times (z \to y)\)).

(Fiber over \(0\) contains the diagonal.) By definition, \(f(x,x) \leq g(x,x) = 0\).

(\(\frac{1}{2} g(x,y) \leq f(x,y) \leq g(x,y)\).) Let’s verify that \(\frac{1}{2} g(x,y) \leq f(x,y).\) We proceed by induction on the length \(p + 1\) of a finite path \(x \to y\) to prove that \[\frac{1}{2} g(x,y) \leq \sum_{ i = 0}^{p-1} g(z_i, z_{i+1}).\] If \(p = 1\), then certainly \(g(x,y) \geq \frac{1}{2} g(x,y)\), so the base case is proved.

If we set \(a \overset{\operatorname{df}}{=} \displaystyle \sum_{i = 0}^{p-1} g(z_i, z_{i + 1})\), then the equation is true if \(a \geq \frac{1}{2}\), since \(g(x,y) \leq 1\). Suppose then that \(a < \frac{1}{2}\). Let \(h\) be the first index \(k\) such that \[\sum_{i < k}^{p- 1} g( z_i, z_{i+1}) \geq \frac{a}{2}.\]

Note that by choice of \(h\), \(\sum_{i < h - 1} g (z_i, z_{i + 1}) < \frac{a}{2}\), and \(\sum_{i > h -1} g(z_i, z_{i + 1}) \leq \frac{a}{2}\).

By the induction hypothesis, \[\frac{1}{2} g(x, z_{h-1}) \leq f(x,z_{h-1}) = \inf \left\{sum_{i < h} g(z_i, z_{i + 1}) \right\} < \frac{a}{2}.\] Therefore, \(\frac{1}{2} g(x, z_{h-1}) \leq \frac{a}{2}\), which implies that \(g(x, z_{h - 1}) \leq a\). Similarly, \(g(z_h, y) \leq a\).

If \(k\) is the integer such that \(\frac{1}{2^k}\) is the closest dyadic lower bound on \(a\) (with \(k \geq 2\) since \(a < \frac{1}{2}\)), then since \(g\) takes dyadic values, \[g(x,z_{h-1}) \leq \frac{1}{2^k} \hspace{2mm} \text{ and } \hspace{2mm} g(z_h, y) \leq \frac{1}{2^k}.\] Since \(\frac{1}{2^{(k + 1)-1}}\), then by how \(g\) was defined, \((x,z_{h - 1})\) and \((z_h,y)\) are in \(U_k\). Since evidently \(g(z_{h - 1}, z_h) \leq a\), \((z_{h - 1}, z_h) \in U_k\) as well. Since \(U_k \circ U_k \circ U_k \subseteq U_{k - 1}\), \((x,y) \in U_{k - 1}\).

Now, \[g(x,y) \leq \dfrac{1}{2^{k- 1}} = 2 \cdot \dfrac{1}{2^k} \leq 2a.\]

Therefore, \(\frac{1}{2} g(x,y) \leq a\). Taking infima, conclude \[\frac{1}{2} g(x,y) \leq f(x,y),\] and the claim is proved.

\(\square\)

Now we show that the uniformity \(\mathscr{U}(f)\) generated by \(f\) coincides with the uniformity \(\mathscr{U}\). \(f^{-1}([0,a])\) contains \(U_k\) if \(2^{-k} < a\), so \(\mathscr{U}(f)\) is certainly coarser than \(\mathscr{U}\). On the other hand, each \(U_k\) from \((U_n)\) contains the set of all points \((x,y)\) such that \(f(x,y) \leq \frac{1}{2^{k + 1}}\), which means that \(\frac{1}{2} g(x,y) \leq \frac{1}{2^{k + 1}}\) amd therefore \(g(x,y) \leq \frac{1}{2^k}\), so this says that each such \((x,y)\) is inside \(U_k\), so \(f^{-1}([0, \frac{1}{2^{k + 1}}])\). Since every member of a filter base for \(\mathscr{U}(f)\) contains a member of a filter base for \(\mathscr{U}\) and vice-versa, they must generate the same uniformity \(\mathscr{U}\). \(\square\)

Theorem. (9.4.1 in Topologie Générale Given a uniformity \(\mathscr{U}\) on a set \(X\), there is a family of pseudometrics on \(X\) such that the uniformity defined by this family is identical with \(\mathscr{U}\).

Proof. For every \(V \in \mathscr{U}\), inductively define a filtration of symmetric entourages \((U_n)\) such that \(U_1 \subseteq V\) and \(U_{n + 1} \circ U_{n + 1} \subset U_n\) for all \(n \geq 1\).

Claim. The sequence \((U_n)\) is a filter base for a uniformity \(\mathscr{U}_V\) coarser than \(\mathscr{U}\).

Proof.

If \(U'\) contains a \(U_i\), then \(U_i \supseteq \Delta_X\) by definition, so \(U'\) contains \(\Delta_X\) also.

If \(U'\) contains \(U_i\), then since \(U_i\) was symmetric, \(U'^{-1}\) also contains \(U_i\).

If \(U'\) contains \(U_i\), then since \(U_i \supseteq U_{i+1} \circ U_{i+1}\), \(U'\) contains \(U_{i+1} \circ U_{i + 1}\) also.

\(\mathscr{U}_V\) is coarser than \(\mathscr{U}\) because the filter base for \(\mathscr{U}_V\) is contained inside \(\mathscr{U}\).

\(\square\)

Furthermore, \(\mathscr{U}\) is the least upper bound of all the uniformities \(U_V\) for \(V\) running through \(\mathscr{U}\). Therefore it suffices to induce each countably-based uniformity \(\mathscr{U}_V\) by a pseudometric, and we have already shown that this is possible. \(\square\)

Hyperimaginary sorts and uniform structures

A uniformity on a set \(X\) given by a filter \(\Phi\) of entourages looks suspiciously like a type-definable equivalence relation. Indeed, the intersection \(\bigcap \Phi\) is an equivalence relation on \(X\), and in the case when \(\Phi\) was induced by a pseudometric, \(\bigcap \Phi\) is the equivalence relation of points distance \(0\) from each other.

More importantly, any type-definable equivalence relation on a model \(X\) is the filter base for a uniformity on \(X\):

Proposition. Let \(E = \bigcap \Phi\) be a type-definable equivalence relation on \(X\). Then for every \(\varphi_i(x,y) \in \Phi\), there exists another \(\varphi_j(x,y) \in \Phi\) such that \[\models \left(\exists z\hspace{1mm} \varphi_j(x,z) \land \varphi_j(z,y) \right) \rightarrow \varphi_i(x,y).\]

Proof. This is just compactness: \[\exists z \hspace{1mm}\Phi(x,z) \land \Phi(z,y) \models \varphi_i(x,y),\] hence \[\left(\exists z \hspace{1mm} \Phi(x,z) \land \Phi(z,y) \right) \land \neg \varphi_i(x,y)\] is inconsistent. Compactness tells us this inconsistency is finitely supported, and since \(\Phi\) can be assumed to be closed under finite conjunctions, there is a single \(\varphi_j(x,y)\) such that \[\left(\exists z \hspace{1mm} \varphi_j(x,z) \land \varphi(z,y) \right) \land \neg \varphi_i(x,y)\] is inconsistent. Since the above is only a finite conjunction of formulas, saying it is inconsistent is the same as saying that its negation holds, but then by material implication, we have therefore shown \[\models \left(\exists z \varphi_j(x, z) \land \varphi(z,y) \right) \rightarrow \varphi_i(x,y).\] \(\square\)

Therefore, in light of the fact that every uniformity is induced by a family of pseudometrics, to every type-definable equivalence relation \(E\) on a model \(M\) we can associate a family of pseudometrics \((f_i^E)\). In light of the fact that every countably-based uniformity is induced by a single pseudometric, when \(E\) is equivalent to a countable conjunction of formulas we can then associate to \(E\) a single pseudometric \(f^E\).

[eatsleepmath]

An illustration of the Cherlin-Hrushovski construction

The following construction, due to Cherlin and Hrushovski, provides an example of an \(\aleph_0\)-categorical theory which is not \(G\)-finite, nor which has the small index property: take an infinite set \(A\), and expand it by equivalence relations \(E_n\) on each power \(A^n\) such that each \(E_n\) has two infinite classes and the finite imaginaries \(\{A^n/E_n\}\) are all independent. Call the resulting structure \(\mathfrak{A}\).

\(\operatorname{Aut}(\mathfrak{A})\) then has \(\left(\mathbb{Z}/2 \mathbb{Z} \right)^{\omega}\) as a quotient.

By increasing the number of equivalence classes, one can encode as a quotient of \(\operatorname{Aut}(\mathfrak{A})\) arbitrary countable products of finite symmetric groups. By introducing more predicates, one can cut down on the number of symmetries and thus encode as a quotient of \(\operatorname{Aut}(\mathfrak{A})\) arbitrary countable products of finite groups. By introducing relations which interpret functions between finite sets of imaginaries in \(\mathfrak{A}^{\operatorname{eq}}\), one can encode as a quotient of \(\operatorname{Aut}(\mathfrak{A})\) an arbitrary separable profinite group. For more detail, see Evans and Hewitt’s 1990 paper Counterexamples to a conjecture on relative categoricity.

The purpose of this post is to explicitly write down (indeed, even draw, with many colors!) what the structure \(\mathfrak{A}\) encoding \(\left(\mathbb{Z}/2 \mathbb{Z} \right)^{\omega}\) as a quotient of \(\operatorname{Aut}(\mathfrak{A})\) looks like. The existence of \(\mathfrak{A}\) is usually justified by taking a Fraïssé limit of an appropriate class of structures, which to me always seems rather black-boxy. So, I went to the trouble of writing down what \(\mathfrak{A}\) might look like. As it turns out, our calculation of \(\mathfrak{A}\) will show, rather nicely, why one should expect such an \(\mathfrak{A}\) to pop out of a Fraïssé construction in the first place.

In an appropriate category \(\mathbf{Struct}\) of multisorted first-order structures and interpretations, we can achieve \((\mathbb{Z}/2\mathbb{Z})^{\omega}\) as a quotient of some \(\operatorname{Aut}(\mathfrak{A})\) with much less work. In an abandoned chapter of my master’s thesis, I showed that given a projective diagram of groups \(G_i\) with projective limit \(G\), one can take the invariant/canonical structures of the actions \[\operatorname{Inv}\left(G_i \curvearrowright G_i\right)\] and form their colimit \(\mathfrak{B}\) in \(\mathbf{Struct}\), which has a sort for each \(G_i \curvearrowright G_i\), with definable functions linking the sorts corresponding to the transition maps in the original projective diagram. The automorphism group of \(\mathfrak{B}\) is \(G\), and it is easy to find a multisorted structure \(\mathfrak{A}\) which interprets \(\mathfrak{B}\) such that the induced continuous map \(\operatorname{Aut}(\mathfrak{A}) \to \operatorname{Aut}(\mathfrak{B})\) is surjective.

Of course, putting the equivalence relations on disjoint sorts completely bypasses the interesting part of the problem of writing down the Cherlin-Hrushovski construction in a \(1\)-sorted structure \(\mathfrak{A}\): we have to arrange the equivalence relations on \(A\), \(A^2\), \(A^3, \dots\) to be independent despite interference from the diagonal and projection maps linking the powers of \(A\).

Here’s an example that shows that this is not a vacuous problem. Given an equivalence relation \(E\) on \(A\), there is an induced equivalence relation \(E'\) on \(A \times A\), given by the kernel of the natural map \[A \times A \twoheadrightarrow A/E \times A/E, \text{ by } (a_1, a_2) \mapsto (a_1/E, a_2/E).\]

(Incidentally, this shows that a product of imaginary sorts is an imaginary sort in \(T^{\operatorname{eq}}\).)

Then it is impossible to find an automorphism of \(A\) which fixes the \(A/E\) while permuting \(A^2/E'\): if \(a\) and \(b\) are not \(E\)-equivalent, then \((a,b)\) and \((b,a)\) are not \(E'\)-equivalent, and any automorphism which interchanges the \(E\)-classes of \(a\) and \(b\) will interchange the \(E'\)-classes of \((a,b)\) and \((b,a)\).

So let’s proceed with the illustration. Let’s just try to encode \(\mathbb{Z}/2\mathbb{Z} \times \mathbb{Z}/2\mathbb{Z}\) on \(A\) and \(A \times A\) first. Getting just \(\mathbb{Z}/2\mathbb{Z}\) is easy, since any equivalence relation with two infinite classes on \(A\) will do. So, our task is to figure out how to specify \(E_2\) on \(A \times A\). The identity map always gives us the identity group element \((0,0)\), so now we just have to achieve the generators \((0,1)\) and \((1,0)\).

We’ll let the underlying set \(A\) be an interval, say \([-1,1]\), and we’ll specify \(E_1\) on \(A\) by coloring \(A\) half green and half-purple:

and so \(A/E_1\) consists of green and purple:

Now we have to figure out how to color \(A \times A\) blue and orange:

Let’s go to a toy example and temporarily replace \(A\) with the finite set \(A = \{a,b,c,d\}\), such that \(E_1 \rightrightarrows A\) is given by coloring \(a,b\) green and \(c,d\) purple. Here’s \(A \times A\):

Since the identity permutation fixes everything, an immediate candidate for an automorphism of \(A\) which fixes green and purple but which interchanges blue and orange (whatever we specify that to be) is the permutation which interchanges \(a\) with \(b\) and \(c\) with \(d\). Here’s what it does on pairs:

Similarly, assuming the previous guess is consistent, if we want to interchange green and purple but fix blue and orange, an immediate candidate is given by interchanging \(a\) with \(c\) and \(b\) with \(d\). Here is its action:

Now, by just eyeballing this we can work out a coloring. Suppose that \((d,a)\) was orange. Then since the red arrows are supposed to permute \(E_2\)-classes, \((c,b)\) must be blue. Since the blue arrows are supposed to fix \(E_2\)-classes, \((b,c)\) must be orange and \((a,d)\) must be blue. Continuing in this way, we arrive at the following coloring of \(A \times A\):

Now let’s go back to \(A = [-1,1]\). There’s an obvious way of tranposing the previous coloring to \(A \times A = [-1,1] \times [-1,1]\), by cutting up \(A \times A\) into \(16\) pieces:

Mutatis mutandis, everything works: the following automorphism induces \((0,1)\):

While this automorphism induces \((1,0)\):

Now it’s clear what to do to extend this to an encoding of \((\mathbb{Z}/2\mathbb{Z})^n\) for any \(n\), e.g. to get \(n = 3\), color \(A^3\) as follows:

and so on, as long as the subdivisions are all happening along a single axis.

Going back to the finite model \(A = \{a,b,c,d\}\), we see that we don’t have the resolution to see \((0,0,1)\) in the \(n = 3\) case, so we have to use \(2^3\) elements instead. But then the same reasoning that we used for \(n = 2\) works.

The fact that we reasoned with automorphisms of finite models (\(A = \{a,b,c,d\}\)) and then extended the automorphisms to an infinite model (\(A = [-1, 1]\)) is an instance of the ultrahomogeneity property of a Fraïssé limit. Indeed, the Fraïssé construction proceeds by taking all possible finite models that we could perform our previous argument with and smashing them together. Another consequence of the general Fraïssé-theoretic machinery is that the resulting \(\mathfrak{A}\) is existentially closed. This rules out the possibility of obstructions like \(E_2 = E’\) as we noted above.

[eatsleepmath]

An ultraproduct of metric spaces is an ultraproduct of metric spaces

I never liked the first definition I saw of an ultraproduct of metric spaces:

Definition. Let \(\mathcal{U}\) be an ultrafilter on \(I\), and let \((X_i, d_i)\) be a sequence of uniformly bounded metric spaces.

Define \(d\) on \(\prod_{i \in I} X\) as follows: \(d\left((x_i)_{i \in I}, (y_i)_{i \in I}\right)\) is the ultralimit \(\lim_{i \to \mathcal{U}} d_i(x_i, y_i)\).

Note that \(d\) is a pseudometric on \(\prod_{i \in I} X_i\).

The ultraproduct of the uniformly bounded metric spaces \(X_i\) with respect to \(\mathcal{U}\) is the metric space \(\prod_{i \to \mathcal{U}} (X_i, d_i)\) obtained by quotienting out the distance-0 balls from \(\left(\prod_{i \to I} X_i, d \right)\).

Ultraproducts of sets are filtered colimits of infinite products.

Definition. Let \(\mathcal{U}\) be an ultrafilter on \(I\), and let \((A_i)_{i \in I}\) be an \(I\)-indexed sequence of sets.

The ultraproduct \(\prod_{i \to \mathcal{U}} A_i\) is defined to be the filtered colimit of the following diagram: the objects are products \(\prod_{i \in P} A_i\) as \(P\) ranges over the sets in the ultrafilter \(\mathcal{U}\), and the transition maps are the truncation maps

\[\prod_{i \in P} A_i \to \prod_{i \in P \cap P'} A_i.\]

In a category with products and filtered colimits, we call the result of this kind of construction a categorical ultraproduct.

In this post, we’re going to show that the above definition can be redeemed: while metric spaces do not form a nice category, pseudometric spaces do—in a way, this is because pseudometric spaces are geometrically axiomatizable (see e.g. the discussion in D1.1 of the Elephant), while metric spaces are not—and so modulo quotienting out the distance-0 balls, an ultraproduct of uniformly bounded metric spaces in the sense of the above definition is the same thing as their categorical ultraproduct in the category of pseudometric spaces.

Precisely put, our goal in this post will be to prove the following

Proposition. Let \((X_i)_{i \in I}\) be a uniformly bounded family of metric spaces. Then the metric space ultraproduct \(\prod_{\mathcal{U}} X_i\) in the sense of the first definition coincides with the quotient of \[\left(\operatorname{\underset{\longrightarrow}{\lim}}_{P \in \mathcal{U}} \left(\prod_{i \in P} (X_i, d_i)\right)\right)\] by distance-\(0\) balls, where the filtered colimit above is computed in the category \(\mathbf{PseudoMet}\) of pseudometric spaces with morphisms the weakly contractive maps.

A product of uniformly bounded metric spaces \(\prod_{i \in I} (X_i, d_i)\) is given a pseudometric \(d\) by \(d\left((x_i)_{i \in I}, (y_i)_{i \in I}\right) \overset{\operatorname{df}}{=} \sup_{i \in I} d_i(x_i, y_i)\).

Let’s figure out how to compute filtered colimits.

Lemma. Let \(\left(X_i, f_{ij} : X_i \to X_j \right)\) be a filtered diagram of pseudometric spaces. Then \(\operatorname{\underset{\longrightarrow}{\lim}} \left(X_i, f_{ij} : X_i \to X_j \right)\) exists, and is given by \[\left( \operatorname{\underset{\longrightarrow}{\lim}} X_i, \overline{d} \right),\] where \(\operatorname{\underset{\longrightarrow}{\lim}} X_i\) is the colimit taken in the \(\mathbf{Set}\), and where \[\overline{d}([x], [y]) \overset{\operatorname{df}}{=} \inf_i d_i(x_i, y_i),\] where \([x]\) and \([y]\) are germs and the infimum is computed only considering those \(X_i\) which have representatives \(x_i\), \(y_i\) for both \([x]\) and \([y]\).

Proof. First, we verify that \(\overline{d}\) defined above is a pseudometric. Symmetry and positivity are clear, so we check the triangle identity. We need to verify \[\inf_i d_i(x_i, y_i) \overset{?}{\leq} \inf_j d_j(x_j, z_j) + \inf_k d_k (z_k, y_k).\]

Now, if this was not true, then \[\inf_i d_i(x_i, y_i) > \inf_j d_j(x_j, z_j) + \inf_k d_k (z_k, y_k),\] so in particular there exist \(j\) and \(k\) such that \[d_j(x_j, z_j) + d_k(z_k, y_k) < \inf_i d_i(x_i, y_i).\] Since we are in a filtered diagram, \(X_j\) and \(X_k\) have an amalamgation \(X_j, X_k \rightrightarrows X_{\ell}\). Since the maps are contractive, \[d_{\ell}(x_{\ell}, y_{\ell}) \leq d_{\ell}(x_{\ell}, z_{\ell}) + d_{\ell}(z_{\ell}, y_{\ell}) \leq d_j(x_j, z_j) + d_k(z_{k}, y_{k}) < \inf_i d_i(x_i, y_i),\] a contradiction.

Now, we convince ourselves that \(\left( \operatorname{\underset{\longrightarrow}{\lim}} X_i, \overline{d} \right)\) is truly a colimit for \(\left(X_i, f_{ij} : X_i \to X_j \right)\). If \((Y, d_Y)\) is a cocone to this diagram, then there is a unique map of sets \(c : \operatorname{\underset{\longrightarrow}{\lim}} X_i \to Y\), and \(c\) is contractive because there is a contractive map \(c_i : X_i \to Y\) for each \(i\) which factors as a function through \(c\), so for any pair \((x_i, y_i)\),

\[\forall j \in J, d_Y(c_i(x_i, y_i)) \leq d_j(x_j, y_j) \hspace{1mm}\implies\hspace{1mm} d_Y(c([x_i], [y_i])) \leq \inf_i d_i (x_i, y_i),\]

proving the lemma. \(\square\)

Proof of the Proposition. First, let us compare the pseudometric spaces \[\prod_{i \in I} (X_i, d_i) \text{  vs  } \prod_{i \to \mathcal{U}} (X_i, d_i).\] There is a natural quotient map \(\prod X_i \to \prod_{i \to \mathcal{U}} X_i\). Is this contractive? Unraveling definitions, we see that we need to check the inequality \[\overline{d}([x_i], [y_i]) = \inf_P \left(\sup_{i \in P} d_i(x_i, y_i) \right) \overset{?}{\leq} \lim_{i \to \mathcal{U}} d_i(x_i, y_i) \overset{\operatorname{df}}{=} a \in \mathbb{R}.\] By definition of ultralimit, we have that for each \(\epsilon\), the \(\epsilon\)-ball \(B_{\epsilon}(a)\) around \(a\) contains \(\mathcal{U}\)-many \(d_i(x_i, y_i)\). Sending \(\epsilon \to 0\), we conclude that the inequality is true.

Actually, we can conclude more. If \(P\) indexes a set \(S \overset{\operatorname{df}}{=} \{d_i(x_i, y_i)\}_{i \in P}\) which witnesses this inequality, we can intersect \(P\) with smaller and smaller \(P'\). These intersections will be nonempty, which means that \(\sup S = a\). So the weak inequality can actually be improved to equality.

Therefore, the quotient map \(\prod X_i \to \prod_{i \to \mathcal{U}} X_i\) is isometric, and so any failure of injectivity must be because points distance \(0\) apart are being glued together. So there is a factorization

where either map to \(\left(\prod_{\mathcal{U}} X_i, d \right)\) is gotten by quotienting distance \(0\) points together. Thus our two descriptions of the metric space ultraproduct are the same. \(\square\)