LYNX

Links

Tags

Categories

数理逻辑复习

搬运自Fermat

Propositional Logic (PL)

语言

  • 字母表:命题符+联结词+辅助符
    • 命题符:$\text{PS}$ (propositional symbol):${P_n|n\in\mathbb{N}}$
  • 命题集 $\text{PROP}$ (proposition):为函数 $C_{\neg},C_{*}$ 下 $PS$ 的归纳闭包
    • $C_{\neg}(A)=(\neg A),C_{*}(A,B)=(A*B),*\in{\vee,\wedge,\rightarrow}$

定理

  • 括号引理:$A$为命题,则$A$中左右括号个数相等
  • 构造序列:$A\in PROP\iff \exists A_0,\cdots,A_n,n\in\mathbb{N},A=A_n$ 且对于任意的 $A_i,i\leq n$ 至少满足下列三条之一
    • $A_i\in PS$
    • $\exists k < i,A_i=A_k$
    • $\exists k,l < i, A_i=(A_k*A_l)$
  • 结构归纳:事实上是对$A$的构造长度作归纳,是自然数上的归纳
    • 数学归纳法:
      • Basis
      • I.H.
      • Ind. Step

语义

  • 真值集$B={T,F}$
    • $\neg:H_\neg:B\rightarrow B$
    • $*:H_{*}:B^2\rightarrow B$s
  • 赋值(模型):函数$v:\text{PS}\rightarrow B$
  • 命题的解释:函数$\hat v:\text{PROP}\rightarrow B$
    • $\hat v(P_n)=v(P_n),n\in \mathbb{N}$
    • $\hat v(\neg A)=H_\neg(\hat v(A))$
    • $\hat v(A*B)=H_\neg(\hat v(A),\hat v(B))$
    • $FV$(free variable):$FV(A)=${$P\in PS|P$出现在$A$中}
  • 满足:
    • $v\vDash \phi$(等价于$\hat v(A)=T$)
    • $v\vDash P\iff v(P)=T$
    • $v\vDash \neg \phi \iff v\not\vDash \phi$
    • $v\vDash \phi_1 \wedge/\vee \phi_2\iff v\vDash \phi_1 \text{and/or}\ \phi_2$
    • $v\vDash \phi_1 \rightarrow \phi_2\iff v\not\vDash\phi_1\ \text{or}\ v\vDash\phi_2$
    • tautology:$\vDash\phi\iff\forall v:v\vDash\phi$
    • 可满足:$\exists v,v\vDash A$
    • 语义结论:$\Gamma\subset PROP,\Gamma\vDash A\iff\forall v$有$\forall B\in\Gamma,\hat v(B)=T$则$\hat v(A)=T$

定理

  • $v\upharpoonright FV(A)$:$v$的限制

    • $v_1\upharpoonright FV(A)=v_2\upharpoonright FV(A)$则$\hat v_1(A)=\hat v_2(A)$
  • $n$元真值函数:$A\in \text{PROP}, FV(A)={Q_1,\cdots,Q_n},H_A:B^n\rightarrow B,\forall (a_1,\cdots,a_n)\in B^n, H_A(a_1,\cdots,a_n)=\hat v(A),v$满足$v(Q_i)=a_i(1\leq i\leq n)$.$H_A$为由$A$定义的真值函数

  • 析合范式($\vee\wedge-nf$):$A$呈形$\bigvee_{i=1}^m(\bigwedge_{k=1}^nP_{i,k}),P_{i,k}$为命题符或命题符之否定

    • $f:B^n\rightarrow B$,存在析合范式$A$,$f=H_A$
  • 合析范式($\wedge\vee-nf$):$A$呈形$\bigwedge_{j=1}^l(\bigvee_{k=1}^nQ_{j,k})$

    • $f:B^n\rightarrow B$,存在合析范式$A$,$f=H_A$
  • 求析合范式,合析范式

  • 逻辑等价:$A\simeq B$指$\forall v,v\vDash A$ iff $v\vDash B$

  • 任何命题均有逻辑等价的析合范式/合析范式

  • 联结词的函数完全组

    • $\{\neg,\wedge,\vee\},\{\neg,\wedge\},\{\neg,\vee\},\{\neg,\rightarrow\}$

语法

自然推理系统

  • sequent:二元组$(\Gamma,\Delta)$,记为$\Gamma\vdash\Delta$,$\Gamma,\Delta$为命题的有穷集合.$\Gamma$为前件,$\Delta$为后件

  • 公理:$\Gamma,A,\Delta\vdash\Lambda,A,\Theta$

  • 规则:

    • $\neg L:\dfrac{\Gamma,\Delta\vdash\Lambda,A}{\Gamma,\neg A,\Delta\vdash\Lambda}$
    • $\neg R$
    • $\vee L$
    • $\vee R$
    • $\wedge L$
    • $\wedge R$
    • $\rightarrow L: \dfrac{\Gamma,\Delta,\Gamma\ \Gamma,B,\Delta\vdash\Lambda}{\Gamma,A\rightarrow B,\Delta\Lambda}$
    • $\rightarrow R$
    • $Cut:\dfrac{\Gamma\vdash\Lambda,A\ \Delta,A\vdash\Theta}{\Gamma,\Delta\vdash\Lambda,\Theta}$
  • 反例:存在赋值$v$,$v\vDash(A_1\wedge\cdots\wedge A_m)\wedge(\neg B_1\wedge\cdots B_n)$,$v$反驳$\Gamma\vdash \Delta$

  • valid:$\forall v,v\vdash(A_1\wedge\cdots\wedge A_n)\rightarrow(B_1\vee\cdots\vee B_n)$,$v$满足$v\vdash\Delta$或$v\vDash\Delta$

  • soundness:$\Gamma\vdash\Delta\Rightarrow\Gamma\vDash\Delta$

  • completeness:$\Gamma\vDash\Delta\Rightarrow\Gamma\vdash\Delta$

  • compactness:$\Gamma$的任意有穷子集可满足则$\Gamma$可满足

