眞势道义逻辑系统

斯米莱－汉森型的系统在古典命题逻辑中引入模态算子□、◇和命题常项Q，道义算子O、P、F通过下述定义引进：

推理规则除分离规则外，引入了必然化规则，即从α可推出□α。公理模式有如下述：

(B0) 古典命题逻辑中的所有重言式

选取上述公理模式可以构造十个带命题常项Q的包含道义逻辑作为部分的真势模态逻辑系统，定义如下：

　　　K=B0～B2

　　　MQ=B0～B2，B6

　　　S4=B0～B2，B4，B6

　　　B=B0～B2，B6，B7

　　　S5=B0～B2，B5，B6(B4和B7在其中可导出)

对上述系统分别添加B3，就得到、、、、。

真势道义逻辑语义 其核心概念是真势模型或真势优先模型，它是一个有序四元组：M=＜W，R，opt，V＞，其中W是可能世界的非空集，R是定义在W上的二元关系，叫做“真势选择”或“真势可通达”关系；opt是W中那些“最令人满意的”、最好的或充分好的元素构成的集合；V是一个赋值，它给系统内的每一原子公式α指派W中的一个子集V(α)，α∈V(α)表示α在W的子集V(α)上真。模态公式的真条件递归定义如下：

①对于任一命题变项p，p当且仅当p∈V(p)

②α当且仅当，α

③α→β当且仅当，若α则β

④□α当且仅当，w∈W(ωRwα)

⑤◇α当且仅当，w∈W(ωRw并且α)

⑥Q当且仅当w∈opt

一公式α在模型u中有效，当且仅当，对于u中的每一w，都有α。公理模式B0～B2在任一模型u中有效，而B3～B7则只在其中R满足一定条件的模型u中有效，它们分别要求R3～R7：

(R3)优延续xy(xRy∧y∈opt)

(R4)传递xyz(xRy∧yRz→xRz)

(R5)欧性xyz(xRx∧yRz→yRx)

(R6)自返x(xRx)

(R7)对称xy(xRy→yRx)

已经证明，K、M、S4、B、S5、、、、、相对于满足其公理模式所要求的R的模型类是可靠并且完全的。