模态逻辑（1）——从命题逻辑开始

导师给了我一篇写模态逻辑和证据理论的论文，一开始看蒙了，然后决定从头开始学模态逻辑，《A New Introduction to Modal Logic》这本书写挺好的，我一直看到system T，然后搞懂了论文中的内容，我打算写几篇博客记录我的学习过程。
模态逻辑 (Modal logic) 研究的是“必然 (Necessity)”和“可能 (Possibility)”及相关概念。模态逻辑基于命题逻辑 (Propositional calculus, PC) ，在命题逻辑中，我们仅考虑事情在现实情况下的真 (Truth) 假 (Falsity)，而模态逻辑还考虑在其他可能情况（或称为可能世界，Possible world，这类情况可能存在但现实不处于这类情况）下，事情是真还是假。

命题逻辑 (Propositional calculus, PC)

命题逻辑是一种二值逻辑，它只有真 (Truth) 和假 (Falsity) 两种结果。命题逻辑的命题形式可以由一套公式来表达，公式由字母（变量）和一系列运算符（¬,∨,∧,⊃,≡\neg,\vee,\wedge,\supset,\equiv¬,∨,∧,⊃,≡）组成，我们只关心被称为合式公式 (Well-formed formulae, wff) 的表达式，wff 定义如下：

一个单独的字母 α\alphaα 是 wff；
如果 α\alphaα 是 wff，则 ¬α\neg \alpha¬α 也是 wff；
如果 α\alphaα 和 β\betaβ 是 wff，则 α∨β\alpha\vee \betaα∨β 也是 wff（其他二元运算符类似）；
有限次使用 1~3 构成的符号串也是 wff。

关于合式公式的更详细解释说明可以参考百度百科和其他资料。这里需要区分一下命题和表达命题形式的公式，命题有真命题和假命题之分，而公式只是一串符号，公式中的字母（变量）全部被替换为命题后，公式就变成了命题。

运算符定义

接下来用真值表直观地表述各种运算符的定义，1 表述真，0 表述假。这些运算符均为真值函数运算符 (Truth-functional operator)，给定输入后，可以明确地推导出输出。

否定 ¬\neg¬ (Negation sign)

	¬\neg¬
1	0
0	1

析取 ∨\vee∨ (Disjunction sign)

∨\vee∨	1	0
1	1	1
0	1	0

合取 ∧\wedge∧ (Conjunction sign)

∧\wedge∧	1	0
1	1	0
0	0	0

蕴含 ⊃\supset⊃ (Implication sign)

⊃\supset⊃	1	0
1	1	0
0	1	1

合式公式 a⊃ba\supset ba⊃b 可以理解为：“if aaa, then bbb”。

等价 ≡\equiv≡ (Equivalence sign)

≡\equiv≡	1	0
1	1	0
0	0	1

合式公式的正确性 (Validity)

合式公式中的字母（变量）全部被替换为命题后，合式公式也变成了一个命题。当且仅当每一种替换方式都能使合式公式变成一个真命题时，称这个合式公式为正确的 (valid)。可以画一个真值表，将合式公式中的变量换成各种 0（真）、1（假）组合，如果合式公式的运算结果全部为 1，那么合式公式是正确的。例如，p∨¬pp\vee \neg pp∨¬p，(p∧q)⊃p(p\wedge q)\supset p(p∧q)⊃p 是正确的合式公式。下面是一个复杂一点的例子：

一些命题逻辑 (PC) 中正确的合式公式

我后面再写博客的话，可能会用这些公式推导新的公式。