命题逻辑的永真推理系统$H$

  • 公理模式

    • A1 : $A\rightarrow B$
    • A2 : $(A\rightarrow(B\rightarrow C))\rightarrow(B\rightarrow(A\rightarrow C))$
    • A3 : $(A\rightarrow B)\rightarrow((B\rightarrow C)\rightarrow(A\rightarrow C))$
    • A4 : $(A\rightarrow(A\rightarrow B))\rightarrow(A\rightarrow B)$
    • A5 : $(A\rightarrow\neg B)\rightarrow(B\rightarrow\neg A)$
    • A6 : $(\neg\neg A)\rightarrow A$
    • A7 : $(A\wedge B)\rightarrow A$
    • A8 : $(A\wedge B)\rightarrow B$
    • A9 : $A\rightarrow(B\rightarrow(A\wedge B))$
    • A10: $A\rightarrow(A\vee B)$
    • A11: $B\rightarrow(A\vee B)$
    • A12: $(A\rightarrow C)\rightarrow((B\rightarrow C)\rightarrow ((A\vee B)\rightarrow C))$
  • 定理

    • T13: $(A\rightarrow B)\rightarrow((C\rightarrow A)\rightarrow(C\rightarrow B))$
    • T14: $(A\rightarrow B)\rightarrow((D\rightarrow(C\rightarrow A))\rightarrow(D\rightarrow(C\rightarrow B)))$
    • T15: $\vdash A\rightarrow (B\rightarrow A)$
    • T16: $\vdash (A\rightarrow(B\rightarrow(A\wedge B)))\rightarrow(A\rightarrow(B\rightarrow A))$
    • T17: $\vdash (\neg A\rightarrow\neg B)\rightarrow(B\rightarrow A)$
    • T18: $\vdash A\rightarrow\neg\neg A$
    • T19: $\vdash (A\rightarrow B)\rightarrow(\neg B\rightarrow\neg A)$
    • T20: $\vdash A\vee\neg A$
    • T21: $A,\neg A\vdash\neg B$
    • T22: $A,\neg A\vdash B$
    • T23: $(B\rightarrow\neg B)\rightarrow\neg B$
    • T24: $\vdash(A\rightarrow (C\wedge\neg C))\rightarrow\neg A$
    • T25: $(B\vee A)\rightarrow(\neg A\rightarrow B)$
    • T26: $(A\rightarrow B)\rightarrow(B\vee\neg A)$
    • T27: $(A\vee B)\rightarrow(B\vee A)$
    • T28: $(A\rightarrow(B\rightarrow C))\rightarrow((A\wedge B)\rightarrow C)$
    • T29: $(C\vee A)\rightarrow((C\vee B)\rightarrow(C\vee(A\wedge B)))$
    • T30: $(C\vee A)\rightarrow((B\rightarrow C)\rightarrow((A\rightarrow B)\rightarrow C))$
    • T31: $(A\rightarrow(C\vee B))\rightarrow(C\vee(A\rightarrow B))$
  • 规则

    • MP:$\dfrac{A\rightarrow B\qquad A}{B}$
  • $\Gamma\vdash_H A$:$\exists P_1,\cdots,P_n=A,i\leq n$,$P_i$为$H$公理或$P_i\in\Gamma$或$\exists j,k < i,P_j=(P_k\rightarrow P_i)$即$P_i$由前$P_j$和$P_k$实施MP而得

    • $H$唯一确定,则$\Gamma\vdash A$或$\Gamma\rightarrow A$
    • 序列$P_1,\cdots,P_n$为证明过程,$n$为证明长度
    • $\text{Th}(\Gamma)={A|\Gamma\vdash A}, A\in\text{Th}$为$Gamma-$定理,$\vdash A$则$A$ 为定理
  • 引理

    • $\Gamma\vdash C\rightarrow(B\rightarrow A)$且$\Gamma\vdash C\rightarrow B$则$\Gamma\vdash C\rightarrow A$
  • 推理定理:$\Gamma,C\vdash A$则$\Gamma\vdash C\rightarrow A$

    • $\Gamma,C=\Gamma\cup{C}$
  • $G’$与$H$

    • $\vdash_H A\iff\vdash A$
    • $\Gamma\vdash\Delta$则$\Gamma\vdash\overline{\Delta}$
      • $\overline{\Delta}=\perp=(C\wedge\neg C)$if$\Delta=\emptyset$else$\bigvee_{i=1}^nB_i,\Delta={B_1,\cdots,B_n}$

First-Order-Logic

语言

  • 字母表

    • 逻辑符集合
      • 变元集$V$
      • 联结词,量词,等词,辅助词
    • 非逻辑符集合$\mathscr{L}$
      • 常元集合$\mathscr{L}_c$
      • 函数集合$\mathscr{L}_f$,$\mu(f) > 0$为$f$的元数
      • 谓词集合$\mathscr{L}_P$,$\mu(P)\ge0$为$f$的元数
  • 项$T$:变元符$\cup$常元符$\cup f(v_1,\cdots)$

    • 自由变元
      • $\text{FV}(x)={x}$,$\text{FV}(c)={x}$
      • $\text{FV}(f(t_1,\cdots))=\bigcup_{i=1}^n\text{FV}(t_i)$
    • 闭项:$\text{FV}(t)=\emptyset$
    • 替换:$s[\frac{t}{x}]$
  • 公式$\Psi$:${t_1\doteq t_2}\cup P(t_1,\cdots) \cup$公式在联结词,量词的组合

    • 自由变元
      • $\text{FV}(t_1\doteq t_2)=\text{FV}(t_1)\cup\text{FV}t_2$
      • $\text{FV}(P(t_1,\cdots))=\bigcup_{i=1}^n\text{FV}(t_i)$
      • 联结词取并
      • $\text{FV}(Qx.A)=FV(A)\backslash{x}$
    • 句子:$\text{FV}(A)=\emptyset$
    • 替换:$A[\frac{t}{x}]$
      • $(Qx.A)[\frac{t}{x}]=Qx.A$
      • $(Qy.A)[\frac{t}{x}]=Qy.(A[\frac{t}{x}]),y\not\in\text{FV}(t)$
      • $(Qy.A)[\frac{t}{x}]=Qz.(A[\frac{z}{y}][\frac{t}{x}]),y\in\text{FV}(t)$

