Both intuitionistic and classical implication can be recovered from linear implication by inserting exponentials: intuitionistic implication is encoded as , while classical implication can be encoded as or (or a variety of alternative possible translations).