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
\(X^{\rm n} \; ≝ \; X\\ (A ⇒ B)^{\rm n} \; ≝ \; !A^{\rm n} ⊸ B^{\rm n}\\ (A ∧ B)^{\rm n} \; ≝ \; A^{\rm n} \& B^{\rm n}\\ True^{\rm n} \; ≝ \; ⊤\\ (A ∨ B)^{\rm n} \; ≝ \; !A^{\rm n} ⊕ !B^{\rm n}\\ False^{\rm n} \; ≝ \; 0\\ (Γ ⊢ A)^{\rm n} \; ≝ \; !Γ^{\rm n} ⊢ A^{\rm n}\)	\(X^{\rm T} \; ≝ \; X\\ (A ⇒ B)^{\rm T} \; ≝ \; !?A^{\rm T} ⊸ ?B^{\rm T}\\ (A ∧ B)^{\rm T} \; ≝ \; ?A^{\rm T} \& ?B^{\rm T}\\ True^{\rm T} \; ≝ \; ⊤\\ (A ∨ B)^{\rm T} \; ≝ \; ?A^{\rm T} ⅋ ?B^{\rm T}\\ False^{\rm T} \; ≝ \; ⊥\\ (¬ A)^{\rm T} \; ≝ \; !?(A^{\rm T})^⊥\\ (Γ ⊢ Δ)^{\rm T} \; ≝ \; ?!Γ^{\rm T} ⊢ ?Δ^{\rm T}\)

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.