Comparison: ILL inside CLL

The Intuitionistic/ and Classical/ files develop the two logics in parallel. This chapter puts them side by side. It proves that every ILL proof is also a CLL proof, and that the converse fails.

Sequents

An ILL sequent Γ ⊢ C has exactly one conclusion. A CLL sequent Γ ⊢ Δ has a list of them. Every ILL rule fits the classical format with Δ a singleton, which is why the translation below goes through rule by rule. Several CLL rules need room for more than one conclusion and have no ILL counterpart:

     Γ ⊢ A,B,Δ           Γ ⊢ ?A,?A,Δ          Γ ⊢ A,Δ            A,Γ ⊢ Δ
    ------------ ⅋R     ------------- ?C    ----------- ^⊥L    ----------- ^⊥R
     Γ ⊢ A⅋B,Δ            Γ ⊢ ?A,Δ           A^⊥,Γ ⊢ Δ          Γ ⊢ A^⊥,Δ

⅋R and ?C have two conclusions in their premise. The negation rules move a formula across ⊢. Applied to a sequent with one conclusion, ^⊥L leaves none and ^⊥R makes two.

Connectives

ILL has 𝟙 ⊗ ⊸ ⊤ & 𝟘 ⊕ ! and a constant ⊥. CLL adds ⅋, ? and an involutive negation A^⊥, and defines A ⊸ B as A^⊥ ⅋ B. In ILL, ⊥ has no rules at all. It is an atom that every model must interpret. In CLL, ⊥ is the unit of ⅋, with rules ⊥L and ⊥R. ⊥R weakens the right-hand side: Γ ⊢ Δ gives Γ ⊢ ⊥, Δ.

Negation

ILL defines ∼A := A ⊸ ⊥. One direction of double negation holds, A ⊢ ∼∼A (Intuitionistic.Sequent.dni). The other, ∼∼A ⊢ A, does not (Intuitionistic.Phase.no_dne). CLL has a primitive negation A^⊥ with A^⊥^⊥ ⊣⊢ A. In CLL the defined A ⊸ ⊥ and the primitive A^⊥ are interderivable (neg_to_perp, perp_to_neg below), so ∼∼A ⊢ A becomes provable once ILL is read classically.

Semantics

In an intuitionistic phase space (Intuitionistic/Phase.v) the closure cl is a free parameter of the model, and ⊥ may be any fact. A classical phase space (Classical/Phase.v) fixes a pole ⫫ instead. The closure is forced to be X ↦ X^⊥⊥, and ⊥ denotes {ε}^⊥, which is the pole itself. The intuitionistic countermodel to ∼∼$0 ⊢ $0 takes ⊥ = ∅. Then ∼∼$0 contains every bag, so it is strictly bigger than $0. A classical model cannot do this, because there ∼∼X is X^⊥⊥ = X for every fact X.

Handling two calculi in one file

The two Sequent files use the same names (ax, cut, tensorR, ex_to, …) and the same notations (⊢, ⊗, …). We Require them without importing their names and refer to the rules through the module aliases I and C, as in I.ax and C.tensorR. Only the notations are imported. Inside a term, %ill and %cll select which reading of a notation is meant. cll_scope is opened last, so unannotated notations are classical.

From LinearLogic.Intuitionistic Require CutElim.[Loading ML file rocq-runtime.plugins.ring ... done]
[Loading ML file rocq-runtime.plugins.zify ... done]
[Loading ML file rocq-runtime.plugins.micromega_core ... done]
[Loading ML file rocq-runtime.plugins.micromega ... done]
[Loading ML file rocq-runtime.plugins.ssrmatching ... done]
[Loading ML file rocq-runtime.plugins.ssreflect ... done]
[Loading ML file rocq-runtime.plugins.btauto ... done]
[Loading ML file rocq-runtime.plugins.nsatz_core ... done]
[Loading ML file rocq-runtime.plugins.nsatz ... done]
From LinearLogic.Classical Require Sequent.
From LinearLogic.Intuitionistic Require Import Formula.
From LinearLogic.Classical Require Import Formula.

Module I := LinearLogic.Intuitionistic.Sequent.
Module IPhase := LinearLogic.Intuitionistic.Phase.
Module C := LinearLogic.Classical.Sequent.

