dr4b and agh and Mindy and zml and oren I did expect, but there was also Jason Weill, whom I sort of remembered from undergrad, the inimitable Jason Crawford, people like Cheryl Platz and Beeler-house Rory both of whom I remember pretty well but somehow but never talked to in the past, Nick Carter from math studies and (I hope I'm getting her name right) Denise Noyes, puzzle master Derek Leung, the awesome papertygre, whose being in Seattle for about a year already I somehow didn't realize, fellow FLoC attendee James Cheney, and one of the KGB co-founders whose name I think was Will Frank.LICS talks were okay this morning. Blass talked about game semantics, and I understood about as much as I did from the abstract; that some people are trying to tweak game semantics to match up with the logic, and other people are trying to find a logic that describes the known most natural operations on games. I remember another talk being about using (classical) linear logic to model DRM, which was hard to care about, since I feel in my guts that DRM is kind of doomed in the long run, and then classical linear logic on top of that, ugh.
Somehow the situation of the first talk — the apparent equal promise of nudging one thing to match the other, or the other to the one — seems inevitable and common to me; that all we can really do in the end is poke around in the vast cosmos of algebraic (or categorical, or topological, or whatever) structures, and poke around in the equally vast cosmos of deductive systems, and discover which ones are isomorphic to which.
Moreover, and this is a point I think I was struggling to formulate last night over dinner with
fancybred and Moritz, all those algebraic (or categorical, or etc.) structures are, by virtue of being ultimately described in some formal system, e.g. ZFC, are "merely" sub-deductive systems of it — and so in some sense every "semantics" is already simply a translation from (a husk of, i.e. the language) a deductive system that is evidently such, into one that perhaps is not so evidently one. Because of this the codomain of every semantics is, in some sense, of equal status to the sort of deductive systems we constructive formalist weenies traffic in.Now I'm vulnerable to a typical variety of objection here, that I'm just saying "everything is syntax" when I ought to say the weaker statement "everything can be construed as syntax" while semantics-fanciers (let's say ZFC-fanciers in particular) might just as well conceptualize my symbol-shunting as being encoded as set-theoretic constructions of strings of symbols. Where there is asymmetry, I think, is the reliability of consensus among different mathematicians. I have low confidence that someone else's basic intuitions about sets (particularly infinite ones!) agree with mine, but very high confidence that they will accept the same finite (or, even stronger, pragmatically finite, what some might call "ultrafinite") strings of symbols as valid proofs, once proof rules are given. So I can avoid the question of whether mathematical objects really exist, if all I care about is that the social process of mathematics is stable; that what I consider a proof is what you consider a proof, and that what I consider a proof today is what I consider a proof tomorrow.
