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:

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

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/⊥, !/?d, !/?c, !/?w

Commutation cases: ⊗, ⅋, ⊕₁, ⊕₂, &, ⊥, ⊤, ! (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]

Confluence

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

• ⊢ A⅋B, (A^⊥⊗B^⊥)⊗(C^⊥⊗D^⊥), C⅋D
• ⊢ A&A, A^⊥&A^⊥

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

• ⅋/⅋ commutation
• ⊗/⊗ commutation

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:

• &/⊕ commutation
• &/⊗ commutation

Exponential Copy

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

Exponential Isomorphism

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

More

You can continue with additional examples.

You can investigate MLL as a Lego game.