Import (notations) I C.

Sanity checks: the same notation, read in either scope.

Check (λ A B : iformula, [A ⊗ B] ⊢ B ⊗ A)%ill.λ A B : iformula, ([A ⊗ B] ⊢ B ⊗ A)%ill
     : iformula → iformula → Prop
Check (λ A B : cformula, [A ⊗ B] ⊢ [B ⊗ A]).λ A B : cformula, [A ⊗ B] ⊢ [B ⊗ A]
     : cformula → cformula → Prop

The embedding

Each ILL connective goes to the CLL connective of the same name. Linear implication goes to the classical A ⊸ B, which unfolds to A^⊥ ⅋ B. So the image of ∼A = A ⊸ ⊥ is (embed A)^⊥ ⅋ ⊥.

Fixpoint embed (A : iformula) : cformula :=
  match A with
  | IAtom p => $p
  | IOne => 𝟙
  | IBot => ⊥
  | ITop => ⊤
  | IZero => 𝟘
  | ITensor A B => embed A ⊗ embed B
  | ILolli A B => embed A ⊸ embed B
  | IWith A B => embed A & embed B
  | IPlus A B => embed A ⊕ embed B
  | IBang A => !embed A
  end.

Embedding commutes with banging a whole context. ILL promotion needs this to become CLL promotion.

Lemma embed_bangs Σ : map embed (‼Σ)%ill = ‼(map embed Σ).Σ: list iformula
map embed (‼Σ)%ill = ‼map embed Σ
Proof.Σ: list iformula
map embed (‼Σ)%ill = ‼map embed Σ by rewrite !map_map. Qed.

Every ILL proof is a CLL proof

The proof is by induction on the ILL derivation. Each ILL rule is the CLL rule of the same name with a one-element conclusion list. Only the list shapes need adjusting:

two-premise multiplicative rules (cut, ⊗R, ⊸L) split the conclusions as Δ₁ ++ Δ₂. One of the two parts is [], so we rewrite [C] as [] ++ [C] or [A ⊗ B] as A ⊗ B :: [] ++ [];
ILL promotion ‼Σ ⊢ !A is CLL promotion ‼Σ ⊢ !A, ⁇Π with no ?-formulas, Π = [];
the ⊸ rules are the derived C.lolliR and C.lolliL.

The translation preserves cut-freeness: c is the same on both sides.

Theorem ill_to_cll c Γ A : (Γ ⊢[c] A)%ill -> map embed Γ ⊢[c] [embed A].c: bool
Γ: list iformula
A: iformula
(Γ ⊢[c] A)%ill → map embed Γ ⊢[c] [embed A]
Proof.c: bool
Γ: list iformula
A: iformula
(Γ ⊢[c] A)%ill → map embed Γ ⊢[c] [embed A]
  induction 1; cbn [map embed] in *; rewrite ?map_app.c: bool
