| 系统T system T 最基本的模态命题演算系统。是命题演算的扩充。由费斯(R. Feys)在哥德尔1933年所提出的一个演算基础上，于1937年正式提出。它由以下四部分作为基础：
(1) 初始符号：
p1，p2，p3，… 命题变项
，L一目常项
→二目常项
(，)括号
(2) 形成规则：
1. 任一命题变项pi是合式公式。
2. 如果A是合式公式，那么A，LA也是合式公式。
3. 如果A、B是合式公式，那么A→B也是合式公式。
4. 所有合式公式由(1)，(2)，(3)给出。
通过定义：
A∨B定义为A→B
A∧B定义为(A→B)
A↔B定义为(A→B)∧(B→A)
MA定义为LA
A⇒B定义为L(A→B)
A⇐⇒B定义为(A⇐B)∧(B⇒A)
知：A∨B，A∧B，A↔B，MA，A⇒B，A⇐⇒B也是T中合式公式。其中L，M，⇒，⇐⇒，分别解释为“必然”，“可能”，“严格蕴涵”，“严格等值”。
(3) 初始公式(公理)
1. A→(B→A)
2. (A→(B→C))→((A→B)→(A→C))
3. (A→B)→(B→A)
4. LA→A
5. L(A→B)→(LA→LB)
(4) 变形(推理)规则：
1. 分离规则：如果A和A→B是定理，则B也是定理。
2. 必然规则：如果A是定理，则LA也是定理。 |