Skip to Content
Mathematic Logics

Model Logic

2019-04-01Original-language archivelegacy assets may be incomplete

模态语言

模式 分支 应用
可能与必然 基本模态逻辑
过去与将来 时态逻辑(temporal) 软硬件系统形式化验证
知道与相信 认知逻辑(epistemic) 知识表示
义务与允许 道义逻辑(deontic) 分布式智能系统进行协同与控制的规范系统
  • 模态逻辑特征
    • 模态逻辑是用于描述关系结构的简单而富于表达力的语言
    • 模态语言为关系结构提供了一种内部和局部的视角
    • 模态逻辑并不是孤立的形式化系统
  • 关系结构 F=(W,R1,⋯ ,Rn)\mathfrak{F}=(W,R_1,\cdots,R_n), WW 为 domain/universe, RiR_i 为 F\mathfrak{F} 上的关系
    • WW 中的元素可以为不同名称如点、状态、世界、时间、状况等。关系结构通常可以表示为简单图形
    • 严格偏序
      • 全序
    • 标注转换系统（LTS）(W,{Ra∣a∈A}),a∈A,Ra⊆W×W(W,\{R_a|a\in A\}),a\in A,R_a\subseteq W\times W
    • 时间的内在结构为全序集 (S,<)(S,<)
      • 假设：1.时间离散 2.有一个没有前驱的时刻 3.有无穷后续时刻进入未来

基本模态逻辑

语言

  • 命题符集合 Φ\Phi
  • 一元模态算子 ♢\diamondsuit
    • 读作 "可能"
    • 对偶算子 □φ:=¬♢¬φ\square\varphi:=\neg\diamondsuit\neg\varphi
      • 读作 "不可能不/必然"
    • φ∧ψ:=¬(¬φ∨¬ψ)\varphi\wedge\psi:=\neg(\neg\varphi\vee\neg\psi)
    • ⊤:=¬⊥\top:=\neg\perp
  • 合式公式(well-formed formula) φ::=p∣⊥∣¬φ∣φ∨ϕ∣♢φ\varphi::=p|\perp|\neg\varphi|\varphi\vee\phi|\diamondsuit\varphi
  • 部分合式公式
    • K:□(φ→ϕ)→(□φ→□ϕ)K:\square(\varphi\rightarrow\phi)\rightarrow(\square\varphi\rightarrow\square\phi)
    • T:□φ→ϕT:\square\varphi\rightarrow\phi
    • 4:□ϕ→□□ϕ4:\square\phi\rightarrow\square\square\phi
    • B:φ→□♢φB:\varphi\rightarrow\square\diamondsuit\varphi
    • D:□φ→♢φD:\square\varphi\rightarrow\diamondsuit\varphi
    • 5:♢φ→□♢ϕ5:\diamondsuit\varphi\rightarrow\square\diamondsuit\phi

标准翻译

  • L1(Φ)\mathcal{L}^1(\Phi) 为一阶语言
    • 具有一元谓词 P0,P1,⋯P_0,P_1,\cdots 对应 Φ\Phi 中命题符 p0,p1,⋯p_0,p_1,\cdots
    • 具有二元关系 RR 对应 ♢\diamondsuit
  • 标准翻译 STx\text{ST}_x:
    • STx(p)=Px\text{ST}_x(p)=P_x
    • STx(⊥)=x≠x\text{ST}_x(\perp)=x\not=x
    • STx(¬ϕ)=¬STx(ϕ)\text{ST}_x(\neg\phi)=\neg\text{ST}_x(\phi)
    • STx(ϕ∨ψ)=STx(ϕ)∨STx(ψ)\text{ST}_x(\phi\vee\psi)=\text{ST}_x(\phi)\vee\text{ST}_x(\psi)
    • STx(♢ϕ)=∃y(Rxy∧STy(ϕ))\text{ST}_x(\diamondsuit\phi)=\exists y(Rxy\wedge\text{ST}_y(\phi)), y 为新变元
  • M,ω⊩φ  ⟺  M⊨STx(φ)[ω]\mathfrak{M},\omega\Vdash\varphi\iff\mathfrak{M}\vDash\text{ST}_x(\varphi)[\omega]
    • STx(φ)[ω]\text{ST}_x(\varphi)[\omega]: ω\omega 被赋给自由变元 yy
  • ∀M,ω⊩φ  ⟺  M⊨∀xSTx(φ)\forall\mathfrak{M},\omega\Vdash\varphi\iff\mathfrak{M}\vDash\forall x\text{ST}_x(\varphi)

