Editing Linear logic (section)

==Encoding classical/intuitionistic logic in linear logic==

Both intuitionistic and classical implication can be recovered from linear implication by inserting exponentials: intuitionistic implication is encoded as {{math|!<VAR>A</VAR> ⊸ <VAR>B</VAR>}}, while classical implication can be encoded as {{math|!?<VAR>A</VAR> ⊸ ?<VAR>B</VAR>}} or {{math|!<VAR>A</VAR> ⊸ ?!<VAR>B</VAR>}} (or a variety of alternative possible translations).{{sfn|Di Cosmo|1996}} The idea is that exponentials allow us to use a formula as many times as we need, which is always possible in classical and intuitionistic logic.

Formally, there exists a translation of formulas of intuitionistic logic to formulas of linear logic in a way that guarantees that the original formula is provable in intuitionistic logic if and only if the translated formula is provable in linear logic. Using the [[Gödel–Gentzen negative translation]], we can thus embed classical [[first-order logic]] into linear first-order logic.