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 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