Girard's translation into linear logic

TheoremAdding a why-not proposition keeps a sequent all why-not#✓fully proved

For every CLL proposition \(a\) and every CLL sequent \(\Delta\), every proposition of the sequent \(?a, \Delta\) has the form \(?b\) for some \(b\) if and only if every proposition of \(\Delta\) does.

theorem Sequent.allQuest_cons_quest {Atom : Type*} (a : Proposition Atom) (Δ : Sequent Atom) :
    Sequent.allQuest (.quest a ::ₘ Δ) = Sequent.allQuest Δ

Used by 1

Used byPromotion in a translated hypothesis context

DefinitionGirard's translation#✓fully proved

Given a map \(f\) from propositional atoms to CLL propositions, the translation \(A \mapsto A^\circ\) of propositional formulas into CLL is defined by recursion: \(a^\circ = f(a)\) for an atom \(a\), \((A \wedge B)^\circ = A^\circ \mathbin{\&} B^\circ\), \((A \vee B)^\circ = {!A^\circ} \oplus {!B^\circ}\), and \((A \to B)^\circ\) is the multiplicative disjunction (par) of \(?\big((A^\circ)^\perp\big)\) and \(B^\circ\), that is, the linear implication \({!A^\circ} \multimap B^\circ\).

def translate (f : Atom → CLL.Proposition Atom') : PL.Proposition Atom → CLL.Proposition Atom'
  | .atom a => f a
  | .and A B => .with (translate f A) (translate f B)
  | .or A B => .oplus (.bang (translate f A)) (.bang (translate f B))
  | .imp A B => .parr (.quest (translate f A)⫠) (translate f B)

Used by 11

Used byPromotion in a translated hypothesis context · Contraction of a translated hypothesis context · Girard's translation preserves provability · Ex falso translates to a CLL theorem · Girard's translation of a reusable hypothesis · Translated hypotheses are provable from their context · Theorems of intuitionistic logic translate to CLL theorems · Theorems of minimal logic translate to CLL theorems · Separating a new hypothesis in the translation · Girard's translation of an implication · Weakening by translated hypotheses

TheoremGirard's translation of an implication#✓fully proved

For every map \(f\) from propositional atoms to CLL propositions and all propositional formulas \(A\) and \(B\), \((A \to B)^\circ = {!A^\circ} \multimap B^\circ\), where \(C^\circ\) denotes Girard's translation of a formula \(C\) with atoms translated by \(f\) and \(\multimap\) is linear implication in CLL.

theorem translate_imp (f : Atom → CLL.Proposition Atom') (A B : PL.Proposition Atom) :
    translate f (.imp A B) = (.bang (translate f A) ⊸ translate f B)

Uses 1

Statement usesGirard's translation

DefinitionGirard's translation of a reusable hypothesis#✓fully proved

Given a map \(f\) from atoms to CLL propositions and a propositional formula \(A\), this is the CLL proposition \(?((A^\circ)^\perp)\), where \(A^\circ\) is Girard's translation of \(A\) with atoms translated by \(f\) and \((\cdot)^\perp\) is linear negation.

def hyp (f : Atom → CLL.Proposition Atom') (A : PL.Proposition Atom) : CLL.Proposition Atom' :=
  .quest (translate f A)⫠

Uses 1 · Used by 9

Statement usesGirard's translation

Used byPromotion in a translated hypothesis context · Contraction of a translated hypothesis context · Cut of a translated hypothesis context against a closed proof · Cut within a translated hypothesis context · Girard's translation preserves provability · Translated hypotheses are provable from their context · Translated hypotheses of a context · Separating a new hypothesis in the translation · Weakening by translated hypotheses

DefinitionTranslated hypotheses of a context#✓fully proved

Given a map \(f\) from propositional atoms to CLL propositions and a multiset \(\Gamma\) of propositional formulas, \(?\Gamma^{\circ\perp}\) is the CLL sequent consisting of the propositions \(?\big((A^\circ)^\perp\big)\) for \(A \in \Gamma\), counted with multiplicity, where \(A^\circ\) is Girard's translation of \(A\) with atoms translated by \(f\).

def hyps (f : Atom → CLL.Proposition Atom') (Γ : Multiset (PL.Proposition Atom)) :
    CLL.Sequent Atom' :=
  Γ.map (hyp f)

Uses 1 · Used by 10

Statement usesGirard's translation of a reusable hypothesis

Used byPromotion in a translated hypothesis context · Contraction of a translated hypothesis context · Cut of a translated hypothesis context against a closed proof · Cut within a translated hypothesis context · Girard's translation preserves provability · Translated hypotheses are provable from their context · Theorems of intuitionistic logic translate to CLL theorems · Theorems of minimal logic translate to CLL theorems · Separating a new hypothesis in the translation · Weakening by translated hypotheses

17 fully proved

Structural rules for ?-contexts

TheoremWeakening by translated hypotheses#✓fully proved

Let \(f\) map propositional atoms to CLL propositions. If a CLL sequent \(\vdash \Delta\) is provable, then for every multiset \(\Gamma\) of propositional formulas the sequent \(\vdash ?\Gamma^{\circ\perp}, \Delta\) is provable, where \(?\Gamma^{\circ\perp}\) is the multiset of the propositions \(?\big((A^\circ)^\perp\big)\) for \(A \in \Gamma\) and \(A^\circ\) is Girard's translation of \(A\) with atoms translated by \(f\).

theorem weaken_hyps {Δ : CLL.Sequent Atom'} (p : Derivable Δ)
    (Γ : Multiset (PL.Proposition Atom)) : Derivable (hyps f Γ + Δ)

Uses 3 · Used by 2

Statement usesTranslated hypotheses of a context

Proof usesGirard's translation of a reusable hypothesis · Girard's translation

Used byGirard's translation preserves provability · Translated hypotheses are provable from their context

TheoremContraction of a translated hypothesis context#✓fully proved

Let \(f\) map atoms to CLL propositions, let \(\Gamma\) be a multiset of propositional formulas, and write \(?\Gamma^{\circ\perp}\) for the CLL sequent of the propositions \(?((B^\circ)^\perp)\), one for each \(B \in \Gamma\) counted with multiplicity, where \(B^\circ\) is Girard's translation of \(B\) with atoms translated by \(f\). For every CLL sequent \(\Delta\), if \(\vdash ?\Gamma^{\circ\perp}, ?\Gamma^{\circ\perp}, \Delta\) is provable in CLL, then so is \(\vdash ?\Gamma^{\circ\perp}, \Delta\).

theorem contract_hyps {Δ : CLL.Sequent Atom'} (Γ : Multiset (PL.Proposition Atom))
    (p : Derivable (hyps f Γ + hyps f Γ + Δ)) : Derivable (hyps f Γ + Δ)

Uses 3 · Used by 1

Statement usesTranslated hypotheses of a context

Proof usesGirard's translation of a reusable hypothesis · Girard's translation

Used byCut within a translated hypothesis context

TheoremPromotion in a translated hypothesis context#✓fully proved

Let \(f\) map atoms to CLL propositions, let \(\Gamma\) be a multiset of propositional formulas, and write \(?\Gamma^{\circ\perp}\) for the CLL sequent of the propositions \(?((B^\circ)^\perp)\), one for each \(B \in \Gamma\) counted with multiplicity, where \(B^\circ\) is Girard's translation of \(B\) with atoms translated by \(f\). For every CLL proposition \(a\), if the sequent \(\vdash a, ?\Gamma^{\circ\perp}\) is provable in CLL, then so is \(\vdash !a, ?\Gamma^{\circ\perp}\).

theorem bang_hyps {Γ : Multiset (PL.Proposition Atom)} {a : CLL.Proposition Atom'}
    (p : Derivable (a ::ₘ hyps f Γ)) : Derivable (.bang a ::ₘ hyps f Γ)

Uses 4 · Used by 1

Statement usesTranslated hypotheses of a context

Proof usesGirard's translation of a reusable hypothesis · Girard's translation · Adding a why-not proposition keeps a sequent all why-not

Used byGirard's translation preserves provability

TheoremCut of a translated hypothesis context against a closed proof#✓fully proved

Let \(f\) map atoms to CLL propositions, let \(\Gamma\) be a multiset of propositional formulas, and write \(?\Gamma^{\circ\perp}\) for the CLL sequent of the propositions \(?((B^\circ)^\perp)\), one for each \(B \in \Gamma\) counted with multiplicity, where \(B^\circ\) is Girard's translation of \(B\) with atoms translated by \(f\). For all CLL propositions \(a\) and \(c\), if \(\vdash a, ?\Gamma^{\circ\perp}\) is provable in CLL and there is a CLL proof of \(\vdash a^\perp, c\), then \(\vdash c, ?\Gamma^{\circ\perp}\) is provable in CLL.

theorem cut_closed {Γ : Multiset (PL.Proposition Atom)} {a c : CLL.Proposition Atom'}
    (p : Derivable (a ::ₘ hyps f Γ)) (q : ⇓(a⫠ ::ₘ ({c} : CLL.Sequent Atom'))) :
    Derivable (c ::ₘ hyps f Γ)

Uses 2 · Used by 1

Statement usesTranslated hypotheses of a context

Proof usesGirard's translation of a reusable hypothesis

Used byGirard's translation preserves provability

TheoremCut within a translated hypothesis context#✓fully proved

Let \(f\) map atoms to CLL propositions, let \(\Gamma\) be a multiset of propositional formulas, and write \(?\Gamma^{\circ\perp}\) for the CLL sequent of the propositions \(?((B^\circ)^\perp)\), one for each \(B \in \Gamma\) counted with multiplicity, where \(B^\circ\) is Girard's translation of \(B\) with atoms translated by \(f\). For all CLL propositions \(a\) and \(c\), if both \(\vdash a, ?\Gamma^{\circ\perp}\) and \(\vdash a^\perp, c, ?\Gamma^{\circ\perp}\) are provable in CLL, then so is \(\vdash c, ?\Gamma^{\circ\perp}\).

theorem cut_hyps {Γ : Multiset (PL.Proposition Atom)} {a c : CLL.Proposition Atom'}
    (p : Derivable (a ::ₘ hyps f Γ)) (q : Derivable (a⫠ ::ₘ c ::ₘ hyps f Γ)) :
    Derivable (c ::ₘ hyps f Γ)

Uses 3 · Used by 1

Statement usesTranslated hypotheses of a context

Proof usesContraction of a translated hypothesis context · Girard's translation of a reusable hypothesis

Used byGirard's translation preserves provability

Translating derivations

TheoremTranslated hypotheses are provable from their context#✓fully proved

Let \(f\) map atoms to CLL propositions, let \(\Gamma\) be a multiset of propositional formulas, and write \(?\Gamma^{\circ\perp}\) for the CLL sequent of the propositions \(?((B^\circ)^\perp)\), one for each \(B \in \Gamma\) counted with multiplicity, where \(B^\circ\) is Girard's translation of \(B\) with atoms translated by \(f\). For every propositional formula \(A \in \Gamma\), the sequent \(\vdash A^\circ, ?\Gamma^{\circ\perp}\) is provable in CLL.

theorem hyp_mem {Γ : Multiset (PL.Proposition Atom)} {A : PL.Proposition Atom} (h : A ∈ Γ) :
    Derivable (translate f A ::ₘ hyps f Γ)

Uses 4 · Used by 1

Statement usesTranslated hypotheses of a context · Girard's translation

Proof usesGirard's translation of a reusable hypothesis · Weakening by translated hypotheses

Used byGirard's translation preserves provability

TheoremSeparating a new hypothesis in the translation#✓fully proved

Let \(f\) map propositional atoms to CLL propositions, let \(\Gamma\) be a finite set of propositional formulas, \(A\) a propositional formula and \(c\) a CLL proposition. Write \(B^\circ\) for Girard's translation of a formula \(B\) with atoms translated by \(f\), and \(?\Delta^{\circ\perp}\) for the multiset of the propositions \(?\big((B^\circ)^\perp\big)\) for \(B \in \Delta\). If the CLL sequent \(\vdash c, ?(\Gamma \cup \{A\})^{\circ\perp}\) is provable, then so is \(\vdash ?\big((A^\circ)^\perp\big), c, ?\Gamma^{\circ\perp}\).

When \(A \in \Gamma\) the conclusion follows by weakening.

theorem of_insert {Γ : Ctx Atom} {A : PL.Proposition Atom} {c : CLL.Proposition Atom'}
    (p : Derivable ((c ::ₘ hyps f (insert A Γ).val))) :
    Derivable (hyp f A ::ₘ c ::ₘ hyps f Γ.val)

Uses 3 · Used by 1

Statement usesGirard's translation of a reusable hypothesis · Translated hypotheses of a context

Proof usesGirard's translation

Used byGirard's translation preserves provability

TheoremGirard's translation preserves provability#✓fully proved

Let \(f\) map atoms to CLL propositions and write \(B^\circ\) for Girard's translation of a propositional formula \(B\) with atoms translated by \(f\). Let \(T\) be a propositional theory such that the one-formula sequent \(\vdash B^\circ\) is provable in CLL for every \(B \in T\). If \(\Gamma\) is a finite set of propositional formulas and \(\Gamma \vdash A\) has a natural-deduction derivation (in minimal propositional logic) using the axioms of \(T\), then the CLL sequent \(\vdash A^\circ, ?\Gamma^{\circ\perp}\) is provable, where \(?\Gamma^{\circ\perp}\) consists of the propositions \(?((B^\circ)^\perp)\), one for each \(B \in \Gamma\).

theorem derivable_of_derivation {T : Theory Atom}
    (hT : ∀ B ∈ T, Derivable ({translate f B} : CLL.Sequent Atom')) {Γ : Ctx Atom}
    {A : PL.Proposition Atom} (d : T.Derivation Γ A) :
    Derivable (translate f A ::ₘ hyps f Γ.val)

Uses 9 · Used by 2

Statement usesTranslated hypotheses of a context · Girard's translation

Proof usesPromotion in a translated hypothesis context · Cut of a translated hypothesis context against a closed proof · Cut within a translated hypothesis context · Girard's translation of a reusable hypothesis · Translated hypotheses are provable from their context · Separating a new hypothesis in the translation · Weakening by translated hypotheses

Used byTheorems of intuitionistic logic translate to CLL theorems · Theorems of minimal logic translate to CLL theorems

TheoremTheorems of minimal logic translate to CLL theorems#✓fully proved

For every map \(f\) from propositional atoms to CLL propositions, if a propositional formula \(A\) is derivable in natural deduction from the empty context with no axioms (minimal logic), then the one-sided CLL sequent \(\vdash A^\circ\) is provable, where \(A^\circ\) is Girard's translation of \(A\) with atoms translated by \(f\).

theorem mpl {A : PL.Proposition Atom} (d : (MPL Atom).Derivation ∅ A) :
    Derivable ({translate f A} : CLL.Sequent Atom')

Uses 3

Statement usesGirard's translation

Proof usesGirard's translation preserves provability · Translated hypotheses of a context

DefinitionThe atom map sending \(\bot\) to \(0\)#✓fully proved

For a type of atoms with a distinguished atom \(\bot\) and decidable equality, this is the map from atoms to CLL propositions that sends \(\bot\) to the additive unit \(0\) and every other atom \(a\) to the CLL atom \(a\).

def botToZero [Bot Atom] (a : Atom) : CLL.Proposition Atom :=
  if a = ⊥ then .zero else .atom a

TheoremEx falso translates to a CLL theorem#✓fully proved

Let \(f\) map atoms to CLL propositions and send the atom \(\bot\) to the additive unit \(0\). Then for every propositional formula \(B\), the one-formula CLL sequent \(\vdash (\bot \to B)^\circ\) is provable, where \((\cdot)^\circ\) is Girard's translation with atoms translated by \(f\).

The translation \((\bot \to B)^\circ\) is the par of \(?\top\) and \(B^\circ\), which is provable by the \(\top\) rule.

theorem efq [Bot Atom] (hf : f ⊥ = .zero) (B : PL.Proposition Atom) :
    Derivable ({translate f (.imp ⊥ B)} : CLL.Sequent Atom')

Uses 1 · Used by 1

Statement usesGirard's translation

Used byTheorems of intuitionistic logic translate to CLL theorems

TheoremTheorems of intuitionistic logic translate to CLL theorems#✓fully proved

Let \(f\) map propositional atoms to CLL propositions and send the atom \(\bot\) to the additive unit \(0\). If a propositional formula \(A\) is derivable in natural deduction from the empty context in intuitionistic propositional logic (no axioms other than ex falso \(\bot \to B\) for every formula \(B\)), then the one-sided CLL sequent \(\vdash A^\circ\) is provable, where \(A^\circ\) is Girard's translation of \(A\) with atoms translated by \(f\).

theorem ipl [Bot Atom] (hf : f ⊥ = .zero) {A : PL.Proposition Atom}
    (d : (IPL Atom).Derivation ∅ A) : Derivable ({translate f A} : CLL.Sequent Atom')

Uses 4

Statement usesGirard's translation

Proof usesGirard's translation preserves provability · Ex falso translates to a CLL theorem · Translated hypotheses of a context

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.