§ Introduction to substructural logics: Ch1

§ Terminology

§ Logic as talking about strings

• The book gives a new (to me) interpretation of rules like $X \vdash A$. It says that this can be read as "the string $X$ is of type $A$", where type is some chomskian/grammarian sense of the word "type".
• This means that we think of $X ; Y$ as "concatenate $X$ and $Y$".
• This allows one to think of $X \vdash A \to B$ as the statement " $X$ when concatenated with a string of type $A$produces a string of type $B$".
• This is interesting, because we can have judgements like $X \vdash A$ and $X \vdash B$ with no problem, we're asserting that the string $X$ is of type $A$, $B$. Which, sure, I guess we can have words that are both nouns and verbs, for example.
• Under this guise, the statement $X \vdash A \land B$ just says that " $X$ is both a noun and a verb".
• Further, if I say $X \vdash A$ and $Y \vdash B$, then one wants to ask "what is type of $X; Y$ ? we want to say "it is the type $A$ next to $B$", which is given by $A \circ B$ (or, $A \otimes B$ in modern notation).
• This is cool, since it gives a nice way to conceptualize the difference between conjunction and tensoring.

§ Tensor versus conjunction as vector spaces

• What I got most out of this was the difference between what they call fusion (what we now call tensoring in linear logic) and conjunction.
• Key idea: Let's suppose we're living in some huge vector space, and the statement $X \vdash A$ should be read as "the vector $X$ lives in the subspace $A$ of the large vector space.
• Then, the rule $X \vdash A$, $X vdash B$ entails $X \vdash A \land B$ means: if $X$ lives in subspace $A$ and $X$ lives in subspace $B$, then $X$ lives in the intersection $A \cap B$.
• On the other hand, the rule $X \vdash A$, $Y \vdash B$ entails $X ; Y \vdash A \circ B$ means: if $X$ lives in subspace $A$, $Y$ lives in subspace $B$, then the vector $X \otimes Y$ lives in subspace $A \otimes B$.
• See that in the case of the conjunction, we are talking about the same $X$, just choosing to restrict where it lives ( $A \cap B$)
• See that in the case of tensor product, we have two elements $X$ and $Y$, which live in two different subspaces $A$ and $B$.

§ Cut and admissibility

• Cut is the theorem that lets you have lemmas.
• It says that if $X \vdash A$, and $Y(A) \vdash B$ then $Y(X) \vdash B$.
• I don't understand what this means in terms of the interpretation of "left hand side as values, right hand side as types", or under "left side is strings, right side is types". The rule $Y(A) \vdash B$ is, at best, some kind of unholy dependently typed nonsense under this interpretation.
• A theory is cut-admissible if the axioms let you prove cut.
• In general, a theory is admissible to some axiom $A$ if the axioms of the theory allows one to prove $A$.