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
@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
@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 Yeah, there is :)