@lambdagrrl The one looks boring, the other doesn't, but they both follow directly from the polarity of the connective, so I guess they're both kinda dull.

@cyrridven I'd say the left rule is interesting cos it produces two sub-goals, whereas the right rule does not

@lambdagrrl Oh, woops, did I mess that up? The branching rules were meant to be listed as interesting. Though the boring rules are actually the non-invertable rules, whereas the others are invertable, so there's a good argument for flipping the boring/interesting distinction.

@cyrridven I was wondering if there was any link to the whole positive vs negative types thing

@lambdagrrl Yeah, there is :)

@cyrridven is there a maximally boring logic where all the rules are boring, and if so is it interesting?

@lambdagrrl Yes, display logic, where all logical rules follow directly from polarity.