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:
“Culture is a sham if it is only a sort of Gothic front put on an iron building—like Tower Bridge—or a classical front put on a steel frame—like the Daily Telegraph building in Fleet Street. Culture, if it is to be a real thing and a holy thing, must be the product of what we actually do for a living—not something added, like sugar on a pill.”
—Eric Gill (1882–1940)
“We want in every man a long logic; we cannot pardon the absence of it, but it must not be spoken. Logic is the procession or proportionate unfolding of the intuition; but its virtue is as silent method; the moment it would appear as propositions and have a separate value, it is worthless.”
—Ralph Waldo Emerson (1803–1882)