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:
“Classical art, in a word, stands for form; romantic art for content. The romantic artist expects people to ask, What has he got to say? The classical artist expects them to ask, How does he say it?”
—R.G. (Robin George)
“What avail all your scholarly accomplishments and learning, compared with wisdom and manhood? To omit his other behavior, see what a work this comparatively unread and unlettered man wrote within six weeks. Where is our professor of belles-lettres, or of logic and rhetoric, who can write so well?”
—Henry David Thoreau (1817–1862)