Exercises rely on the C1ick ⅋ c⊗LLec⊥ interactive proof system for manipulating sequent calculus proofs of Linear Logic.

Start by getting familiar with the system by using its tutorial (from "`Here is a short tutorial`

" to "`That's it!`

": skip the final 7 examples).

You can then either replay the examples given in Michele Pagani's lecture:

- 1 ⅋ X
- (H ⊸ M) ⊗ (S ⊸ H) ⊢ S ⊸ M
- (H ⊸ A) ⊗ (H ⊸ M) ⊢ H ⊸ (M ⊗ A)
- (H ⊸ A) ⊗ (H ⊸ M) ⊢ (H ⊗ H) ⊸ (M ⊗ A)
- (H ⊸ A) & (H ⊸ M) ⊢ H ⊸ (M & A)
- (H ⊸ M) & (S ⊸ H) ⊢ S ⊸ M
- (H
^{⊥}⊕ M) & (S^{⊥}⊕ H) ⊢ S^{⊥}⊕ M

or move to the Linear Logic Tutorial (be careful: some proposed sequents are not provable!).

Prove that if you have 35€ and you go to Michele's restaurant, you can get Vin, 2 verres d'Eau, Quiche, Canard and Raisin, if it is definitely not a good season for bananas and oranges.

```
Menu à 35 euros
Entrée :
Quiche Lorraine ou Saumon Fumé
et Plat :
Pot-au-Feu ou Filet de Canard
et Dessert :
un fruit selon la saison (Banane ou Raisin ou Oranges)
ou
un gâteau (Tarte aux Pommes ou Mille-Feuilles)
Vin et Eau à volonté !
```

Play with reduction steps: try to predict the result before asking the machine to reduce the cut.
Then you can use the `↶/↷`

buttons to replay.

Key cases:
*ax*,
⊗/⅋,
⊕_{1}/&,
⊕_{2}/&,
1/⊥,
!/?*d*,
!/?*c*,
!/?*w*

Commutation cases:
⊗,
⅋,
⊕_{1},
⊕_{2},
&,
⊥,
⊤,
! (including !/!),
?*d*,
?*c*,
?*w*

Booleans can be encoded in LL as additive Booleans 1⊕1. This means that there are exactly two cut-free proofs of this formula which are chosen as representing `true`

and `false`

respectively.

```
─── 1 ─── 1
⊢ 1 ⊢ 1
─────── ⊕1 and ─────── ⊕2
⊢ 1 ⊕ 1 ⊢ 1 ⊕ 1
```

A function from Booleans to Booleans can then be encoded as a proof of 1⊕1 ⊢ 1⊕1 or equivalently of ⊢ ⊥&⊥, 1⊕1, meaning that when it is cut against the encoding of an input it reduces (by cut-elimination) to the encoding of the output.

Using the links below you get a partial proof with a cut: you should complete the right-hand side according to the function you want to encode and you can test it then by filling the left part(s).

- Give a proof of 1⊕1 ⊢ 1⊕1 encoding negation.
`[solution]`

- Give a proof of 1⊕1 ⊢ (1⊕1)⊗(1⊕1) which duplicates a Boolean.
`[solution]`

- Give a proof of 1⊕1 ⊢ 1 which erases a Boolean.
`[solution]`

- Give a proof of 1⊕1, 1⊕1 ⊢ 1⊕1 encoding conjunction of Booleans.
`[solution]`

Try to get two different cut-free proofs by reducing the cut in the following proofs:

By reducing the cuts in differents ways obtain two proofs which differ by commutation of rules (as shown in the `MLL proof nets`

lecture):

Reduce the following cut step-by-step to see how it is able to search for the ⅋ rule inside the proof and to erase it: ⅋ eraser.

Reduce the following cut to move the ! rule down in the proof: ! down.

Additional commutations:

A proof of a formula !A can be duplicated by cut elimination: !A duplicator. Follow it step-by-step.

- Reduce !A⊗!B ⊢ !A⊗!B and compare with !A⊗!B ⊢ !A⊗!B
- Reduce !(A&B) ⊢ !(A&B) and compare with !(A&B) ⊢ !(A&B)

You can continue with additional examples.

You can investigate MLL as a Lego game.