Synthetic Mathematics in the Amazon

Talking about Synthetic Mathematics in the middle of the Amazon rainforest felt slightly surreal.

Parintins is famous for the Festival do Boi-Bumbá, for the river, for the forest, for the extraordinary cultural life of the Amazon. It is not the place most people imagine when they think about categorical logic, proof theory, Curry–Howard, or the future of AI-assisted mathematics.

And yet perhaps it was exactly the right place.

My talk at EMALCA Amazonas 2026 was about revolutions in mathematics: how mathematics periodically changes not only its results, but its understanding of what mathematics itself is.

The first great revolution of the twentieth century was the revolution of rigor. Frege, Hilbert, Gentzen, Gödel, Turing, Church: suddenly proofs themselves became mathematical objects. Formalization ceased to be merely philosophical and became technical infrastructure. Mathematics acquired syntax.

That revolution produced modern logic, proof theory, computability theory, formal systems, and eventually computer science itself.

But a second revolution was quietly unfolding in parallel.

The Curry–Howard correspondence — “proofs as programs, propositions as types” — revealed that proofs were not merely static certificates of truth. They had computational content. They could be transformed, executed, normalized, composed. Category theory then provided the missing global language of structure: proofs became morphisms, composition became central, and semantics became unavoidable.

I increasingly think that this second revolution is still incomplete.

We have the theory. We have fragments of the practice. But mathematics as a whole still has not fully absorbed the structural viewpoint introduced by categorical logic and semantics. Neither have Computer Science or Logic done the same. Why?

But now AI arrives.

Large language models can generate mathematical text at astonishing scale. They conjecture, sketch proofs, suggest strategies, translate between formalisms, and increasingly interact with proof assistants. Systems like Lean, Rocq, Isabelle, and Agda are no longer niche curiosities. Formal verification is becoming practical infrastructure.

And AI also reopens the oldest foundational wounds.

LLMs operate probabilistically, not semantically. They produce convincing mathematical language without any guarantees of correctness. They manipulate symbols fluently while remaining disconnected from proof in the classical sense.

This is why the current moment feels less like a purely technological revolution and more like the collision of earlier mathematical revolutions.

The first revolution demanded rigor. The second revealed deep structures connecting proofs, programs, and categories. The third — the AI revolution — suddenly makes those abstract structural questions operationally necessary.

What counts as a proof?
How do we represent mathematical structure?
How do we verify transformations?
What is the semantic content of a generated argument?
How do we move between informal mathematical language and formal systems?

These questions are no longer philosophical luxuries. They are engineering problems for the future of mathematics.

This is one reason I spoke about Dialectica categories in Parintins.

Gödel’s Dialectica interpretation and Girard’s linear logic both force us to think carefully about structure, interaction, resources, witnesses, and transformations. Category theory provides a language capable of relating these ideas without collapsing their distinctions.

I am not claiming that category theory “solves AI”.

Far from it. But I am claiming that the automation of mathematics makes it impossible to ignore semantics any longer.

For decades, categorical logic often seemed abstract, beautiful, and somewhat distant from mainstream mathematical practice. Today the situation is changing. As mathematical reasoning becomes partially automated, questions about meaning, translation, compositionality, verification, and structure move from the foundations to the center.

And perhaps this is why speaking about these ideas in the Amazon felt unexpectedly appropriate.

The Amazon constantly reminds us that scale changes everything. Small local interactions produce vast global structures. Networks matter. Flows matter. Translation between levels matters. Structure matters.

Mathematics is entering a similar moment. We are moving from isolated proofs to ecosystems of formalization, machine assistance, semantic translation, and large-scale mathematical computation. The foundational questions of the twentieth century are returning — but now under computational pressure.

The second revolution is no longer optional.

 

 

Kolmogorov and Alexandrov on a trip. From CultureMath, 2022. 

 

Problems, Problems Everywhere 

There’s a particular kind of mathematical paper that begins with a modest goal and ends up quietly connecting half a century of ideas across logic, category theory, and the philosophy of mathematics. Today I want to talk about one of those papers.

In Kolmogorov–Veloso Problems and Dialectica Categories, Samuel and I set out to understand something that sounds deceptively simple: what is a problem?

Now, if you’re a working mathematician, you might be tempted to answer: “a problem is something I can’t solve yet.” Fair enough. But historically, people have taken this question much more seriously—and much more abstractly.

Kolmogorov, for instance, thought of problems as primitive mathematical objects. Not sets, not functions, not proofs—but problems. Meanwhile, Veloso developed a notion of problems that behave beautifully… provided you are willing to assume the Axiom of Choice. And Blass came along and reframed problems as games of questions and answers, connecting them to computation and complexity.

So naturally, we thought: what could possibly tie all of these together?

Enter Dialectica categories.

If you’ve ever met a Dialectica construction, you’ll know it has a certain personality. It takes something familiar—a category—and turns it into something slightly uncanny: objects become pairs of “witnesses” and “counter-witnesses,” morphisms become strategies, and suddenly everything starts to look like a dialogue. Or a duel.

