Sequent calculus talks about left and right rules. Is there terminology within sequent calculus for boring rules (L∧,R∨,L→) versus interesting rules (R∧,L∨,R→)?
@cyrridven why is L→ boring and R→ interesting? that seems like it's the wrong way around to me
@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.
@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.