November 20th, 2012

beartato phd

(no subject)

Here's the trajectory of an idea that keeps coming back to me:

At Penn, I got interested in the idea of type theories where the types come equipped with a metric, that is, the inhabitants of a type are at some "distance" from one another; each type has a sort of geometry. The whole metric business was relevant for differential privacy, which was in turn relevant because we were ostensibly interested in fairly free-form computations being done over public networks, and privacy was a concern. Anyhow it gives an interesting and rich type theory, where there are, for instance, (at least) two different product-types, an & and a ⊗, just like in linear or bunched logic.

More recently, I found myself asking: where might such a numeric metric on inhabitants of a type "come from"? Well, although in principle these distance-numbers are continuous-valued, maybe we can think about a discrete graph, and the metric is counting the number of steps we have to take on that graph to get from one value of a type to another. Maybe the continuous-valued metric can be thought of as a kind of asymptotic "continuum limit" of distances in such a graph. This is what I was thinking of this past summer. In that case, & and a ⊗ become operations on graphs: & is the straight-up categorical product on graphs, and ⊗ is a funny thing that is product-y on vertices and somewhat coproduct-y on edges.

I tried getting a handle on the category of directed graphs with these operations as a logic, and didn't get too far. I know it proves strictly more things than bunched logic, but I don't know a proof system that characterizes it on the nose. I thought as a warm-up, I'd try doing logic over objects in the arrow category Sets, which is a lot like the category of graphs. An object in this category can be thought of as a graph where the only edges allowed are self-loops at a vertex. Squinting at it harder, we see that the only thing we can discern about any vertex is how many self-loops it has. So we might as well say Sets is the category of multisets of natural numbers. Ok, then what's & in this category? We take the cartesian product of the elements of a multiset, and in each slot take the product of the numbers. so {0,5} & {10,11,12} = {0,50,0,55,0,60}. What's the ⊗? We take the cartesian product of the elements, but take the sum of the numbers: {0,5} & {10,11,12} = {10,15,11,16,12,17}. Returning to the categorical perspective, we ask when morphisms exist between two objects A and B --- this is the thing that corresponds to logical entailment. All that matters is if you have some vertices in A, you have to have some vertices in B, and if your vertex in A has some self-loops, the vertex in B that it maps to has to have some self-loops. So for the purposes of "entailability", there's only three objects in Sets that we can tell apart, call them {}, {0}, and {0,1}. This is a bit more interesting than regular logic, which only has two truth values once I decategorify!

Actually, let me call {0,1} instead "2". So somehow I've tricked myself into thinking about a three-valued logic, with the following connectives:
& | 0 1 2  ⊗ | 0 1 2
--+------  --+------
0 | 0 0 0  0 | 0 0 0
1 | 0 1 1  1 | 0 1 2
2 | 0 1 2  2 | 0 2 2
and they seem to naturally invite me to define duals:
⊕ | 0 1 2 ⅋ | 0 1 2 --+------ --+------ 0 | 0 1 2 0 | 0 0 2 1 | 1 1 2 1 | 0 1 2 2 | 2 2 2 2 | 2 2 2

but WAIT WAIT WAIT I want an intuitionistic logic. Can I turn a Kripke-crank and get an intuitionistic logic out of a classical multi-valued one? "Intuitionistic sequent calculi for finitely many-valued logics" [Reznik and Curmin 2001] and "On intuitionistic many-valued logics" [Hanazwa and Takano 1984] seem to suggest I can, but I haven't finished digesting either one yet.


I'm finding both of these papers hard to digest still. I keep instead noticing that in my particular case, all the connectives I want to have are asking for a kind of max or min in some order, which is more special-case than the full generality of arbitrary truth-value functions that the papers consider. Even ⊗ is asking for the maximum of its two arguments, for the order 0 ≥ 2 ≥ 1. This means quantifiers can naturally be invented that just take n-way maxes in the same order. Leading to a positive/multiplicative ∀, maybe?


Hm, no, I think this many-valued logic intuition isn't useful for analyzing the logic-of-graphs as such. I can't get it to stpp satisfying A implies A ⊗ A.


Another interesting paper, though: Läuchli's completeness theorem from a topos-theoretic perspective [Menni 2007]