Classical Linear Logic

TODO

• First-order polymorphism.
• Logical equivalences.
• Cut elimination.

References

• [J.-Y. Girard, Linear Logic: its syntax and semantics] [Gir95]

inductive CLL.Proposition {Atom : Type u} : Type u

Propositions.

• atom {Atom : Type u} (x : Atom) : Proposition
• atomDual {Atom : Type u} (x : Atom) : Proposition
• one {Atom : Type u} : Proposition
• zero {Atom : Type u} : Proposition
• top {Atom : Type u} : Proposition
• bot {Atom : Type u} : Proposition
• tensor {Atom : Type u} (a b : Proposition) : Proposition
• parr {Atom : Type u} (a b : Proposition) : Proposition
• oplus {Atom : Type u} (a b : Proposition) : Proposition
• with {Atom : Type u} (a b : Proposition) : Proposition
• bang {Atom : Type u} (a : Proposition) : Proposition
• quest {Atom : Type u} (a : Proposition) : Proposition

instance CLL.instDecidableEqProposition {Atom✝ : Type u_1} [DecidableEq Atom✝] : DecidableEq Proposition

Equations

• CLL.instDecidableEqProposition = CLL.decEqProposition✝

instance CLL.instBEqProposition {Atom✝ : Type u_1} [BEq Atom✝] : BEq Proposition

Equations

• CLL.instBEqProposition = { beq := CLL.beqProposition✝ }

def CLL.Proposition.Pos {Atom : Type u} (a : Proposition) : Prop

Positive propositions.

Equations

• (CLL.Proposition.atom x).Pos = True
• CLL.Proposition.one.Pos = True
• CLL.Proposition.zero.Pos = True
• (a_2.tensor b).Pos = True
• (a_2.oplus b).Pos = True
• a_2.bang.Pos = True
• a.Pos = False

def CLL.Proposition.Neg {Atom : Type u} (a : Proposition) : Prop

Negative propositions.

Equations

• (CLL.Proposition.atomDual x).Neg = True
• CLL.Proposition.bot.Neg = True
• CLL.Proposition.top.Neg = True
• (a_2.parr b).Neg = True
• (a_2.with b).Neg = True
• a_2.quest.Neg = True
• a.Neg = False

instance CLL.Proposition.pos_decidable {Atom : Type u} (a : Proposition) : Decidable a.Pos

Whether a Proposition is positive is decidable.

Equations

• One or more equations did not get rendered due to their size.

instance CLL.Proposition.neg_decidable {Atom : Type u} (a : Proposition) : Decidable a.Neg

Whether a Proposition is negative is decidable.

Equations

• One or more equations did not get rendered due to their size.

def CLL.Proposition.dual {Atom : Type u} (a : Proposition) : Proposition

Propositional duality.

Equations

• (CLL.Proposition.atom x).dual = CLL.Proposition.atomDual x
• (CLL.Proposition.atomDual x).dual = CLL.Proposition.atom x
• CLL.Proposition.one.dual = CLL.Proposition.bot
• CLL.Proposition.bot.dual = CLL.Proposition.one
• CLL.Proposition.zero.dual = CLL.Proposition.top
• CLL.Proposition.top.dual = CLL.Proposition.zero
• (a_2.tensor b).dual = a_2.dual.parr b.dual
• (a_2.parr b).dual = a_2.dual.tensor b.dual
• (a_2.oplus b).dual = a_2.dual.with b.dual
• (a_2.with b).dual = a_2.dual.oplus b.dual
• a_2.bang.dual = a_2.dual.quest
• a_2.quest.dual = a_2.dual.bang

theorem CLL.Proposition.dual.neq {Atom : Type u} (a : Proposition) : a ≠ a.dual

No proposition is equal to its dual.

theorem CLL.Proposition.dual.eq_iff {Atom : Type u} (a b : Proposition) : a = b ↔ a.dual = b.dual

Two propositions are equal iff their respective duals are equal.

theorem CLL.Proposition.dual.involution {Atom : Type u} (a : Proposition) : a.dual.dual = a

Duality is an involution.

def CLL.Proposition.linImpl {Atom : Type u} (a b : Proposition) : Proposition

Linear implication.

Equations

• a.linImpl b = a.dual.parr b

@[reducible, inline]

abbrev CLL.Sequent {Atom : Type u} : Type u

A sequent in CLL is a list of propositions.

Equations

• CLL.Sequent = List CLL.Proposition

def CLL.Sequent.allQuest {Atom : Type u} (Γ : Sequent) : Prop

Checks that all propositions in Γ are question marks.

Equations

• Γ.allQuest = ∀ (a : CLL.Proposition), a ∈ Γ → ∃ (b : CLL.Proposition), a = b.quest

inductive CLL.Proof {Atom : Type u} : Sequent → Prop

Sequent calculus for CLL.

• ax {Atom : Type u} {a : Proposition} : Proof [a, a.dual]
• cut {Atom : Type u} {a : Proposition} {Γ Δ : List Proposition} : Proof (a :: Γ) → Proof (a.dual :: Δ) → Proof (Γ ++ Δ)
• exchange {Atom : Type u} {Γ Δ : List Proposition} : Γ.Perm Δ → Proof Γ → Proof Δ
• one {Atom : Type u} : Proof [Proposition.one]
• bot {Atom : Type u} {Γ : Sequent} : Proof Γ → Proof (Proposition.bot :: Γ)
• parr {Atom : Type u} {a b : Proposition} {Γ : List Proposition} : Proof (a :: b :: Γ) → Proof (a.parr b :: Γ)
• tensor {Atom : Type u} {a : Proposition} {Γ : List Proposition} {b : Proposition} {Δ : List Proposition} : Proof (a :: Γ) → Proof (b :: Δ) → Proof (a.tensor b :: (Γ ++ Δ))
• oplus₁ {Atom : Type u} {a : Proposition} {Γ : List Proposition} {b : Proposition} : Proof (a :: Γ) → Proof (a.oplus b :: Γ)
• oplus₂ {Atom : Type u} {b : Proposition} {Γ : List Proposition} {a : Proposition} : Proof (b :: Γ) → Proof (a.oplus b :: Γ)
• with {Atom : Type u} {a : Proposition} {Γ : List Proposition} {b : Proposition} : Proof (a :: Γ) → Proof (b :: Γ) → Proof (a.with b :: Γ)
• top {Atom : Type u} {Γ : List Proposition} : Proof (Proposition.top :: Γ)
• quest {Atom : Type u} {a : Proposition} {Γ : List Proposition} : Proof (a :: Γ) → Proof (a.quest :: Γ)
• weaken {Atom : Type u} {Γ : Sequent} {a : Proposition} : Proof Γ → Proof (a.quest :: Γ)
• contract {Atom : Type u} {a : Proposition} {Γ : List Proposition} : Proof (a.quest :: a.quest :: Γ) → Proof (a.quest :: Γ)
• bang {Atom : Type u} {Γ : Sequent} {a : Proposition} : Γ.allQuest → Proof (a :: Γ) → Proof (a.bang :: Γ)