A: iformula
[embed A] ⊢[c] [embed A]
c: bool
Γ, Δ: list iformula
A, C: iformula
H: c = true
H0: (Γ ⊢[c] A)%ill
H1: (A :: Δ ⊢[c] C)%ill
IHill1: map embed Γ ⊢[c] [embed A]
IHill2: embed A :: map embed Δ ⊢[c] [embed C]
map embed Γ ++ map embed Δ ⊢[c] [embed C]
c: bool
Γ, Γ': list iformula
C: iformula
H: Γ ≡ₚ Γ'
H0: (Γ ⊢[c] C)%ill
IHill: map embed Γ ⊢[c] [embed C]
map embed Γ' ⊢[c] [embed C]
c: bool
[] ⊢[c] [𝟙]
c: bool
Γ: list iformula
C: iformula
H: (Γ ⊢[c] C)%ill
IHill: map embed Γ ⊢[c] [embed C]
𝟙 :: map embed Γ ⊢[c] [embed C]
c: bool
Γ, Δ: list iformula
A, B: iformula
H: (Γ ⊢[c] A)%ill
H0: (Δ ⊢[c] B)%ill
IHill1: map embed Γ ⊢[c] [embed A]
IHill2: map embed Δ ⊢[c] [embed B]
map embed Γ ++ map embed Δ ⊢[c] [embed A ⊗ embed B]
c: bool
Γ: list iformula
A, B, C: iformula
H: (A :: B :: Γ ⊢[c] C)%ill
IHill: embed A :: embed B :: map embed Γ ⊢[c] [embed C]
embed A ⊗ embed B :: map embed Γ ⊢[c] [embed C]
c: bool
Γ: list iformula
A, B: iformula
H: (A :: Γ ⊢[c] B)%ill
IHill: embed A :: map embed Γ ⊢[c] [embed B]
map embed Γ ⊢[c] [embed A ⊸ embed B]
c: bool
Γ, Δ: list iformula
A, B, C: iformula
H: (Γ ⊢[c] A)%ill
H0: (B :: Δ ⊢[c] C)%ill
IHill1: map embed Γ ⊢[c] [embed A]
IHill2: embed B :: map embed Δ ⊢[c] [embed C]
embed A ⊸ embed B :: map embed Γ ++ map embed Δ ⊢[c] [embed C]
c: bool
Γ: list iformula
A, B: iformula
H: (Γ ⊢[c] A)%ill
H0: (Γ ⊢[c] B)%ill
IHill1: map embed Γ ⊢[c] [embed A]
IHill2: map embed Γ ⊢[c] [embed B]
map embed Γ ⊢[c] [embed A & embed B]
c: bool
Γ: list iformula
A, B, C: iformula
H: (A :: Γ ⊢[c] C)%ill
IHill: embed A :: map embed Γ ⊢[c] [embed C]
embed A & embed B :: map embed Γ ⊢[c] [embed C]
c: bool
Γ: list iformula
A, B, C: iformula
H: (B :: Γ ⊢[c] C)%ill
IHill: embed B :: map embed Γ ⊢[c] [embed C]
embed A & embed B :: map embed Γ ⊢[c] [embed C]
c: bool
Γ: list iformula
map embed Γ ⊢[c] [⊤]
c: bool
Γ: list iformula
A, B: iformula
H: (Γ ⊢[c] A)%ill
IHill: map embed Γ ⊢[c] [embed A]
map embed Γ ⊢[c] [embed A ⊕ embed B]
c: bool
Γ: list iformula
A, B: iformula
H: (Γ ⊢[c] B)%ill
IHill: map embed Γ ⊢[c] [embed B]
map embed Γ ⊢[c] [embed A ⊕ embed B]
c: bool
Γ: list iformula
A, B, C: iformula
H: (A :: Γ ⊢[c] C)%ill
H0: (B :: Γ ⊢[c] C)%ill
IHill1: embed A :: map embed Γ ⊢[c] [embed C]
IHill2: embed B :: map embed Γ ⊢[c] [embed C]
embed A ⊕ embed B :: map embed Γ ⊢[c] [embed C]
c: bool
Γ: list iformula
C: iformula
𝟘 :: map embed Γ ⊢[c] [embed C]
c: bool
Σ: list iformula
A: iformula
H: (‼Σ ⊢[c] A)%ill
IHill: map embed (‼Σ)%ill ⊢[c] [embed A]
map embed (‼Σ)%ill ⊢[c] [!embed A]
c: bool
Γ: list iformula
A, C: iformula
H: (A :: Γ ⊢[c] C)%ill
IHill: embed A :: map embed Γ ⊢[c] [embed C]
!embed A :: map embed Γ ⊢[c] [embed C]
c: bool
Γ: list iformula
A, C: iformula
H: (Γ ⊢[c] C)%ill
IHill: map embed Γ ⊢[c] [embed C]
!embed A :: map embed Γ ⊢[c] [embed C]
c: bool
Γ: list iformula
A, C: iformula
H: (!A :: !A :: Γ ⊢[c] C)%ill
IHill: !embed A :: !embed A :: map embed Γ ⊢[c] [embed C]
!embed A :: map embed Γ ⊢[c] [embed C]
  - (* ax *)c: bool
A: iformula
[embed A] ⊢[c] [embed A] apply C.ax.
  - (* cut: the cut formula is the only conclusion of the left premise *)c: bool
Γ, Δ: list iformula
A, C: iformula
H: c = true
H0: (Γ ⊢[c] A)%ill
H1: (A :: Δ ⊢[c] C)%ill
IHill1: map embed Γ ⊢[c] [embed A]
IHill2: embed A :: map embed Δ ⊢[c] [embed C]
map embed Γ ++ map embed Δ ⊢[c] [embed C]
    change [embed C] with ([] ++ [embed C]).c: bool
