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

Computing with Additive Booleans

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]


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.

Additional commutations:

Exponential Copy

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

Exponential Isomorphism


You can continue with additional examples.

You can investigate MLL as a Lego game.