Exercise Sheet 1:

Teacher: Michele Pagani

Some MALL equivalences

\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 }             } }     } }

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

LJ into LL	LK into LL
$X^{n} ≝ X (A \Rightarrow B)^{n} ≝! A^{n} ⊸ B^{n} (A \land B)^{n} ≝ A^{n} & B^{n} T r u e^{n} ≝ ⊤ (A \lor B)^{n} ≝! A^{n} \oplus! B^{n} F a l s e^{n} ≝ 0 (Γ ⊢ A)^{n} ≝! Γ^{n} ⊢ A^{n}$	$X^{T} ≝ X (A \Rightarrow B)^{T} ≝! ? A^{T} ⊸ ? B^{T} (A \land B)^{T} ≝ ? A^{T} & ? B^{T} T r u e^{T} ≝ ⊤ (A \lor B)^{T} ≝ ? A^{T} ⅋ ? B^{T} F a l s e^{T} ≝ ⊥ (\neg A)^{T} ≝! ? (A^{T})^{⊥} (Γ ⊢ Δ)^{T} ≝ ?! Γ^{T} ⊢ ? Δ^{T}$

The $(∙)^{n}$ translation allows to encode the rules associated with the intuitionistic conjunction:

\frac{Γ ⊢ A Δ ⊢ B}{Γ, Δ ⊢ A \land B} \land R \frac{Γ, A ⊢ C}{Γ, A \land B ⊢ C} \land_{1} 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}                     }                 }             }         }     } }

The $(∙)^{T}$ translation allows to encode the rules associated with the classical disjunction:

\frac{Γ ⊢ A, B, Δ}{Γ ⊢ A \lor B, Δ} \lor R \frac{Γ, A ⊢ Δ Γ^{'}, B ⊢ Δ^{'}}{Γ, Γ^{'}, A \lor B ⊢ Δ, Δ^{'}} \lor 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}{ & }

Difficult part: prove that these arrows are strict.

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