模态语言

• 模态逻辑特征
  • 模态逻辑是用于描述关系结构的简单而富于表达力的语言
  • 模态语言为关系结构提供了一种内部和局部的视角
  • 模态逻辑并不是孤立的形式化系统
• 关系结构 $\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$
• 一元模态算子 $\diamondsuit$
  • 读作 “可能”
  • 对偶算子 $\square\varphi:=\neg\diamondsuit\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|\diamondsuit\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\diamondsuit\varphi$
  • $D:\square\varphi\rightarrow\diamondsuit\varphi$
  • $5:\diamondsuit\varphi\rightarrow\square\diamondsuit\phi$

标准翻译

• $\mathcal{L}^1(\Phi)$ 为一阶语言
  • 具有一元谓词 $P_0,P_1,\cdots$ 对应 $\Phi$ 中命题符 $p_0,p_1,\cdots$
  • 具有二元关系 $R$ 对应 $\diamondsuit$
• 标准翻译 $\text{ST}_x$:
  • $\text{ST}_x(p)=P_x$
  • $\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(\diamondsuit\phi)=\exists y(Rxy\wedge\text{ST}_y(\phi))$, y 为新变元
• $\mathfrak{M},\omega\Vdash\varphi\iff\mathfrak{M}\vDash\text{ST}_x(\varphi)[\omega]$
  • $\text{ST}_x(\varphi)[\omega]$: $\omega$ 被赋给自由变元 $y$
• $\forall\mathfrak{M},\omega\Vdash\varphi\iff\mathfrak{M}\vDash\forall x\text{ST}_x(\varphi)$

语义

• Kripke 模型：$\mathfrak{M}=(W,R,L)=(\mathfrak{F},L)$
  • 状态 $\omega\in W$
  • $R$ 为 $W$ 上的关系
  • $L:W\rightarrow 2^\Phi$ 为标记函数，把 $W$ 每个点标记上再该点为真的命题符
• $\mathfrak{M},\omega\Vdash\varphi$ 基本模态公式 $\varphi$ 在状态 $\omega$ 被满足
  • $\mathfrak{M},\omega\Vdash p,p\in\Phi\iff p\in L(\omega)$
  • $\mathfrak{M},\omega\Vdash \perp$ 从不成立
  • $\mathfrak{M},\omega\Vdash\neg\varphi\iff \mathfrak{M},\omega\Vdash\varphi$ 不成立
  • $\mathfrak{M},\omega\Vdash\varphi\vee\psi\iff\mathfrak{M},\omega\Vdash\varphi$ 或 $\mathfrak{M},\omega\Vdash\psi$
  • $\mathfrak{M},\omega\Vdash\diamondsuit\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$

线性时间时态逻辑 (LTL)

语言

• 线性时间时态算子
  • $\mathcal{U}$: until
  • $\bigcirc$: next-time
• 常用时态算子
  • $\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
  • $\phi_1\mathcal{R}\phi_2:=\neg(\neg\phi_1\mathcal{U}\neg\phi_2)$: Release
• $\psi::=p|\perp|\neg\psi|\psi_1\vee\psi_2|\bigcirc\psi|\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}$ 的时间线 $x$ 上，公式 $\psi$ 为真
  • $\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$

分支时间时态逻辑

语言

BTL

• 命题符 $\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|\varphi_1\vee\varphi_2|\neg\varphi|\exists\psi$

Sublanguage

• 路径公式：$\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\diamondsuit\neg\varphi$
    • $\forall\diamondsuit\varphi:=\neg\exists\square\neg\varphi$
    • $\exists\diamondsuit\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)$

语义 Computation 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 x,\forall i\in\mathbb{N},\mathfrak{M},s_i\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))$

语法

正规模态逻辑 $\Lambda$

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

$K$

• 公理
  • TAUT: 所有重言式
  • K: $\square(p\rightarrow q)\rightarrow(\square p\rightarrow \square q)$
  • Dual: $\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}$
• $K$-系统对应基本模态逻辑
  • soundness
  • completeness
• 最小的正规模态逻辑为 $K$

$K\Gamma$

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

其它

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