数理逻辑复习
2019-06-09

搬运自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$无理数
    • 希伯索斯
  • 牛顿-莱布尼茨 无穷概念
    • 柯西
  • 集合论 罗素悖论
    • 公理逻辑论