# Translations of classical logic

From LLWiki

Revision as of 23:11, 5 October 2009 by Olivier Laurent (Talk | contribs)

## Contents |

## T-translation

Formulas are translated as:

This is extended to sequents by .

This allows one to translate the rules of classical logic into linear logic:

### Alternative presentation

It is also possible to define by:

If we define , we have and thus we obtain the same translation of proofs.

## Q-translation

Formulas are translated as:

The translation of any formula starts with , we define such that .

The translation of sequents is .

This allows one to translate the rules of classical logic into linear logic:

We use .

### Alternative presentation

It is also possible to define as the primitive construction.

If we define , we have and thus we obtain the same translation of proofs.