§ Introduction to substructural logics: Ch1
§ Logic as talking about strings
- The book gives a new (to me) interpretation of rules like . It says that this can be read as "the string is of type ", where type is some chomskian/grammarian sense of the word "type".
- This means that we think of as "concatenate and ".
- This allows one to think of as the statement " when concatenated with a string of type produces a string of type ".
- This is interesting, because we can have judgements like and with no problem, we're asserting that the string is of type , . Which, sure, I guess we can have words that are both nouns and verbs, for example.
- Under this guise, the statement just says that " is both a noun and a verb".
- Further, if I say and , then one wants to ask "what is type of ? we want to say "it is the type next to ", which is given by (or, 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 should be read as "the vector lives in the subspace of the large vector space.
- Then, the rule , entails means: if lives in subspace and lives in subspace , then lives in the intersection .
- On the other hand, the rule , entails means: if lives in subspace , lives in subspace , then the vector lives in subspace .
- See that in the case of the conjunction, we are talking about the same , just choosing to restrict where it lives ( )
- See that in the case of tensor product, we have two elements and , which live in two different subspaces and .
§ Cut and admissibility
- Cut is the theorem that lets you have lemmas.
- It says that if , and then .
- 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 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 if the axioms of the theory allows one to prove .