导师给了我一篇写模态逻辑和证据理论的论文，一开始看蒙了，然后决定从头开始学模态逻辑，《A New Introduction to Modal Logic》这本书写挺好的，我一直看到system T，然后搞懂了论文中的内容，我打算写几篇博客记录我的学习过程。
模态逻辑 (Modal logic) 研究的是“必然 (Necessity)”和“可能 (Possibility)”及相关概念。模态逻辑基于命题逻辑 (Propositional calculus, PC) ，在命题逻辑中，我们仅考虑事情在现实情况下的真 (Truth) 假 (Falsity)，而模态逻辑还考虑在其他可能情况（或称为可能世界，Possible world，这类情况可能存在但现实不处于这类情况）下，事情是真还是假。
命题逻辑是一种二值逻辑，它只有真 (Truth) 和假 (Falsity) 两种结果。命题逻辑的命题形式可以由一套公式来表达，公式由字母（变量）和一系列运算符（ ¬ , ∨ , ∧ , ⊃ , ≡ neg,vee,wedge,supset,equiv ¬,∨,∧,⊃,≡）组成，我们只关心被称为合式公式 (Well-formed formulae, wff) 的表达式，wff 定义如下：
一个单独的字母 α alpha α 是 wff；如果 α alpha α 是 wff，则 ¬ α neg alpha ¬α 也是 wff；如果 α alpha α 和 β beta β 是 wff，则 α ∨ β alphavee beta α∨β 也是 wff（其他二元运算符类似）；有限次使用 1~3 构成的符号串也是 wff。关于合式公式的更详细解释说明可以参考百度百科和其他资料。这里需要区分一下命题和表达命题形式的公式，命题有真命题和假命题之分，而公式只是一串符号，公式中的字母（变量）全部被替换为命题后，公式就变成了命题。
运算符定义接下来用真值表直观地表述各种运算符的定义，1 表述真，0 表述假。这些运算符均为真值函数运算符 (Truth-functional operator)，给定输入后，可以明确地推导出输出。
否定 ¬ neg ¬ (Negation sign) ¬ neg ¬1001析取 ∨ vee ∨ (Disjunction sign) ∨ vee ∨10111010合取 ∧ wedge ∧ (Conjunction sign) ∧ wedge ∧10110000蕴含 ⊃ supset ⊃ (Implication sign) ⊃ supset ⊃10110011合式公式 a ⊃ b asupset b a⊃b 可以理解为：“if a a a, then b b b”。
等价 ≡ equiv ≡ (Equivalence sign) ≡ equiv ≡10110001合式公式的正确性 (Validity) 合式公式中的字母（变量）全部被替换为命题后，合式公式也变成了一个命题。当且仅当每一种替换方式都能使合式公式变成一个真命题时，称这个合式公式为正确的 (valid)。可以画一个真值表，将合式公式中的变量换成各种 0（真）、1（假）组合，如果合式公式的运算结果全部为 1，那么合式公式是正确的。例如， p ∨ ¬ p pvee neg p p∨¬p， ( p ∧ q ) ⊃ p (pwedge q)supset p (p∧q)⊃p 是正确的合式公式。下面是一个复杂一点的例子：
我后面再写博客的话，可能会用这些公式推导新的公式。