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:
“The basic difference between classical music and jazz is that in the former the music is always greater than its performance—Beethoven’s Violin Concerto, for instance, is always greater than its performance—whereas the way jazz is performed is always more important than what is being performed.”
—André Previn (b. 1929)
“The much vaunted male logic isn’t logical, because they display prejudices—against half the human race—that are considered prejudices according to any dictionary definition.”
—Eva Figes (b. 1932)