# Translations of intuitionistic logic

The genesis of linear logic comes with a decomposition of the intuitionistic implication. Once linear logic properly defined, it corresponds to a translation of intuitionistic logic into linear logic, often called *Girard's translation*. In fact Jean-Yves Girard has defined two translations in his linear logic paper^{[1]}. We call them the call-by-name translation and the call-by-value translation.

These translations can be extended to translations of classical logic into linear logic.

## Contents |

## Call-by-name Girard's translation

Formulas are translated as:

This is extended to sequents by .

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

## Call-by-value 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 intuitionistic 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.

## Call-by-value Girard's translation

The original version of the call-by-value translation given by Jean-Yves Girard^{[1]} is an optimisation of the previous one using properties of positive formulas.

Formulas are translated as:

The translation of any formula is a positive formula.

The translation of sequents is .

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

We use .

## References

- ↑
^{1.0}^{1.1}Girard, Jean-Yves.*Linear logic*. Theoretical Computer Science. Volume 50, Issue 1, pp. 1-101, doi:10.1016/0304-3975(87)90045-4, 1987.