You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
John Baez (Jul 27 2025 at 09:58):Terry Tao recently wrote some nice comments on blue-team and red-team thinking in cybersecurity and other issues. This triggered some thoughts in me, and I wrote:
Logicians are starting to think harder about this blue team / red team distinction. Constructive logic, the logic of verification, codifies some of the blue team principles you enunciate. But co-constructive logic, which seems to be a more recent topic of interest, is the logic of refutation. It codifies some of the red team principles.
Mike Shulman has recently written about a form of logic that combines the constructive and co-constructive aspects. His paper is rather technical, but here's a revealing quote:
"Intuitionistic logic is often explained informally (e.g. in [TvD88a]) by the so-called Brouwer–Heyting–Kolmogorov (BHK) interpretation, which explains the meaning of the logical connectives and quantifiers “pragmatically” in terms of what counts as a proof of them. [...] Practicing constructive mathematicians, however, have found that it is often not sufficient to know what counts as a proof of a statement: it is often just as important, if not more so, to know what counts as a refutation of a statement. [...] To repeat, the problem is that the BHK interpretation and resulting intuitionistic logic privilege proofs over refutations. [...] This suggests a BHK-like explanation of logical connectives in terms of both what counts as a proof and what counts as a refutation. We now explore what such an explanation might look like."
Studying this formally, as Mike is doing, might be useful for AI safety, etc.
- Mike Shulman, Affine logic for constructive mathematics.
It might be nice for Mike to talk directly to Terry about this.
Mike Shulman (Jul 28 2025 at 00:11):That's a nice perspective of Terry's on the uses and abuses of pattern engines, and I also like your observation about the relation to game semantics, linear logic, and Chu constructions (which, as Sidney Congard pointed out, predate my work). I'd certainly be happy to talk about it further with you, Terry, or anyone else (though not via microblogging).
David Corfield (Jul 28 2025 at 17:21):Someone the other day pointed out Clark Barwick's work on isolatability of points in a space, higher groupoids measuring space of ways of isolating two points. It put me somewhat in mind of Mike's ideas on duality of proof and refutation.