Γ, Δ: list iformula
A, C: iformula
H: c = true
H0: (Γ ⊢[c] A)%ill
H1: (A :: Δ ⊢[c] C)%ill
IHill1: map embed Γ ⊢[c] [embed A]
IHill2: embed A :: map embed Δ ⊢[c] [embed C]
map embed Γ ++ map embed Δ ⊢[c] [] ++ [embed C] by eapply C.cut.
  - (* ex *)c: bool
Γ, Γ': list iformula
C: iformula
H: Γ ≡ₚ Γ'
H0: (Γ ⊢[c] C)%ill
IHill: map embed Γ ⊢[c] [embed C]
map embed Γ' ⊢[c] [embed C] eapply C.ex'; [done | by apply Permutation_map | done].
  - (* 𝟙R *)c: bool
[] ⊢[c] [𝟙] apply C.oneR.
  - (* 𝟙L *)c: bool
Γ: list iformula
C: iformula
H: (Γ ⊢[c] C)%ill
IHill: map embed Γ ⊢[c] [embed C]
𝟙 :: map embed Γ ⊢[c] [embed C] by apply C.oneL.
  - (* ⊗R *)c: bool
Γ, Δ: list iformula
A, B: iformula
H: (Γ ⊢[c] A)%ill
H0: (Δ ⊢[c] B)%ill
IHill1: map embed Γ ⊢[c] [embed A]
IHill2: map embed Δ ⊢[c] [embed B]
map embed Γ ++ map embed Δ ⊢[c] [embed A ⊗ embed B] change [embed A ⊗ embed B] with (embed A ⊗ embed B :: [] ++ []).c: bool
Γ, Δ: list iformula
A, B: iformula
H: (Γ ⊢[c] A)%ill
H0: (Δ ⊢[c] B)%ill
IHill1: map embed Γ ⊢[c] [embed A]
IHill2: map embed Δ ⊢[c] [embed B]
map embed Γ ++ map embed Δ ⊢[c] embed A ⊗ embed B :: [] ++ []
    by apply C.tensorR.
  - (* ⊗L *)c: bool
Γ: list iformula
A, B, C: iformula
H: (A :: B :: Γ ⊢[c] C)%ill
IHill: embed A :: embed B :: map embed Γ ⊢[c] [embed C]
embed A ⊗ embed B :: map embed Γ ⊢[c] [embed C] by apply C.tensorL.
  - (* ⊸R *)c: bool
Γ: list iformula
A, B: iformula
H: (A :: Γ ⊢[c] B)%ill
IHill: embed A :: map embed Γ ⊢[c] [embed B]
map embed Γ ⊢[c] [embed A ⊸ embed B] by apply C.lolliR.
  - (* ⊸L *)c: bool
Γ, Δ: list iformula
A, B, C: iformula
H: (Γ ⊢[c] A)%ill
H0: (B :: Δ ⊢[c] C)%ill
IHill1: map embed Γ ⊢[c] [embed A]
IHill2: embed B :: map embed Δ ⊢[c] [embed C]
embed A ⊸ embed B :: map embed Γ ++ map embed Δ ⊢[c] [embed C] change [embed C] with ([] ++ [embed C]).c: bool
Γ, Δ: list iformula
A, B, C: iformula
H: (Γ ⊢[c] A)%ill
H0: (B :: Δ ⊢[c] C)%ill
IHill1: map embed Γ ⊢[c] [embed A]
IHill2: embed B :: map embed Δ ⊢[c] [embed C]
embed A ⊸ embed B :: map embed Γ ++ map embed Δ ⊢[c] [] ++ [embed C] by apply C.lolliL.
  - (* &R *)c: bool
Γ: list iformula
A, B: iformula
H: (Γ ⊢[c] A)%ill
H0: (Γ ⊢[c] B)%ill
IHill1: map embed Γ ⊢[c] [embed A]
IHill2: map embed Γ ⊢[c] [embed B]
map embed Γ ⊢[c] [embed A & embed B] by apply C.withR.
  - (* &L₁ *)c: bool