语义

  • Kripke 模型：M=(W,R,L)=(F,L)\mathfrak{M}=(W,R,L)=(\mathfrak{F},L)
    • 状态 ω∈W\omega\in W
    • RR 为 WW 上的关系
    • L:W→2ΦL:W\rightarrow 2^\Phi 为标记函数，把 WW 每个点标记上再该点为真的命题符
  • M,ω⊩φ\mathfrak{M},\omega\Vdash\varphi 基本模态公式 φ\varphi 在状态 ω\omega 被满足
    • M,ω⊩p,p∈Φ  ⟺  p∈L(ω)\mathfrak{M},\omega\Vdash p,p\in\Phi\iff p\in L(\omega)
    • M,ω⊩⊥\mathfrak{M},\omega\Vdash \perp 从不成立
    • M,ω⊩¬φ  ⟺  M,ω⊩φ\mathfrak{M},\omega\Vdash\neg\varphi\iff \mathfrak{M},\omega\Vdash\varphi 不成立
    • M,ω⊩φ∨ψ  ⟺  M,ω⊩φ\mathfrak{M},\omega\Vdash\varphi\vee\psi\iff\mathfrak{M},\omega\Vdash\varphi 或 M,ω⊩ψ\mathfrak{M},\omega\Vdash\psi
    • M,ω⊩♢φ  ⟺  \mathfrak{M},\omega\Vdash\diamondsuit\varphi\iff 存在 v∈W,Rwv,M,ω⊩φv\in W,Rwv,\mathfrak{M},\omega\Vdash\varphi
      • M,ω⊩□φ  ⟺  \mathfrak{M},\omega\Vdash\square\varphi\iff 对于任意的 v∈W,Rwv,M,ω⊩φv\in W,Rw v,\mathfrak{M},\omega\Vdash\varphi
  • 盲状态：不能到达任意后续状态的状态，□φ\square\varphi 空真
  • F,ω⊩φ\mathfrak{F},\omega\Vdash\varphi：任意的 LL, M,ω⊩φ\mathfrak{M},\omega\Vdash\varphi
  • F⊩φ\mathfrak{F}\Vdash\varphi: 任意的 ω\omega, F,ω⊩φ\mathfrak{F},\omega\Vdash\varphi
  • F⊩φ\mathbb{F}\Vdash\varphi: 任意的 F∈F,F⊩φ\mathfrak{F}\in\mathbb{F},\mathfrak{F}\Vdash\varphi
    • ΛF\Lambda_\mathbb{F}: F\mathbb{F} 的逻辑，对 F\mathbb{F} 有效的所有公式的集合
  • ⊩φ\Vdash\varphi: 任意的 F\mathbb{F}, F⊩φ\mathbb{F}\Vdash\varphi

线性时间时态逻辑 (LTL)

语言

  • 线性时间时态算子
    • U\mathcal{U}: until
    • ◯\bigcirc: next-time
  • 常用时态算子
    • ♢ϕ:=⊤Uϕ\diamondsuit\phi:=\top\mathcal{U}\phi: Finally
    • □ϕ:=¬♢¬ϕ\square\phi:=\neg\diamondsuit\neg\phi: Globally
    • ♢∞ϕ:=□♢ϕ\overset{\infty}{\diamondsuit}\phi:=\square\diamondsuit\phi: Infinitely Often
    • □∞ϕ:=♢□ϕ\overset{\infty}{\square}\phi:=\diamondsuit\square\phi: Almost Everywhere
    • ϕ1Rϕ2:=¬(¬ϕ1U¬ϕ2)\phi_1\mathcal{R}\phi_2:=\neg(\neg\phi_1\mathcal{U}\neg\phi_2): Release
  • ψ::=p∣⊥∣¬ψ∣ψ1∨ψ2∣◯ψ∣ψ1Uψ2,p∈Φ\psi::=p|\perp|\neg\psi|\psi_1\vee\psi_2|\bigcirc\psi|\psi_1\mathcal{U}\psi_2,p\in\Phi

