*some*AI class, I can't be too choosy) I don't see why the other, more broad, AI might be a bit more reasonable. Many nitpicky calculus proofs involving actual numbers == bad. Besides which, just taking two classes and sitting in on one might be a fine idea. Kaustuv asked me out of nowhere about decidability of linear logic fragments. I don't know if he read about my thinking about them, or just spontaneously got interested in them too just now. My grandiose dreams of making progress on the MELL question are sort of falling apart rather quickly, though. Also my thought on adding exponentials and a funny disjunction to BI to recover ILL as a subset doesn't work out because the disjunction totally fucks all four relevant cases of cut elimination. Foo. Research is hard. I think I will go shopping now (for food).

However! I later looked into the proof of undecidability of full propositional linear logic, and it's really cute. The paper which sketched the proof gave a reduction to and-branching two-counter finite-state machines. You get to posit some bunch of finite states, and some transitions between them labelled by "Increment Counter A", "Increment Counter B", "Decrement Counter A", "Decrement Counter B", "Fork to states Q and Q'", or "Halt", and the machine is considered to accept if all of its forked children halt with both counters set to zero. This seemed really primitive, so I looked up the reference, a 1961 paper by Marvin Minsky of all people, titled "Recursive Unsolvability [something something]". The proof that a (slightly different sort of) two-counter machine involves grungy Goedel-numbering sort of work, representing the binary tape encoded as a single integer k and head position x as counter A being 2^k 3^{2^x} and counter B being 0. You can do multiplication and conditional division by shunting things between the two counters exactly like typical brainfuck tricks and hacks. The importance of the additive conjunction in making things undecidable is providing the and-branching of the original automaton, which translates into being able to test for zero by conjunctively forking off a copy of yourself which doesn't do anything except zero out the other counter and stop. The test-for-zero-and-branch is in turn critical for being able to test whether one of these huge honking Goedel numbers is divisible by some prime or product of a few small primes. Proofs can be so cute sometimes. Meanwhile, I think I do have a very ugly proof to show that ! in MELL might as well only occur negatively at the very top level in the context, in the sense that decidability for this restricted form of MELL provability questions implies decidability for all of MELL. Not that this is any major milestone, and in fact I would not at all be surprised if it's already been done, but it seems like a nice small fact to know. I should actually check that the well-ordering foo goes through correctly.