Home - 数学杂记

众所周知 Gentzen style 的 intuitionistic logic 中，structural rules 有三条：contraction、weakening、exchange。

而 substructural rules 就是限制了 structural rules 后的一些 intuitionistic logic 的变形。

譬如 Linear logic 就是禁止🙅‍了 contraction、weakening rules 后得到的。此时 conjunction ∧\wedge、disjunction ∨\vee 都会被分裂成两种，分别叫

  • multiplicative conjunction ∗*.
  • additive conjunction ∧\wedge.
  • multiplicative disjunction ++.
  • additive disjunction ∨\vee.

每一个 logic connective（包括 conjunction、disjunction、implication）都有 L、R 两个 inference rules。

# CLL system 以及 ILL

接下来我们介绍完整的 inference rules。实际上还可以引入

Classical Linear Logic System：注意，下述 A，B 不是 atomic 的，而是一个 formula：

A,B::=p\mid A+B\mid A*B\mid A\wedge B\mid A\vee B\mid A\imp B\mid A\rightarrow B\mid \bot\mid \top\mid\mathbf{0}\mid\mathbf{1}\mid !A\mid ?A

  • Axiom：

    A⊢AIdΓ⊢A,ΔΓ′,A⊢Δ′Γ′,Γ⊢Δ′,ΔCut\frac{}{A\vdash A}\text{Id}\hspace{3.0em}\frac{\Gamma\vdash A,\Delta\quad \Gamma',A\vdash \Delta'}{\Gamma',\Gamma\vdash \Delta',\Delta}\text{Cut}

  • Structural rules:

    Γ,A,A′,Γ′⊢BΓ,A′,A′,Γ′⊢BExchange\frac{\Gamma,A,A',\Gamma'\vdash B}{\Gamma,A',A',\Gamma'\vdash B}\text{Exchange}

  • Strong rules:

    这里我们两两给出，注意体会，conjunction 和 disjunction 关于 "⊢\vdash" 左右的对称。

    “∗*“和”++”：

    Γ,A,B⊢ΔΓ,A∗B⊢Δ*LΓ⊢A,ΔΓ′⊢B,Δ′Γ,Γ′⊢A∗B,Δ,Δ′*RΓ⊢A,B,ΔΓ⊢A+B,Δ+RΓ,A⊢ΔΓ′,B⊢Δ′Γ,Γ′,A+B⊢Δ,Δ′+L\frac{\Gamma,A,B\vdash \Delta}{\Gamma,A*B\vdash \Delta}\text{*L}\hspace{3.0em}\frac{\Gamma\vdash A,\Delta\quad\Gamma'\vdash B,\Delta'}{\Gamma,\Gamma'\vdash A*B,\Delta,\Delta'}\text{*R}\\ \frac{\Gamma\vdash A,B,\Delta}{\Gamma\vdash A+B,\Delta}\text{+R}\hspace{3.0em}\frac{\Gamma,A\vdash \Delta\quad\Gamma',B\vdash \Delta'}{\Gamma,\Gamma',A+B\vdash \Delta,\Delta'}\text{+L}

    不知道能不能看出来，*L\text{*L} 和+R\text{+R}、*R\text{*R} 和+L\text{+L} 就是将A,BA,B 从左侧移到了右侧！

    “∧\wedge “和”∨\vee”：

    Γ,A⊢ΔΓ,A∧B⊢Δ∧LΓ,B⊢ΔΓ,A∧B⊢Δ∧LΓ⊢A,ΔΓ⊢B,ΔΓ⊢A∧B,Δ∧RΓ⊢A,ΔΓ⊢A∨B,Δ∨RΓ⊢B,ΔΓ⊢A∨B,Δ∨RΓ,A⊢ΔΓ,B⊢ΔΓ,A∨B⊢Δ∨L\frac{\Gamma,A\vdash \Delta}{\Gamma,A\wedge B\vdash \Delta}\wedge\text{L}\hspace{3.0em}\frac{\Gamma,B\vdash \Delta}{\Gamma,A\wedge B\vdash \Delta}\wedge\text{L} \hspace{3.0em} \frac{\Gamma\vdash A,\Delta\quad\Gamma\vdash B,\Delta}{\Gamma\vdash A\wedge B,\Delta}\wedge\text{R}\\ \frac{\Gamma\vdash A,\Delta}{\Gamma\vdash A\vee B,\Delta}\vee\text{R}\hspace{3.0em} \frac{\Gamma\vdash B,\Delta}{\Gamma\vdash A\vee B,\Delta}\vee\text{R}\hspace{3.0em} \frac{\Gamma,A\vdash\Delta\quad\Gamma,B\vdash\Delta}{\Gamma,A\vee B\vdash\Delta}\vee\text{L}

    能看出来，∨R\vee\text{R} 和∧L\wedge\text{L}、∨L\vee \text{L} 和∧R\wedge \text{R} 也是将A,BA,B 从一侧移到另一侧！

    “implications”:

    Γ,A⊢BΓ⊢A− ⁣∘B− ⁣∘RΓ⊢A,ΔΓ′,B⊢Δ′Γ,Γ′,A− ⁣∘B⊢Δ,Δ′− ⁣∘L\newcommand\imp{\mathrel{-\mkern-3mu\circ}}\\ \frac{\Gamma,A\vdash B}{\Gamma\vdash A\imp B}\imp\text{R}\hspace{3.0em}\frac{\Gamma\vdash A,\Delta\quad\Gamma',B\vdash \Delta'}{\Gamma,\Gamma',A\imp B\vdash\Delta,\Delta'}\imp\text{L}

    Γ,A⊢ΔΓ⊢A→B,Δ→RΓ⊢B,ΔΓ⊢A→B,Δ→RΓ⊢A,ΔΓ,B⊢ΔΓ,A→B⊢Δ→L\frac{\Gamma,A\vdash\Delta}{\Gamma\vdash A\rightarrow B,\Delta}\rightarrow\text{R}\hspace{3.0em}\frac{\Gamma\vdash B,\Delta}{\Gamma\vdash A\rightarrow B,\Delta}\rightarrow\text{R}\hspace{3.0em} \frac{\Gamma\vdash A,\Delta\quad\Gamma,B\vdash\Delta}{\Gamma,A\rightarrow B\vdash\Delta}\rightarrow\text{L}

    以及我们可以引入+,∗,∧,∨+,*,\wedge,\vee 的单位元，分别是0,1,⊤,⊥\mathbf{0},\mathbf{1},\top,\bot：

    0⊢0LΓ⊢ΔΓ⊢Δ,00RΓ⊢ΔΓ,1⊢Δ1L⊢11R(no ⊤L)Γ⊢⊤,Δ⊤RΓ,⊥⊢Δ⊥L(no ⊥R)\frac{}{\mathbf{0}\vdash}\mathbf{0}\text{L}\hspace{3.0em}\frac{\Gamma\vdash\Delta}{\Gamma\vdash\Delta,\mathbf{0}}\mathbf{0}\text{R}\\ \frac{\Gamma\vdash \Delta}{\Gamma,\mathbf{1}\vdash \Delta}\mathbf{1}\text{L}\hspace{3.0em}\frac{}{\vdash\mathbf{1}}\mathbf{1}\text{R}\\ (\text{no }\top\text{L})\hspace{3.0em}\frac{}{\Gamma\vdash\top,\Delta}\top\text{R}\\ \frac{}{\Gamma,\bot\vdash\Delta}\bot\text{L}\hspace{3.0em}(\text{no }\bot\text{R})

    以及引入 storage 和 costorage：

    Γ⊢ΔΓ,!A⊢Δ!WΓ,!A,!A⊢ΔΓ,!A⊢Δ!CΓ,A⊢ΔΓ,!A⊢Δ!L!Γ⊢A,?Δ!Γ⊢!A,?Δ!RΓ⊢ΔΓ⊢?A,Δ?WΓ⊢?A,?A,ΔΓ⊢?A,Δ?CΓ⊢A,ΔΓ⊢?A,Δ?R!Γ,A⊢?Δ!Γ,?A⊢?Δ?L\frac{\Gamma\vdash\Delta}{\Gamma,!A\vdash\Delta}!\text{W}\hspace{3.0em} \frac{\Gamma,!A,!A\vdash\Delta}{\Gamma,!A\vdash\Delta}!\text{C}\hspace{3.0em} \frac{\Gamma,A\vdash\Delta}{\Gamma,!A\vdash\Delta}!\text{L}\hspace{3.0em} \frac{!\Gamma\vdash A,?\Delta}{!\Gamma\vdash !A,?\Delta}!\text{R}\\ \frac{\Gamma\vdash\Delta}{\Gamma\vdash?A,\Delta}?\text{W}\hspace{3.0em} \frac{\Gamma\vdash?A,?A,\Delta}{\Gamma\vdash?A,\Delta}?\text{C}\hspace{3.0em} \frac{\Gamma\vdash A,\Delta}{\Gamma\vdash ?A,\Delta}?\text{R}\hspace{3.0em} \frac{!\Gamma,A\vdash?\Delta}{!\Gamma,?A\vdash?\Delta}?\text{L}

    也可以看出?? 和!! 的左右对称性。

实际上，上述系统是有冗余的。譬如Cut\text{Cut} 这条规则就是可以证明不需要有的。此外，如果我们定义\sim A:=A\imp\mathbf{0}，你会发现

?A\equiv \sim!\sim A\equiv !(A\imp \mathbf{0})\imp\mathbf{0}

也就是说?? 实际上也是没必要的。但是为了可读性、证明复杂性等等，我们还是显式地引入说明。

Definition：Intuitionistic Linear Logic（ILL）就是限制 "⊢\vdash" 右侧只能有一个项（譬如Γ⊢A,Δ\Gamma\vdash A,\Delta 就是不合法的），并且去除关于+,?,0+,?,\mathbf{0} 后剩下的规则。

# IL 到 ILL 的 embedding

我们可以将 Intuitionistic Logic embed 到 ILL，譬如(⋅)(\cdot) 就是一个 embedding mapping：

\begin{aligned} & (p) && :=p\\ & (\bot) && :=\bot\\ & (\neg A) && :=!(A)\imp\bot\\ & (A\wedge B) && :=(A)\wedge (B)\\ & (A\vee B) && :=!(A)\vee !(B)\\ & (A\rightarrow B) && :=!(A)\imp (B)\\ \end{aligned}

Theorem: 如果在 IL 里有Γ⊢A\Gamma\vdash A，那么在 CLL 里就有!(Γ)⊢(A)!(\Gamma)\vdash (A)。

譬如 IL 里有p→q⊢¬p∨qp\rightarrow q\vdash \neg p\vee q，那么在 CLL 里就有!(!p\imp q)\vdash !(!p\imp\bot)\vee !q。

# Identity expansion & Cut Elimination

注意到，上述规则对于某个 connective，都是LL、RR 成对出现的。

而且上述规则定义的LL、RR 规则都是和谐的（L, R rules are in harmony）。

这个和谐体现在两方面：identity expansion 和 cut elimination，或者感性地理解，L 规则和 R 规则是平衡的。

接下来我们都以 "∧\wedge" 为例说明这件事。

  • Identity expansion：

    假如我们不允许A∧B⊢A∧B\frac{}{A\wedge B\vdash A\wedge B} 这个 identity 规则。但我们发现，它是可以用∧R,∧L\wedge R,\wedge L 推导出来的：

    A∧B⊢A∧B  ⟹  A⊢AA∧B⊢A(∧L)B⊢BA∧B⊢B(∧L)A∧B⊢A∧B(∧R)\frac{}{A\wedge B\vdash A\wedge B}\implies \frac{\frac{\frac{}{A\vdash A}}{A\wedge B\vdash A}(\wedge\text{L})\quad\frac{\frac{}{B\vdash B}}{A\wedge B\vdash B}(\wedge\text{L})}{A\wedge B\vdash A\wedge B}(\wedge\text{R})

    而其中只用到了对于A,BA,B 的 identity 规则。这就叫 identity expansion。

    这其实说明，我们只需要关于 atomic proposition 的 identity 规则就行了。其余的都可以推导出来。

  • Cut elimination:

    假如我们不允许Γ⊢A∧B,ΔΓ′,A∧B⊢Δ′Γ,Γ′⊢Δ,Δ′\frac{\Gamma\vdash A\wedge B,\Delta\quad \Gamma',A\wedge B\vdash \Delta'}{\Gamma,\Gamma'\vdash\Delta,\Delta'} 这条规则直接把 "A∧BA\wedge B" 当作一个整体给 cut 掉。同样我们可以:

    Γ⊢A,ΔΓ⊢B,ΔΓ⊢A∧B,Δ(∧R)Γ′,A⊢Δ′Γ′,A∧B⊢Δ′(∧L)Γ,Γ′⊢Δ,Δ′  ⟹  Γ⊢A,ΔΓ′,A⊢Δ′Γ,Γ′⊢Δ,Δ′\frac{\frac{\Gamma\vdash A,\Delta\quad\Gamma\vdash B,\Delta}{\Gamma\vdash A\wedge B,\Delta}(\wedge\text{R})\quad\frac{\Gamma',A\vdash \Delta'}{\Gamma',A\wedge B\vdash \Delta'}(\wedge\text{L})}{\Gamma,\Gamma'\vdash\Delta,\Delta'}\implies \frac{\Gamma\vdash A,\Delta\quad\Gamma',A\vdash \Delta'}{\Gamma,\Gamma'\vdash \Delta,\Delta'}

    直接转换为对AA 的 cut，也可以得到相同的结果。

一对和谐合理的 L、R 规则必须通过 identity expansion 和 cut elimination。但是反之却不一定，有可能 rules 太过强了。

接下来我们看一个反例。假如说，有一个 connective，譬如叫 “∘\circ”，它有∧L\wedge L 和∗R*R：

Γ,A⊢ΔΓ,A∘B⊢Δ∘LΓ,B⊢ΔΓ,A∘B⊢Δ∘LΓ⊢A,ΔΓ′⊢B,Δ′Γ,Γ′⊢A∘B,Δ,Δ′∘R\frac{\Gamma,A\vdash\Delta}{\Gamma,A\circ B\vdash \Delta}\circ L\hspace{3.0em} \frac{\Gamma,B\vdash\Delta}{\Gamma,A\circ B\vdash \Delta}\circ L\hspace{3.0em} \frac{\Gamma\vdash A,\Delta\quad\Gamma'\vdash B,\Delta'}{\Gamma,\Gamma'\vdash A\circ B,\Delta,\Delta'}\circ R

这会怎样？首先会发现 identity expansion、cut elimination 都会 fail！如下：

A⊢A???⊢BA⊢A∘B(∘R)A∘B⊢A∘B(∘L)Γ⊢A,ΔΓ′⊢B,Δ′Γ,Γ′⊢A∘B,Δ,Δ′(∘R)Γ′′,A⊢Δ′′Γ′′,A∘B⊢Δ′′(∘L)Γ′′,Γ,Γ′⊢Δ′′,Δ,Δ′  ⟹  Γ⊢A,ΔΓ′′,A⊢Δ′′Γ′′,Γ⊢Δ′′,Δ\frac{\frac{\frac{}{A\vdash A}\quad \frac{???}{\vdash B}}{A\vdash A\circ B}(\circ R)}{A\circ B\vdash A\circ B}(\circ L)\hspace{3.0em} \frac{\frac{\Gamma\vdash A,\Delta\quad\Gamma'\vdash B,\Delta'}{\Gamma,\Gamma'\vdash A\circ B,\Delta,\Delta'}(\circ R)\quad \frac{\Gamma'',A\vdash\Delta''}{\Gamma'',A\circ B\vdash \Delta''}(\circ L)}{\Gamma'',\Gamma,\Gamma'\vdash \Delta'',\Delta,\Delta'}\implies\frac{\Gamma\vdash A,\Delta\quad\Gamma'',A\vdash \Delta''}{\Gamma'',\Gamma\vdash \Delta'',\Delta}

这意味着什么？假设我们允许下面两条规则：

A∘B⊢A∘B∘IdΓ,A∘B⊢ΔΓ′⊢A∘B,Δ′Γ,Γ′⊢Δ,Δ′∘Cut\frac{}{A\circ B\vdash A\circ B}\circ\text{Id}\hspace{3.0em}\frac{\Gamma,A\circ B\vdash \Delta\quad \Gamma'\vdash A\circ B,\Delta'}{\Gamma,\Gamma'\vdash \Delta,\Delta'}\circ\text{Cut}

那么会怎样？答：会导致 weakening 这条 structural rules 被推导出来！也就是说，一个 connective 的 L、R 规则不和谐，会对全局的 structural rules 有影响！

Γ⊢AB⊢BΓ,B⊢A∘B(∘R)A⊢AA∘B⊢A(∘L)Γ,B⊢A(∘Cut)\frac{\frac{\Gamma\vdash A\quad\frac{}{B\vdash B}}{\Gamma,B\vdash A\circ B}(\circ R)\quad\frac{\frac{}{A\vdash A}}{A\circ B\vdash A}(\circ L)}{\Gamma,B\vdash A}(\circ \text{Cut})

也就是我们用Γ⊢A\Gamma\vdash A 推导出了Γ,B⊢A\Gamma,B\vdash A，这原本应该是不允许的！

# Algebra & Semantics

Definition

\mathcal{X}:=(X,\wedge,\vee,\bot,\imp,*,\mathbf{1}) is an IL-algebra (Intuitionistic Linear algebra) if:

  • (X,∧,∨,⊥)(X,\wedge,\vee,\bot) is a lattice with bottom ⊥\bot.
  • (X,∗,1)(X,*,\mathbf{1}) is a commutative monoid with unit 1\mathbf{1}.
  • if x≤x′,y≤y′x\leq x',y\leq y' then x∗y≤x′∗y′x*y\leq x'*y' and x'\imp y\leq x\imp y'.
  • x∗y≤zx*y\leq z if and only if x\leq y\imp z.

An IL-algebra is a CL-algebra (Classical Linear algebra) if:

  • there is an element 0∈X\mathbf{0}\in X and x=(x\imp\mathbf{0})\imp\mathbf{0} for all x∈Xx\in X.

此外我们称一个 ©IL-algebra 是 complete 也就是称XX 是一个 complete lattice。

Lemma：在一个 IL-algebra 中：

  • x∗⋁iyi=⋁i(x∗yi)x*\bigvee_i y_i=\bigvee_i(x*y_i).
  • x\imp(y\imp z)=x*y\imp z.
  • \bot\imp\bot is the top of XX.

在一个 CL-algebra 中，如果记\sim X:=X\imp\mathbf{0}，那么：

  • x∨y=∼(∼x∨∼y)x\vee y=\sim(\sim x\vee\sim y).
  • x\imp y=\sim(x*\sim y).

那么对于任意一个 IL-algebra 的实例XX，加上一个 assignment function [∣⋅∣][|\cdot|]，都形成一个 model。

[∣p∣]=x∈X[∣⊥∣]=⊥[∣1∣]=1[∣A⋈B∣]:=[∣A∣]⋈[∣B∣],⋈∈{∗,+,∧,∨}[∣∅∣]=1[∣Γ=A1,...,An∣]=[∣A1∣]∗...∗[∣An∣]\begin{aligned} &\left [|p|\right ]=x\in X\\ & [|\bot|]=\bot\\ & [|\mathbf{1}|]=\mathbf{1}\\ & \left [|A\bowtie B|\right ]:=\left [| A\right |]\bowtie\left [| B\right |],\bowtie\in\{*,+,\wedge,\vee\}\\ & [|\emptyset|]=\mathbf{1}\\ &[|\Gamma=A_1,...,A_n|]=[|A_1|]*...*[|A_n|] \end{aligned}

那么对于任意一个 model，soundness，completeness 就要求了

Γ⊢A if and only if [∣Γ∣]≤[∣A∣]\Gamma\vdash A\text{ if and only if }[|\Gamma|]\leq [|A|]

注意我们这讨论 ILL 右侧只有一个 formula。如果右侧也有很多的话，其实是：

A1,...,An⊢B1,...,Bm  ⟺  [∣A1∣]∗...∗[∣An∣]≤[∣B1∣]+...+[∣Bn∣]A_1,...,A_n\vdash B_1,...,B_m\iff[|A_1|]*...*[|A_n|]\leq [|B_1|]+...+[|B_n|]

举个例子，譬如考虑在ZN\mathbb{Z}_N 上，有：

\begin{aligned} & [|\sim A|]:=N-[|A|]\\ & [|A*B|]:=[|A|]+[|B|]-N\\ & [|A+B|]:=[|A|]+[|B|]\\ & [|A\vee B|]:=\max([|A|],[|B|])\\ & [|A\wedge B|]:=\min([|A|],[|B|])\\ & [|A\imp B|]:=N-[|A|]+[|B|]\\ & [|\mathbf{0}|]:=0\\ & [|\mathbf{1}|]:=N \end{aligned}

那么我们发现，之前的 inference rules system 都是自洽的。譬如我们 check 一条，例如∘L\circ L：

\frac{\Gamma\vdash A\quad\Gamma',B\vdash \Delta}{\Gamma,\Gamma',A\imp B\vdash\Delta}\imp\text{L}

对应的就是：

[∣Γ∣]≤A[∣Γ′∣]+[∣B∣]−N≤[∣Δ∣][∣Γ∣]+[∣Γ′∣]+(N−[∣A∣]+[∣B∣])−2N≤[∣Δ∣]\frac{[|\Gamma|]\leq A\quad [|\Gamma'|]+[|B|]-N\leq [|\Delta|]}{[|\Gamma|]+[|\Gamma'|]+(N-[|A|]+[|B|])-2N\leq [|\Delta|]}

这是显然成立的。

# Categorical semantics

其实 symmetric monoidal closed category 就是一个满足 IL-algebra 要求的结构。

特别是 closed 要求−⊗b-\otimes b 一定有 adjoint functor b\imp - 就特别像 Heyting algebra 的要求。

… 挖坑待补