语义

  • 模型 M=(S,x,L)\mathfrak{M}=(S,x,L)
    • SS: 非空状态集
    • x:N→Sx:N\rightarrow S：状态的无穷序列
    • L:W→2ΦL:W\rightarrow2^\Phi
  • M,x⊨ψ\mathfrak{M},x\vDash\psi: 在模型 M\mathfrak{M} 的时间线 xx 上，公式 ψ\psi 为真
    • M,x⊨p,p∈Ψ  ⟺  p∈L(s0)\mathfrak{M},x\vDash p,p\in\Psi\iff p\in L(s_0)
    • M,x⊨⊥\mathfrak{M},x\vDash\perp 从不成立
    • M,x⊨¬ψ  ⟺  M,x⊨ψ\mathfrak{M},x\vDash \neg\psi\iff\mathfrak{M},x\vDash \psi 不成立
    • M,x⊨ψ1∨ψ2  ⟺  M,x⊨ψ1\mathfrak{M},x\vDash \psi_1\vee\psi_2\iff\mathfrak{M},x\vDash \psi_1 或 M,x⊨ψ2\mathfrak{M},x\vDash \psi_2
    • M,x⊨ψ1Uψ2  ⟺  ∃j(M,xj⊨ψ2\mathfrak{M},x\vDash \psi_1\mathcal{U}\psi_2\iff\exists j(\mathfrak{M},x^j\vDash \psi_2 且 ∀k<j(M,xk⊨ψ1))\forall k<j(\mathfrak{M},x^k\vDash \psi_1))
    • M,x⊨◯ψ  ⟺  M,x1⊨ψ\mathfrak{M},x\vDash\bigcirc\psi\iff\mathfrak{M},x^1\vDash\psi
      • xix^i 表示 ss 的后缀 si,si+1,⋯s_i,s_{i+1},\cdots

分支时间时态逻辑

语言

BTL

  • 命题符 Ψ\Psi
  • 线性时态算子
  • 路径选择算子 ∃\exists: for some futures
    • ∀ψ:=¬∃¬ψ\forall\psi:=\neg\exists\neg\psi: for all futures
  • 路径公式：ψ::=ϕ∣ψ1∨ψ2∣¬ψ∣◯ψ∣ψ1Uψ2\psi::=\phi|\psi_1\vee\psi_2|\neg\psi|\bigcirc\psi|\psi_1\mathcal{U}\psi_2
  • 状态公式：φ::=p∣⊥∣φ1∨φ2∣¬φ∣∃ψ\varphi::=p|\perp|\varphi_1\vee\varphi_2|\neg\varphi|\exists\psi

Sublanguage

  • 路径公式：ψ::=◯φ∣φ1Uφ2\psi::=\bigcirc\varphi|\varphi_1\mathcal{U}\varphi_2
    • 不允许线性时态算子的布尔组合和嵌套
    • 状态公式不变
  • 等价于：
    • 基本时态算子：∃◯,∃□,∃U\exists\bigcirc,\exists\square,\exists\mathcal{U}
      • ∀◯φ:=¬∃◯¬φ\forall\bigcirc\varphi:=\neg\exists\bigcirc\neg\varphi
      • ∀□φ:=¬∃♢¬φ\forall\square\varphi:=\neg\exists\diamondsuit\neg\varphi
      • ∀♢φ:=¬∃□¬φ\forall\diamondsuit\varphi:=\neg\exists\square\neg\varphi
      • ∃♢φ:=∃(⊥Uφ)\exists\diamondsuit\varphi:=\exists(\perp\mathcal{U}\varphi)
      • ∀(φ1Uφ2):=¬∃(¬φ2U¬φ2)∧¬∃□¬φ2\forall(\varphi_1\mathcal{U}\varphi_2):=\neg\exists(\neg\varphi_2\mathcal{U}\neg\varphi_2)\wedge\neg\exists\square\neg\varphi_2
    • φ::=p∣⊥∣¬φ∣φ1∨φ2∣∃◯φ∣∃□φ∣∃(φ1Uφ2)\varphi::=p|\perp|\neg\varphi|\varphi_1\vee\varphi_2|\exists\bigcirc\varphi|\exists\square\varphi|\exists(\varphi_1\mathcal{U}\varphi_2)

语义 Computation Tree Logic

