The n-Category Café

Works fine for me in any of five different ways: Acrobat Reader embedded in a Firefox tab, standalone Acrobat, kpdf, xpdf, and gv.

Oh, I was assuming you meant the first pdf link (the slides). But I guess you meant the second (the tutorial). If I just click on the link to the tutorial then Firefox gives me an embedded Acrobat Reader which, like yours, fails to read past the first page. However, if I save the tutorial (by right-clicking on the link) then I can view it fine with any of the four pdf viewers mentioned in my previous comment — including Acrobat. Odd.

Tom wrote:

Odd.

This is known problem — especially for large PDF files, I think. It happens, for example, when I use Firefox to access the copy of Derek Wise’s thesis on my website.

But when Peirce used a circle or box for negation, the tensor operation inside remained the same, i.e., inside and outside two inscriptions correspond to their conjunction. So it looks like Peirce’s box is rather different.

That’s right: Peirce in effect uses just two primitives (“and” and “not”). The “or” operation is derived.

The specific rules of inference used by Peirce are actually very clever (I particularly have in mind his rule of “iteration”) and have been rediscovered or partly rediscovered over the years (e.g., by Paul Taylor – I’d have to look it up to see what he calls it, but he seems to deem it significant). It is this rule which Gerry and I sought to analyze in our Alpha paper in a linear logic kind of way.

An Alpha graph is a graphical expression which corresponds to a Boolean formula, consisting of (labeled) “spots” and boxes (what Peirce calls “seps”, short for lines of separation) in the plane (called the “sheet of assertion”). A labeled spot can be thought of as a propositional variable. To conjoin two Alpha graphs, just juxtapose them in the plane; to negate an Alpha graph, surround it by a box. The empty sheet of assertion represents the constant “true”.

The three rules of inference (really rule schemes) are

• “Weakening”: An Alpha graph $G$ can be weakened by excising any subgraph $H$ which is surrounded by an even number of boxes, or by adding in as a subgraph any Alpha graph $H$ so that it is surrounded by an odd number of boxes. The soundness of this rule for propositional logic is by an induction where the base cases are the inferences $$G = G^\prime \wedge H \to G^\prime$$ $$\neg(G^\prime) \to \neg(G^\prime \wedge H) = G$$
• One may freely remove or insert a pair of boxes, one enclosing the other, provided there are no spots between them. This just corresponds to the bi-implication $$G \leftrightarrow \neg \neg G$$
• “Iteration”. In this rule, if $H$ is a subgraph of $G$, one can freely insert a second copy of $H$ inside $G$ as another subgraph, provided the copy is not placed outside any box containing $H$ [I hope I’ve remembered this correctly; it’s been a while]. This rule is invertible (“de-iteration”). Again the soundness of these rules is proved by an induction where the base case corresponds to a bi-implication $$H \wedge \neg G^\prime \leftrightarrow H \wedge \neg(H \wedge G^\prime)$$ The forward implication for this case follows by applying the operator $H \wedge -$ to an instance of weakening. The backward implication uses standard properties of the cartesian product $\wedge$ in conjunction with the fact that there is an arrow $$H \wedge \neg(H \wedge G^\prime) \to \neg G^\prime.$$

In terms of categorical linear logic, this last arrow corresponds to a strength of the contravariant functor $\neg$ on a *-autonomous category, as I mentioned in comments on Week 268.

So Gerry and I explain the iteration rule as an amalgamation of standard properties of cartesian product together with a fact well-known to categorical logicians: that in the theory of symmetric monoidal closed categories $V$, every definable functor $V \to V$ (whether covariant or contravariant) carries a canonical strength. The fact that it’s all about strengths makes it a kind of monoidal approach, but I ought to think about this myself a little further in connection with the Week 268 discussion and hopefully tie some of these threads together more tightly.