# Exercise Sheet 1:

Teacher: Michele Pagani

\newcommand\n{\mathrm{n}}

# Some MALL equivalences

## Ex1: Equivalences in LL sequent calculus

### Distributivity: $A ⊗ (B ⊕ C) ≡ (A ⊗ B) ⊕ (A ⊗ C)$

\infer{⊢ A ⊗ (B ⊕ C) ⊸ (A ⊗ B) ⊕ (A ⊗ C)}{ \infer{ A ⊗ (B ⊕ C) ⊢ (A ⊗ B) ⊕ (A ⊗ C) }{ \infer{A, B ⊕ C ⊢ (A ⊗ B) ⊕ (A ⊗ C)}{ \infer{A, B ⊢ (A ⊗ B) ⊕ (A ⊗ C)}{ \infer{A, B ⊢ A ⊗ B}{ A ⊢ A & B ⊢ B } } & \infer{A, C ⊢ (A ⊗ B) ⊕ (A ⊗ C)}{ \infer{A, C ⊢ A ⊗ C}{ A ⊢ A & C ⊢ C} } } } }
\infer{⊢ (A ⊗ B) ⊕ (A ⊗ C) ⊸ A ⊗ (B ⊕ C)}{ \infer{(A ⊗ B) ⊕ (A ⊗ C) ⊢ A ⊗ (B ⊕ C)}{ \infer{A ⊗ B ⊢ A ⊗ (B ⊕ C)}{ \infer{A, B ⊢ A ⊗ (B ⊕ C)}{ A ⊢ A & \infer{B ⊢ B ⊕ C}{ B ⊢ B } } } & \infer{A ⊗ C ⊢ A ⊗ (B ⊕ C)}{ \infer{A, C ⊢ A ⊗ (B ⊕ C)}{ A ⊢ A & \infer{C ⊢ B ⊕ C}{ C ⊢ C } } } } }

### Absoption: $A ⊗ 0 ≡ 0$

\infer{⊢ A ⊗ 0 ⊸ 0}{ \infer{A ⊗ 0 ⊢ 0}{ \infer[0 \text{L}]{A, 0 ⊢ 0}{\phantom{A, 0 ⊢ 0}} } }

# Translations of LJ and LK into LL

### Call-by-name translations

LJ into LL LK into LL
$% $ $% $

## Ex2: $(\bullet)^\n$ and intuitionistic conjunction

The $(\bullet)^\n$ translation allows to encode the rules associated with the intuitionistic conjunction:

\cfrac{Γ ⊢ A \qquad Δ ⊢ B}{Γ, Δ ⊢ A ∧ B}∧ \text{R} \qquad \cfrac{Γ, A ⊢ C}{Γ, A ∧ B ⊢ C} ∧_1 \text{L}
\infer{!Γ^\n, !Δ^\n ⊢ A^\n \& B^\n}{ \infer[\text{l-w}]{!Γ^\n, !Δ^\n ⊢ A^\n}{!Γ^\n ⊢ A^\n} & \infer[\text{exch.}]{ !Γ^\n, !Δ^\n ⊢ B^\n}{ \infer[\text{l-w}]{!Δ^\n, !Γ^\n ⊢ B^\n}{!Δ^\n ⊢ B^\n} } }

And:

\infer[\text{cut}]{!Γ^\n, !(A^\n \& B^\n) ⊢ C^\n}{ \infer{!Γ^\n, !A^\n ⊗ !B^\n ⊢ C^\n}{ \infer{!Γ^\n, !A^\n, !B^\n ⊢ C^\n}{ !Γ^\n, !A^\n ⊢ C^\n } } & \infer{!(A^\n \& B^\n) ⊢ !A^\n ⊗ !B^\n}{ \infer{!(A^\n \& B^\n) ⊢ !A^\n ⊗ !B^\n}{ \infer{!(A^\n \& B^\n), !(A^\n \& B^\n) ⊢ !A^\n ⊗ !B^\n}{ \infer[\text{prom.}]{!(A^\n \& B^\n) ⊢ !A^\n}{ \infer[\text{der.}]{!(A^\n \& B^\n) ⊢ A^\n}{\infer{A^\n \& B^\n ⊢ A^\n}{A^\n ⊢ A^\n}} } & \infer[\text{prom.}]{!(A^\n \& B^\n) ⊢ !B^\n}{ \infer[\text{der.}]{!(A^\n \& B^\n) ⊢ B^\n}{ \infer{A^\n \& B^\n ⊢ B^\n}{B^\n ⊢ B^\n} } } } } } }

## Ex3: $(\bullet)^T$ and classical disjunction

The $(\bullet)^T$ translation allows to encode the rules associated with the classical disjunction:

\cfrac{Γ ⊢ A, B, Δ}{Γ ⊢ A ∨ B, Δ}∨ \text{R} \qquad \cfrac{Γ, A ⊢ Δ \qquad Γ' , B ⊢ Δ'}{Γ,Γ', A ∨ B ⊢ Δ, Δ'} ∨ \text{L}
\infer{?!Γ^T ⊢ ?(?A^T ⅋ ?B^T), ?Δ^T}{ \infer{?!Γ^T ⊢ ?A^T ⅋ ?B^T, ?Δ^T}{ ?!Γ^T ⊢ ?A^T, ?B^T, ?Δ^T } }

And:

\infer{?!Γ^T,?!Γ'^T, ?!(?A^T ⅋ ?B^T) ⊢ ?Δ^T, ?Δ'^T}{ & }

# 3. Exponential lattice

  digraph {
rankdir=BT;
"!" -> ".", "!?!";
"!?!" -> "!?", "?!";
"!?", "?!" -> "?!?" -> "?";
"." -> "?";
}


Difficult part: prove that these arrows are strict.

In order to prove $!?!A \not⊢ !A$, suppose the cut-elimination theorem, and then: proof by contradiction.

Tags:

Updated: