Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Made a stub for admissible rule with a few examples, after seeing the discussion about negation here
Thanks! I tweaked it a little. I wasn’t sure what you meant by “strictness” so I replaced it by a sentence that I do understand; can you explain what you meant?
I was basically trying to say what you did in the edit. Initially I wrote that admissible or not should not affect what is considered a model (for the “specified” admissible rules), but thinking about cut in particular, a 1-variable sequent calculus with admissible cut can only have models where composition is strictly associative, but if cut is a primitive rule then you can make a distinction between (cut;cut);cut and cut;(cut;cut), so you could have models that are weakly associative. I’m not sure if that’s a sensible distinction though because if you do want composition to be associative you should add equalities for it.
I don’t agree that an admissible cut can only have models where composition is strictly associative. In fact, I think it’s easier to deal with non-strict models when cut is admissible than when it’s not, since in the former case you don’t have to put the associativity isomorphisms and their coherence into the syntax. As a simple example, the free category on a graph is also the free bicategory on the same graph (in the appropriate weak bicategorical sense), and you can prove that by induction over a cut-free presentation of it, which essentially amounts to choosing to bracket all composites in one direction.
Hm, I guess you’re right, as long as you relax the strictness of you notion of model it doesn’t matter if the syntax is strict? Would another example be that the free strictly associative monoidal category is also the free monoidal category, but crucially the former has functors that strictly preserve the monoid whereas the latter only pseudo preserves them?
Yes, that’s right.
1 to 6 of 6