用∀，terms表示示例Kripke模型的形式公理定理 [英] formal axiomatic def of an example Kripke model in terms of ∀, ∃

问题描述

我正在寻找 Kripke模型的形式公理化定义，假设∀，∃假设简单的谓词逻辑，布尔逻辑，...

I am looking for a formal axiomatic definition of an example Kripke model in terms of ∀, ∃ assuming knowledge of simple predicate logic, boolean logic,...

我遇到的所有Kripke模型描述都只是通过释义引入英语语言概念(即☐ =必要性").虽然肯定有帮助和激励，但并不能保证我会像其他人一样对Kripke模型有相同的解释.

All descriptions of Kripke models I encounter simply introduce new notations through paraphrasing to english linguistic concepts (i.e. ☐ = "necessity"). While certainly both helpfull and motivating, it does not assure that I will have the same interpretation of what a Kripke model is as someone else.

(此问题是对问题 Kripke语义:可以使用学习软件的答案很好的结果.

(this question is the result from good answer at question Kripke semantics: learning software available?)

推荐答案

您可以轻松地用forall替换盒子，并且菱形存在(或将其重写为对偶).但是，在Kripke模型中解释的重点是，这些公式是在纯局部水平上评估的.如果您将Kripke模型想象为仅在顶点上带有标签(标签与命题相对应)的有向图，则公式总是在状态下求值.根据克里普克斯可能的世界哲学，这通常被称为世界.

You can easily replace the box with the forall, and the diamond with exists (or just rewrite it to the dual). But the point of the interpretation in Kripke models, is that the formulae are evaluated at a purely local level. If you imagine a Kripke model as just a directed graph with labels on the vertices (the labels corresponds to the propositions), then a formula is always* evaluated at a state. This is often called a world, as per Kripkes possible world philosophy.

现在，您如何评价它?好吧，简单地说，如果且仅当对于所有可到达的世界(当前顶点的传出邻域)phi为真时，方格phi被评估为真(在世界/州/顶点).将此与一阶逻辑进行比较，在逻辑上，当且仅当phi对于所有对象(全局！)为true时，forall phi为true.

Now, how do you evaluate it? Well, simply by saying that box phi is evaluated to true (in a world/state/vertex) if and only if for all reachable worlds (the outgoing neighbourhood of the current vertex) phi is true. Compare this to in first order logic, where forall phi is true if and only if phi is true for all objects (globally!).

现在，将钻石替换为不是用double not框，但是，如果需要，只要且仅当存在可到达的世界时，钻石phi才会被评估为true(在世界/州/顶点).

(顶点具有向外的邻居)，其中phi为true.再次，将其与一阶逻辑进行比较，如果存在一个对象(全局)中phi为true，则存在phi为true.

Now, the diamond follows by replacing it with the dual not box not, but if you want, diamond phi is evaluated to true (in a world/state/vertex) if and only if exists reachable worlds (the vertex has an outgoing neighbour) in which phi is true. Again, compare this to first order logic, where exists phi is true if there is an object (globally) where phi is true.

Ps.我们在其中计算公式的顶点具有许多不同的名称:状态，世界和节点等.这取决于您在哪个逻辑领域工作，例如在计算机科学(CTL，CTL *，ATL，LTL等)中，我们称这些顶点为"<状态>状态"，因为它们可以表示系统的某些内部状态，例如在认知逻辑，道义逻辑，十二进制逻辑中或您拥有什么，我们可能将它们称为(可能的)世界.

Ps. The vertices in which we evaluate formulae have many different names: states, worlds and nodes, amongst others. It depends on which field of logic you are working in, e.g. in computer science (CTL, CTL*, ATL, LTL, etc), we call the vertices states as they might represent some internal state of a system, where as in epistemic logic, deontic logic, doxastic logics or what have you, we might call them (possible) worlds.

编辑，尝试使其更清晰:

在FOL中，将在结构/模型中全局评估公式. forall phi表示phi对于域的每个成员均有效.在Kripke语义中，在域的成员中对公式进行求值 w ，并且框phi表示对于 w 的每个邻居，phi是案子. Diamond phi在 w 中是正确的，前提是存在phi的 w 邻居.

In FOL, a formula is evaluated globally in the structure/model. forall phi means that phi holds for every member of the domain. In Kripke semantics, a formula is evaluated in a member of the domain w and box phi means that for every neighbours of w, phi is the case. diamond phi is true in w iff there is a neighbour of w in which phi holds.

这篇关于用∀，terms表示示例Kripke模型的形式公理定理的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！