This is my note learning Linear Logic by **Frank Pfenning**.

## 1 Formalize

The notation below shows how to tracks all the ephemeral propositions in the judgment explicitly during inference:

in which $\Delta$ is the $\mathit{resources}$ and $C$ as the goal we have to achieve. We have to use all the resources in $\Delta$ $\mathit{exactly~once}$ in the proof that we can achieve C.

Structural rules:

We use sequent calculus to express linear logic, in which **left rules** show how to **use** a proposition (achieve a goal), **right rules** show how to **prove** a proposition. Each proposition $\Delta\vdash P$ actually means $\Delta\vdash P~eph$.

## 2 Linear Logic vs Intuitionistic Logic

- there is no weakening in Linear Logic like the following rule
- there is no contraction in Linear Logic like the following rule

## 3 Harmony - Local

### 3.1 Local Completeness - Identity Expansion

In natural deduction, we justify that the proof for the original proposition can be reconstructed via Elimination and then Introduction to show that the Elimination and Introduction rules match for local completeness.

However, in sequent calculus, we need to show that the identity rule at a compound type can be expanded to the identity rule at smaller types. Or in another words, we can construct the identity rule on compound type based on identity rules on smaller types using left and right rules.

### 3.2 Local Soundness - Cut Reduction

In natural deduction, we demonstrate that a more direct proof of the conclusion of an elimination can be found that first introduces and then eliminates to show that the Elimination and Introduction rules match for local soundness.

However, in sequent calculus, we need to show that we can reduce a cut at a compound type to cuts on smaller types.

## 4 Harmony - Global

### 4.1 Linear Cut Admissibility - Soundness

The admissibility of cut can be formalized as ($\Rightarrow$ means we can prove the corresponding judgement using $\vdash$ without using cut rule): if $\begin{array}{c}\mathcal{D}\\Delta\Rightarrow A\end{array}$ and $\begin{array}{c}\mathcal{E}\\Delta’,A\Rightarrow C\end{array}$ then $\begin{array}{c}\mathcal{F}\\Delta,\Delta’\Rightarrow C\end{array}$

Same as the proof in intuitionistic logic, we build the proof by the combination of the last inference rule that is applied in $\mathcal{D}$ and $\mathcal{E}$. To simplify the cases we need to consider, we classify the cases as follows:

- The last inference rule is initial sequent in $\mathcal{D}$ or $\mathcal{E}$
- Case 1: the last inference rule in $\mathcal{D}$ is initial sequent
- Case 2: the last inference rule in $\mathcal{E}$ is initial sequent using cut formula $A$
- There is no case for not using A, as all resources must be consumed in Linear Logic

- The last inference rule is not initial sequent in $\mathcal{D}$ and $\mathcal{E}$
- Case 3: $A$ is the principle formula of the last inference rule (which is not initial sequent) in both $\mathcal{D}$ and $\mathcal{E}$
- It must be derived by a left rule applied as last inference rule in $\mathcal{E}$ and by a right rule applied as last inference rule in $\mathcal{D}$. Apparently, all the cases have been covered in
**Cut Reduction**. It can be proved by induction hypothesis on the smaller type, sub deduction of $\mathcal{D}$ and $\mathcal{E}$ used in the result of the reduction.

- It must be derived by a left rule applied as last inference rule in $\mathcal{E}$ and by a right rule applied as last inference rule in $\mathcal{D}$. Apparently, all the cases have been covered in
- Case 4: $A$ is not the principle formula of the last inference rule (which is not initial sequent) in $\mathcal{D}$
- Case 5: $A$ is not the principle formula of the last inference rule (which is not initial sequent) in $\mathcal{E}$

- Case 3: $A$ is the principle formula of the last inference rule (which is not initial sequent) in both $\mathcal{D}$ and $\mathcal{E}$

**Proof:** By induction on the structure of $A$, derivation $\mathcal{D}$ and $\mathcal{E}$

- Case 1: the last inference rule in $\mathcal{D}$ is initial sequentThus $\Delta=A$. We have $\Delta’,A\Rightarrow C$, which shows $\Delta,\Delta’\Rightarrow C$.
- Case 2: the last inference rule in $\mathcal{E}$ is initial sequentThus $\Delta’=\cdot$ and $A=C$. We have $\Delta\Rightarrow A$ by $\mathcal{D}$, which shows $\Delta,\Delta’\Rightarrow C$.
Case 4: A is not the principle formula of the last inference rule (which is not initial sequent) in $\mathcal{D}$. We do case analyse by all the left rules that can be applied as the last inference rule in $\mathcal{D}$

- Case 4.1 $\otimes L$
- Case 4.2 $\multimap L$
- Case 4.3 $1 L$
- Case 4.4 $\& L_1$
- Case 4.5 $\& L_2$. The proof is symmetric to 4.4
- Case 4.6 $\oplus L$
- Case 4.7 $0 L$

Case 5: A is not the principle formula of the last inference rule (which is not initial sequent) in $\mathcal{E}$. We do case analyse by all the left and right rules that can be applied as the last inference rule in $\mathcal{E}$

- Case 5.1 $\otimes L$
- Case 5.2 $\multimap L$
- Case 5.3 $1 L$
- Case 5.4 $\& L_1$
- Case 5.5 $\& L_2$. The proof is symmetric to Cae 5.4.
- Case 5.6 $\oplus L$
- Case 5.7 $0 L$
- Case 5.8 $\otimes R$
- Case 5.9 $\multimap R$
- Case 5.10 $1 R$
- Case 5.11 $\& R$
- Case 5.12 $\top R$
- Case 5.13 $\oplus R_1$
- Case 5.14 $\oplus R_2$. The proof is symmetric to Case 5.13.