Γ: list iformula
A, B, C: iformula
H: (A :: Γ ⊢[c] C)%ill
IHill: embed A :: map embed Γ ⊢[c] [embed C]
embed A & embed B :: map embed Γ ⊢[c] [embed C] by apply C.withL1.
  - (* &L₂ *)c: bool
Γ: list iformula
A, B, C: iformula
H: (B :: Γ ⊢[c] C)%ill
IHill: embed B :: map embed Γ ⊢[c] [embed C]
embed A & embed B :: map embed Γ ⊢[c] [embed C] by apply C.withL2.
  - (* ⊤R *)c: bool
Γ: list iformula
map embed Γ ⊢[c] [⊤] apply C.topR.
  - (* ⊕R₁ *)c: bool
Γ: list iformula
A, B: iformula
H: (Γ ⊢[c] A)%ill
IHill: map embed Γ ⊢[c] [embed A]
map embed Γ ⊢[c] [embed A ⊕ embed B] by apply C.plusR1.
  - (* ⊕R₂ *)c: bool
Γ: list iformula
A, B: iformula
H: (Γ ⊢[c] B)%ill
IHill: map embed Γ ⊢[c] [embed B]
map embed Γ ⊢[c] [embed A ⊕ embed B] by apply C.plusR2.
  - (* ⊕L *)c: bool
Γ: list iformula
A, B, C: iformula
H: (A :: Γ ⊢[c] C)%ill
H0: (B :: Γ ⊢[c] C)%ill
IHill1: embed A :: map embed Γ ⊢[c] [embed C]
IHill2: embed B :: map embed Γ ⊢[c] [embed C]
embed A ⊕ embed B :: map embed Γ ⊢[c] [embed C] by apply C.plusL.
  - (* 𝟘L *)c: bool
Γ: list iformula
C: iformula
𝟘 :: map embed Γ ⊢[c] [embed C] apply C.zeroL.
  - (* !R: no ?-formulas on the right, Π = [] *)c: bool
Σ: list iformula
A: iformula
H: (‼Σ ⊢[c] A)%ill
IHill: map embed (‼Σ)%ill ⊢[c] [embed A]
map embed (‼Σ)%ill ⊢[c] [!embed A]
    rewrite embed_bangs in *.c: bool
Σ: list iformula
A: iformula
H: (‼Σ ⊢[c] A)%ill
IHill: ‼map embed Σ ⊢[c] [embed A]
‼map embed Σ ⊢[c] [!embed A] by apply (C.bangR _ _ []).
  - (* !D *)c: bool
Γ: list iformula
A, C: iformula
H: (A :: Γ ⊢[c] C)%ill
IHill: embed A :: map embed Γ ⊢[c] [embed C]
!embed A :: map embed Γ ⊢[c] [embed C] by apply C.bangD.
  - (* !W *)c: bool
Γ: list iformula
A, C: iformula
H: (Γ ⊢[c] C)%ill
IHill: map embed Γ ⊢[c] [embed C]
!embed A :: map embed Γ ⊢[c] [embed C] by apply C.bangW.
  - (* !C *)c: bool
Γ: list iformula
A, C: iformula
H: (!A :: !A :: Γ ⊢[c] C)%ill
IHill: !embed A :: !embed A :: map embed Γ ⊢[c] [embed C]
!embed A :: map embed Γ ⊢[c] [embed C] by apply C.bangC.
Qed.

Two negations agree classically

In CLL, the defined negation B ⊸ ⊥ = B^⊥ ⅋ ⊥ and the primitive B^⊥ prove each other. In one direction, ⅋L sends the ⊥ to a branch of its own, where ⊥L closes it. In the other direction, ⊥R adds a ⊥ to the conclusions.

Lemma neg_to_perp B : [B ⊸ ⊥] ⊢cf [B^⊥].B: cformula
[B ⊸ ⊥] ⊢cf [B^⊥]
Proof.B: cformula
[B ⊸ ⊥] ⊢cf [B^⊥]
  change [B ⊸ ⊥] with (B ⊸ ⊥ :: [] ++ []).B: cformula
B ⊸ ⊥ :: [] ++ [] ⊢cf [B^⊥] change [B^⊥] with ([B^⊥] ++ []).B: cformula
B ⊸ ⊥ :: [] ++ [] ⊢cf [B^⊥] ++ []
  apply C.parL; [apply C.ax | apply C.botL].