语义

  • 结构:$\mathbb{M}=(M,I)$对$\mathscr{L}$做解释
    • 论域$M$为非空集
    • $I$为定义域为$\mathscr{L}$的映射
      • $c\in\mathscr{L}_c,c_{\mathbb{M}}=I(c)\in M$
      • $f\in\mathscr{L}_f,f_{\mathbb{M}}=I(f):M^n\rightarrow M$
      • $P\in\mathscr{L}_p,\mu(P) > 0,P_{\mathbb{M}}=I(P)\subseteq M^n$
      • $P\in\mathscr{L}_p,\mu(P)=0,I(P)\in B={T,F}$
  • 模型:$(\mathbb{M},\sigma)$是对一阶语言的解释
    • $\sigma:V\rightarrow M$为赋值
  • 解释
    • 项:$t_{\mathbb{M}[\sigma]}\in M$
      • $x_{\mathbb{M}[\sigma]}=\sigma(x)$
      • $c_{\mathbb{M}[\sigma]}=c_M$
      • $(f(t_1,\cdots))_{\mathbb{M}[\sigma]}=f_M((t_1)_{\mathbb{M}[\sigma]},\cdots)$
    • 公式:$A_{\mathbb{M}[\sigma]}\in{T,F}$
      • 排中律
      • 联结词:同古典逻辑
      • $(P(t_1,\cdots))_{\mathbb{M}[\sigma]}=T\iff \langle (t_1)_{\mathbb{M}[\sigma]},\cdots,\rangle\in P_M$
      • $(t_1\doteq t_2)_{\mathbb{M}[\sigma]}=T\iff (t_1)_{\mathbb{M}[\sigma]}=(t_2)_{\mathbb{M}[\sigma]}$
      • $(\forall x.A)_{\mathbb{M}[\sigma]}=T\iff$对所有$a\in M,A_\mathbb{M}[\sigma[x:=a]]=T$
      • $(\exists x.A)_{\mathbb{M}[\sigma]}=T\iff$对某个$a\in M,A_\mathbb{M}[\sigma[x:=a]]=T$
      • $(\sigma[x_i:=a])(x_j)=a\iff i=j$,otherwise$\sigma(x_j)$
  • 可满足:$A_{\mathbb{M}[\sigma]}=T,M\vDash_\sigma A$
    • $M\vDash A$
    • $M\vDash_\sigma \Gamma$
    • $\vDash A$, $\vDash \Gamma$
    • $\Gamma\vDash A$指$\forall (M,\sigma), M\vDash_\sigma\Gamma,$则$M\vDash_\sigma A$
    • $\Gamma\vDash A\iff\Gamma\cup{\neg A}$不可满足

Godel编码

  • $\langle a_0,\cdots,a_n\rangle=\prod_{i=0}^nP_i^{a_i}$
  • $\text{ep}:\mathbb{N}^2\rightarrow\mathbb{N}$为$x$的素因子分解式中$P_n$的幂次
  • Godel编码: #
    • Godel编码与语法对象一一对应

替换定理

  • $(t[\frac{s}{x}])_{\mathbb{M}[\sigma]}=t_{M[\sigma[x:=s_{\mathbb{M}[\sigma]}]]}$
  • $(A[\frac{t}{x}])_{\mathbb{M}[\sigma]}=A_M[\sigma[x:=t_{\mathbb{M}[\sigma]}]]$

Hintikka集

  • 公式集$\Psi$为Hintikka集指其满足以下19条
    • 2$\neg$,2$\rightarrow$,2$\wedge$,2$\vee$,(2$\leftrightarrow$),2$\exists$,2$\forall$,3$\doteq$,f,P
  • Hintikka集可满足
  • T上二元关系:$s\sim t\iff s\doteq t\iff [s]=[t]$

语法

自然推理系统

  • 公理:$\Gamma,A,\Delta\vdash\Lambda,A,\Theta$

  • 规则:

    • $\neg L:\dfrac{\Gamma,\Delta\vdash\Lambda,A}{\Gamma,\neg A,\Delta\vdash\Lambda}$
    • $\neg R$
    • $\vee L$
    • $\vee R$
    • $\wedge L$
    • $\wedge T$
    • $\rightarrow L: \dfrac{\Gamma,\Delta,\Gamma\quad\Gamma,B,\Delta\vdash\Lambda}{\Gamma,A\rightarrow B,\Delta\Lambda}$
    • $\rightarrow R$
    • $\forall L: \dfrac{\Gamma,A[t/x],\forall x A(x),\Delta\vdash\Lambda}{\Gamma,\forall xA(x),\Delta\vdash\Lambda}$
    • $\forall R: \dfrac{\Gamma\vdash,A[y/x],\Theta}{\Gamma\vdash\Lambda,\forall x A(x),\Theta}$,$y$为新变元
    • $\exists L:\dfrac{\Gamma,A[y/x],\Delta\vdash\Lambda}{\Gamma,\exists xA(x),\Delta\vdash\Gamma}$,$y$为新变元
    • $\exists R:\dfrac{\Gamma\vdash\Lambda,A[t/x],\exists xA(x),\Theta}{\Gamma\vdash\Lambda,\exists xA(x),\Theta}$
    • $\text{Cut}:\dfrac{\Gamma\vdash\Lambda,A\ \Delta,A\vdash\Theta}{\Gamma,\Delta\vdash\Lambda,\Theta}$
  • Cut规则可由其它规则导出

  • $\Gamma\vdash \Lambda$可证:存在证明树

  • $A_1,\cdots,A_m\vdash B_1,\cdots,B_n\iff \wedge_{i=1}^mA_i\vdash\wedge_{i=1}^nB_i$

  • $\Gamma\vdash\Delta\Rightarrow \Gamma,\Theta\vdash \Delta,\Psi$

  • 导出规则$(A(t)=A[\frac{t}{x}])$

    • 反证法:$\dfrac{\neg A,\Gamma\vdash B,\neg A,\Gamma\vdash\neg B}{\Gamma\vdash A}$
    • 分情况:$\dfrac{A,\Gamma\vdash B\qquad\neg A,\Gamma\vdash B}{\Gamma\vdash B}$
    • 逆否推演:$\dfrac{\Gamma\vdash A\rightarrow B}{\Gamma\vdash\neg B\rightarrow\neg A}$
    • 矛盾规则:$\dfrac{\Gamma\vdash A\qquad\Gamma\vdash\neg A}{\Gamma\vdash B}$
    • MP:$\dfrac{\Gamma\vdash A\qquad\Gamma\vdash A\rightarrow B}{\Gamma\vdash B}$
    • 三段论:$\dfrac{\Gamma\vdash A(t)\qquad\Gamma\vdash\forall x(A(x)\rightarrow B(x))}{\Gamma\vdash B(t)}$
  • $\Gamma\vdash\Delta$有效:$\vDash(\wedge_{i=1}^nA_i)\rightarrow(\vee_{j=1}^mB_j)$

    • ${}\vdash{}$非有效
    • 有反例即非有效
  • 除Cut外规则上矢列有效$\iff$下矢列有效

  • Soundness:$\Gamma\vdash\Delta$则$\Gamma\vDash\Delta$

