Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthormaxsnew
    • CommentTimeDec 12th 2017

    Made a stub for admissible rule with a few examples, after seeing the discussion about negation here

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeDec 12th 2017

    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?

    • CommentRowNumber3.
    • CommentAuthormaxsnew
    • CommentTimeDec 13th 2017

    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.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeDec 14th 2017

    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.

    • CommentRowNumber5.
    • CommentAuthormaxsnew
    • CommentTimeDec 15th 2017

    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?

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeDec 16th 2017

    Yes, that’s right.