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
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.