完全性定理

  • $\Gamma$为公式集

  • $\text{Incon}(\Gamma)$矛盾指$\Delta\vdash$

    • $\iff\forall A$存在$\Gamma$有穷子集$\Delta,\Delta\vdash A$
  • $\text{Con}(\Gamma)$协调指$\Gamma$不矛盾

  • 极大协调

    • $\text{Con}(\Gamma)$
    • $\text{Con}(\Delta)$且$\Gamma\subseteq\Delta$则$\Gamma=\Delta$
    • 当且仅当
      • $\text{Con}(\Gamma)$
      • $(\forall A)\text{Con}(\Gamma\cup{A}),A\in\Gamma$
    • 当且仅当
      • $\text{Con}(\Gamma)$
      • $\forall A,A\in\Gamma\vee\neg A\in\Gamma$
    • 存在$\Gamma$有穷子集$\Delta\vdash A\iff A\in\Gamma$
  • 若$\Gamma$可满足,$\text{Con}(\Gamma)$;若$\text{Incon}(\Gamma)$,不可满足

  • $\Gamma\vdash A$,则$\text{Con}(\Gamma\cup{A})$;$G\vdash A$不可证,则$\text{Con}(\Gamma\cup {\neg A})$

  • Gentzen系统$Ge$为$G$加上以下三个等词公理

    • $\vdash s\doteq s$
    • $s_1\doteq t_1,\cdots,s_n\doteq t_n\vdash f(s_1,\cdots,s_n)\doteq f(t_1,\cdots,t_n)$
    • $s_1\doteq t_1,\cdots,s_n\doteq t_n, p(s_1,\cdots,s_n)\vdash p(t_1,\cdots,t_n)$
  • $Ge$中可证以下矢列

    • $\vdash(s\doteq t)\rightarrow(t\doteq s)$
    • $\vdash(s\doteq t)\rightarrow(t\doteq u\rightarrow s\doteq u)$
  • $\Gamma e$为以下句子集合

    • $\forall x(x\doteq x),\forall\vec x\forall\vec y(\vec x\dot=\vec y\rightarrow f(\vec x)\doteq f(\vec y))$,这里$f$为任何函数
    • $\forall\vec x\forall\vec y(\vec x\doteq\vec y\rightarrow(p(\vec x)\rightarrow p(\vec y)))$,这里$p$为任何谓词
    • 我们有$\Gamma\vdash\Delta$在$Ge$中可证$\iff\Gamma e,\Gamma\vdash\Delta$在$G$中可证
  • Henkin集

    • $\Gamma$极大协调
    • 若$\exists x.A\in\Gamma$,则有项$t$使$A[\frac{t}{x}]\in\Gamma$
  • $\text{Con}(\Phi)$,则存在$\mathscr{L’}=\mathscr{L}\cup{c_n|c\in N}$的公式集$\Psi$,使$\Psi\supseteq\Psi$且$\Psi$为$\mathscr{L’}$的Henkin集

  • Henkin集为Hintikka集

  • $\Gamma$协调则$\Gamma$可满足

  • Completeness:$\Gamma\vdash A\iff\Gamma\vDash A$

  • Compactness:若对任何$\Gamma$的有穷子集$\Delta$,$\Delta$可满足,则$\Gamma$可满足

