logic - Kripke语义学习软件可用?




modal-dialog boolean-logic (2)

我不确定用于教授模态逻辑的关系语义的教育软件是否存在。 不过，我可以尝试回答一些你所问的问题。

首先，模态运算符的必要性和可能性是对命题进行操作，而不是真值。 因此，如果φ是一个命题，那么φφ和φφ都是命题。 因为无论是真还是假都是命题，☐ 真 ， 假 ， 假和假都不是有意义的符号序列。

其次，你所说的“二元公理”通常是模态算子的相互可定义性的表达。 它可以作为模式逻辑的公理化发展的一个公理引入，或者作为模态操作符的语义的结果推导出来。

第三，经典量词不是模态运算符，也不表达模态概念。 事实上，模态逻辑通常是通过将模态操作符引入命题逻辑或谓词逻辑来定义的。 我认为你的困惑是因为模态操作符的语义看起来和量词的语义相似。 例如，必要性操作符的语义看起来类似于通用量词的语义：

  • 对于量化域中的所有α，⊧∀x.φ（x）≡φ（α）为真
  • w在每个可能的世界中都是真实的

将可能性算子与存在量词进行比较时可以看到相似性。 事实上，模态操作符可以被定义为可能世界上的量词。 据我所知，相反是不正确的。

我卡在Kripke语义 ，并想知道是否有educational software通过它我可以测试语句的等效性等，因为我开始认为它更容易学习的例子（即使抽象变量）。

我会用的

  • ☐A必须写A
  • for A可能是A.

做错误，错误，真实，错误评估值，如果是的话，那么什么值或什么样的值设置（{true，false}或者{必要，可能}）？ [1]

我想我读了所有的Kripke models使用duality axiom ：

（☐A） - >（¬♢¬A）

即如果有必要paytax那么不允许不paytax
（无论何时缴纳税款...）

IE2。 如果有必要的话，不允许不要earnmoney
（不管何时赚钱真的是必要的，到目前为止的逻辑）

因为A-> B相当于¬A<-B让我们测试

¬☐A< - ♢¬A

如果它不允许upvote那么它不需要upvote

这个公理双重作用：

♢A->¬☐¬A

如果允许的话，那么它不需要不earnmoney

不是所有的模态都是相同的，不同的Kripke model更适合模拟一个模态：不是所有的Kripke models使用相同的axioms 。 （古典量词是否也是模态？如果Kripke models这样的话，它们可以模拟它们吗？）

我将通过常用公理的列表，并试图找到例子，使其似乎违反直觉或不必要的假设...

  • ☐（A-> B） - >（☐A->☐B）：

如果（它的必要（赚钱暗示支付））那么（（赚钱的必要性）暗示（支付的必要性））

注意赚钱并不意味着纳税，暗示A-> B的虚假并不影响公理的真值。

呃，它太花时间来说我的问题，试图理解这一切...随意编辑




logic   modal-dialog   boolean-logic   reasoning