Or, as it turns out, a problem.

One of the small delights of this paper is realizing that Kolmogorov had already intuited something like this decades earlier. His abstract notion of a problem—so far removed from computation or complexity—fits remarkably well into the Dialectica perspective. It’s as if he had glimpsed the categorical structure before the language was available.

Veloso’s problems, on the other hand, are a bit more demanding. They work beautifully—but only if you’re willing to pay the price of the Axiom of Choice. This gives the whole story a slightly mischievous twist: some problems exist only if you believe in certain kinds of choice, while others are perfectly happy in a more constructive world.

And then there’s Blass, who brings everything down to earth with his questions-and-answers framework. Suddenly, problems are not just abstract entities—they are interactive processes. You ask, I answer; I challenge, you respond. It’s mathematics as conversation, or perhaps as negotiation.

What the categorical perspective does—quietly, but powerfully—is show that these are not competing views. They are different facets of the same underlying structure. A version of the Dialectica construction acts as a kind of translator, moving between Kolmogorov’s abstractions, Veloso’s set-theoretic universe, and Blass’s interactive games.

Along the way, something else becomes clear: the Axiom of Choice is not just a technical convenience. It shapes the very nature of the problems we are allowed to talk about. With full choice, Veloso’s world opens up. With weaker forms—countable or dependent choice—we get more nuanced landscapes. And without choice, we are back in a more constructive, and perhaps more disciplined, universe.

So, what is a problem?

After all this, we still don’t have a single answer—and that’s probably a good thing. Instead, we have a small constellation of answers, connected by categorical structure:

•   a problem as an abstract mathematical entity (Kolmogorov),
•   a problem as a set-theoretic construction (Veloso),
•   a problem as an interactive process (Blass),
•   and a problem as a kind of a Dialectica object, living somewhere in between.

If there’s a moral to the story, it might be this: sometimes the best way to understand a concept is not to define it once and for all, but to see how it transforms as you move between different worlds.

And if those worlds happen to be connected by category theory—well, that’s just a bonus.

---------------------------------------------------------------------------------

de Paiva, Valeria, and Samuel G. da Silva. "Kolmogorov-Veloso problems and Dialectica categories." arXiv preprint arXiv:2107.07854 (2021). 

Remembering Marta Bunge

 

The Bunge Family: Mario, Eric, Marta and Silvia

Some mathematical projects are less about proving theorems and more about bringing people together. Editing the special volume of Theory and Applications of Categories in honor of Marta Bunge felt very much like that.

I worked on it together with Maria Manuel Clementino and Jonathan Funk, and what stayed with me throughout was not just the range of mathematics in the papers, but the sense of a community that Marta helped build—across countries, generations, and styles of doing category theory.

One piece of the volume that is particularly close to my heart is the Remembrances postface. I wrote it with Andrée Ehresmann and Silvia Bunge, Marta’s daughter. We wanted to say something about Marta that doesn’t usually make it into journal articles: her generosity, her way of mentoring, and the many personal connections that sustained her mathematical life.

Another part of this project that I’m especially happy about is that we managed to republish Marta’s PhD thesis as a TAC reprint. The thesis, supervised by Peter Freyd and William Lawvere, is a beautiful piece of work, and making it accessible again felt long overdue.

And here is where the story becomes very much about people. Eric Bunge and Silvia Bunge scanned a copy of the thesis—but, as these things go, a few pages were missing. That could have stalled the whole effort. Instead, it set off a small chain of generosity: after a message from Prof. Michael Barr, Pamela Freyd arranged for the librarian at Penn to send us a complete digital version.

At that point came another remarkable contribution: Nathanael Arkor sat down and typed the entire thesis—quickly and carefully—turning a set of scans into a clean, usable document. It’s the kind of work that is easy to overlook, but absolutely essential if we want mathematical texts to remain alive and accessible. Many others helped along the way, including Matías Menni and Maria Manuel Clementino, and the whole process ended up feeling like a genuine collective effort.

There is one more piece of the story that I find especially meaningful. Marta’s personal collection of books has now been donated to the Mathematics Library of the University of São Paulo, thanks to the generosity of Eric and Silvia Bunge, who made sure the books were shipped there. I would also like to thank Stella Madruga, who helped receive and set up the collection, and Prof. Hugo Mariano, who helped make the connection in the first place. It’s hard to imagine a better continuation of a mathematical life than having one’s books find new readers.

Looking back, this volume is of course a mathematical object. But it is also something else: a trace of a network of people, ideas, and acts of care that continue to shape the field.

If you’d like to take a look:

• The foreword to the volume is here: http://www.tac.mta.ca/tac/volumes/40/fwd/40-fwd.pdf

• The reprinted thesis is here: http://198.164.44.141/tac/reprints/articles/30/tr30.pdf

---

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.