Examples

Basic Properties

Multiplicatives

• A⊗B ⊢ B⊗A ≈ A⅋B ⊢ B⅋A (commutativity)
• (A⊗B)⊗C ⊢ A⊗(B⊗C) ≈ A⅋(B⅋C) ⊢ (A⅋B)⅋C (associativity)
• A⊗(B⊗C) ⊢ (A⊗B)⊗C ≈ (A⅋B)⅋C ⊢ A⅋(B⅋C) (associativity)
• A ⊢ A⊗1 ≈ A⅋⊥ ⊢ A (unit)
• A⊗1 ⊢ A ≈ A ⊢ A⅋⊥ (unit)
• (A⊸B)⊗C ⊢ A⊸(B⊗C) ≈ (A⅋B)⊗C ⊢ A⅋(B⊗C) (linear distributivity)
• A⊸A ≈ A^⊥⅋A (identity)
• A⊸B, B⊸C ⊢ A⊸C (composition)

Additives

• A&B ⊢ B&A ≈ A⊕B ⊢ B⊕A (commutativity)
• (A&B)&C ⊢ A&(B&C) ≈ A⊕(B⊕C) ⊢ (A⊕B)⊕C (associativity)
• A&(B&C) ⊢ (A&B)&C ≈ (A⊕B)⊕C ⊢ A⊕(B⊕C) (associativity)
• A ⊢ A&⊤ ≈ A⊕0 ⊢ A (unit)
• A&⊤ ⊢ A ≈ A ⊢ A⊕0 (unit)
• A ⊢ A&A ≈ A⊕A ⊢ A (idempotency)
• A&A ⊢ A ≈ A ⊢ A⊕A (idempotency)
• A ⊢ ⊤ ≈ 0 ⊢ A (terminal / initial)

Exponentials

• !A ⊢ A (dereliction)
• !A ⊢ !!A (digging)
• !A ⊢ !?!A
• !?!?A ⊢ !?A
• !?!A ⊢ !?A
• !?!A ⊢ ?!A

Multiplicative-Additive Interactions

• A⊗(B⊕C) ⊢ (A⊗B)⊕(A⊗C) (distributivity)
• (A⊗B)⊕(A⊗C) ⊢ A⊗(B⊕C) (distributivity)
• A⊗0 ⊢ 0 (absorption)
• 0 ⊢ A⊗0 (absorption)

Exponential-Multiplicative Interactions

• !A ⊢ !A⊗!A (contraction)
• !A ⊢ 1 (weakening)
• !A⊗!B ⊢ !(A⊗B) (monoidality)
• !1 ⊢ 1 (unit monoidality)

Exponential-Additive Interactions

• !A⊕!B ⊢ !(A⊕B)
• !(A&B) ⊢ !A&!B

Exponential-Multiplicative-Additive Interactions

• !(A&B) ⊢ !A⊗!B ≈ ?A⅋?B ⊢ ?(A⊕B) (exponential isomorphism)
• !A⊗!B ⊢ !(A&B) ≈ ?(A⊕B) ⊢ ?A⅋?B (exponential isomorphism)
• !⊤ ⊢ 1 ≈ ⊥ ⊢ ?0 (unit exponential isomorphism)
• 1 ⊢ !⊤ ≈ ?0 ⊢ ⊥ (unit exponential isomorphism)

Datatypes

Booleans

• A⊗A⊸A⊗A (multiplicative Booleans)
• 1⊕1 (additive Booleans)

Church Natural Numbers

• !(A⊸A)⊸!(A⊸A)

Binary Lists

• !(A⊸A)⊸!(A⊸A)⊸!(A⊸A)

Translations

Decorations

• A⊸!B⊸A (K combinator)
• (A⊸B⊸C)⊸(A⊸B)⊸!A⊸C (S combinator)
• ((A⊸?B)⊸A)⊸?A (Peirce's law)

Girard's Encodings

• !A⊸!B⊸A (K combinator)
• !(!A⊸!B⊸C)⊸!(!A⊸B)⊸!A⊸C (S combinator)
• !(!A⊸B), !(!B⊸C) ⊢ !A⊸C (composition)

Double Negation Translations

• A ⊢ (A⊸R)⊸R
• ((A⊸R)⊸R)⊸R ⊢ A⊸R
• ((A⊸R)⊸R)⊗((B⊸R)⊸R) ⊢ ((A⊗B)⊸R)⊸R
• ((A⊸R)⊸R)⊕((B⊸R)⊸R) ⊢ ((A⊕B)⊸R)⊸R

Intuitionistic vs. Classical Linear Provabilities

• (A⊸(0⊸B)⊸A')⊸((A⊸A')⊸0)⊸B' (Schellinx' formula)
• ((A⊸A')⊸0)⊸A⊗⊤ (Lafont's formula)
• ((((0⊸1)⊸1)⊸0)⊸0)⊸1 (Wu's formula)
• (((A⊗⊤)&(B⊗⊤))⊸0)⊸((A⊸A')⊕(B⊸B')) (Laurent's formula)

Miscellaneous

• A⊗(A⊸A) ⊢ A⊗!(A⊸A) (variant on Beffara's formula)
• !(A⅋B)⊸(?!?A⅋?!?B)
• ⊢ ?A, ?(B⅋B), ?(A^⊥⅋B^⊥), ?(⊥⊗⊥) (lcm of 1 and 2)