logic - 以 ∀, ∃ 表示的示例 Kripke 模型的形式公理化定义

Answer 1

您可以轻松地用 forall 替换 box，并且用存在的 diamond 替换（或将其重写为对偶）。但是 Kripke 模型的解释要点是，公式是在纯粹的局部级别上评估的。如果您将 Kripke 模型想象为在顶点上带有标签的有向图（标签对应于命题），那么公式总是*在 state 下进行评估。根据克里普克斯的可能世界哲学，这通常被称为世界。

现在，你如何评价它？好吧，简单地说，当且仅当对于所有可到达的世界（当前顶点的传出邻域）phi 为真时，盒子 phi 被评估为真（在世界/状态/顶点中）。将此与一阶逻辑进行比较，其中当且仅当 phi 对于所有对象（全局！）都为真时，forall phi 为真。

现在，菱形随后将其替换为对偶非框，但如果您愿意，当且仅当存在可达世界（顶点具有传出邻居）时，菱形 phi 被评估为真（在世界/状态/顶点中）其中 phi 为真。同样，将此与一阶逻辑进行比较，如果存在 phi 为真的对象（全局），则存在 phi 为真。

附言。我们评估公式的顶点有许多不同的名称：状态、世界和节点等等。这取决于您在哪个逻辑领域工作，例如在计算机科学（CTL、CTL*、ATL、LTL 等）中，我们将顶点状态称为顶点状态，因为它们可能代表系统的某些内部状态，如在认知逻辑中，道义逻辑，道德逻辑或你有什么，我们可以称它们为（可能的）世界。

编辑，试图让它更清楚：

在 FOL 中，公式在结构/模型中进行全局评估。forall phi 意味着 phi 适用于域的每个成员。在 Kripke 语义中，公式在域w的成员中 进行评估，并且框 phi 意味着对于w的每个邻居，phi 都是这种情况。钻石 phi 在w中为真，当且仅当w存在 phi 的邻居。