一阶逻辑的永真推理系统$PK$

  • $A$ 的全称化:$\forall x_1\forall x_2\cdots\forall x_n.A$

    • $n=0$即为$A$
  • 公理

    • 第一组
      • A1:$A\rightarrow B$
      • A2:$(A\rightarrow(B\rightarrow C))\rightarrow(B\rightarrow(A\rightarrow C))$
      • A3:$(A\rightarrow B)\rightarrow((B\rightarrow C)\rightarrow(A\rightarrow C))$
      • A4:$(A\rightarrow(A\rightarrow B))\rightarrow(A\rightarrow B)$
      • A5:$(A\rightarrow\neg B)\rightarrow(B\rightarrow\neg A)$
      • A6:$(\neg\neg A)\rightarrow A$
      • A7:$(A\wedge B)\rightarrow A$
      • A8:$(A\wedge B)\rightarrow B$
      • A9:$A\rightarrow(B\rightarrow(A\wedge B))$
      • A10:$A\rightarrow(A\vee B)$
      • A11:$B\rightarrow(A\vee B)$
      • A12:$(A\rightarrow C)\rightarrow((B\rightarrow C)\rightarrow ((A\vee B)\rightarrow C))$
    • 第二组
      • A13:$\forall A\rightarrow A[\frac{t}{x}]$
      • A14:$A[\frac{t}{x}]\rightarrow\exists xA$
      • A15:$A\rightarrow\forall xA,x\not\in\text{FV}(A)$
      • A16:$\exists xA\rightarrow A,x\not\in\text{FV}(A)$
      • A17:$\forall(A\rightarrow B)\rightarrow(\forall xA\rightarrow\forall xB)$
      • A18:$\exists(A\rightarrow B)\rightarrow(\exists A\rightarrow\exists B)$
    • 第三组等词定理
      • A19:$x\dot=x$
      • A20:$(x_1\dot=y_1)\rightarrow\cdots((x_n\dot=y_n)\rightarrow(f(x_1,\cdots,x_n)\dot=f(y_1,\cdots,y_n))$
      • A21:$(x_1\dot=y_1)\rightarrow\cdots((x_n\dot=y_n)\rightarrow(P(x_1,\cdots,x_n)\dot=P(y_1,\cdots,y_n))$
    • 第四组:前面各组公理的全称化
  • 规则:MP:$\dfrac{A\rightarrow B\qquad A}{B}$

  • $\Gamma\vdash_{\text{PK}}A$指存在序列$A_1,\cdots,A_n=A$,$i\leq n$时满足以下任一条

    • $A_i$为公理
    • $A_i\in\Gamma$
    • $\exists j,k < i,A_j=(A_k\rightarrow A_i)$
  • 定理:$\Gamma,C\vdash A$则$\Gamma\vdash C\rightarrow A$

  • 泛化性定理:$x\not\in\text{FV}(\Gamma)$,若$\Gamma\vdash A$则$\Gamma\vdash\forall xA$

  • 上层定理

    • 常元$c$不在$\Gamma,A$中出现,若$\Gamma\vdash A[\frac{c}{x}]$则$\Gamma\vdash\forall xA$
    • 常元$c$不在$\Gamma,A,B$中出现且$x\not\in\text{FV}(B)$,若$\Gamma,A[\frac{c}{x}]\vdash B$则$\Gamma,\exists xA\vdash B$
    • $\vdash\forall x.A\leftrightarrow\neg\exists x\neg A$
    • $\vdash\exists x.A\leftrightarrow\neg\forall x\neg A$
  • $\vdash A$在$G$中可证$\iff A$在PK中可证

实例

初等算术语言$\mathcal{A}$

初等算术的标准模型

群论语言$\mathcal{B}$

集合论

Cantor集合论

  • 外延原则:$A=B\leftrightarrow\forall x(x\in A\rightarrow x\in B)$
  • 概括原则:$\forall P,\exists S, a\in S\rightarrow P(a),$记为$S={x|P(x)}$
  • Russell悖论:$P(x)=x\not\in x$

公理集合论

  • 集合论语言

    • 谓词$\in$(2)
    • 常元$\emptyset$
    • 函数符
      • 对偶函数符,(2)
      • 幂集函数符$\mathcal{P}$(1)
      • 并集函数符$\cup$(1)
    • 变元符$x,y,z,A,B,C$
  • 约定

    • $A\subseteq B$即$\forall x(x\in A\rightarrow x\in B)$
    • ${a}$即${a,a}$
    • $a^+$即$a\cup{a}$
    • $A\cup B$即${x|x\in A\vee x\in B}$
    • $(\forall x\in A)\phi$即$\forall x(x\in A\rightarrow\phi)$
    • $(\exists x\in A)\phi$即$\exists x(x\in A\wedge\phi)$
  • ZF公理

    • 外延性公理$\forall A\forall B(\forall x(x\in A\leftrightarrow x\in B)\rightarrow A=B)$

    • 空集公理$\exists B\forall x(\neg(x\in B))$

      • 若有常元$\emptyset$可记为$\forall x(x\not\in \emptyset)$
    • 对偶公理$\forall u\forall v\exists B\exists x(x\in B\leftrightarrow(x=u\vee x=v))$

      • 若有函数,则可记为$\forall u\forall v\exists x(x\in{u,v}\leftrightarrow(x=u\vee x=v))$
    • $\forall A\exists B\forall x(x\in B\leftrightarrow(\exists b\in A)(x\in b))$

      • 若有函数$\cup$则可记为$\forall A\exists B\forall x(x\in B\leftrightarrow(\exists b\in A)(x\in b))$
    • 幂集公理$\forall a\exists B\forall x(x\in B\leftrightarrow x\subseteq a)$

      • 若有函数$\mathcal{P}$则可记为$\forall x(x\in \mathcal{P}(a)\leftrightarrow x\subseteq a)$
    • 子集公理S-公式$\phi$,$\text{FV}(\phi)\subseteq{x_1,\cdots,x_k,x},B\not\in\text{FV}(\phi)$,有$\forall\vec x\forall C\exists B\forall x(x\in B\leftrightarrow(x\in C\wedge\phi))$

      • 以Cantor记号记:$B={x\in C|\phi}$
      • 避免Russell悖论
    • 无穷公理:$\exists A(\emptyset\in A\wedge(\forall a\in A)(a^+\in A))$

      • 不唯一
      • $\text{Ind}(A)=\emptyset\in A\wedge(\forall a\in A)(a^+\in A)$,满足者称归纳集
      • $\mathbb{N}={x|x\in A\wedge\forall B(\text{Ind(B)}\rightarrow x\in B)}$
      • Peano算术模型:$(\mathbb{N},0,\text{Suc})$
        • Peano 公理
          • $(e\in S)$
          • $(\forall a\in S)(f(a)\in S)$
          • $(\forall b\in S)(\forall c\in S)(f(b)=f(c)\to b=c)$
          • $(\forall a\in S)(f(a)\not=e)$
          • $(\forall A\subseteq S)(((e\in A)\wedge(\forall a\in A)(f(a)\in A))\to(A=S))$
  • ZFC:ZF+AC

    • 选择公理(AC):$\forall A\exists\tau((\tau:P(A)-{\emptyset}\rightarrow A)\wedge(\forall B\in (P(A)-{\emptyset}))(\tau(B)\in B))$
    • Zorn 引理:设$S$为偏序集,$S$中每个链皆有界,则$S$有极大元
      • 等价于选择公理
    • 独立性结果
      • $\text{con}(ZF)\Rightarrow\text{con}(ZF+AC)$
      • $\text{con}(ZF)\Rightarrow\text{con}(ZF+\neg AC)$

Herbrand定理

  • 前束范式:一阶语言的公式呈形$Q_1x_1.(Q_2x_2.(\cdots,Q_nx_n.(B)))$,$Q_i\in{\forall,\exists}(i\leq n),B$中无量词

    • 记为$Q_1x_1\cdots Q_nx_n.B$
    • $Q^*$ 为$Q$的对偶
  • 命题

    • $x\not\in\text{FV}(B)$,则$\vdash Qx.B\leftrightarrow B$
    • $y$ 为新变元,$\vdash Qx.B\leftrightarrow Qy.B[\frac{y}{x}]$
    • $\vdash\neg\forall x.A\leftrightarrow\exists x.\neg A.$
    • $\vdash\neg\exists x.A\leftrightarrow\forall x.\neg A.$
    • $x\not\in\text{FV}(B)$,则$\vdash (Qx.A\cdot B)\leftrightarrow Qx.(A\cdot B)$
  • $\forall A,\exists B,\vdash A\leftrightarrow Q_1x_1\cdots Q_nx_n.B$,$x_1,\cdots,x_n$互异且$B$中无量词

  • Skolem范式:前束范式的Skolem范式$A^s$归纳定义如下:

    • 若$A$中无量词,则$A^s=A$
    • $(\forall x.A)^s=\forall x.(A^s)$
    • 若$\text{FV}(\exists x.A)=\emptyset$,则$(\exists x.A)^s$为$(A[\frac{c}{x}])^s$,$c$ 为新常元
    • 若$\text{FV}(\exists x.A)={x_1,\cdots,x_n}$,则$(\exists x.A)^s=(A[\frac{f(x_1,\cdots,x_n)}{x}])^s$,$f$为$n$元新函数
  • $A$为闭前束范式(即无自由变元),$A$可满足$\iff A^s$可满足

  • Herbrand域$H_A$

    • $A$中无常元,则$H_0={c_0},c_0\in\mathscr{L}_c$
    • $A$中有常元,则$H_0=${$c|c\in\mathscr{L}_{c}$且出现在$A$中}
    • $H_{n+1}=H_n\cup${$f(t_1,\cdots,t_m)|f$为$A$中的$m$元函数且$t_1,\cdots,t_m\in H_n$}
    • $H_A=\cup{H_n|n\in N}$
      • 其中元素为$\mathscr{L}$-闭项
  • $A$对应于$\mathbb{M}$的Herbrand结构$\mathbb{H}_A=(H_A,I_A)$

    • $I_A(c)=c$若$c\in H_A$否则$c_0$
    • $I_A(f)(t_1,\cdots,t_m)=f(t_1,\cdots,t_m)$若$f$出现在$A$中否则$c_0$
    • $I_A(P)={ < t_1,\cdots,t_m > \in H_A^m|\mathbb{M}\vDash P(t_1,\cdots,t_m)}$
  • $\mathscr{L}$-闭公式$A$为Skolem范式,$\mathbb{M}\vDash A$则$\mathbb{H}_A\vDash A$

    • $\mathscr{L}$-闭公式$A$为Skolem范式,$A$可满足$\iff A$在某个Herbrand结构中满足
  • Herbrand定理:$\mathscr{L}$-闭公式$A$为Skolem范式$\forall x_1\cdots\forall x_n.B$,$B$中无量词,令$\Gamma={B[\frac{t_1}{x_1}]\cdots[\frac{t_n}{x_n}]|t_1,\cdots,t_n\in H_A}$,$A$可满足$\iff\Gamma$可满足

模态语言

模式 分支 应用
可能与必然 基本模态逻辑
过去与将来 时态逻辑(temporal) 软硬件系统形式化验证
知道与相信 认知逻辑(epistemic) 知识表示
义务与允许 道义逻辑(deontic) 分布式智能系统进行协同与控制的规范系统
  • 模态逻辑特征

    • 模态逻辑是用于描述关系结构的简单而富于表达力的语言
    • 模态语言为关系结构提供了一种内部和局部的视角
    • 模态逻辑并不是孤立的形式化系统
  • 关系结构$\mathfrak{F}=(W,R_1,\cdots,R_n)$,$W$为domain/universe,$R_i$为$\mathfrak{F}$上的关系

    • $W$中的元素可以为不同名称如点,状态,世界,时间,状况等.关系结构通常可以表示为简单图形
    • 严格偏序
      • 全序
    • 标注转换系统(LTS)$(W,{R_a|a\in A}),a\in A,R_a\subseteq W\times W$
    • 时间的内在结构为全序集$(S, < )$
      • 假设:
        1.时间离散
        2.有一个没有前驱的时刻
        3.有无穷后续时刻进入未来

基本模态逻辑

语言

  • 命题符集合$\Phi$
  • 一元模态算子$\diamonds$
    • 读作可能
    • 对偶算子$\square\varphi:=\neg\diamonds\neg\varphi$
      • 读作不可能不/必然
    • $\varphi\wedge\psi:=\neg(\neg\varphi\vee\neg\psi)$
    • $\top:=\neg\perp$
  • 合式公式(well-formed formula) $\varphi::=p|\perp|\neg\varphi|\varphi\vee\phi|\diamonds\varphi$
  • 部分合式公式
    • $K:\square(\varphi\rightarrow\phi)\rightarrow(\square\varphi\rightarrow\square\phi)$
    • $T:\square\varphi\rightarrow\phi$
    • $4:\square\phi\rightarrow\square\square\phi$
    • $B:\varphi\rightarrow\square\diamonds\varphi$
    • $D:\square\varphi\rightarrow\diamonds\varphi$
    • $5:\diamonds\varphi\rightarrow\square\diamonds\phi$

语义

  • Kripke模型:$\mathfrak{M}=(W,R,L)$

    • $L:W\rightarrow 2^\Phi$为标记函数,把$W$每个点标记上再该点为真的命题符
    • 状态 $\omega\in W$
  • $\mathfrak{M},\omega\Vdash\varphi$基本模态公式$\varphi$在状态$\omega$被满足

    • $\mathfrak{M},\omega\Vdash p,p\in\Phi\iff p\in L(W)$
    • $\mathfrak{M},\omega\Vdash \perp$从不成立
    • $\mathfrak{M},\omega\Vdash\neg\varphi\iff \mathfrak{M},\omega\Vdash\phi$不成立
    • $\mathfrak{M},\omega\Vdash\varphi\vee\psi\iff\mathfrak{M},\omega\Vdash\varphi$或$\mathfrak{M},\omega\Vdash\psi$
    • $\mathfrak{M},\omega\Vdash\diamond\varphi\iff$存在$v\in W,Rwv,\mathfrak{M},\omega\Vdash\varphi$
      • $\mathfrak{M},\omega\Vdash\square\varphi\iff$对于任意的$v\in W,Rw v,\mathfrak{M},\omega\Vdash\varphi$
  • 盲状态:不能到达任意后续状态的状态,$\square\varphi$空真

  • $\mathfrak{F},\omega\Vdash\varphi$:任意$L$,$\mathfrak{M},\omega\Vdash\varphi$

  • $\mathfrak{F}\Vdash\varphi$:任意的$\omega$, $\mathfrak{F},\omega\Vdash\varphi$

  • $\mathbb{F}\Vdash\varphi$:任意的$\mathfrak{F}\in\mathbb{F},\mathfrak{F}\Vdash\varphi$

    • $\Lambda_\mathbb{F}$:$\mathbb{F}$的逻辑,对$\mathbb{F}$有效的所有公式的集合
  • $\Vdash\varphi$:任意的$\mathbb{F}$,$\mathbb{F}\Vdash\varphi$

线性时间时态逻辑

语言

  • 线性时间时态算子

    • $\mathcal{U}$:until
    • $\bigcirc$:next-time
  • 常用时态算子

    • $\diamond\phi:=\top\mathcal{U}\phi$:Finally
    • $\square\phi:=\neg\diamond\neg\phi$:Globally
    • $\overset{\infty}{\diamond}\phi:=\square\diamond\phi$:Infinitely Often
    • $\overset{\infty}{\square}\phi:=\diamond\square\phi$:Almost Everywhere
    • $\phi_1\mathcal{R}\phi_2:=\neg(\neg\phi_1\mathcal{U}\neg\phi_2)$
  • $\psi::=p|\perp|\neg\psi|\psi_1\vee\psi_2|\bigcirc|\psi_1\mathcal{U}\psi_2,p\in\Phi$

语义

  • 模型$\mathfrak{M}=(S,x,L)$

    • $S$: 非空状态集
    • $x:N\rightarrow S$:状态的无穷序列
    • $L:W\rightarrow2^\Phi$
  • $\mathfrak{M},x\vDash\psi$:在模型$\mathfrak{M}$的时间线上,公式$\psi$为真(Linear-time Temporal Logic (LTL))

    • $\mathfrak{M},x\vDash p,p\in\Psi\iff p\in L(s_0)$
    • $\mathfrak{M},x\vDash\perp$从不成立
    • $\mathfrak{M},x\vDash \neg\psi\iff\mathfrak{M},x\vDash \psi$不成立
    • $\mathfrak{M},x\vDash \psi_1\vee\psi_2\iff\mathfrak{M},x\vDash \psi_1$或$\mathfrak{M},x\vDash \psi_2$
    • $\mathfrak{M},x\vDash \psi_1\mathcal{U}\psi_2\iff\exists j(\mathfrak{M},x^j\vDash \psi_2$且$\forall k < j(\mathfrak{M},x^k\vDash \psi_1))$
    • $\mathfrak{M},x\vDash\bigcirc\psi\iff\mathfrak{M},x^1\vDash\psi$
      • $x^i$表示$s$的后缀$s_i,s_{i+1},\cdots$

分支时间时态逻辑

语言

  • 命题符$\Psi$

  • 线性时态算子

  • 路径选择算子$\exists$:for some futures

    • $\forall\psi:=\neg\exists\neg\psi$:for all futures
  • 路径公式:$\psi::=\phi|\psi_1\vee\psi_2|\neg\psi|\bigcirc\psi|\psi_1\mathcal{U}\psi_2$

  • 状态公式:$\varphi::=p|\perp|\phi_1\vee\phi_2|\neg\varphi|\exists\psi$

子语言

  • 路径公式:$\psi::=\bigcirc\varphi,\varphi_1\mathcal{U}\varphi_2$

    • 不允许线性时态算子的布尔组合和嵌套
    • 状态公式不变
  • 等价于:

    • 基本时态算子:$\exists\bigcirc,\exists\square,\exists\mathcal{U}$
    • $\forall\bigcirc\varphi:=\neg\exists\bigcirc\neg\varphi$
    • $\forall\square\varphi:=\neg\exists\diamond\neg\varphi$
    • $\forall\diamond\varphi:=\neg\exists\square\neg\varphi$
    • $\exists\diamond\varphi:=\exists(\perp\mathcal{U}\varphi)$
    • $\forall(\varphi_1\mathcal{U}\varphi_2):=\neg\exists(\neg\varphi_2\mathcal{U}\neg\varphi_2)\wedge\neg\exists\square\neg\varphi_2$
  • $\varphi::=p|\perp|\neg\varphi|\varphi_1\vee\varphi_2|\exists\bigcirc\varphi|\exists\square\varphi|\exists(\varphi_1\mathcal{U}\varphi_2)$

语义 Coputation-Tree-Logic-CTL

  • Kripke模型:$\mathfrak{M}=(S,R,L)$

    • $S$:非空状态集
      • $R\subset S\times S$是一个完全的二元关系
    • 完全:$\forall s\in S\exists t\in S:(s,t)\in R$
    • $L:S\rightarrow2^\Phi$
  • 全路径(full path)$x=(s_0,s_1,\cdots)$:$\forall i\in\mathbb{N}:(s_i,s_{i+1})\in R$

  • $\mathfrak{M},s_0\vDash\varphi$:在$\mathfrak{M}$的状态$s_0$为真

    • (S1)
      • $\mathfrak{M},s_0\vDash p\iff p\in L(s_0)$
      • $\mathfrak{M},s_0\vDash\perp$从不成立
    • (S2)
      • $\mathfrak{M},s_0\vDash\varphi_1\vee\varphi_2\iff\mathfrak{M},s_0\vDash\varphi_1$或$\mathfrak{M},s_0\vDash\varphi_2$
      • $\mathfrak{M},s_0\vDash\neg\varphi\iff\mathfrak{M},s_0\vDash\varphi$不成立
    • (S3) $\mathfrak{M},s_0\vDash\exists\psi\iff\mathfrak{M}$中存在全路径$x,\mathfrak{M},x\vDash\psi$
  • $\mathfrak{M},x\vDash\psi$:在$\mathfrak{M}$中的全路径$x$为真

    • (P1) $\mathfrak{M},x\vDash\varphi\iff\mathfrak{M},s_0\vDash\varphi$
    • (P2)
      • $\mathfrak{M},x\vDash\psi_1\vee\psi_2\iff\mathfrak{M},x\vDash\psi_1$或$\mathfrak{M},x\vDash\psi_2$
      • $\mathfrak{M},x\vDash\neg\psi\iff\mathfrak{M},x\vDash\psi$不成立
    • (P3)
      • $\mathfrak{M},x\vDash\psi_1\mathcal{U}\psi_2\iff\exists j(\mathfrak{M},x^j\vDash\psi_2$且$\forall k < j(\mathfrak{M},x^k\vDash\psi_1))$
      • $\mathfrak{M},x\vDash\bigcirc\varphi\iff\mathfrak{M},x^1\vDash\psi$

CTL

  • S1,S2,S3
  • S4
    • $\mathfrak{M},s_0\vDash\exists\bigcirc\varphi\iff\exists s_1,Rs_0s_1,\mathfrak{M},s_1\vDash\varphi$
    • $\mathfrak{M},s_0\vDash\exists\square\exists x,\forall i\in\mathbb{N}:\mathfrak{M},s_0\vDash\psi$
    • $\mathfrak{M},s_0\vDash\exists(\varphi_1\mathcal{U}\varphi_2)\iff\exists x,\exists j(\mathfrak{M},s_j\vDash\psi_2$且$\forall k < j(\mathfrak{M},s_k\vDash\psi_1))$

语法

Hilbert公理系统K

  • 公理

    • (TAUT)所有重言式
    • (K)$\square(p\rightarrow q)\rightarrow(\square p\rightarrow q)$
    • (Dual)$\diamond p\leftrightarrow\neg\square\neg p$
  • 规则

    • (MP, Modus Ponens):$\dfrac{\varphi\rightarrow\psi,\varphi}{\psi}$
    • (US, Uniform Substitutious): $\dfrac{\varphi}{\theta}$
      • $\theta$为将$\varphi$中命题符一致地替换为任意的公式而得到的公式
    • (N, Generalization):$\dfrac{\varphi}{\square\varphi}$
  • K-系统对于所有的框架可靠且完全

    • 对应基本模态逻辑
  • 最小的正规模态逻辑为K

K$\Gamma$

  • K4
    • 增加公理$\diamond\diamond p\rightarrow\diamond p$
    • 对应传递框架

正规模态逻辑$\Lambda$

  • 包含TAUT,K,Dual
  • 对规则MP,US,N封闭

标准翻译

  • $\mathcal{L}^1(\Phi)$为一阶语言

    • 具有一元谓词$P_0,P_1,\cdots$对应$\Phi$中命题符$p_0,p_1,\cdots$
    • 具有二元关系$R$对应$\diamond$
  • 标准翻译$\text{ST}_x$:

    • $\text{ST}_x(p)=Px$
    • $\text{ST}_x(\perp)=x\not=x$
    • $\text{ST}_x(\neg\phi)=\neg\text{ST}_x(\phi)$
    • $\text{ST}_x(\phi\vee\psi)=\text{ST}_x(\phi)\vee\text{ST}_x(\psi)$
    • $\text{ST}_x(\diamond\phi)=\exists y(Rxy\wedge\text{ST}_y(\phi))$
  • $\mathfrak{M},\omega\Vdash\varphi\iff\mathfrak{M}\vDash\text{ST}_x(\varphi)[\omega]$

  • $\forall\mathfrak{M},\omega\Vdash\varphi\iff\mathfrak{M}\vDash\forall x\text{ST}_x(\varphi)[\omega]$

其他

  • 文章结构:Fundamental Thm, Main Thm, Theorem, Lemma, Proposition, Law, Thesis
  • 三次数学危机
    • 小数$\to$无理数
      • 希伯索斯
    • 牛顿-莱布尼茨 无穷概念
      • 柯西
    • 集合论 罗素悖论
      • 公理逻辑论
数理逻辑

第一讲 命题逻辑

定义1.1

命题符:$P_0,P_1,P_2…P_n,n\in\mathbb{N}$,记$PS={P_n|n\in\mathbb{N}}$.本书中,命题符之集$PS$为可数无穷集,即$|PS|=\aleph_0$

定义1.3

所有命题的集合$PROP$是满足以下条件的最小集合

  1. $PS\subseteq PROP$
  2. 若$A\in PROP$,则$C_{\lnot}(A)\in PROP$
  3. 若$A,B\in PROP$,则$C_{\wedge(A,B)},C_{\vee}(A,B)$和$C_{\to}(A,B)\in PROP$

引理 1.5

$A\in PROP$等价于存在有穷序列$A_0,A_1…A_n$使$A$为$A_n$且对任何$i\le n$

  1. $A_i\in PS$
  2. 或 存在$k < i$使$A_i$为$(\lnot A_k)$
  3. 或 存在$k,j < i$使$A_i$为$(A_k\ast A_l)$,这里$\ast$为$\wedge,\vee,\to$之一

命题 1.9

  1. $v$满足$A$,记为$v\models A$,指$\hat{v}(A)=T$
  2. $A$为永真式,记为$\models A$,指对任何$v$有$\hat{v}(A)=T$
  3. $A$可满足,指有$v$使$v\models A$
  4. 设$\Gamma$为命题集,$A$为$T$的语义结论,记为$\Gamma\models A$,指对所有$v$,若对任何$B\in\Gamma$有$\hat{v}(B)=T$则$\hat{v}=T$

定义 1.13

设$A,B$为命题$A$与$B$逻辑等价,记为$A\simeq B$,指对任何赋值$v,v\models A$ iff $v\models B$

第八讲 命题逻辑的永真推理系统

公理
A01 $A\to A$
A02 $(A\to(B\to C))\to(B\to(A\to C))$
A03 $(A\to B)\to((B\to C)\to(A\to C))$
A04 $(A\to(A\to B))\to(A\to B)$
A05 $(A\to\lnot B)\to(B\to\lnot A)$
A06 $(\lnot\lnot A)\to A$
A07 $(A\wedge B)\to A$
A08 $(A\wedge B)\to B$
A09 $A\to(B\to(A\wedge B))$
A10 $A\to(A\vee B)$
A11 $B\to(A\vee B)$
A12 $(A\to C)\to((B\to C)\to((A\vee B)\to C))$
T13 $(A\to B)\to((C\to A)\to(C\to B))$
T14 $(A\to B)\to([D\to(C\to A)]\to[D\to(C\to B)])$
T15 $\vdash A\to(B\to A)$
T16 $\vdash[C\to(B\to A)]\to[(C\to B)\to(C\to A)]$
T17 $\vdash(\lnot A\to\lnot B)\to(B\to S)$
T18 $\vdash A\to \lnot\lnot A$
T19 $\vdash(A\to B)\to(\lnot B\to\lnot A)$
T20 $\vdash A\vee\lnot A$
T21 $A,\lnot A\vdash\lnot B$
T22 $A,\lnot A\vdash B$
T23 $(B\to\lnot B)\to\lnot B$
T24 $\vdash(A\to(C\wedge\lnot C)\to\lnot A$
T25 $(B\vee A)\to(\lnot A\to B)$
T26 $(A\to B)\to(B\vee\lnot A)$
T27 $(A\vee B)\to(B\vee A)$
T28 $(A\to(B\to C))\to((A\wedge B)\to C)$
T29 $(C\vee A)\to((C\vee B)\to(C\vee(A\wedge B)))$
T30 $(C\vee A)\to[(B\to C)\to((A\to B)\to C)]$
T31 $(A\to(C\vee B))\to(C\vee(A\to B))$

定理 8.3(推理定理)

若$\Gamma,C\vdash A$,则$\Gamma\vdash C\to A$,这里$\Gamma,C$为$\Gamma\cup\{C\}$的简写

1 / 1