Logic ForAll

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 , S…

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…

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 manipula…

Skolem is not constructive (but sometimes it can be) On what goes wrong when you try to eliminate quantifiers intuitionistically proof theory constructive 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 wi…

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 …

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 D…

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 Hypothe…

Gavin Bierman Over the last thirty years, I have repeatedly returned to a particular question in logic: What should modal logic look like in a constructive world? This question first appeared in my work in the early 1990s and has since shaped a series of papers, collaborations, workshops, and talks. Looking back, it is clear that these efforts form a small research lineage centered on the interac…

This blog post is based on a talk recently given at Chapman University, developed within the context of our joint Topos–Chapman collaboration. I thank the audience for a lively discussion. Milly Maietti In the 1990s, intuitionistic linear logic was booming. There were multiple typed calculi, multiple categorical models, and a growing body of results showing soundness and completeness between them…

A standard story in proof theory textbooks says that an intuitionistic sequent calculus is obtained from a classical one by imposing a single-conclusion restriction. Gentzen’s LJ arises from LK by allowing at most one formula in the succedent. From this, many readers conclude that constructivism is about cardinality: classical logic allows multiple conclusions; intuitionistic logic does not. The …

In Homer’s Odyssey, Penelope survives not by force, but by craft. She weaves by day and unweaves by night. The weaving keeps the suitors at bay; the unweaving buys her time. It is not indecision. It is strategy. It is control over her own narrative. I have decided to learn from Penelope. Over the next months (or years), I will be rewriting my old papers. Not because the mathematics is wrong. Not …

Maybe you haven't heard about `Manels'? As Gemini explains: A "manel" is a panel of professionals, often at conferences or in media, composed entirely of men. It is often seen as a failure of diversity, equity, and inclusion (DEI) , implying that women are either not qualified to contribute or that their perspectives are unnecessary. One of the most widely cited and "outrageous" examples of a man…

Harold wasn't ill, as far as I know. He seemed to be enjoying his life as an avant-guarde musician, and was due to perform two days (or something like it) after he died. I read it in the website of the venue when I tried to learn more. This seems so unfair! Harold A. J. M. Schellinx was very, very clever and a good person. He helped me a lot when we were both starting. I finished my doctorate ear…

Phew! I almost completely missed it! This year's Ada Lovelace heroes are Larisa Maksimova and Ewa Orlowska. Someone once said (and I repeated it dozens of times in talks and in writing) that starting a project is easy; difficult is keeping it up, year after year.  Maintenance is much harder than starting new things. It's not sexy, I can be very boring. I seem to be falling prey to this difficulty…

On July 6–7, 2024, the Hausdorff Institute of Mathematics hosted the Women in Formal Mathematics workshop, a two-day event dedicated to showcasing and supporting women in formal proofs, logic, and automated deduction. The workshop was organized within the trimester program Prospects of Formal Mathematics, with support from Women in EuroProofNet 2024 (WEPN) . This blog post should probably have be…

I was always very keen on the idea that philosophical logicians and programming language designers interested in non-classical modal logics should talk to each other about their problems, about what kinds of  intuitionistic or constructive modal logics they would like to have and  why. Their goals are clearly different, but there is a large overlap in the mathematical contents of their common sub…

I have been an Honorary Fellow at the School of Computer Science in the University of Birmingham, UK since 2000. I am still officially one  until 2028 and have an official letter saying it. But the University re-organized its website and I have not been able to get my webpage to resurface at all. The problem with this state of affairs is that many of my papers stopped  being available, which is a…

This picture from the first blog post of the Topos Institute celebrates the official opening of Topos in Jan 2021.  Topos already existed then, but  it seems nice to celebrate from that picture, which is  4 years and 3 months old, give or take a few days. Many things happened in these years and I find it instructive to go over some of what has happened to me and my research. It is also humbling t…

This post is simply a condensed version of an interview that Brendan gave to Eric Gilliam . I wanted to reproduce it here as I want to think about what my answers would be. (the full text of the interview is found in the link above) What is Topos from a very high level? Topos is a new structure for doing research for the public benefit. In pursuit of this goal, we combine a focus on fundamental, …