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 !A ⊸ B, and classical implication as !A ⊸ ?B. 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 formulae of intuitionistic logic to formulae of linear logic in a way which 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.
Read more about this topic: Linear Logic
Famous quotes containing the words classical and/or logic:
“Et in Arcadia ego.
[I too am in Arcadia.]”
—Anonymous, Anonymous.
Tomb inscription, appearing in classical paintings by Guercino and Poussin, among others. The words probably mean that even the most ideal earthly lives are mortal. Arcadia, a mountainous region in the central Peloponnese, Greece, was the rustic abode of Pan, depicted in literature and art as a land of innocence and ease, and was the title of Sir Philip Sidney’s pastoral romance (1590)
“The usefulness of madmen is famous: they demonstrate society’s logic flagrantly carried out down to its last scrimshaw scrap.”
—Cynthia Ozick (b. 1928)