Some unfinished business with Dialectica categories
I've recently put two Lab notes in my Drafts repository, both about extending Dialectica constructions beyond their usual setting. Neither is meant as a research paper, at least not in its present form. So why write them, and why make them public? Part of the answer is that mathematical research produces more than papers. We make calculations, test examples, revisit old assumptions, and sometimes discover that things we expected to work simply don't. Much of this disappears into notebooks, files and conversations with colleagues, but some of it is worth keeping, especially when it concerns questions that have been around for a long time. These two notes are about such questions.
Dialectica categories come from Gödel's functional interpretation of arithmetic. In my thesis I described a categorical construction whose objects are triples: an object of witnesses, an object of counterexamples, and a subobject of their product, a relation telling us when a witness stands up to a counterexample. Over any cartesian closed category this gives models of linear logic, and a categorical account of much of the structure implicit in Gödel's interpretation.
But there are choices hidden in this description. Why should relations be subobjects? And why should the base category be cartesian closed? The two Lab notes take up these questions one at a time.
Two ways of generalizing Dialectica
The first note, Dialectica categories without subobjects, changes the notion of relation. Instead of a subobject of the product of witnesses and counterexamples, we take a map from that product into an object of truth values L. The object L is a lineale, an ordered algebraic structure with just the operations needed to interpret linear logic. Ordinary true-or-false relations are one possibility among many: by changing the lineale we can have relations valued in the natural numbers, in the integers, or in other algebraic structures. A commutative group ordered by equality is already a lineale, and then the conditions on morphisms become equations.
This is not a new idea. Reading relations as maps into truth values is an old observation, and for the Girard variant of the construction the lineale-valued calculations were published long ago, in the Multirelations technical report and in my 2006 article comparing Dialectica and Chu. For the original construction, though, they were never written down anywhere public. The note does exactly that, modality included.
The second note, Dialectica Constructions over Monoidal Bases, changes something else. It keeps the lineale-valued relations of the first note, but replaces the cartesian closed base with a symmetric monoidal closed category with products. Our reason for wanting this was vector spaces. Lafont and Streicher showed that finite-dimensional vector spaces sit beautifully inside the Chu construction, and we wanted the same for Dialectica.
Over a monoidal base, copying and discarding are no longer available for free, as they are in a cartesian category. The Dialectica construction uses witnesses in ways that need exactly these operations, so the note makes the comonoid structure on witnesses explicit. The tensor of two dialectica objects then uses the monoidal tensor on witnesses and the real product on counterexamples, and the note works out the rest of the connectives with their coherence. Graded sets, that is, sets where every element has a size, provide a happy example, modality included: the tensor adds sizes, just as generating functions multiply.
Vector spaces, however, are much less cooperative. The construction can be carried out over them, but with lineale-valued relations the tensor and the product coincide, and the distinction between them is one linear logic cannot do without. Going back to subspaces as relations keeps the two apart, but then I haven't found an internal hom. This is especially interesting because Chu constructions work so well with vector spaces. The two constructions, often presented as close cousins, behave quite differently here. I don't think this shows that Dialectica cannot give interesting categories of vector spaces, but it does show that the obvious approaches are not enough, and that is worth knowing.
Why not papers?
A research paper is usually expected to present a substantial new result, explain its significance, and place it within a developed argument. These notes have a different purpose. Their positive results are expected, even if the calculations had never been written down, and their negative results leave us with questions rather than a satisfying alternative construction. Doing everything that could be done around them would turn a fairly straightforward investigation into a much larger project, without making its central observations more useful. I would rather have the calculations available now than wait for a paper that may never be written.
This matters most for negative results. When an approach fails, we tend not to publish it, and then someone else spends months rediscovering the same obstruction. A failed construction is not an impossibility theorem, of course, but knowing exactly where it gets stuck can save other people a lot of time.
Why are these notes needed?
We have many categorical constructions that produce models of logic, but we don't always understand their range as well as we should. We know the standard examples and the general theorems, and the space between them is often surprisingly unexplored. What happens when we change the notion of relation, or the base category? Which assumptions are essential, and which are merely convenient? Which logical operations survive the change?
These questions matter particularly for Dialectica constructions because of their origins in proof interpretation. The distinction between witnesses and counterexamples is not decoration: it carries logical information, and changing the surrounding categorical structure shows which parts of that information really matter. The notes are small contributions to this larger map. They settle a few calculations, expose some hidden assumptions, and leave questions open. Not everything needs to become a journal paper to be useful, and perhaps by making these investigations public we make it easier for someone to find the vector-space construction we haven't found yet.
