On Skolemization... again

 

Skolemization and Why It Fails Constructively

There is a standard move in classical logic that feels so innocent.

You take a formula with existential quantifiers depending on universals, and you replace those existential witnesses with function symbols. You eliminate existential quantifiers altogether, at the price of expanding the language. The result is equisatisfiable, often easier to manipulate, and forms the backbone of many proof procedures.

The move is called Skolemization.

In classical logic, it works beautifully.

In constructive logic—more precisely, in intuitionistic logic—it does not.

Or rather: it does not work in general. And understanding why it fails, and when it still works, seems to be more subtle than one might expect.

This is the labyrinth.

---

The classical thread

Very roughly, Skolemization transforms a formula like

$$\forall x \, \exists y \, P(x,y$$

into something like

$$\exists f \, \forall x \, P(x, f(x)).$$

Or, more commonly in proof theory, we simply replace the existential with a Skolem function symbol  and consider

$$\forall x \, P(x, f(x)).$$

Classically, this is justified because truth is about existence, not construction. If for every $x$ there exists some $y$ then there is no harm in imagining a function $f$ that picks one such $y$ for each $x$. The logic does not ask us to compute $f$, only to accept its existence.

This step is so standard that one almost forgets it is a step.

---

The constructive issue

From a constructive point of view, however,

$$\forall x \, \exists y \, P(x,y)$$

is not just a statement about existence—it is a statement about the ability to produce a $y$ from an $x$.

To replace this with a function f  is to claim something stronger: that there is a uniform method assigning to each $x$ a specific witness $f(x)$.

And this is not, in general, justified.

The gap is subtle but real. A constructive proof of

$$\forall x \, \exists y \, P(x,y)$$

may proceed in ways that do not yield a single, global function $f$. The witnesses may depend on the structure of the proof, on case distinctions, or on information that is not uniformly available.

In other words: the existential quantifier may be locally justified without giving rise to a global choice function.

Skolemization silently inserts that global choice.

This is where it breaks.

---

A conversation

Many years ago, I asked Grigori Mints about this.

He had written about Skolemization  and he was "the''expert in intuitionistic logic, and I was curious whether the problem had, in some sense, been solved. Whether there was a clean constructive analogue of the classical transformation, a best formulation for the constraints under which we have the ability to skolemize constructively.

His answer was immediate and unequivocal:

No—Skolemization does not work for intuitionistic logic.

But, he added, it is worth understanding when it does work, and why.

---

When does it work?

This is where things become interesting.

There are situations in which something like Skolemization is admissible constructively. But these tend to come with extra structure, extra assumptions, or restrictions on the form of the formula.

For instance (and here I am deliberately being schematic rather than definitive):

• When the proof already contains enough uniformity to extract a function.
• When the domain over which $x$ ranges has special properties (e.g., decidability conditions).
• When one works not in pure intuitionistic logic, but in systems enriched with choice principles.
• When the formulas involved are restricted (e.g., certain fragments where realizability guarantees uniform witnesses).

In these cases, the thread appears: one can pass from “for all $x$, there exists a $y$” to something function-like. But the thread is not given for free. It has to be constructed.

---

What is the real issue?

What seems to be at stake is not just Skolemization itself, but the relationship between:

• existence and construction,
• local witnesses and global functions,
• proofs and programs.

From the perspective of the Curry–Howard correspondence, this becomes even sharper. A proof of

$$\forall x \, \exists y \, P(x,y$$

corresponds to a function that, given $x$, returns not just a $y$, but a pair $(y, \text{proof that } P(x,y))$

So why isn’t that already a Skolem function?

This is exactly the point where my understanding becomes less clear.

Is the issue intensionality? Is it about the structure of proofs versus the structure of terms? Is it about normalization, or about the admissibility of certain transformations on proofs?

Or is it simply that Skolemization, as usually formulated, forgets too much of the computational content?

---

Not a conclusion

I do not have a clean answer.

What I have instead is a sense that Skolemization marks a boundary: a place where classical and constructive reasoning diverge in a way that is not merely technical, but conceptual.

Understanding that boundary—mapping where the transformation fails, where it can be repaired, and what is lost or gained in the process—seems to me a worthwhile problem.

This post is not a solution.

It is a piece of thread.

 

 Some references: 

1. (Russian) The Skolem method in intuitionistic calculi, G. E. Mints, 1972.

2.  The Skolemization of prenex formulas in intermediate logics, Rosalie Iemhoff, 2019.

3. The Skolemization of existential quantifiers in intuitionistic logic, Matthias Baaz, Rosalie Iemhoff,  APAL, 2006 

 

 

---

 

Skolem is not constructive

(but sometimes it can be)

On what goes wrong when you try to eliminate quantifiers intuitionistically

proof theoryconstructive logic

---

Skolemization works. That's the starting point — not a caveat, not a qualification. In classical first-order logic, it is a perfectly sound and complete procedure for eliminating existential quantifiers. It feels right. Given a formula with alternating quantifiers, you replace each existential one with a function symbol that witnesses the existential choice in terms of the universal variables above it. The prenex formula ∀x ∃y P(x,y) becomes ∀x P(x, f(x)), where f is a fresh Skolem function. The resulting formula is satisfiable if and only if the original is. It looks right because it is right.

So why doesn't it work constructively?

What goes wrong

In classical logic, ∀x ∃y P(x,y) being true means there exists a choice function picking a witness for each x. The Skolem function f simply names that function. The move is sound because classical logic is comfortable with non-constructive existence: "there is some y" doesn't require you to say which one, or how to find it.

Skolemization hides an application of the Axiom of Choice. Classically, that's fine. Constructively, it's the whole problem.

Constructively, a proof of ∀x ∃y P(x,y) is a function that, given any x, produces a specific y together with a proof that P(x,y) holds. So far so good — that looks exactly like a Skolem function! But the catch comes when you try to preserve this under proof transformations. The issue is not just semantic but syntactic: Skolemization changes the formula, and intuitionistic logic is sensitive to the structure of formulas in ways classical logic is not.

More precisely, the classical equivalence

classically valid, intuitionistically invalid

∀x ∃y P(x,y) ⟺ ∃f ∀x P(x, f(x))

fails constructively. The right-to-left direction is fine: given a function f and a proof that ∀x P(x, f(x)), you can obviously produce a witness for any given x. The left-to-right direction is the problem. Passing from a proof of the left side to an explicit choice function f in the metalanguage is precisely what the Axiom of Choice does. Intuitionistic logic does not have AC as a theorem, and for good reason: there are models — realizability models, sheaf models — where AC fails.

The philosophical point

There is something deeper going on here than a missing axiom. Classical logic treats truth as a property of statements independent of any proof. A statement is true or false, and if it's true there's nothing more to say about how or why. Constructive logic treats truth as tied to the existence of a construction — a proof, a program, a witness. When you Skolemize, you are packaging up the witnessing information into a function and pretending it was there all along. Classically, the function exists abstractly. Constructively, you need to hand it to me.

Sometimes it's constructively valid

Herbrand's theorem is itself a classical result, so it doesn't rescue constructive Skolemization directly. But its output is more honest than an abstract Skolem function: the theorem says that if a prenex formula is classically valid, then some finite disjunction of ground instances of its matrix is propositionally valid. You get actual explicit ground terms as witnesses — not an abstract choice function whose existence is merely asserted. That's a more tractable form of existence, even if the theorem that produces it is classical, and even if finding the right finite disjunction is in general only semi-decidable.

In dependent type theory (think Martin-Löf type theory or its descendants), the Skolem function is already present in the type of the proof. A term of type Πx:A. Σy:B. P(x,y) is literally a dependent function that maps each x to a pair (y, proof). You can project out the first component to get your Skolem function. No axiom needed — it's just projection. In the right foundational setting, Skolemization is not a trick but a triviality.

In dependent type theory, Skolemization reduces to the fact that the first projection of a dependent pair is a function. No magic required.

Realizability semantics enforces constructive content directly. In Kleene's number realizability, a proof of ∀x ∃y P(x,y) is realized by a computable function f such that for each x, f(x) is a realizer for P(x, f(x)). The Skolem function is literally the realizer — and it is required to be an actual computable function, not an abstract one. The semantics does the work that AC would otherwise do, by demanding computation.

Gödel's Dialectica interpretation (1958) makes witnessing explicit by translating intuitionistic arithmetic into a system of computable functionals. Interestingly, Gödel himself used Skolemization in arriving at the interpretation — he Skolemizes to extract the witnessing terms, then interprets those terms as computable functionals. (Troelstra's analysis in Gödel's Collected Works, vol. II makes this clear.) The point is not that Dialectica avoids Skolemization, but that it uses it in a setting where the Skolem functions are required to be computable — which is precisely the constructive content the interpretation is designed to capture.

The upshot

Skolemization is a classical procedure that packages up witnessing information into unnamed functions, relying on AC to justify the packaging. Constructively, you cannot take that shortcut — you have to carry the witnesses explicitly, which is exactly what dependent types, realizability semantics, and the Dialectica interpretation all do in their different ways.

The moral is not that Skolemization is wrong. It is right — classically. The constructive failure is informative precisely because the procedure is so well-motivated: it reveals that classical and constructive logic diverge not at some exotic corner case, but at the very heart of what it means to assert that something exists.

Related: Gödel's Dialectica interpretation (1958) · Herbrand's theorem · Martin-Löf type theory · Kleene realizability 

Ariadne Posts: On Not Yet Knowing the Way Out

My previous series of blog posts—what I’ve been calling the Penelope posts—has been about revisiting past work. These are papers written with collaborators, work that has been peer-reviewed, presented, and, in some sense, settled. Writing about them is an exercise in reconstruction: not of the proofs themselves, but of their meaning. Why did they matter? Why do they still matter to me now?

This new series is different.

These are posts about things I do not understand.

I want to write about problems in logic and mathematics where I can see the shape of a solution, but not quite reach it. Situations where existing answers feel partial, or unsatisfying, or somehow misaligned with the question. Places where the definitions work, some theorems go through, but something conceptual still feels missing.

These are not expository posts. They are not surveys. They are not polished.

They are explorations.

I am calling them the Ariadne posts, after Ariadne of Greek mythology.

In the myth, Ariadne gives Theseus two things: a sword to face the Minotaur, and a thread—a simple ball of yarn—to find his way back out of the labyrinth. The thread is the real insight. It is not heroic. It does not solve the problem directly. But it makes survival, and return, possible.

That is what I am looking for here: not solutions, but threads.

In mathematics and logic, we are very good at celebrating the Theseus moments—the clean theorem, the decisive proof, the elegant framework. But much of the real work happens earlier, in the dark: when we do not yet know what the right definitions are, when multiple approaches almost work, when we are unsure whether the difficulty lies in the problem or in our understanding of it.

These posts live in that space.

Each Ariadne post will start with a problem or a line of thought that I find compelling but unresolved. I will try to articulate what is known, but more importantly, what feels unsatisfactory about what I know. Where do existing approaches fall short? What do they fail to explain? What intuitions do they obscure?

The goal is not to criticize for the sake of it, but to make visible the gaps—the places where a thread might be needed.

There is also something else I want to recover in invoking Ariadne.

In the story, her contribution is essential. Without her, Theseus does not return. And yet, she is not the hero of the tale. Worse, she is abandoned—left behind on Naxos, her insight overshadowed by the narrative of heroic conquest.

It is a strange fate for someone whose idea is, in many ways, the most mathematical part of the story: a minimal, structural intervention that transforms an impossible task into a tractable one.

These posts are, in part, a small act of correction.

They are an attempt to value the thread as much as the sword.

---

By the way painting by Angelika Kaufmann (1741-1807), another barely remembered woman

 

A Recipe for Models, Told Twice

 Dr Andrea Schalk, School of Computer Science at The University of Manchester

One of the pleasures of long mathematical collaborations is watching how the same ideas get told differently by different people. Andrea Schalk and I worked together on models of linear logic for some years, and the pair of papers I want to discuss today — one a conference extended abstract from AMAST 1999, the other its journal incarnation in Theoretical Computer Science in 2004 — illustrate this rather vividly. The mathematics is essentially the same. The sensibility is not.

The idea itself

The question we were trying to answer was: can you build a unified framework that explains why so many different models of linear logic — coherence spaces, hypercoherences, phase spaces, the category of relations — all work in structurally similar ways? And can you do it cleanly enough that you understand why they sometimes collapse (tensor equalling par, products equalling coproducts) and sometimes don't?

The answer turned out to be pleasingly simple. Start with Rel, the category of sets and relations, which is compact closed and serves as the ambient universe. Choose two ingredients: an endofunctor F on Rel (playing the role of "how you read the structure of an object") and a poset L (or P in the journal version) that is symmetric monoidal closed. 

Then consider pairs  (A, α) where A is a set and α : FA → L is a function — a "poset-valued set," or an L_F-set. Morphisms are relations R : A ⇸ B such that whenever x (FR) y, we have α(x) ≤ β(y). That's it. The poset L controls the categorical structure of the whole thing. 

1. Coherence spaces? Take L = 3, the three-element poset {⌢ < 1 < ⌣} and F = the diagonal functor.
2. Hypercoherences? Take L = 3 and F = the finite powerset functor.
3. Phase spaces? F constant, L a complete lattice of "facts."
4. The category Rel itself? Let L be a singleton. 

The tensor, the linear function space, the negation, the exponential modality, all arise by lifting the corresponding structure from L through F into the new category. The "collapse" (why tensor = par in coherence spaces, for instance) is explained: it happens because those operations coincide in 3.

The 1999 paper: my voice
The AMAST extended abstract has a particular flavour. It opens with the motivation from comparing Chu's construction with Dialectica categories — a very personal starting point for me, since the Dialectica categories were my PhD thesis work, and I had long been curious about how far you could get without built-in duality. The paper leans into the conceptual story: why are we doing this, what are we hoping to learn, what surprised us. There's a certain directness to it, a willingness to foreground the puzzle.

There's also a slightly unconventional technical choice that reflects this: the objects are called L_F-sets (with the poset coming first), signaling that the algebraic structure of L is the conceptual driver. The notation is a little idiosyncratic, even playful. The paper says "we are independently pursuing the work on these two classes of models" — meaning dialectica and games sit outside the framework, a gap openly acknowledged rather than quietly elided.

The 2004 paper: Andrea's voice
The TCS journal version is altogether more systematic. The objects are now called P_F-sets, a small notational shift but a telling one — P for poset, cleaner and more standard. The introduction is careful and measured. It lists exactly what the construction controls (classical versus intuitionistic, coincidence of products and coproducts, coincidence of tensor and par) as a precise taxonomy before saying anything else. The proofs are spelled out fully, including the ones the extended abstract wisely deferred to an appendix or left implicit. 

Andrea's exposition has a different quality of care — the kind that comes from wanting every step to be airtight and every claim to be precisely scoped. Where my version is somewhat conversational, hers is architectural. The section on generalizing away from Rel is notably honest: "our proof of symmetric monoidal closure does make use of the fact that the base category is compact closed, and we currently cannot see an obvious way of generalizing this."

Both versions thank Martin Hyland, which seems right.

What this illustrates

 Mathematical papers are not just records of results. They are also, inevitably, records of perspective — of what the author finds surprising, what they think needs explaining, where they think the edges of the work lie. The same theorem can be framed as the answer to a puzzle you've been carrying for years, or as a modular construction tool for future use. Neither framing is wrong. They illuminate different things.

Reading these two papers side by side, I'm struck by how much the conference-paper form suited the first one: the space constraint forced a clarity of motivation that sometimes gets diluted in full journal treatment. And I'm equally struck by how much Andrea's careful expansion added — the fill-in lemma becomes genuinely transparent in the longer version in a way it wasn't before.

Further directions

Both papers are honest about the limits of the construction. The two classes of models that don't fit — dialectica categories and games models — are flagged in both versions, and the 2004 paper additionally notes the difficulty of generalising away from Rel as the base category: the proof of symmetric monoidal closure leans on Rel being compact closed in an essential way, and it's not obvious how to relax that. This dependence always bothered me — compact closure of Rel means that tensor, par, and linear implication all coincide there, and that linear true equals linear false, which is precisely the kind of collapse we are trying to avoid. 

One direction that might seem worth exploring is replacing the poset L with a quantale — a complete lattice with a compatible monoid structure — which would merge the two separate assumptions on L into a single algebraic object. But the completeness of a quantale always felt artificial here: we are modelling propositional linear logic, and that much lattice-theoretic machinery seems like more than the situation calls for.

A brief note on connections

 The dialectica categories that motivated this work in the first place continue to sit just outside the framework — as the conclusions of both papers honestly note. That tension remains interesting to me: the P_F-set construction is "one-sided" in the sense that duality comes from L rather than from a built-in pairing, while Dialectica categories are irreducibly "two-sided." Whether there's a common generalisation that comfortably houses both is a question I haven't stopped thinking about.

---

The papers can be found at “[PDF]Poset-valued sets or how to build models for linear logics” and Building Models of Linear Logic.

 

 

 

The logic of using things exactly once — and why it matters

 What a 1999 gathering of logicians was quietly getting right about the future of computing

August 1999 · Dagstuhl Castle, Germany.

 In August 1999, about two dozen researchers gathered at Schloss Dagstuhl — a castle in the German countryside that has hosted some of the most productive meetings in computer science — for a seminar on Linear Logic and its Applications. The meeting was organized by Dick Crouch, Eike Ritter, Josef van Genabith, and me. Looking back, it is striking how many of the ideas debated there have since moved from "interesting theoretical curiosity" to genuine practical importance. 

 Linear Logic was introduced by Jean-Yves Girard in 1987. Its central idea is deceptively simple: instead of treating logical assumptions as facts that can be used freely and repeatedly, treat them as resources — things that get consumed when used. Want to use something twice? You have to say so explicitly. This turns out to be a surprisingly powerful lens for thinking about computation. 

"Linear Logic is a refinement of Classical Logic: using Girard's well-known translation we can investigate the usage of resources in proofs of traditional theorems."

One of the liveliest threads at the seminar concerned natural language. Several talks explored how the resource-sensitivity of Linear Logic maps beautifully onto the combinatorics of sentence meaning — the way words and phrases "combine" their meanings exactly once to produce the meaning of a whole sentence. This is the foundation of the glue semantics approach to natural language, which uses an implicational fragment of Linear Logic to assemble meanings compositionally. The core proof-search challenge — finding all distinct derivations efficiently, since each derivation corresponds to a distinct reading of an ambiguous sentence — anticipated concerns that are very much alive in today's work on parsing and semantic composition.

Another major theme was functional programming and memory management. The intuition is elegant: if a variable is used exactly once (a "linear" variable), then the object it refers to has exactly one pointer to it at any given time, which means it can safely be updated in place without copying. Several talks at the seminar explored how far this idea could be pushed — and where it runs into difficulties, particularly with higher-order functions. This line of thinking is now central to the design of modern systems programming languages. Rust's celebrated ownership and borrowing system is a direct descendant of these ideas, and linear types have since made their way into Haskell as well, a sign that the functional programming community has come to take resource-awareness seriously. 

The seminar also featured what became perhaps its most contentious debate: whether Linear Logic really is "the" logic of resources, or whether a rival system — the Logic of Bunched Implications, BI, proposed by Peter O'Hearn and David Pym — did a better job. The BI proponents argued that Linear Logic captured a process reading of resources (independent parallel computations) but not a fully satisfactory spatial reading (separate regions of memory). This dispute, which generated "the most controversy in the meeting" turned out to matter enormously: BI became the foundation of Separation Logic, which is now one of the most important frameworks for formally verifying the correctness of programs that manipulate memory. O'Hearn received the ACM Turing Award in 2023, in part for this work. 

Not every thread has yet reached its destination, and that is part of what makes this area exciting. Applications of Linear Logic to logic programming, planning, and concurrency have had a long and productive history, and there is no reason to think the story is finished — these are hard problems, and resource-aware reasoning keeps finding new angles on them. What makes a seminar like this valuable is precisely that ideas from different communities — proof theorists, linguists, programming language researchers, verification specialists — get to collide and cross-pollinate, with payoffs that can take years or decades to fully materialise.

One striking absence from the 1999 programme was Differential Linear Logic, introduced by Ehrhard and Regnier a few years later. By adding a notion of differentiation — in the calculus sense — to the logical framework, it opened a connection between proof theory and the mathematics of smooth functions and power series that nobody had anticipated. It gave a logical account of the "Taylor expansion" of proofs, and has since made contact with probabilistic programming, neural network semantics, and the theory of quantitative information flow. A quarter century on, Differential Linear Logic is still actively developing: the right categorical semantics, the proper treatment of higher types, and the connections to adjacent fields are not yet fully settled. It is a reminder that a logical idea, once it takes hold, can keep ramifying in unexpected directions long after the original seminar has ended.  

Twenty-five years later, it is fair to say that the core intuition of the 1999 meeting has aged very well. Thinking carefully about how resources are used — in memory, in concurrency, in meaning assembly, in the very structure of proofs — remains one of the most fertile ideas at the intersection of logic and computer science. Some of the seeds planted at Dagstuhl are still growing.

The original seminar report is available from Dagstuhl [here].  

 

What If Cantor Was Wrong?

A blog post about infinity, categories, and a mathematical mystery.

Cantor showed that not all infinities are equal: the infinity of the natural numbers (ℵ₀) is genuinely smaller than the infinity of the real numbers (called c, the continuum). He then asked what seems like a natural follow-up: is there anything in between? His conjecture that the answer is no became known as the Continuum Hypothesis (CH).

He spent years trying to prove it. He failed. He had a breakdown. He died without knowing the answer. As it turned out, there was a good reason: Gödel (1940) and Cohen (1963) together showed that CH is neither provable nor disprovable from the standard axioms of mathematics. It is, in a precise sense, independent of everything we build mathematics on.

This is, philosophically speaking, quite alarming. But also liberating.

So Let's Assume It's False

If CH is false, there are cardinals strictly between aleph_0 and c (all of them infinite, of course). Set theorists have identified dozens of these that arise naturally in analysis and topology — measuring things like how many functions you need to dominate all others, or how many small sets it takes to cover the real line. These are called cardinal invariants of the continuum, or small cardinals, and their relationships to each other form a rich landscape, summarised in the beautiful Cichoń's Diagram.

This is where my friend Samuel Gomes da Silva comes in. Samuel is a set theorist at the Federal University of Bahia in Brazil, thinking hard about these cardinals and how to prove inequalities between them. I am a category theorist — my home territory is Dialectica categories, which I introduced in my PhD thesis in the late 1980s as a categorical version of Gödel's Dialectica interpretation. They turned out, somewhat surprisingly, to be models of Linear Logic — but that was not the original plan. Even more surprisingly, these categories had found an exciting connection to set theory through the insight of Andreas Blass, but no one had fully explained why.

Samuel and I started talking, and realised we were looking at the same mountain from opposite sides. Our paper — Dialectica Categories, Cardinalities of the Continuum, and Combinatorics of Ideals — is the attempt to build a path between those two viewpoints.

The Mystery We Were Trying to Solve

Here is the core puzzle, articulated beautifully by Blass himself:

"It is an empirical fact that proofs of inequalities between cardinal characteristics of the continuum usually proceed by representing the characteristics as norms of objects in PV and then exhibiting explicit morphisms between those objects."

Translation for non-specialists: there is a category (a mathematical structure of objects and arrows between them) — closely related to my Dialectica categories — such that almost every  known proof of an inequality between small cardinals can be encoded as a morphism in that category. This is not a theorem anyone had proved. It was just... observed. An empirical fact. A pattern that kept showing up.

Blass pointed it out. Everyone nodded. Everyone just kept using the pattern without asking why it worked. Samuel and I found that strange: we felt that empirical facts deserve explanations.

The Key Idea (Gently)

The category in question — called PV, after de Paiva and Vojt́áš — has objects that are triples: a set of "problems," a set of "solutions," and a relation saying which solutions solve which problems. A morphism between two such objects is a way of translating problems and solutions between them, kind of preserving the solving relationship.

The norm of such an object — a cardinal number naturally associated to it — turns out to be: the minimum number of solutions needed to cover all problems. That is an "Abelard and Eloise cardinal," as we fondly called them in the paper, because their definitions always have the shape "for all... there exists..." — the classic back-and-forth of a logical argument, or a medieval philosophical debate.

The beautiful discovery is that most of the small cardinals that set theorists care about — b, d, add, cov, non, cof — can all be expressed as norms of natural objects in PV. And when one norm is smaller than another, there is (almost always) a morphism that witnesses this, in a constructive and categorical way.

In our paper, we showed this works beautifully for pre-orders and for ideals (a notion of "smallness" for collections of sets). For any reasonable notion of "bounded" in a pre-order, the associated cardinal invariants — how many bounded sets you need to cover everything, how large an unbounded family must be — all fall out as norms of Dialectica objects. The morphisms between them encode exactly the "witness-choosing" arguments that set theorists had been writing out by hand for decades.

What We Conjectured 

We proposed four conjectural principles in the paper. The most important, roughly speaking, are:
   1. Most natural cardinal invariants in set theory are "Abelard and Eloise" cardinals — they can be expressed as norms of objects in Dialectica.
    2. Pre-orders are the archetypal case — understanding b(P) and d(P) for a pre-order P gives you the right intuition for all the others.
    3. Any reasonable proof of an inequality between such cardinals, even one written without thinking about categories, secretly encodes a morphism — the morphism is hiding in the "witness-choosing" steps.
    4. The deepest explanation will ultimately be categorical — there is something about the structure of Dialectica categories that makes them the natural home for this kind of mathematics.

We were honest in the paper: we hadn't fully answered our Main Question. We still haven't. But we had identified the right question to ask, which is, in mathematics, sometimes most of the work.

A Personal Note

I was not supposed to care about cardinal invariants. I was a categorical logician, interested in the internal structure of proofs, in models of computation, in the geometry of inference. The idea that the categories I built to model a fragment of logic would end up being the natural language for a corner of set theory about the size of infinity — that was not in my plan.

But that is what mathematics does. It finds its own connections across whatever disciplinary boundaries we have invented. Samuel and I came from different mathematical cultures, spoke different technical dialects, and cared about different problems. And yet the mathematics insisted that we were talking about the same thing.

That, perhaps, is the real moral of the Continuum Hypothesis: even a question we cannot answer has rich and surprising structure. Even undecidability is fertile ground. We might not know if there's something between ℵ₀ and c. But if there is, we're starting to understand what it looks like.

---------------------------------------------------------------------------------------
The paper discussed in this post is: Samuel G. da Silva and Valeria C. V. de Paiva, "Dialectical categories, cardinalities of the continuum and combinatorics of ideals," Logic Journal of the IGPL, Vol. 25, No. 4, 2017. Yes, there’s a typo in the name of the paper, it should be Dialectica, not Dialectical, this is what the errata is about—only this.