CTL∗^*

  • Kripke 模型：M=(S,R,L)\mathfrak{M}=(S,R,L)
    • SS：非空状态集
    • R⊂S×SR\subset S\times S 是一个完全的二元关系
      • 完全：∀s∈S∃t∈S:(s,t)∈R\forall s\in S\exists t\in S:(s,t)\in R
    • L:S→2ΦL:S\rightarrow2^\Phi
  • 全路径(full path) x=(s0,s1,⋯ )x=(s_0,s_1,\cdots)：∀i∈N:(si,si+1)∈R\forall i\in\mathbb{N}:(s_i,s_{i+1})\in R
  • M,s0⊨φ\mathfrak{M},s_0\vDash\varphi: 在 M\mathfrak{M} 的状态 s0s_0 为真
    • (S1)
      • M,s0⊨p  ⟺  p∈L(s0)\mathfrak{M},s_0\vDash p\iff p\in L(s_0)
      • M,s0⊨⊥\mathfrak{M},s_0\vDash\perp 从不成立
    • (S2)
      • M,s0⊨φ1∨φ2  ⟺  M,s0⊨φ1\mathfrak{M},s_0\vDash\varphi_1\vee\varphi_2\iff\mathfrak{M},s_0\vDash\varphi_1 或 M,s0⊨φ2\mathfrak{M},s_0\vDash\varphi_2
      • M,s0⊨¬φ  ⟺  M,s0⊨φ\mathfrak{M},s_0\vDash\neg\varphi\iff\mathfrak{M},s_0\vDash\varphi 不成立
    • (S3) M,s0⊨∃ψ  ⟺  M\mathfrak{M},s_0\vDash\exists\psi\iff\mathfrak{M} 中存在全路径 x,M,x⊨ψx,\mathfrak{M},x\vDash\psi
  • M,x⊨ψ\mathfrak{M},x\vDash\psi: 在 M\mathfrak{M} 中的全路径 xx 为真
    • (P1) M,x⊨φ  ⟺  M,s0⊨φ\mathfrak{M},x\vDash\varphi\iff\mathfrak{M},s_0\vDash\varphi
    • (P2)
      • M,x⊨ψ1∨ψ2  ⟺  M,x⊨ψ1\mathfrak{M},x\vDash\psi_1\vee\psi_2\iff\mathfrak{M},x\vDash\psi_1 或 M,x⊨ψ2\mathfrak{M},x\vDash\psi_2
      • M,x⊨¬ψ  ⟺  M,x⊨ψ\mathfrak{M},x\vDash\neg\psi\iff\mathfrak{M},x\vDash\psi 不成立
    • (P3)
      • M,x⊨ψ1Uψ2  ⟺  ∃j(M,xj⊨ψ2\mathfrak{M},x\vDash\psi_1\mathcal{U}\psi_2\iff\exists j(\mathfrak{M},x^j\vDash\psi_2且∀k<j(M,xk⊨ψ1))\forall k<j(\mathfrak{M},x^k\vDash\psi_1))
      • M,x⊨◯φ  ⟺  M,x1⊨ψ\mathfrak{M},x\vDash\bigcirc\varphi\iff\mathfrak{M},x^1\vDash\psi

CTL

  • S1,S2,S3
  • S4
    • M,s0⊨∃◯φ  ⟺  ∃s1,Rs0s1,M,s1⊨φ\mathfrak{M},s_0\vDash\exists\bigcirc\varphi\iff\exists s_1,Rs_0s_1,\mathfrak{M},s_1\vDash\varphi
    • M,s0⊨∃□x,∀i∈N,M,si⊨ψ\mathfrak{M},s_0\vDash\exists\square x,\forall i\in\mathbb{N},\mathfrak{M},s_i\vDash\psi
    • M,s0⊨∃(φ1Uφ2)  ⟺  ∃x,∃j(M,sj⊨ψ2\mathfrak{M},s_0\vDash\exists(\varphi_1\mathcal{U}\varphi_2)\iff\exists x,\exists j(\mathfrak{M},s_j\vDash\psi_2且∀k<j(M,sk⊨ψ1))\forall k<j(\mathfrak{M},s_k\vDash\psi_1))

语法

正规模态逻辑 Λ\Lambda

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

KK

  • 公理
    • TAUT: 所有重言式
    • K: □(p→q)→(□p→□q)\square(p\rightarrow q)\rightarrow(\square p\rightarrow \square q)
    • Dual: ♢p↔¬□¬p\diamondsuit p\leftrightarrow\neg\square\neg p
  • 规则
    • MP (Modus Ponens): φ→ψ,φψ\frac{\varphi\rightarrow\psi,\varphi}{\psi}
    • US (Uniform Substitutious): φθ\frac{\varphi}{\theta}
      • θ\theta 为将 φ\varphi 中命题符一致地替换为任意的公式而得到的公式
    • N (Generalization): φ□φ\frac{\varphi}{\square\varphi}
  • KK-系统对应基本模态逻辑
    • soundness
    • completeness
  • 最小的正规模态逻辑为 KK

KΓK\Gamma

  • K4K4
    • 增加公理 ♢♢p→♢p\diamondsuit\diamondsuit p\rightarrow\diamondsuit p
    • 对应传递框架

其它

  • 定理等级
    • Fundamental Thm
    • Main Thm
    • Theorem
    • Lemma
    • Proposition
    • Law
    • Thesis
  • 三次数学危机
    • 小数→\rightarrow无理数
      • 希伯索斯
    • ∞\infty (牛顿-莱布尼茨)
      • 柯西
    • 罗素悖论 (集合论)
      • 公理逻辑论