Here's the counterexamples that occurred to me this morning. The first one I found was
(A ⊗ ⊤) ∧ 1 ⊢ A ∧ 1
which is a special case of the distributivity property
(A ⊗ B) ∧ 1 ⊢ (A ∧ 1) ⊗ (B ∧ 1)
Both are true of my intended interpretation in Grph, but not provable in BI.
The operations of "∧ 1" and "⊗ ⊤" are kind of interesting in their own right. The graph A ∧ 1 strips all edges off of A, leaving only the vertices behind. (Since 1 is the one-vertex, no-edge graph, and edges in the cartesian product A ∧ B of two graphs generally consist of pairs of edges, one from A, one from B) the graph A ⊗ ⊤ takes A and adds self-loops at every vertex (since ⊤ is the one-vertex, one-self-edge graph, and edges in the tensor product A ⊗ B consist of pairs that are either a vertex from A and an edge from B, or an edge from A and a vertex from B).
But in that case it's clear that if you add some self-edges, then obliterate all edges, including the ones you just added, it's the same thing as just obliterating all edges, thus (A ⊗ ⊤) ∧ 1 ⊢ A ∧ 1.
In the separation-logic-ish interpretation of BI as talking about memory in a program, this seems to be hypothesizing a heap about which we know
(a) It divides into two parts, one of which has property A, and the other half we know nothing in particular about
(b) That it is empty
and it actually seems reasonable to conclude that therefore property A does hold of the heap, since any part of the empty heap is empty, and the current heap is empty.
So this dredges up dim memories I have of
neelk and noam and rob talking in front of a whiteboard somewhere in Wean about extra-axiomatic stuff that you might want to add in a separation logic that would imply things likeA ∧ 1 ⊢ A ⊗ A
whose heuristic "proof" also involves making hay out of the known emptiness of A.
Oh wait, and the graph model validates this sentence, too! So this is a third counterexample.
Stillll though I think my previous rambling might possibly lead to a purely-equational reduction of BI to first-order logic, but I guess I'm now convinced that in order to do so, it has to depart somewhat from my graph-ish intuitions. I start suspecting I have to replace the binary + on booleans with something noncommutative, so that I end up representing paths through the BI context-tree...
Anyway, ♥ ♥ ♥ math ♥ ♥ ♥.