Qed.

Lemma perp_to_neg B : [B^⊥] ⊢cf [B ⊸ ⊥].B: cformula
[B^⊥] ⊢cf [B ⊸ ⊥]
Proof.B: cformula
[B^⊥] ⊢cf [B ⊸ ⊥] apply C.parR.B: cformula
[B^⊥] ⊢cf [B^⊥; ⊥] C.ex_to [B^⊥] [⊥; B^⊥].B: cformula
[B^⊥] ⊢cf [⊥; B^⊥] apply C.botR, C.ax. Qed.

Double-negation elimination, classically

The image of ∼∼A ⊢ A has a short cut-free CLL proof:

                   -------- ax
                    A ⊢ A
                  ---------- ⊥R
                   A ⊢ ⊥, A
                 ------------ ⊸R          ----- ⊥L
                  ⊢ A ⊸ ⊥, A               ⊥ ⊢
                 ------------------------------- ⊸L
                       (A ⊸ ⊥) ⊸ ⊥ ⊢ A

The left premise of ⊸L is the sequent ⊢ ∼A, A, which has two conclusions. It "proves ∼A" while keeping A in reserve. In ILL, ⊸L would need ⊢ ∼A alone, and that sequent is not provable.

Lemma classical_dne A : map embed [∼∼A]%ill ⊢cf [embed A].A: iformula
map embed [∼∼A] ⊢cf [embed A]
Proof.A: iformula
map embed [∼∼A] ⊢cf [embed A]
  cbn [map embed].A: iformula
[(embed A ⊸ ⊥) ⊸ ⊥] ⊢cf [embed A]
  change [_ ⊸ ⊥] with (((embed A ⊸ ⊥) ⊸ ⊥) :: [] ++ []).A: iformula
(embed A ⊸ ⊥) ⊸ ⊥ :: [] ++ [] ⊢cf [embed A]
  change [embed A] with ([embed A] ++ []).A: iformula
(embed A ⊸ ⊥) ⊸ ⊥ :: [] ++ [] ⊢cf [embed A] ++ []
  apply C.lolliL; [apply C.lolliR, C.botR, C.ax | apply C.botL].
Qed.

CLL is not conservative over ILL

So the embedding is not full. Some ILL sequents are unprovable but have a provable image. ∼∼$0 ⊢ $0 is one: ILL refutes it with a phase-space countermodel (IPhase.no_dne), and CLL proves it by classical_dne.

Theorem not_conservative :
  ∃ Γ A, ¬ (Γ ⊢ A)%ill ∧ map embed Γ ⊢ [embed A].∃ (Γ : list iformula) (A : iformula), ¬ (Γ ⊢ A)%ill ∧ map embed Γ ⊢ [embed A]
Proof.∃ (Γ : list iformula) (A : iformula), ¬ (Γ ⊢ A)%ill ∧ map embed Γ ⊢ [embed A]
  exists [∼∼$0]%ill, $0%ill.¬ ([∼∼$0] ⊢ $0)%ill ∧ map embed [∼∼$0] ⊢ [embed $0] split.¬ ([∼∼$0] ⊢ $0)%ill
map embed [∼∼$0] ⊢ [embed $0]
  -¬ ([∼∼$0] ⊢ $0)%ill apply IPhase.no_dne.
  -map embed [∼∼$0] ⊢ [embed $0] apply C.cf_to_full, classical_dne.
Qed.

What is known

The counterexample uses ⊥ essentially: ⊥R is the step that produced the two-conclusion sequent A ⊢ ⊥, A. Without ⊥ the situation is better. Schellinx (1991) showed that CLL is conservative over the fragment of ILL built from ⊗, ⊸, &, ⊕, ! and 𝟙: for sequents in this fragment, map embed Γ ⊢ [embed A] implies Γ ⊢ A. The proof starts from a cut-free CLL derivation, which by the subformula property only mentions images of ILL formulas, and reads it back as an ILL derivation. Extra conclusions do appear in it, for instance while ⊸R is decomposed into ⅋R and ^⊥R, but without ⊥ none of them can be used to prove something ILL cannot. We state this as a remark only; it is not formalized here.