# Linear Logic Winter School 2022

## Exercise Sessions on Sequent Calculus

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

### Session 1: Building Proofs

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:

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é !
``````

### Session 2: Eliminating Cuts

#### Cut Elimination Steps

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).

1. Give a proof of 1⊕1 ⊢ 1⊕1 encoding negation. `[solution]`
2. Give a proof of 1⊕1 ⊢ (1⊕1)⊗(1⊕1) which duplicates a Boolean. `[solution]`
3. Give a proof of 1⊕1 ⊢ 1 which erases a Boolean. `[solution]`
4. Give a proof of 1⊕1, 1⊕1 ⊢ 1⊕1 encoding conjunction of Booleans. `[solution]`

#### Confluence

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

#### Rule Commutations

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.